From: Alex Ozdemir Date: Tue, 5 Apr 2022 02:49:30 +0000 (-0700) Subject: Write-up for Pythonic API quickstart (#8566) X-Git-Tag: cvc5-1.0.0~9 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2c7ea88a3af9ff451e69a781a1499803c60df99;p=cvc5.git Write-up for Pythonic API quickstart (#8566) --- diff --git a/docs/api/python/pythonic/quickstart.rst b/docs/api/python/pythonic/quickstart.rst index 764b1573f..53a48d5f8 100644 --- a/docs/api/python/pythonic/quickstart.rst +++ b/docs/api/python/pythonic/quickstart.rst @@ -1,2 +1,74 @@ -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:: + /api/python/quickstart.py + /api/cpp/quickstart.cpp + /api/java/QuickStart.java + /api/python/pythonic/quickstart.py + /api/smtlib/quickstart.smt2 diff --git a/docs/conf.py.in b/docs/conf.py.in index c3a25867c..aa5104782 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -160,6 +160,11 @@ examples_types = { 'lang': 'java', 'group': 'java' }, + '^.*pythonic.*\.py$': { + 'title': 'Python (pythonic)', + 'lang': 'python', + 'group': 'py-pythonicapi' + }, '^.*\.py$': { 'title': 'Python (base)', 'lang': 'python', diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst index fff6b97e1..e6009ebd5 100644 --- a/docs/examples/bitvectors.rst +++ b/docs/examples/bitvectors.rst @@ -5,6 +5,6 @@ Theory of Bit-Vectors .. api-examples:: /api/cpp/bitvectors.cpp /api/java/BitVectors.java - /test/pgms/example_bitvectors.py + /api/python/pythonic/bitvectors.py /api/python/bitvectors.py /api/smtlib/bitvectors.smt2 diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst index 30bfc2e99..90012a28e 100644 --- a/docs/examples/bitvectors_and_arrays.rst +++ b/docs/examples/bitvectors_and_arrays.rst @@ -5,6 +5,6 @@ Theory of Bit-Vectors and Arrays .. api-examples:: /api/cpp/bitvectors_and_arrays.cpp /api/java/BitVectorsAndArrays.java - /test/pgms/example_bitvectors_and_arrays.py + /api/python/pythonic/bitvectors_and_arrays.py /api/python/bitvectors_and_arrays.py /api/smtlib/bitvectors_and_arrays.smt2 diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst index 1367aeec0..9308d51ae 100644 --- a/docs/examples/combination.rst +++ b/docs/examples/combination.rst @@ -4,6 +4,6 @@ Theory Combination .. api-examples:: /api/cpp/combination.cpp /api/java/Combination.java - /test/pgms/example_combination.py + /api/python/pythonic/combination.py /api/python/combination.py /api/smtlib/combination.smt2 diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst index aaed8f8bb..eb7c2147b 100644 --- a/docs/examples/datatypes.rst +++ b/docs/examples/datatypes.rst @@ -5,6 +5,6 @@ Theory of Datatypes .. api-examples:: /api/cpp/datatypes.cpp /api/java/Datatypes.java - /test/pgms/example_datatypes.py + /api/python/pythonic/datatypes.py /api/python/datatypes.py /api/smtlib/datatypes.smt2 diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst index c638f8dcf..ce204b8bc 100644 --- a/docs/examples/extract.rst +++ b/docs/examples/extract.rst @@ -5,6 +5,6 @@ Theory of Bit-Vectors: :code:`extract` .. api-examples:: /api/cpp/extract.cpp /api/java/Extract.java - /test/pgms/example_extract.py + /api/python/pythonic/extract.py /api/python/extract.py /api/smtlib/extract.smt2 diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst index 1e704d4a7..a5ebc9524 100644 --- a/docs/examples/floatingpoint.rst +++ b/docs/examples/floatingpoint.rst @@ -5,5 +5,5 @@ Theory of Floating-Points .. api-examples:: /api/cpp/floating_point_arith.cpp /api/java/FloatingPointArith.java - /test/pgms/example_floating_point.py + /api/python/pythonic/floating_point.py /api/python/floating_point.py diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst index 87bbe50f4..428e53e5b 100644 --- a/docs/examples/helloworld.rst +++ b/docs/examples/helloworld.rst @@ -7,6 +7,6 @@ We create a solver, declare a Boolean variable and check whether it is entailed .. api-examples:: /api/cpp/helloworld.cpp /api/java/HelloWorld.java - /test/pgms/example_helloworld.py + /api/python/pythonic/helloworld.py /api/python/helloworld.py /api/smtlib/helloworld.smt2 diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst index e561cf17a..96be09b25 100644 --- a/docs/examples/lineararith.rst +++ b/docs/examples/lineararith.rst @@ -9,6 +9,6 @@ The two checks are separated by using :code:`push` and :code:`pop`. .. api-examples:: /api/cpp/linear_arith.cpp /api/java/LinearArith.java - /test/pgms/example_linear_arith.py + /api/python/pythonic/linear_arith.py /api/python/linear_arith.py /api/smtlib/linear_arith.smt2 diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst index 3a57736ed..57f8dd63f 100644 --- a/docs/examples/quickstart.rst +++ b/docs/examples/quickstart.rst @@ -5,6 +5,6 @@ Quickstart Example .. api-examples:: /api/cpp/quickstart.cpp /api/java/QuickStart.java - /test/pgms/example_quickstart.py + /api/python/pythonic/quickstart.py /api/python/quickstart.py /api/smtlib/quickstart.smt2 diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst index abb7aa9ea..5ba0ca78b 100644 --- a/docs/examples/sets.rst +++ b/docs/examples/sets.rst @@ -5,6 +5,6 @@ Theory of Sets .. api-examples:: /api/cpp/sets.cpp /api/java/Sets.java - /test/pgms/example_sets.py + /api/python/pythonic/sets.py /api/python/sets.py /api/smtlib/sets.smt2 diff --git a/examples/api/python/pythonic/README.md b/examples/api/python/pythonic/README.md new file mode 100644 index 000000000..3eb91dde7 --- /dev/null +++ b/examples/api/python/pythonic/README.md @@ -0,0 +1,10 @@ +# 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. diff --git a/examples/api/python/pythonic/bitvectors.py b/examples/api/python/pythonic/bitvectors.py new file mode 100644 index 000000000..8e56add43 --- /dev/null +++ b/examples/api/python/pythonic/bitvectors.py @@ -0,0 +1,35 @@ +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)) diff --git a/examples/api/python/pythonic/bitvectors_and_arrays.py b/examples/api/python/pythonic/bitvectors_and_arrays.py new file mode 100644 index 000000000..199e736f3 --- /dev/null +++ b/examples/api/python/pythonic/bitvectors_and_arrays.py @@ -0,0 +1,26 @@ +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))) diff --git a/examples/api/python/pythonic/combination.py b/examples/api/python/pythonic/combination.py new file mode 100644 index 000000000..4070daa7c --- /dev/null +++ b/examples/api/python/pythonic/combination.py @@ -0,0 +1,35 @@ +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)) diff --git a/examples/api/python/pythonic/datatypes.py b/examples/api/python/pythonic/datatypes.py new file mode 100644 index 000000000..79074e4c0 --- /dev/null +++ b/examples/api/python/pythonic/datatypes.py @@ -0,0 +1,44 @@ +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)))) diff --git a/examples/api/python/pythonic/exceptions.py b/examples/api/python/pythonic/exceptions.py new file mode 100644 index 000000000..68f7f8840 --- /dev/null +++ b/examples/api/python/pythonic/exceptions.py @@ -0,0 +1,23 @@ +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 diff --git a/examples/api/python/pythonic/extract.py b/examples/api/python/pythonic/extract.py new file mode 100644 index 000000000..2923dc8b2 --- /dev/null +++ b/examples/api/python/pythonic/extract.py @@ -0,0 +1,15 @@ +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))) diff --git a/examples/api/python/pythonic/floating_point.py b/examples/api/python/pythonic/floating_point.py new file mode 100644 index 000000000..556379e9a --- /dev/null +++ b/examples/api/python/pythonic/floating_point.py @@ -0,0 +1,25 @@ +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)), + ) + ) diff --git a/examples/api/python/pythonic/helloworld.py b/examples/api/python/pythonic/helloworld.py new file mode 100644 index 000000000..e4b0ea903 --- /dev/null +++ b/examples/api/python/pythonic/helloworld.py @@ -0,0 +1,5 @@ +from cvc5.pythonic import * + +if __name__ == '__main__': + var = Bool('Hello World!') + solve(var) diff --git a/examples/api/python/pythonic/id.py b/examples/api/python/pythonic/id.py new file mode 100644 index 000000000..2de976f69 --- /dev/null +++ b/examples/api/python/pythonic/id.py @@ -0,0 +1,12 @@ +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() diff --git a/examples/api/python/pythonic/linear_arith.py b/examples/api/python/pythonic/linear_arith.py new file mode 100644 index 000000000..9241744cf --- /dev/null +++ b/examples/api/python/pythonic/linear_arith.py @@ -0,0 +1,15 @@ +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() diff --git a/examples/api/python/pythonic/quickstart.py b/examples/api/python/pythonic/quickstart.py new file mode 100644 index 000000000..570c9422a --- /dev/null +++ b/examples/api/python/pythonic/quickstart.py @@ -0,0 +1,39 @@ +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) + + + diff --git a/examples/api/python/pythonic/sets.py b/examples/api/python/pythonic/sets.py new file mode 100644 index 000000000..bccd86d21 --- /dev/null +++ b/examples/api/python/pythonic/sets.py @@ -0,0 +1,20 @@ +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))), + ) + ) diff --git a/examples/api/python/pythonic/transcendentals.py b/examples/api/python/pythonic/transcendentals.py new file mode 100644 index 000000000..0d4d04f2b --- /dev/null +++ b/examples/api/python/pythonic/transcendentals.py @@ -0,0 +1,7 @@ +from cvc5.pythonic import * + +if __name__ == '__main__': + x, y = Reals("x y") + solve(x > Pi(), + x < 2 * Pi(), + y ** 2 < Sine(x))