diff options
author | makaimann <makaim@stanford.edu> | 2020-02-19 13:54:17 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-19 15:54:17 -0600 |
commit | c82720479efcf922136f0919f6fc26a502b2515a (patch) | |
tree | f9007e124cfc07490e914ae1e1e05747e1e1ee11 /examples/api | |
parent | c6a9ab9da205df7cbf192edc142ee151404dcb1b (diff) |
Add Python bindings using Cython -- see below for more details (#2879)
Diffstat (limited to 'examples/api')
-rwxr-xr-x | examples/api/python/bitvectors.py | 121 | ||||
-rwxr-xr-x | examples/api/python/bitvectors_and_arrays.py | 91 | ||||
-rwxr-xr-x | examples/api/python/combination.py | 99 | ||||
-rwxr-xr-x | examples/api/python/datatypes.py | 137 | ||||
-rwxr-xr-x | examples/api/python/extract.py | 51 | ||||
-rwxr-xr-x | examples/api/python/helloworld.py | 21 | ||||
-rwxr-xr-x | examples/api/python/linear_arith.py | 70 | ||||
-rwxr-xr-x | examples/api/python/sets.py | 85 | ||||
-rwxr-xr-x | examples/api/python/strings.py | 87 |
9 files changed, 762 insertions, 0 deletions
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py new file mode 100755 index 000000000..773974cc7 --- /dev/null +++ b/examples/api/python/bitvectors.py @@ -0,0 +1,121 @@ +#!/usr/bin/env python + +##################### +#! \file bitvectors.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## bit-vector solver through the Python API. This is a direct translation + ## of bitvectors-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setLogic("QF_BV") # Set the logic + # 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 CVC4 to prove that the three pieces of code above are all + # equivalent by encoding the problem in the bit-vector theory. + + # Creating a bit-vector type of width 32 + bitvector32 = slv.mkBitVectorSort(32) + + # Variables + x = slv.mkConst(bitvector32, "x") + a = slv.mkConst(bitvector32, "a") + b = slv.mkConst(bitvector32, "b") + + # First encode the assumption that x must be equal to a or b + x_eq_a = slv.mkTerm(kinds.Equal, x, a) + x_eq_b = slv.mkTerm(kinds.Equal, x, b) + assumption = slv.mkTerm(kinds.Or, x_eq_a, x_eq_b) + + # Assert the assumption + slv.assertFormula(assumption) + + # Introduce a new variable for the new value of x after assignment. + # x after executing code (0) + new_x = slv.mkConst(bitvector32, "new_x") + # x after executing code (1) or (2) + new_x_ = slv.mkConst(bitvector32, "new_x_") + + # Encoding code (0) + # new_x = x == a ? b : a + ite = slv.mkTerm(kinds.Ite, x_eq_a, b, a) + assignment0 = slv.mkTerm(kinds.Equal, new_x, ite) + + # Assert the encoding of code (0) + print("Asserting {} to CVC4".format(assignment0)) + slv.assertFormula(assignment0) + print("Pushing a new context.") + slv.push() + + # Encoding code (1) + # new_x_ = a xor b xor x + a_xor_b_xor_x = slv.mkTerm(kinds.BVXor, a, b, x) + assignment1 = slv.mkTerm(kinds.Equal, new_x_, a_xor_b_xor_x) + + # Assert encoding to CVC4 in current context + print("Asserting {} to CVC4".format(assignment1)) + slv.assertFormula(assignment1) + new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_) + + print("Checking validity assuming:", new_x_eq_new_x_) + print("Expect valid.") + print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_)) + print("Popping context.") + slv.pop() + + # Encoding code (2) + # new_x_ = a + b - x + a_plus_b = slv.mkTerm(kinds.BVPlus, a, b) + a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x) + assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_x) + + # Assert encoding to CVC4 in current context + print("Asserting {} to CVC4".format(assignment2)) + slv.assertFormula(assignment2) + + print("Checking validity assuming:", new_x_eq_new_x_) + print("Expect valid.") + print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_)) + + + x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm() + v = [new_x_eq_new_x_, x_neq_x] + print("Check Validity Assuming: ", v) + print("Expect invalid.") + print("CVC4:", slv.checkValidAssuming(v)) + + # Assert that a is odd + extract_op = slv.mkOp(kinds.BVExtract, 0, 0) + lsb_of_a = slv.mkTerm(extract_op, a) + print("Sort of {} is {}".format(lsb_of_a, lsb_of_a.getSort())) + a_odd = slv.mkTerm(kinds.Equal, lsb_of_a, slv.mkBitVector(1, 1)) + print("Assert", a_odd) + print("Check satisifiability") + slv.assertFormula(a_odd) + print("Expect sat") + print("CVC4:", slv.checkSat()) diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py new file mode 100755 index 000000000..7e3d8f478 --- /dev/null +++ b/examples/api/python/bitvectors_and_arrays.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python + +##################### +#! \file bitvectors_and_arrays.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## bit-vector and array solvers through the Python API. This is a direct + ## translation of bitvectors_and_arrays-new.cpp. +import pycvc4 +from pycvc4 import kinds + +import math + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setOption("produce-models", "true") + slv.setOption("output-language", "smtlib") + slv.setLogic("QF_AUFBV") + + # Consider the following code (where size 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. + + # Setting up the problem parameters + k = 4 + index_size = int(math.ceil(math.log(k, 2))) + + # Sorts + elementSort = slv.mkBitVectorSort(32) + indexSort = slv.mkBitVectorSort(index_size) + arraySort = slv.mkArraySort(indexSort, elementSort) + + # Variables + current_array = slv.mkConst(arraySort, "current_array") + + # Making a bit-vector constant + zero = slv.mkBitVector(index_size, 0) + + # Test making a constant array + constarr0 = slv.mkConstArray(arraySort, slv.mkBitVector(32, 0)) + + # Asserting that current_array[0] > 0 + current_array0 = slv.mkTerm(kinds.Select, current_array, zero) + current_array0_gt_0 = slv.mkTerm(kinds.BVSgt, + current_array0, + slv.mkBitVector(32, 0)) + slv.assertFormula(current_array0_gt_0) + + # Building the assertions in the loop unrolling + index = slv.mkBitVector(index_size, 0) + old_current = slv.mkTerm(kinds.Select, current_array, index) + two = slv.mkBitVector(32, 2) + + assertions = [] + for i in range(1, k): + index = slv.mkBitVector(index_size, i) + new_current = slv.mkTerm(kinds.BVMult, two, old_current) + # current[i] = 2*current[i-1] + current_array = slv.mkTerm(kinds.Store, current_array, index, new_current) + # current[i-1] < current[i] + current_slt_new_current = slv.mkTerm(kinds.BVSlt, old_current, new_current) + assertions.append(current_slt_new_current) + old_current = slv.mkTerm(kinds.Select, current_array, index) + + query = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.And, assertions)) + + print("Asserting {} to CVC4".format(query)) + slv.assertFormula(query) + print("Expect sat.") + print("CVC4:", slv.checkSatAssuming(slv.mkTrue())) + + # Getting the model + print("The satisfying model is: ") + print(" current_array =", slv.getValue(current_array)) + print(" current_array[0]", slv.getValue(current_array0)) diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py new file mode 100755 index 000000000..1b488d7d5 --- /dev/null +++ b/examples/api/python/combination.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python + +##################### +#! \file combination.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## combination solver through the Python API. This is a direct translation + ## of combination-new.cpp. +import pycvc4 +from pycvc4 import kinds + +def prefixPrintGetValue(slv, t, level=0): + print("slv.getValue({}): {}".format(t, slv.getValue(t))) + for c in t: + prefixPrintGetValue(slv, c, level + 1) + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setOption("produce-models", "true") # Produce Models + slv.setOption("output-language", "cvc4") # Set the output-language to CVC's + slv.setOption("default-dag-thresh", "0") # Disable dagifying the output + slv.setOption("output-language", "smt2") # use smt-lib v2 as output language + slv.setLogic("QF_UFLIRA") + + # Sorts + u = slv.mkUninterpretedSort("u") + integer = slv.getIntegerSort() + boolean = slv.getBooleanSort() + uToInt = slv.mkFunctionSort(u, integer) + intPred = slv.mkFunctionSort(integer, boolean) + + # Variables + x = slv.mkConst(u, "x") + y = slv.mkConst(u, "y") + + # Functions + f = slv.mkConst(uToInt, "f") + p = slv.mkConst(intPred, "p") + + # Constants + zero = slv.mkReal(0) + one = slv.mkReal(1) + + # Terms + f_x = slv.mkTerm(kinds.ApplyUf, f, x) + f_y = slv.mkTerm(kinds.ApplyUf, f, y) + sum_ = slv.mkTerm(kinds.Plus, f_x, f_y) + p_0 = slv.mkTerm(kinds.ApplyUf, p, zero) + p_f_y = slv.mkTerm(kinds.ApplyUf, p, f_y) + + # Construct the assertions + assertions = slv.mkTerm(kinds.And, + [ + slv.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) + slv.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) + slv.mkTerm(kinds.Leq, sum_, one), # f(x) + f(y) <= 1 + p_0.notTerm(), # not p(0) + p_f_y # p(f(y)) + ]) + + slv.assertFormula(assertions) + + print("Given the following assertions:", assertions, "\n") + print("Prove x /= y is valid.\nCVC4: ", + slv.checkValidAssuming(slv.mkTerm(kinds.Distinct, x, y)), "\n") + + print("Call checkSat to show that the assertions are satisfiable") + print("CVC4:", slv.checkSat(), "\n") + + print("Call slv.getValue(...) on terms of interest") + print("slv.getValue({}): {}".format(f_x, slv.getValue(f_x))) + print("slv.getValue({}): {}".format(f_y, slv.getValue(f_y))) + print("slv.getValue({}): {}".format(sum_, slv.getValue(sum_))) + print("slv.getValue({}): {}".format(p_0, slv.getValue(p_0))) + print("slv.getValue({}): {}".format(p_f_y, slv.getValue(p_f_y)), "\n") + + print("Alternatively, iterate over assertions and call" + " slv.getValue(...) on all terms") + prefixPrintGetValue(slv, assertions) + + print("Alternatively, print the model", "\n") + slv.printModel() + + print() + print("You can also use nested loops to iterate over terms") + for a in assertions: + print("term:", a) + for t in a: + print(" + child: ", t) + + print() diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py new file mode 100755 index 000000000..c5eda1741 --- /dev/null +++ b/examples/api/python/datatypes.py @@ -0,0 +1,137 @@ +#!/usr/bin/env python + +##################### +#! \file datatypes.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## datatypes solver through the Python API. This is a direct translation + ## of datatypes-new.cpp. + +import pycvc4 +from pycvc4 import kinds + +def test(slv, consListSort): + # Now our old "consListSpec" is useless--the relevant information + # has been copied out, so we can throw that spec away. We can get + # the complete spec for the datatype from the DatatypeSort, and + # this Datatype object has constructor symbols (and others) filled in. + + consList = consListSort.getDatatype() + + # t = cons 0 nil + # + # Here, consList["cons"] gives you the DatatypeConstructor. To get + # the constructor symbol for application, use .getConstructor("cons"), + # which is equivalent to consList["cons"].getConstructor(). Note that + # "nil" is a constructor too + + t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil"))) + + print("t is {}\nsort of cons is {}\n sort of nil is {}".format( + t, + consList.getConstructorTerm("cons").getSort(), + consList.getConstructorTerm("nil").getSort())) + + # t2 = head(cons 0 nil), and of course this can be evaluated + # + # Here we first get the DatatypeConstructor for cons (with + # consList["cons"]) in order to get the "head" selector symbol + # to apply. + + t2 = slv.mkTerm(kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), t) + + print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2))) + + # You can also iterate over a Datatype to get all its constructors, + # and over a DatatypeConstructor to get all its "args" (selectors) + for i in consList: + print("ctor:", i) + for j in i: + print(" + args:", j) + print() + + # You can also define parameterized datatypes. + # This example builds a simple parameterized list of sort T, with one + # constructor "cons". + sort = slv.mkParamSort("T") + paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort) + paramCons = pycvc4.DatatypeConstructorDecl("cons") + paramNil = pycvc4.DatatypeConstructorDecl("nil") + paramHead = pycvc4.DatatypeSelectorDecl("head", sort) + paramTail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) + paramCons.addSelector(paramHead) + paramCons.addSelector(paramTail) + paramConsListSpec.addConstructor(paramCons) + paramConsListSpec.addConstructor(paramNil) + + paramConsListSort = slv.mkDatatypeSort(paramConsListSpec) + paramConsIntListSort = paramConsListSort.instantiate([slv.getIntegerSort()]) + paramConsList = paramConsListSort.getDatatype() + + a = slv.mkConst(paramConsIntListSort, "a") + print("term {} is of sort {}".format(a, a.getSort())) + + head_a = slv.mkTerm(kinds.ApplySelector, paramConsList["cons"].getSelectorTerm("head"), a) + print("head_a is {} of sort {}".format(head_a, head_a.getSort())) + print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort()) + + assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkReal(50)) + print("Assert", assertion) + slv.assertFormula(assertion) + print("Expect sat.") + print("CVC4:", slv.checkSat()) + + +if __name__ == "__main__": + slv = pycvc4.Solver() + + # 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. + + consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name + cons = pycvc4.DatatypeConstructorDecl("cons") + head = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort()) + tail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) + cons.addSelector(head) + cons.addSelector(tail) + consListSpec.addConstructor(cons) + nil = pycvc4.DatatypeConstructorDecl("nil") + consListSpec.addConstructor(nil) + + print("spec is {}".format(consListSpec)) + + # Keep in mind that "DatatypeDecl" is the specification class for + # datatypes---"DatatypeDecl" is not itself a CVC4 Sort. + # Now that our Datatype is fully specified, we can get a Sort for it. + # This step resolves the "SelfSort" reference and creates + # symbols for all the constructors, etc. + + consListSort = slv.mkDatatypeSort(consListSpec) + test(slv, consListSort) + + print("### Alternatively, use declareDatatype") + + cons2 = pycvc4.DatatypeConstructorDecl("cons") + head2 = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort()) + tail2 = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) + cons2.addSelector(head2) + cons2.addSelector(tail2) + nil2 = pycvc4.DatatypeConstructorDecl("nil") + ctors = [cons2, nil2] + consListSort2 = slv.declareDatatype("list2", ctors) + test(slv, consListSort2) diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py new file mode 100755 index 000000000..1bfdf652a --- /dev/null +++ b/examples/api/python/extract.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python + +##################### +#! \file extract.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## bit-vector solver through the Python API. This is a direct translation + ## of extract-new.cpp. + +from pycvc4 import Solver +from pycvc4.kinds import BVExtract, Equal + +if __name__ == "__main__": + slv = Solver() + slv.setLogic("QF_BV") + + bitvector32 = slv.mkBitVectorSort(32) + + x = slv.mkConst(bitvector32, "a") + + ext_31_1 = slv.mkOp(BVExtract, 31, 1) + x_31_1 = slv.mkTerm(ext_31_1, x) + + ext_30_0 = slv.mkOp(BVExtract, 30, 0) + x_30_0 = slv.mkTerm(ext_30_0, x) + + ext_31_31 = slv.mkOp(BVExtract, 31, 31) + x_31_31 = slv.mkTerm(ext_31_31, x) + + ext_0_0 = slv.mkOp(BVExtract, 0, 0) + x_0_0 = slv.mkTerm(ext_0_0, x) + + # test getting indices + assert ext_30_0.getIndices() == (30, 0) + + eq = slv.mkTerm(Equal, x_31_1, x_30_0) + print("Asserting:", eq) + slv.assertFormula(eq) + + eq2 = slv.mkTerm(Equal, x_31_31, x_0_0) + print("Check validity assuming:", eq2) + print("Expect valid") + print("CVC4:", slv.checkValidAssuming(eq2)) diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py new file mode 100755 index 000000000..472cf945b --- /dev/null +++ b/examples/api/python/helloworld.py @@ -0,0 +1,21 @@ +#!/usr/bin/env python + +##################### +#! \file helloworld.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A very simple CVC4 tutorial example, adapted from helloworld-new.cpp +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!") + print(helloworld, "is", slv.checkValidAssuming(helloworld)) diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py new file mode 100755 index 000000000..6ae6427b1 --- /dev/null +++ b/examples/api/python/linear_arith.py @@ -0,0 +1,70 @@ +#!/usr/bin/env python + +##################### +#! \file linear_arith.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A simple demonstration of the solving capabilities of the CVC4 +## linear arithmetic solver through the Python API. This is a direct +## translation of linear_arith-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setLogic("QF_LIRA") + + # Prove that if given x (Integer) and y (Real) and some constraints + # then the maximum value of y - x is 2/3 + + # Sorts + real = slv.getRealSort() + integer = slv.getIntegerSort() + + # Variables + x = slv.mkConst(integer, "x") + y = slv.mkConst(real, "y") + + # Constants + three = slv.mkReal(3) + neg2 = slv.mkReal(-2) + two_thirds = slv.mkReal(2, 3) + + # Terms + three_y = slv.mkTerm(kinds.Mult, three, y) + diff = slv.mkTerm(kinds.Minus, y, x) + + # Formulas + x_geq_3y = slv.mkTerm(kinds.Geq, x, three_y) + x_leq_y = slv.mkTerm(kinds.Leq, x ,y) + neg2_lt_x = slv.mkTerm(kinds.Lt, neg2, x) + + assertions = slv.mkTerm(kinds.And, x_geq_3y, x_leq_y, neg2_lt_x) + + print("Given the assertions", assertions) + slv.assertFormula(assertions) + + slv.push() + diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds) + print("Prove that", diff_leq_two_thirds, "with CVC4") + print("CVC4 should report VALID") + print("Result from CVC4 is:", + slv.checkValidAssuming(diff_leq_two_thirds)) + slv.pop() + + print() + + slv.push() + diff_is_two_thirds = slv.mkTerm(kinds.Equal, diff, two_thirds) + slv.assertFormula(diff_is_two_thirds) + print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with CVC4") + print("CVC4 should report SAT") + print("Result from CVC4 is:", slv.checkSat()) + slv.pop() diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py new file mode 100755 index 000000000..584880b2b --- /dev/null +++ b/examples/api/python/sets.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python + +##################### +#! \file sets.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A simple demonstration of the solving capabilities of the CVC4 +## sets solver through the Python API. This is a direct translation +## of sets-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + + # Optionally, set the logic. We need at least UF for equality predicate, + # integers (LIA) and sets (FS). + slv.setLogic("QF_UFLIAFS") + + # Produce models + slv.setOption("produce-models", "true") + slv.setOption("output-language", "smt2") + + integer = slv.getIntegerSort() + set_ = slv.mkSetSort(integer) + + # Verify union distributions over intersection + # (A union B) intersection C = (A intersection C) union (B intersection C) + + A = slv.mkConst(set_, "A") + B = slv.mkConst(set_, "B") + C = slv.mkConst(set_, "C") + + unionAB = slv.mkTerm(kinds.Union, A, B) + lhs = slv.mkTerm(kinds.Intersection, unionAB, C) + + intersectionAC = slv.mkTerm(kinds.Intersection, A, C) + intersectionBC = slv.mkTerm(kinds.Intersection, B, C) + rhs = slv.mkTerm(kinds.Union, intersectionAC, intersectionBC) + + theorem = slv.mkTerm(kinds.Equal, lhs, rhs) + + print("CVC4 reports: {} is {}".format(theorem, + slv.checkValidAssuming(theorem))) + + # Verify emptset is a subset of any set + + A = slv.mkConst(set_, "A") + emptyset = slv.mkEmptySet(set_) + + theorem = slv.mkTerm(kinds.Subset, emptyset, A) + + print("CVC4 reports: {} is {}".format(theorem, + slv.checkValidAssuming(theorem))) + + # Find me an element in 1, 2 intersection 2, 3, if there is one. + + one = slv.mkReal(1) + two = slv.mkReal(2) + three = slv.mkReal(3) + + singleton_one = slv.mkTerm(kinds.Singleton, one) + singleton_two = slv.mkTerm(kinds.Singleton, two) + singleton_three = slv.mkTerm(kinds.Singleton, three) + one_two = slv.mkTerm(kinds.Union, singleton_one, singleton_two) + two_three = slv.mkTerm(kinds.Union, singleton_two, singleton_three) + intersection = slv.mkTerm(kinds.Intersection, one_two, two_three) + + x = slv.mkConst(integer, "x") + + e = slv.mkTerm(kinds.Member, x, intersection) + + result = slv.checkSatAssuming(e) + + print("CVC4 reports: {} is {}".format(e, result)) + + if result: + print("For instance, {} is a member".format(slv.getValue(x))) diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py new file mode 100755 index 000000000..5c8e91997 --- /dev/null +++ b/examples/api/python/strings.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python + +##################### +#! \file strings.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A simple demonstration of the solving capabilities of the CVC4 +## strings solver through the Python API. This is a direct translation +## of strings-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + # Set the logic + slv.setLogic("S") + # Produce models + slv.setOption("produce-models", "true") + # The option strings-exp is needed + slv.setOption("strings-exp", "true") + # Set output language to SMTLIB2 + slv.setOption("output-language", "smt2") + + # String type + string = slv.getStringSort() + + # std::string + str_ab = "ab" + # String constants + ab = slv.mkString(str_ab) + abc = slv.mkString("abc") + # String variables + x = slv.mkConst(string, "x") + y = slv.mkConst(string, "y") + z = slv.mkConst(string, "z") + + # String concatenation: x.ab.y + lhs = slv.mkTerm(kinds.StringConcat, x, ab, y) + # String concatenation: abc.z + rhs = slv.mkTerm(kinds.StringConcat, abc, z) + # x.ab.y = abc.z + formula1 = slv.mkTerm(kinds.Equal, lhs, rhs) + + # Length of y: |y| + leny = slv.mkTerm(kinds.StringLength, y) + # |y| >= 0 + formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkReal(0)) + + # Regular expression: (ab[c-e]*f)|g|h + r = slv.mkTerm(kinds.RegexpUnion, + slv.mkTerm(kinds.RegexpConcat, + slv.mkTerm(kinds.StringToRegexp, slv.mkString("ab")), + slv.mkTerm(kinds.RegexpStar, + slv.mkTerm(kinds.RegexpRange, slv.mkString("c"), slv.mkString("e"))), + slv.mkTerm(kinds.StringToRegexp, slv.mkString("f"))), + slv.mkTerm(kinds.StringToRegexp, slv.mkString("g")), + slv.mkTerm(kinds.StringToRegexp, slv.mkString("h"))) + + # String variables + s1 = slv.mkConst(string, "s1") + s2 = slv.mkConst(string, "s2") + # String concatenation: s1.s2 + s = slv.mkTerm(kinds.StringConcat, s1, s2) + + # s1.s2 in (ab[c-e]*f)|g|h + formula3 = slv.mkTerm(kinds.StringInRegexp, s, r) + + # Make a query + q = slv.mkTerm(kinds.And, + formula1, + formula2, + formula3) + + # check sat + result = slv.checkSatAssuming(q) + print("CVC4 reports:", q, "is", result) + + if result: + print("x = ", slv.getValue(x)) + print(" s1.s2 =", slv.getValue(s)) |