1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Theory of Linear Arithmetic
===========================
This example asserts three constraints over an integer variable :code:`x` and a real variable :code:`y`.
Firstly, it checks that these constraints entail an upper bound on the difference :code:`y - x <= 2/3`.
Secondly, it checks that this bound is tight by asserting :code:`y - x = 2/3` and checking for satisfiability.
The two checks are separated by using :code:`push` and :code:`pop`.
.. api-examples::
<examples>/api/cpp/linear_arith.cpp
<examples>/api/c/linear_arith.c
<examples>/api/java/LinearArith.java
<examples>/api/python/pythonic/linear_arith.py
<examples>/api/python/linear_arith.py
<examples>/api/smtlib/linear_arith.smt2
|
