diff options
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/bitvectors-new.cpp | 18 | ||||
-rw-r--r-- | examples/api/bitvectors.cpp | 12 | ||||
-rw-r--r-- | examples/api/combination-new.cpp | 7 | ||||
-rw-r--r-- | examples/api/combination.cpp | 4 | ||||
-rw-r--r-- | examples/api/extract-new.cpp | 6 | ||||
-rw-r--r-- | examples/api/extract.cpp | 4 | ||||
-rw-r--r-- | examples/api/helloworld-new.cpp | 2 | ||||
-rw-r--r-- | examples/api/helloworld.cpp | 3 | ||||
-rw-r--r-- | examples/api/java/BitVectors.java | 8 | ||||
-rw-r--r-- | examples/api/java/Combination.java | 7 | ||||
-rw-r--r-- | examples/api/java/HelloWorld.java | 2 | ||||
-rw-r--r-- | examples/api/java/LinearArith.java | 5 | ||||
-rw-r--r-- | examples/api/linear_arith-new.cpp | 6 | ||||
-rw-r--r-- | examples/api/linear_arith.cpp | 5 | ||||
-rwxr-xr-x | examples/api/python/bitvectors.py | 20 | ||||
-rwxr-xr-x | examples/api/python/combination.py | 6 | ||||
-rwxr-xr-x | examples/api/python/extract.py | 8 | ||||
-rwxr-xr-x | examples/api/python/helloworld.py | 4 | ||||
-rwxr-xr-x | examples/api/python/linear_arith.py | 6 | ||||
-rwxr-xr-x | examples/api/python/sets.py | 6 | ||||
-rw-r--r-- | examples/api/sets-new.cpp | 8 | ||||
-rw-r--r-- | examples/api/sets.cpp | 6 |
22 files changed, 79 insertions, 74 deletions
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index 4578da733..ebb8ee7ee 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -87,9 +87,9 @@ int main() slv.assertFormula(assignment1); Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); - cout << " Check validity assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl; + cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; cout << " Popping context. " << endl; slv.pop(); @@ -103,15 +103,15 @@ int main() cout << "Asserting " << assignment2 << " to CVC4 " << endl; slv.assertFormula(assignment2); - cout << " Check validity assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl; + cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); std::vector<Term> v{new_x_eq_new_x_, x_neq_x}; - cout << " Check Validity Assuming: " << v << endl; - cout << " Expect invalid. " << endl; - cout << " CVC4: " << slv.checkValidAssuming(v) << endl; + cout << " Check entailment assuming: " << v << endl; + cout << " Expect NOT_ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(v) << endl; // Assert that a is odd Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 259eb48ff..494a45abc 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -87,8 +87,8 @@ int main() { Expr new_x_eq_new_x_ = em.mkExpr(kind::EQUAL, new_x, new_x_); cout << " Querying: " << new_x_eq_new_x_ << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; + cout << " Expect entailed. " << endl; + cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl; cout << " Popping context. " << endl; smt.pop(); @@ -103,14 +103,14 @@ int main() { smt.assertFormula(assignment2); cout << " Querying: " << new_x_eq_new_x_ << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl; Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr(); std::vector<Expr> v{new_x_eq_new_x_, x_neq_x}; cout << " Querying: " << v << endl; - cout << " Expect invalid. " << endl; - cout << " CVC4: " << smt.query(v) << endl; + cout << " Expect NOT_ENTAILED. " << endl; + cout << " CVC4: " << smt.checkEntailed(v) << endl; // Assert that a is odd Expr extract_op = em.mkConst(BitVectorExtract(0, 0)); diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp index 5284a0119..546d9ee9c 100644 --- a/examples/api/combination-new.cpp +++ b/examples/api/combination-new.cpp @@ -82,9 +82,10 @@ int main() cout << "Given the following assertions:" << endl << assertions << endl << endl; - cout << "Prove x /= y is valid. " << endl - << "CVC4: " << slv.checkValidAssuming(slv.mkTerm(DISTINCT, x, y)) - << "." << endl << endl; + cout << "Prove x /= y is entailed. " << endl + << "CVC4: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." + << endl + << endl; cout << "Call checkSat to show that the assertions are satisfiable. " << endl diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 646e6b17a..2e972a543 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -86,8 +86,8 @@ int main() { cout << "Given the following assumptions:" << endl << assumptions << endl - << "Prove x /= y is valid. " - << "CVC4 says: " << smt.query(em.mkExpr(kind::DISTINCT, x, y)) + << "Prove x /= y is entailed. " + << "CVC4 says: " << smt.checkEntailed(em.mkExpr(kind::DISTINCT, x, y)) << "." << endl; cout << "Now we call checksat on a trivial query to show that" << endl diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index 0f0f8243a..705cdd90f 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -47,9 +47,9 @@ int main() slv.assertFormula(eq); Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); - cout << " Check validity assuming: " << eq2 << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << slv.checkValidAssuming(eq2) << endl; + cout << " Check entailment assuming: " << eq2 << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(eq2) << endl; return 0; } diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index a008ec718..e2558df28 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -48,8 +48,8 @@ int main() { Expr eq2 = em.mkExpr(kind::EQUAL, x_31_31, x_0_0); cout << " Querying: " << eq2 << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << smt.query(eq2) << endl; + cout << " Expect entailed. " << endl; + cout << " CVC4: " << smt.checkEntailed(eq2) << endl; return 0; } diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp index ab869f03c..f442c1412 100644 --- a/examples/api/helloworld-new.cpp +++ b/examples/api/helloworld-new.cpp @@ -24,7 +24,7 @@ int main() { Solver slv; Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); - std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld) + std::cout << helloworld << " is " << slv.checkEntailed(helloworld) << std::endl; return 0; } diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index befeaa7bd..49a334504 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -23,6 +23,7 @@ int main() { ExprManager em; Expr helloworld = em.mkVar("Hello World!", em.booleanType()); SmtEngine smt(&em); - std::cout << helloworld << " is " << smt.query(helloworld) << std::endl; + std::cout << helloworld << " is " << smt.checkEntailed(helloworld) + << std::endl; return 0; } diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 17111b63a..bb2245a6f 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -86,8 +86,8 @@ public class BitVectors { Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_); System.out.println(" Querying: " + new_x_eq_new_x_); - System.out.println(" Expect valid. "); - System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_)); + System.out.println(" Expect entailed. "); + System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_)); System.out.println(" Popping context. "); smt.pop(); @@ -102,7 +102,7 @@ public class BitVectors { smt.assertFormula(assignment2); System.out.println(" Querying: " + new_x_eq_new_x_); - System.out.println(" Expect valid. "); - System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_)); + System.out.println(" Expect entailed. "); + System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_)); } } diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 0c9ca84d6..53b1fa92d 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -83,10 +83,9 @@ public class Combination { System.out.println("Given the following assumptions:"); System.out.println(assumptions); - System.out.println("Prove x /= y is valid. " + - "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) + - "."); - + System.out.println("Prove x /= y is entailed. " + + "CVC4 says: " + smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y)) + + "."); System.out.println("Now we call checksat on a trivial query to show that"); System.out.println("the assumptions are satisfiable: " + diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 393ce40f0..a08f3d452 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -30,6 +30,6 @@ public class HelloWorld { Expr helloworld = em.mkVar("Hello World!", em.booleanType()); SmtEngine smt = new SmtEngine(em); - System.out.println(helloworld + " is " + smt.query(helloworld)); + System.out.println(helloworld + " is " + smt.checkEntailed(helloworld)); } } diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 2ddf92584..e060263b4 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -61,8 +61,9 @@ public class LinearArith { smt.push(); Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds); System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4."); - System.out.println("CVC4 should report VALID."); - System.out.println("Result from CVC4 is: " + smt.query(diff_leq_two_thirds)); + System.out.println("CVC4 should report ENTAILED."); + System.out.println( + "Result from CVC4 is: " + smt.checkEntailed(diff_leq_two_thirds)); smt.pop(); System.out.println(); diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp index a4ff9a2cc..887c35d24 100644 --- a/examples/api/linear_arith-new.cpp +++ b/examples/api/linear_arith-new.cpp @@ -62,9 +62,9 @@ int main() slv.push(); Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report VALID." << endl; - cout << "Result from CVC4 is: " - << slv.checkValidAssuming(diff_leq_two_thirds) << endl; + cout << "CVC4 should report ENTAILED." << endl; + cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds) + << endl; slv.pop(); cout << endl; diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index f1c8b861c..9e605f85c 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -62,8 +62,9 @@ int main() { smt.push(); Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds); cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report VALID." << endl; - cout << "Result from CVC4 is: " << smt.query(diff_leq_two_thirds) << endl; + cout << "CVC4 should report ENTAILED." << endl; + cout << "Result from CVC4 is: " << smt.checkEntailed(diff_leq_two_thirds) + << endl; smt.pop(); cout << endl; diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 773974cc7..8e4e1b682 100755 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -4,7 +4,7 @@ #! \file bitvectors.py ## \verbatim ## Top contributors (to current version): - ## Makai Mann + ## Makai Mann, Aina Niemetz ## 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. @@ -82,9 +82,9 @@ if __name__ == "__main__": 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("Checking entailment assuming:", new_x_eq_new_x_) + print("Expect ENTAILED.") + print("CVC4:", slv.checkEntailment(new_x_eq_new_x_)) print("Popping context.") slv.pop() @@ -98,16 +98,16 @@ if __name__ == "__main__": 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_)) + print("Checking entailment assuming:", new_x_eq_new_x_) + print("Expect ENTAILED.") + print("CVC4:", slv.checkEntailed(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)) + print("Check entailment assuming: ", v) + print("Expect NOT_ENTAILED.") + print("CVC4:", slv.checkEntailed(v)) # Assert that a is odd extract_op = slv.mkOp(kinds.BVExtract, 0, 0) diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index 1b488d7d5..7a8055bdf 100755 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -4,7 +4,7 @@ #! \file combination.py ## \verbatim ## Top contributors (to current version): - ## Makai Mann + ## Makai Mann, Aina Niemetz ## 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. @@ -69,8 +69,8 @@ if __name__ == "__main__": 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("Prove x /= y is entailed.\nCVC4: ", + slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n") print("Call checkSat to show that the assertions are satisfiable") print("CVC4:", slv.checkSat(), "\n") diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index 1bfdf652a..2b8714739 100755 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -4,7 +4,7 @@ #! \file extract.py ## \verbatim ## Top contributors (to current version): - ## Makai Mann + ## Makai Mann, Aina Niemetz ## 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. @@ -46,6 +46,6 @@ if __name__ == "__main__": 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)) + print("Check entailment assuming:", eq2) + print("Expect ENTAILED") + print("CVC4:", slv.checkEntailed(eq2)) diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py index 472cf945b..5607d7f83 100755 --- a/examples/api/python/helloworld.py +++ b/examples/api/python/helloworld.py @@ -4,7 +4,7 @@ #! \file helloworld.py ## \verbatim ## Top contributors (to current version): -## Makai Mann +## Makai Mann, Aina Niemetz ## 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. @@ -18,4 +18,4 @@ from pycvc4 import kinds if __name__ == "__main__": slv = pycvc4.Solver() helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!") - print(helloworld, "is", slv.checkValidAssuming(helloworld)) + print(helloworld, "is", slv.checkEntailed(helloworld)) diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index 6ae6427b1..bab9680b3 100755 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -4,7 +4,7 @@ #! \file linear_arith.py ## \verbatim ## Top contributors (to current version): -## Makai Mann +## Makai Mann, Aina Niemetz ## 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. @@ -54,9 +54,9 @@ if __name__ == "__main__": 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("CVC4 should report ENTAILED") print("Result from CVC4 is:", - slv.checkValidAssuming(diff_leq_two_thirds)) + slv.checkEntailed(diff_leq_two_thirds)) slv.pop() print() diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 584880b2b..b69c56b56 100755 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -4,7 +4,7 @@ #! \file sets.py ## \verbatim ## Top contributors (to current version): -## Makai Mann +## Makai Mann, Aina Niemetz ## 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. @@ -48,7 +48,7 @@ if __name__ == "__main__": theorem = slv.mkTerm(kinds.Equal, lhs, rhs) print("CVC4 reports: {} is {}".format(theorem, - slv.checkValidAssuming(theorem))) + slv.checkEntailed(theorem))) # Verify emptset is a subset of any set @@ -58,7 +58,7 @@ if __name__ == "__main__": theorem = slv.mkTerm(kinds.Subset, emptyset, A) print("CVC4 reports: {} is {}".format(theorem, - slv.checkValidAssuming(theorem))) + slv.checkEntailed(theorem))) # Find me an element in 1, 2 intersection 2, 3, if there is one. diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp index 2ca3db9d2..21ef925df 100644 --- a/examples/api/sets-new.cpp +++ b/examples/api/sets-new.cpp @@ -52,8 +52,8 @@ int main() Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - cout << "CVC4 reports: " << theorem << " is " - << slv.checkValidAssuming(theorem) << "." << endl; + cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) + << "." << endl; } // Verify emptset is a subset of any set @@ -63,8 +63,8 @@ int main() Term theorem = slv.mkTerm(SUBSET, emptyset, A); - cout << "CVC4 reports: " << theorem << " is " - << slv.checkValidAssuming(theorem) << "." << endl; + cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) + << "." << endl; } // Find me an element in {1, 2} intersection {2, 3}, if there is one. diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 9fb342431..eb6a5a350 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -55,7 +55,8 @@ int main() { Expr theorem = em.mkExpr(kind::EQUAL, lhs, rhs); - cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl; + cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem) + << "." << endl; } // Verify emptset is a subset of any set @@ -65,7 +66,8 @@ int main() { Expr theorem = em.mkExpr(kind::SUBSET, emptyset, A); - cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl; + cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem) + << "." << endl; } // Find me an element in {1, 2} intersection {2, 3}, if there is one. |