-Quickstart
-==========
+Quickstart Guide
+================
+
+First, we create two constants ``x`` and ``y`` of sort ``Real``,
+and two constants ``a`` and ``b`` of sort ``Integer``.
+Notice that these are *symbolic* constants, but not actual values.
+
+.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
+ :language: python
+ :lines: 6-7
+
+We define the following constraints regarding ``x`` and ``y``:
+
+.. math::
+
+ (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)
+
+We check whether there is a solution to these constraints:
+
+.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
+ :language: python
+ :lines: 15
+
+In this case, there is, so we get output:
+
+.. code:: text
+
+ [x = 1/6, y = 1/6]
+
+We can also get an explicit model (assignment) for the constraints.
+
+.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
+ :language: python
+ :lines: 19-22
+
+With the model, we can evaluate variables and terms:
+
+.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
+ :language: python
+ :lines: 24-26
+
+This will print:
+
+.. code:: text
+
+ x: 1/6
+ y: 1/6
+ x - y: 0
+
+
+We can also get these values in other forms:
+
+.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
+ :language: python
+ :lines: 29-32
+
+
+Next, we assert the same assertions as above, but with integers.
+This time, there is no solution, so "no solution" is printed.
+
+.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
+ :language: python
+ :lines: 36
+
+
+Example
+-------
+
+.. api-examples::
+ <examples>/api/python/quickstart.py
+ <examples>/api/cpp/quickstart.cpp
+ <examples>/api/java/QuickStart.java
+ <examples>/api/python/pythonic/quickstart.py
+ <examples>/api/smtlib/quickstart.smt2
'lang': 'java',
'group': 'java'
},
+ '^<examples>.*pythonic.*\.py$': {
+ 'title': 'Python (pythonic)',
+ 'lang': 'python',
+ 'group': 'py-pythonicapi'
+ },
'^<examples>.*\.py$': {
'title': 'Python (base)',
'lang': 'python',
.. api-examples::
<examples>/api/cpp/bitvectors.cpp
<examples>/api/java/BitVectors.java
- <pythonicapi>/test/pgms/example_bitvectors.py
+ <examples>/api/python/pythonic/bitvectors.py
<examples>/api/python/bitvectors.py
<examples>/api/smtlib/bitvectors.smt2
.. api-examples::
<examples>/api/cpp/bitvectors_and_arrays.cpp
<examples>/api/java/BitVectorsAndArrays.java
- <pythonicapi>/test/pgms/example_bitvectors_and_arrays.py
+ <examples>/api/python/pythonic/bitvectors_and_arrays.py
<examples>/api/python/bitvectors_and_arrays.py
<examples>/api/smtlib/bitvectors_and_arrays.smt2
.. api-examples::
<examples>/api/cpp/combination.cpp
<examples>/api/java/Combination.java
- <pythonicapi>/test/pgms/example_combination.py
+ <examples>/api/python/pythonic/combination.py
<examples>/api/python/combination.py
<examples>/api/smtlib/combination.smt2
.. api-examples::
<examples>/api/cpp/datatypes.cpp
<examples>/api/java/Datatypes.java
- <pythonicapi>/test/pgms/example_datatypes.py
+ <examples>/api/python/pythonic/datatypes.py
<examples>/api/python/datatypes.py
<examples>/api/smtlib/datatypes.smt2
.. api-examples::
<examples>/api/cpp/extract.cpp
<examples>/api/java/Extract.java
- <pythonicapi>/test/pgms/example_extract.py
+ <examples>/api/python/pythonic/extract.py
<examples>/api/python/extract.py
<examples>/api/smtlib/extract.smt2
.. api-examples::
<examples>/api/cpp/floating_point_arith.cpp
<examples>/api/java/FloatingPointArith.java
- <pythonicapi>/test/pgms/example_floating_point.py
+ <examples>/api/python/pythonic/floating_point.py
<examples>/api/python/floating_point.py
.. api-examples::
<examples>/api/cpp/helloworld.cpp
<examples>/api/java/HelloWorld.java
- <pythonicapi>/test/pgms/example_helloworld.py
+ <examples>/api/python/pythonic/helloworld.py
<examples>/api/python/helloworld.py
<examples>/api/smtlib/helloworld.smt2
.. api-examples::
<examples>/api/cpp/linear_arith.cpp
<examples>/api/java/LinearArith.java
- <pythonicapi>/test/pgms/example_linear_arith.py
+ <examples>/api/python/pythonic/linear_arith.py
<examples>/api/python/linear_arith.py
<examples>/api/smtlib/linear_arith.smt2
.. api-examples::
<examples>/api/cpp/quickstart.cpp
<examples>/api/java/QuickStart.java
- <pythonicapi>/test/pgms/example_quickstart.py
+ <examples>/api/python/pythonic/quickstart.py
<examples>/api/python/quickstart.py
<examples>/api/smtlib/quickstart.smt2
.. api-examples::
<examples>/api/cpp/sets.cpp
<examples>/api/java/Sets.java
- <pythonicapi>/test/pgms/example_sets.py
+ <examples>/api/python/pythonic/sets.py
<examples>/api/python/sets.py
<examples>/api/smtlib/sets.smt2
--- /dev/null
+# Notes
+
+These files are copied from [the pythonic API's repository](https://github.com/cvc5/cvc5_pythonic_api).
+
+They were copied with this script:
+
+ for f in ~/$CVC_PYTHONIC/test/pgms/example_*; do; ff=$(echo ${f:t} | sed 's/example_//'); cat $f | sed 's/_pythonic_api/.pythonic/' > examples/api/python/pythonic/$ff ; done;
+
+Notice that the script fixes up the import statements to align with a version
+of the cvc5 python APIs that are packaged together.
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ # The following example has been adapted from the book A Hacker's Delight
+ # by Henry S. Warren.
+ #
+ # Given a variable x that can only have two values, a or b. We want to
+ # assign to x a value other than the current one. The straightforward code
+ # to do that is:
+ #
+ # (0) if (x == a ) x = b;
+ # else x = a;
+ #
+ # Two more efficient yet equivalent methods are:
+ #
+ # (1) x = a xor b xor x;
+ #
+ # (2) x = a + b - x;
+ #
+ # We will use cvc5 to prove that the three pieces of code above are all
+ # equivalent by encoding the problem in the bit-vector theory.
+
+ x, a, b = BitVecs('x a b', 32)
+ x_is_a_or_b = Or(x == a, x == b)
+
+ # new_x0 set per (0)
+ new_x0 = If(x == a, b, a)
+ # new_x1 set per (1)
+ new_x1 = a ^ b ^ x
+ # new_x2 set per (2)
+ new_x2 = a + b - x
+
+ prove(Implies(x_is_a_or_b, new_x0 == new_x1))
+
+ prove(Implies(x_is_a_or_b, new_x0 == new_x2))
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ # Consider the following (where k is some previously defined constant):
+ #
+ #
+ # Assert (current_array[0] > 0);
+ # for (unsigned i = 1; i < k; ++i) {
+ # current_array[i] = 2 * current_array[i - 1];
+ # Assert (current_array[i-1] < current_array[i]);
+ # }
+ #
+ # We want to check whether the assertion in the body of the for loop holds
+ # throughout the loop.
+ k = 4
+ idx_bits = int(math.ceil(math.log(k, 2)))
+
+ init_array = Array('init_arr', BitVecSort(idx_bits), BitVecSort(32))
+ array = init_array
+ assertions = []
+ for i in range(1, k):
+ array = Store(array, i, 2 * Select(array, i - 1))
+ assertions.append(Select(array, i - 1) < Select(array, i))
+ # Does *not* hold.
+ # If the first element is large enough, the multiplication overflows.
+ prove(Implies(Select(init_array, 0) > 0, And(*assertions)))
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == "__main__":
+
+ U = DeclareSort("U")
+ x, y = Consts("x y", U)
+
+ f = Function("f", U, IntSort())
+ p = Function("p", IntSort(), BoolSort())
+
+ assumptions = [f(x) >= 0, f(y) >= 0, f(x) + f(y) <= 1, Not(p(0)), p(f(y))]
+
+ prove(Implies(And(assumptions), x != y))
+
+ s = Solver()
+ s.add(assumptions)
+ assert sat == s.check()
+ m = s.model()
+
+ def print_val(t):
+ print("{}: {}".format(t, m[t]))
+
+ # print the of some terms
+ print_val(f(x))
+ print_val(f(y))
+ print_val(f(x) + f(y))
+ print_val(p(0))
+ print_val(p(f(y)))
+
+ # print value of *all* terms
+ def print_all_subterms(t):
+ print_val(t)
+ for c in t.children():
+ print_all_subterms(c)
+ print_all_subterms(And(assumptions))
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ # This example builds a simple "cons list" of integers, with
+ # two constructors, "cons" and "nil."
+
+ # Building a datatype consists of two steps.
+ # First, the datatype is specified.
+ # Second, it is "resolved" to an actual sort, at which point function
+ # symbols are assigned to its constructors, selectors, and testers.
+
+ decl = Datatype("list")
+ decl.declare("cons", ("head", IntSort()), ("tail", decl))
+ decl.declare("nil")
+ List = decl.create()
+
+ # Using constructors and selectors:
+ t = List.cons(0, List.nil)
+ print("t is:", t)
+ print("head of t is:", List.head(t))
+ print("after simplify:", simplify(List.head(t)))
+ print()
+
+ # You can iterate over constructors and selectors
+ for i in range(List.num_constructors()):
+ ctor = List.constructor(i)
+ print("ctor:", ctor)
+ for j in range(ctor.arity()):
+ print(" + arg:", ctor.domain(j))
+ print(" + selector:", List.accessor(i, j))
+ print()
+
+ # You can use testers
+ print("t is a 'cons':", simplify(List.is_cons(t)))
+ print()
+
+ # This Python API does not support type parameters or updators for
+ # datatypes. See the base Python API for those features, or construct them
+ # using Python functions/classes.
+
+ a = Int('a')
+ solve(List.head(List.cons(a, List.nil)) > 50)
+
+ prove(Not(List.is_nil(List.cons(a, List.nil))))
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ s = Solver()
+ s.set("produce-models", True)
+ try:
+ # invalid option
+ s.set("non-existing-option", True)
+ except:
+ pass
+
+ try:
+ # type error
+ Int("x") + BitVec("a", 5)
+ except:
+ pass
+
+ s += BoolVal(False)
+ s.check()
+ try:
+ s.model()
+ except:
+ pass
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ x = BitVec('x', 32)
+
+ # Consider the bits of x: 01234567
+ # (we assume 8 bits to make the visualization simple)
+ #
+ # If 1234567
+ # equals 0123456
+ #
+ # then 0 == 7 (by induction over the bits)
+
+ prove(Implies(Extract(31, 1, x) == Extract(30, 0, x),
+ Extract(31, 31, x) == Extract(0, 0, x)))
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == "__main__":
+ x, y, z = FPs("x y z", Float32())
+ set_default_rounding_mode(RoundNearestTiesToEven())
+
+ # FP addition is *not* commutative. This finds a counterexample.
+ assert not is_tautology(fpEQ(x + y, y + x))
+
+ # Without NaN or infinities, is is commutative. This proof succeeds.
+ assert is_tautology(
+ Implies(
+ Not(Or(fpIsNaN(x), fpIsNaN(y), fpIsInf(x), fpIsInf(y))), fpEQ(x + y, y + x)
+ )
+ )
+
+ pi = FPVal(+3.14, Float32())
+
+ # FP addition is *not* associative in the range (-pi, pi).
+ assert not is_tautology(
+ Implies(
+ And(x >= -pi, x <= pi, y >= -pi, y <= pi, z >= -pi, z <= pi),
+ fpEQ((x + y) + z, x + (y + z)),
+ )
+ )
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ var = Bool('Hello World!')
+ solve(var)
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ A = Set("A", SetSort(IntSort()))
+ B = Set("B", SetSort(IntSort()))
+ C = Set("C", SetSort(IntSort()))
+
+ assert A.get_id() != B.get_id()
+ assert C.get_id() != B.get_id()
+ assert A.get_id() == A.get_id()
+ assert B.get_id() == B.get_id()
+ assert C.get_id() == C.get_id()
--- /dev/null
+from cvc5.pythonic import *
+
+slv = SolverFor('QF_LIRA')
+
+x = Int('x')
+y = Real('y')
+
+slv += And(x >= 3 * y, x <= y, -2 < x)
+slv.push()
+print(slv.check(y-x <= 2/3))
+slv.pop()
+slv.push()
+slv += y-x == 2/3
+print(slv.check())
+slv.pop()
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+
+ # Let's introduce some variables
+ x, y = Reals('x y')
+ a, b = Ints('a b')
+
+ # We will confirm that
+ # * 0 < x
+ # * 0 < y
+ # * x + y < 1
+ # * x <= y
+ # are satisfiable
+ solve(0 < x, 0 < y, x + y < 1, x <= y)
+
+ # If we get the model (the satisfying assignment) explicitly, we can
+ # evaluate terms under it.
+ s = Solver()
+ s.add(0 < x, 0 < y, x + y < 1, x <= y)
+ assert sat == s.check()
+ m = s.model()
+
+ print('x:', m[x])
+ print('y:', m[y])
+ print('x - y:', m[x - y])
+
+ # We can also get these values in other forms:
+ print('string x:', str(m[x]))
+ print('decimal x:', m[x].as_decimal(4))
+ print('fraction x:', m[x].as_fraction())
+ print('float x:', float(m[x].as_fraction()))
+
+ # The above constraints are *UNSAT* for integer variables.
+ # This reports "no solution"
+ solve(0 < a, 0 < b, a + b < 1, a <= b)
+
+
+
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == "__main__":
+ A, B, C = [Set(name, IntSort()) for name in "ABC"]
+
+ # holds
+ prove((A | B) & C == (A & C) | (B & C))
+
+ # holds
+ prove(IsSubset(EmptySet(IntSort()), A))
+
+ # x must be 2.
+ x = Int("x")
+ solve(
+ IsMember(
+ x,
+ (Singleton(IntVal(1)) | Singleton(IntVal(2)))
+ & (Singleton(IntVal(2)) | Singleton(IntVal(3))),
+ )
+ )
--- /dev/null
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+ x, y = Reals("x y")
+ solve(x > Pi(),
+ x < 2 * Pi(),
+ y ** 2 < Sine(x))
projects / cvc5.git / commitdiff