Write-up for Pythonic API quickstart (#8566)

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.

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))

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)))

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))

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))))

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

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)))

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)),
+        )
+    )

examples/api/python/pythonic/helloworld.py

@@ -0,0 +1,5 @@
+from cvc5.pythonic import *
+
+if __name__ == '__main__':
+    var = Bool('Hello World!')
+    solve(var)

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()

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()

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)
+
+
+

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))),
+        )
+    )

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))