From cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 31 Mar 2020 18:12:16 -0700 Subject: Rename checkValid/query to checkEntailed. (#4191) This renames api::Solver::checkValidAssuming to checkEntailed and removes api::Solver::checkValid. Internally, SmtEngine::query is renamed to SmtEngine::checkEntailed, and these changes are further propagated to the Result class. --- examples/SimpleVC.java | 7 ++++--- examples/SimpleVC.ml | 6 +++--- examples/SimpleVC.php | 6 +++--- examples/SimpleVC.pl | 6 +++--- examples/SimpleVC.py | 6 +++--- examples/SimpleVC.rb | 6 +++--- examples/SimpleVC.tcl | 6 +++--- examples/api/bitvectors-new.cpp | 18 +++++++++--------- examples/api/bitvectors.cpp | 12 ++++++------ examples/api/combination-new.cpp | 7 ++++--- examples/api/combination.cpp | 4 ++-- examples/api/extract-new.cpp | 6 +++--- examples/api/extract.cpp | 4 ++-- examples/api/helloworld-new.cpp | 2 +- examples/api/helloworld.cpp | 3 ++- examples/api/java/BitVectors.java | 8 ++++---- examples/api/java/Combination.java | 7 +++---- examples/api/java/HelloWorld.java | 2 +- examples/api/java/LinearArith.java | 5 +++-- examples/api/linear_arith-new.cpp | 6 +++--- examples/api/linear_arith.cpp | 5 +++-- examples/api/python/bitvectors.py | 20 ++++++++++---------- examples/api/python/combination.py | 6 +++--- examples/api/python/extract.py | 8 ++++---- examples/api/python/helloworld.py | 4 ++-- examples/api/python/linear_arith.py | 6 +++--- examples/api/python/sets.py | 6 +++--- examples/api/sets-new.cpp | 8 ++++---- examples/api/sets.cpp | 6 ++++-- examples/simple_vc_cxx.cpp | 6 +++--- 30 files changed, 104 insertions(+), 98 deletions(-) (limited to 'examples') diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index e77a5e99f..798dc08af 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -55,8 +55,9 @@ public class SimpleVC { new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)). impExpr(new Expr(twox_plus_y_geq_3)); - System.out.println("Checking validity of formula " + formula + " with CVC4."); - System.out.println("CVC4 should report VALID."); - System.out.println("Result from CVC4 is: " + smt.query(formula)); + System.out.println( + "Checking entailment of formula " + formula + " with CVC4."); + System.out.println("CVC4 should report ENTAILED."); + System.out.println("Result from CVC4 is: " + smt.checkEntailed(formula)); } } diff --git a/examples/SimpleVC.ml b/examples/SimpleVC.ml index c89341dc8..d9d78586b 100644 --- a/examples/SimpleVC.ml +++ b/examples/SimpleVC.ml @@ -79,13 +79,13 @@ let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3) let bformula = new_Expr(formula) in -print_string "Checking validity of formula " ; +print_string "Checking entailment of formula " ; print_string (get_string (formula->toString ())) ; print_string " with CVC4." ; print_newline () ; -print_string "CVC4 should report VALID." ; +print_string "CVC4 should report ENTAILED." ; print_newline () ; print_string "Result from CVC4 is: " ; -print_string (get_string (smt->query(bformula)->toString ())) ; +print_string (get_string (smt->checkEntailed(bformula)->toString ())) ; print_newline () ;; diff --git a/examples/SimpleVC.php b/examples/SimpleVC.php index 329446703..031c0a1c5 100755 --- a/examples/SimpleVC.php +++ b/examples/SimpleVC.php @@ -50,7 +50,7 @@ my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three); my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3)); -print "Checking validity of formula " . $formula->toString() . " with CVC4.\n"; -print "CVC4 should report VALID.\n"; -print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n"; +print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n"; +print "CVC4 should report ENTAILED.\n"; +print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n"; diff --git a/examples/SimpleVC.pl b/examples/SimpleVC.pl index 998c28bb0..20ad6c737 100755 --- a/examples/SimpleVC.pl +++ b/examples/SimpleVC.pl @@ -50,7 +50,7 @@ my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three); my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3)); -print "Checking validity of formula " . $formula->toString() . " with CVC4.\n"; -print "CVC4 should report VALID.\n"; -print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n"; +print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n"; +print "CVC4 should report ENTAILED.\n"; +print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n"; diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py index 4c21d35c0..5550974c9 100755 --- a/examples/SimpleVC.py +++ b/examples/SimpleVC.py @@ -53,9 +53,9 @@ def main(): formula = Expr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(Expr(twox_plus_y_geq_3)) - print("Checking validity of formula " + formula.toString() + " with CVC4.") - print("CVC4 should report VALID.") - print("Result from CVC4 is: " + smt.query(formula).toString()) + print("Checking entailment of formula " + formula.toString() + " with CVC4.") + print("CVC4 should report ENTAILED .") + print("Result from CVC4 is: " + smt.checkEntailed(formula).toString()) return 0 diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb index 0d19ef49f..4f289d34f 100755 --- a/examples/SimpleVC.rb +++ b/examples/SimpleVC.rb @@ -49,9 +49,9 @@ twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three) formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3)) -puts "Checking validity of formula " + formula.toString + " with CVC4." -puts "CVC4 should report VALID." -puts "Result from CVC4 is: " + smt.query(formula).toString +puts "Checking entailment of formula " + formula.toString + " with CVC4." +puts "CVC4 should report ENTAILED." +puts "Result from CVC4 is: " + smt.checkEntailed(formula).toString exit diff --git a/examples/SimpleVC.tcl b/examples/SimpleVC.tcl index ed0decb26..4e1c76c5a 100755 --- a/examples/SimpleVC.tcl +++ b/examples/SimpleVC.tcl @@ -48,7 +48,7 @@ set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three] set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]] -puts "Checking validity of formula [Expr_toString $formula] with CVC4." -puts "CVC4 should report VALID." -puts "Result from CVC4 is: [Result_toString [SmtEngine_query smt $formula]]" +puts "Checking entailment of formula [Expr_toString $formula] with CVC4." +puts "CVC4 should report ENTAILED." +puts "Result from CVC4 is: [Result_toString [SmtEngine_checkEntailed smt $formula]]" 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 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 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. diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 25a05a1a7..cfd14b089 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -50,9 +50,9 @@ int main() { em.mkExpr(kind::AND, x_positive, y_positive). impExpr(twox_plus_y_geq_3); - cout << "Checking validity of formula " << formula << " with CVC4." << endl; - cout << "CVC4 should report VALID." << endl; - cout << "Result from CVC4 is: " << smt.query(formula) << endl; + cout << "Checking entailment of formula " << formula << " with CVC4." << endl; + cout << "CVC4 should report ENTAILED." << endl; + cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl; return 0; } -- cgit v1.2.3