diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-31 18:12:16 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-31 18:12:16 -0700 |
| commit | cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 (patch) | |
| tree | e69411603787d99cea12d729ec0a0a2ae8889f20 | |
| parent | 186b3872a3de454d0f30224dc2e0a396163c3fdc (diff) | |
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.
268 files changed, 693 insertions, 691 deletions
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<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. 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; } diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fa727088e..fff4bef85 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -768,22 +768,22 @@ bool Result::isSatUnknown(void) const && d_result->isSat() == CVC4::Result::SAT_UNKNOWN; } -bool Result::isValid(void) const +bool Result::isEntailed(void) const { - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::VALID; + return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC4::Result::ENTAILED; } -bool Result::isInvalid(void) const +bool Result::isNotEntailed(void) const { - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::INVALID; + return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED; } -bool Result::isValidUnknown(void) const +bool Result::isEntailmentUnknown(void) const { - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN; + return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN; } bool Result::operator==(const Result& r) const @@ -3585,7 +3585,7 @@ Term Solver::simplify(const Term& t) CVC4_API_SOLVER_TRY_CATCH_END; } -Result Solver::checkValid(void) const +Result Solver::checkEntailed(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); @@ -3593,14 +3593,15 @@ Result Solver::checkValid(void) const || CVC4::options::incrementalSolving()) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; + CVC4_API_ARG_CHECK_NOT_NULL(term); - CVC4::Result r = d_smtEngine->query(); + CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; } -Result Solver::checkValidAssuming(Term assumption) const +Result Solver::checkEntailed(const std::vector<Term>& terms) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); @@ -3608,29 +3609,13 @@ Result Solver::checkValidAssuming(Term assumption) const || CVC4::options::incrementalSolving()) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; - CVC4_API_ARG_CHECK_NOT_NULL(assumption); - - CVC4::Result r = d_smtEngine->query(*assumption.d_expr); - return Result(r); - - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(!d_smtEngine->isQueryMade() - || CVC4::options::incrementalSolving()) - << "Cannot make multiple queries unless incremental solving is enabled " - "(try --incremental)"; - for (const Term& assumption : assumptions) + for (const Term& term : terms) { - CVC4_API_ARG_CHECK_NOT_NULL(assumption); + CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector<Expr> eassumptions = termVectorToExprs(assumptions); - CVC4::Result r = d_smtEngine->query(eassumptions); + std::vector<Expr> exprs = termVectorToExprs(terms); + CVC4::Result r = d_smtEngine->checkEntailed(exprs); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 3c99d2480..1a1cd3b61 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -114,22 +114,21 @@ class CVC4_PUBLIC Result bool isSatUnknown() const; /** - * Return true if corresponding query was a valid checkValid() or - * checkValidAssuming() query. + * Return true if corresponding query was an entailed checkEntailed() query. */ - bool isValid() const; + bool isEntailed() const; /** - * Return true if corresponding query was an invalid checkValid() or - * checkValidAssuming() query. + * Return true if corresponding query was a checkEntailed() query that is + * not entailed. */ - bool isInvalid() const; + bool isNotEntailed() const; /** - * Return true if query was a checkValid() or checkValidAssuming() query - * and CVC4 was not able to determine (in)validity. + * Return true if query was a checkEntailed() () query and CVC4 was not able + * to determine if it is entailed. */ - bool isValidUnknown() const; + bool isEntailmentUnknown() const; /** * Operator overloading for equality of two results. @@ -2555,24 +2554,19 @@ class CVC4_PUBLIC Solver Result checkSatAssuming(const std::vector<Term>& assumptions) const; /** - * Check validity. - * @return the result of the validity check. + * Check entailment of the given formula w.r.t. the current set of assertions. + * @param term the formula to check entailment for + * @return the result of the entailment check. */ - Result checkValid() const; + Result checkEntailed(Term term) const; /** - * Check validity assuming the given formula. - * @param assumption the formula to assume - * @return the result of the validity check. - */ - Result checkValidAssuming(Term assumption) const; - - /** - * Check validity assuming the given formulas. - * @param assumptions the formulas to assume - * @return the result of the validity check. + * Check entailment of the given set of given formulas w.r.t. the current + * set of assertions. + * @param terms the terms to check entailment for + * @return the result of the entailmentcheck. */ - Result checkValidAssuming(const std::vector<Term>& assumptions) const; + Result checkEntailed(const std::vector<Term>& terms) const; /** * Create datatype sort. diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index bbff6f58b..d81d0c0bf 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -87,9 +87,9 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": bint isSat() except + bint isUnsat() except + bint isSatUnknown() except + - bint isValid() except + - bint isInvalid() except + - bint isValidUnknown() except + + bint isEntailed() except + + bint isNotEntailed() except + + bint isEntailmentUnknown() except + string getUnknownExplanation() except + string toString() except + @@ -168,8 +168,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": void assertFormula(Term term) except + Result checkSat() except + Result checkSatAssuming(const vector[Term]& assumptions) except + - Result checkValid() except + - Result checkValidAssuming(const vector[Term]& assumptions) except + + Result checkEntailed(const vector[Term]& assumptions) except + Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors) Term declareFun(const string& symbol, Sort sort) except + Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 188753122..60bd89cbd 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -749,19 +749,11 @@ cdef class Solver: explanation = r.getUnknownExplanation().decode() return Result(name, explanation) - def checkValid(self): - cdef c_Result r = self.csolver.checkValid() - name = r.toString().decode() - explanation = "" - if r.isValidUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) - @expand_list_arg(num_req_args=0) - def checkValidAssuming(self, *assumptions): + def checkEntailed(self, *assumptions): ''' Supports the following arguments: - Result checkValidAssuming(List[Term] assumptions) + Result checkEntailed(List[Term] assumptions) where assumptions can also be comma-separated arguments of type (boolean) Term @@ -771,10 +763,10 @@ cdef class Solver: cdef vector[c_Term] v for a in assumptions: v.push_back((<Term?> a).cterm) - r = self.csolver.checkValidAssuming(<const vector[c_Term]&> v) + r = self.csolver.checkEntailed(<const vector[c_Term]&> v) name = r.toString().decode() explanation = "" - if r.isValidUnknown(): + if r.isEntailmentUnknown(): explanation = r.getUnknownExplanation().decode() return Result(name, explanation) diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 79cc465ac..20f2dcff9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -513,7 +513,7 @@ void QueryCommand::invoke(SmtEngine* smtEngine) { try { - d_result = smtEngine->query(d_expr); + d_result = smtEngine->checkEntailed(d_expr); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 10fc76bf7..2e1716543 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1766,7 +1766,7 @@ Result SmtEngine::check() { resourceManager->out()) { Result::UnknownExplanation why = resourceManager->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; - return Result(Result::VALIDITY_UNKNOWN, why, d_filename); + return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename); } // Make sure the prop layer has all of the assertions @@ -1791,7 +1791,8 @@ Result SmtEngine::check() { Result SmtEngine::quickCheck() { Assert(d_fullyInited); Trace("smt") << "SMT quickCheck()" << endl; - return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename); + return Result( + Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename); } theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const @@ -1807,7 +1808,8 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const { std::stringstream ss; ss << "Cannot " << c - << " unless immediately preceded by SAT/INVALID or UNKNOWN response."; + << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN " + "response."; throw RecoverableModalException(ss.str().c_str()); } @@ -2380,35 +2382,34 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) return checkSatisfiability(assumptions, inUnsatCore, false); } -Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) +Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore) { - Dump("benchmark") << QueryCommand(assumption, inUnsatCore); - return checkSatisfiability(assumption.isNull() - ? std::vector<Expr>() - : std::vector<Expr>{assumption}, - inUnsatCore, - true) - .asValidityResult(); + Dump("benchmark") << QueryCommand(expr, inUnsatCore); + return checkSatisfiability( + expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, + inUnsatCore, + true) + .asEntailmentResult(); } -Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore) +Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore) { - return checkSatisfiability(assumptions, inUnsatCore, true).asValidityResult(); + return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult(); } Result SmtEngine::checkSatisfiability(const Expr& expr, bool inUnsatCore, - bool isQuery) + bool isEntailmentCheck) { return checkSatisfiability( expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, inUnsatCore, - isQuery); + isEntailmentCheck); } Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, bool inUnsatCore, - bool isQuery) + bool isEntailmentCheck) { try { @@ -2416,7 +2417,8 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, finalOptionsAreSet(); doPendingPops(); - Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" + Trace("smt") << "SmtEngine::" + << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" << assumptions << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -2434,7 +2436,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, setProblemExtended(); - if (isQuery) + if (isEntailmentCheck) { size_t size = assumptions.size(); if (size > 1) @@ -2540,8 +2542,8 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, d_smtMode = SMT_MODE_SAT_UNKNOWN; } - Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" - << assumptions << ") => " << r << endl; + Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") + << "(" << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. if(options::checkModels()) { @@ -2587,7 +2589,7 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) { throw RecoverableModalException( "Cannot get unsat assumptions unless immediately preceded by " - "UNSAT/VALID response."); + "UNSAT/ENTAILED."); } finalOptionsAreSet(); if (Dump.isOn("benchmark")) @@ -2625,7 +2627,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) } bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv); - return quickCheck().asValidityResult(); + return quickCheck().asEntailmentResult(); }/* SmtEngine::assertFormula() */ /* @@ -3218,13 +3220,13 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) Expr heap; Expr nil; Model* m = getAvailableModel("get separation logic heap and nil"); - if (m->getHeapModel(heap, nil)) + if (!m->getHeapModel(heap, nil)) { - return std::make_pair(heap, nil); + InternalError() + << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil " + "expressions from theory model."; } - InternalError() - << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil " - "expressions from theory model."; + return std::make_pair(heap, nil); } std::vector<Expr> SmtEngine::getExpandedAssertions() @@ -3294,8 +3296,8 @@ UnsatCore SmtEngine::getUnsatCoreInternal() if (d_smtMode != SMT_MODE_UNSAT) { throw RecoverableModalException( - "Cannot get an unsat core unless immediately preceded by UNSAT/VALID " - "response."); + "Cannot get an unsat core unless immediately preceded by " + "UNSAT/ENTAILED response."); } d_proofManager->traceUnsatCore(); // just to trigger core creation @@ -3800,7 +3802,7 @@ const Proof& SmtEngine::getProof() if (d_smtMode != SMT_MODE_UNSAT) { throw RecoverableModalException( - "Cannot get a proof unless immediately preceded by UNSAT/VALID " + "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED " "response."); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2cb227fc9..37b89cfb7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -152,7 +152,9 @@ class CVC4_PUBLIC SmtEngine */ bool isFullyInited() { return d_fullyInited; } - /** Return true if a query() or checkSat() has already been made. */ + /** + * Return true if a checkEntailed() or checkSatisfiability() has been made. + */ bool isQueryMade() { return d_queryMade; } /** Return the user context level. */ @@ -211,8 +213,8 @@ class CVC4_PUBLIC SmtEngine std::string getFilename() const; /** - * Get the model (only if immediately preceded by a SAT - * or INVALID query). Only permitted if produce-models is on. + * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED + * query). Only permitted if produce-models is on. */ Model* getModel(); @@ -230,9 +232,9 @@ class CVC4_PUBLIC SmtEngine /** * Block the current model values of (at least) the values in exprs. - * Can be called only if immediately preceded by a SAT or INVALID query. Only - * permitted if produce-models is on, and the block-models option is set to a - * mode other than "none". + * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query. + * Only permitted if produce-models is on, and the block-models option is set + * to a mode other than "none". * * This adds an assertion to the assertion stack of the form: * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn))) @@ -310,18 +312,21 @@ class CVC4_PUBLIC SmtEngine Result assertFormula(const Expr& e, bool inUnsatCore = true); /** - * Check validity of an expression with respect to the current set - * of assertions by asserting the query expression's negation and - * calling check(). Returns valid, invalid, or unknown result. + * Check if a given (set of) expression(s) is entailed with respect to the + * current set of assertions. We check this by asserting the negation of + * the (big AND over the) given (set of) expression(s). + * Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result. * * @throw Exception */ - Result query(const Expr& assumption = Expr(), bool inUnsatCore = true); - Result query(const std::vector<Expr>& assumptions, bool inUnsatCore = true); + Result checkEntailed(const Expr& assumption = Expr(), + bool inUnsatCore = true); + Result checkEntailed(const std::vector<Expr>& assumptions, + bool inUnsatCore = true); /** * Assert a formula (if provided) to the current context and call - * check(). Returns sat, unsat, or unknown result. + * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result. * * @throw Exception */ @@ -456,9 +461,9 @@ class CVC4_PUBLIC SmtEngine Expr expandDefinitions(const Expr& e); /** - * Get the assigned value of an expr (only if immediately preceded - * by a SAT or INVALID query). Only permitted if the SmtEngine is - * set to operate interactively and produce-models is on. + * Get the assigned value of an expr (only if immediately preceded by a SAT + * or NOT_ENTAILED query). Only permitted if the SmtEngine is set to operate + * interactively and produce-models is on. * * @throw ModalException, TypeCheckingException, LogicException, * UnsafeInterruptException @@ -483,15 +488,15 @@ class CVC4_PUBLIC SmtEngine /** * Get the assignment (only if immediately preceded by a SAT or - * INVALID query). Only permitted if the SmtEngine is set to + * NOT_ENTAILED query). Only permitted if the SmtEngine is set to * operate interactively and produce-assignments is on. */ std::vector<std::pair<Expr, Expr> > getAssignment(); /** - * Get the last proof (only if immediately preceded by an UNSAT - * or VALID query). Only permitted if CVC4 was built with proof - * support and produce-proofs is on. + * Get the last proof (only if immediately preceded by an UNSAT or ENTAILED + * query). Only permitted if CVC4 was built with proof support and + * produce-proofs is on. * * The Proof object is owned by this SmtEngine until the SmtEngine is * destroyed. @@ -624,9 +629,9 @@ class CVC4_PUBLIC SmtEngine std::vector<std::vector<Expr> >& tvecs); /** - * Get an unsatisfiable core (only if immediately preceded by an - * UNSAT or VALID query). Only permitted if CVC4 was built with - * unsat-core support and produce-unsat-cores is on. + * Get an unsatisfiable core (only if immediately preceded by an UNSAT or + * ENTAILED query). Only permitted if CVC4 was built with unsat-core support + * and produce-unsat-cores is on. */ UnsatCore getUnsatCore(); @@ -714,8 +719,8 @@ class CVC4_PUBLIC SmtEngine * * Note that the cumulative timer only ticks away when one of the * SmtEngine's workhorse functions (things like assertFormula(), - * query(), checkSat(), and simplify()) are running. Between calls, - * the timer is still. + * checkEntailed(), checkSat(), and simplify()) are running. + * Between calls, the timer is still. * * When an SmtEngine is first created, it has no time or resource * limits. @@ -774,7 +779,10 @@ class CVC4_PUBLIC SmtEngine /** Flush statistic from this SmtEngine. Safe to use in a signal handler. */ void safeFlushStatistics(int fd) const; - /** Returns the most recent result of checkSat/query or (set-info :status). */ + /** + * Returns the most recent result of checkSat/checkEntailed or + * (set-info :status). + */ Result getStatusOfLastCommand() const { return d_status; } /** @@ -881,7 +889,7 @@ class CVC4_PUBLIC SmtEngine /** * Internal method to get an unsatisfiable core (only if immediately preceded - * by an UNSAT or VALID query). Only permitted if CVC4 was built with + * by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with * unsat-core support and produce-unsat-cores is on. Does not dump the * command. */ @@ -1007,13 +1015,13 @@ class CVC4_PUBLIC SmtEngine bool userVisible = true, const char* dumpTag = "declarations"); - /* Check satisfiability (used for query and check-sat). */ + /* Check satisfiability (used to check satisfiability and entailment). */ Result checkSatisfiability(const Expr& assumption, bool inUnsatCore, - bool isQuery); + bool isEntailmentCheck); Result checkSatisfiability(const std::vector<Expr>& assumptions, bool inUnsatCore, - bool isQuery); + bool isEntailmentCheck); /** * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is @@ -1123,9 +1131,9 @@ class CVC4_PUBLIC SmtEngine /** * The list of assumptions from the previous call to checkSatisfiability. - * Note that if the last call to checkSatisfiability was a validity check, - * i.e., a call to query(a1, ..., an), then d_assumptions contains one single - * assumption ~(a1 AND ... AND an). + * Note that if the last call to checkSatisfiability was an entailment check, + * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains + * one single assumption ~(a1 AND ... AND an). */ std::vector<Expr> d_assumptions; @@ -1189,10 +1197,10 @@ class CVC4_PUBLIC SmtEngine bool d_fullyInited; /** - * Whether or not a query() or checkSat() has already been made through - * this SmtEngine. If true, and incrementalSolving is false, then - * attempting an additional query() or checkSat() will fail with a - * ModalException. + * Whether or not a checkEntailed() or checkSatisfiability() has already been + * made through this SmtEngine. If true, and incrementalSolving is false, + * then attempting an additional checkEntailed() or checkSat() will fail with + * a ModalException. */ bool d_queryMade; @@ -1214,7 +1222,8 @@ class CVC4_PUBLIC SmtEngine bool d_globalNegation; /** - * Most recent result of last checkSat/query or (set-info :status). + * Most recent result of last checkSatisfiability/checkEntailed or + * (set-info :status). */ Result d_status; diff --git a/src/util/result.cpp b/src/util/result.cpp index 433dcbf29..916e16b4f 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -29,59 +29,68 @@ namespace CVC4 { Result::Result() : d_sat(SAT_UNKNOWN), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_NONE), d_unknownExplanation(UNKNOWN_REASON), - d_inputName("") {} + d_inputName("") +{ +} Result::Result(enum Sat s, std::string inputName) : d_sat(s), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_SAT), d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { + d_inputName(inputName) +{ PrettyCheckArgument(s != SAT_UNKNOWN, "Must provide a reason for satisfiability being unknown"); } -Result::Result(enum Validity v, std::string inputName) +Result::Result(enum Entailment e, std::string inputName) : d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), + d_entailment(e), + d_which(TYPE_ENTAILMENT), d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { - PrettyCheckArgument(v != VALIDITY_UNKNOWN, - "Must provide a reason for validity being unknown"); + d_inputName(inputName) +{ + PrettyCheckArgument(e != ENTAILMENT_UNKNOWN, + "Must provide a reason for entailment being unknown"); } -Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation, +Result::Result(enum Sat s, + enum UnknownExplanation unknownExplanation, std::string inputName) : d_sat(s), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_SAT), d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { + d_inputName(inputName) +{ PrettyCheckArgument(s == SAT_UNKNOWN, "improper use of unknown-result constructor"); } -Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation, +Result::Result(enum Entailment e, + enum UnknownExplanation unknownExplanation, std::string inputName) : d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), + d_entailment(e), + d_which(TYPE_ENTAILMENT), d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { - PrettyCheckArgument(v == VALIDITY_UNKNOWN, + d_inputName(inputName) +{ + PrettyCheckArgument(e == ENTAILMENT_UNKNOWN, "improper use of unknown-result constructor"); } Result::Result(const std::string& instr, std::string inputName) : d_sat(SAT_UNKNOWN), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_NONE), d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { + d_inputName(inputName) +{ string s = instr; transform(s.begin(), s.end(), s.begin(), ::tolower); if (s == "sat" || s == "satisfiable") { @@ -90,38 +99,56 @@ Result::Result(const std::string& instr, std::string inputName) } else if (s == "unsat" || s == "unsatisfiable") { d_which = TYPE_SAT; d_sat = UNSAT; - } else if (s == "valid") { - d_which = TYPE_VALIDITY; - d_validity = VALID; - } else if (s == "invalid") { - d_which = TYPE_VALIDITY; - d_validity = INVALID; - } else if (s == "incomplete") { + } + else if (s == "entailed") + { + d_which = TYPE_ENTAILMENT; + d_entailment = ENTAILED; + } + else if (s == "not_entailed") + { + d_which = TYPE_ENTAILMENT; + d_entailment = NOT_ENTAILED; + } + else if (s == "incomplete") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = INCOMPLETE; - } else if (s == "timeout") { + } + else if (s == "timeout") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = TIMEOUT; - } else if (s == "resourceout") { + } + else if (s == "resourceout") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = RESOURCEOUT; - } else if (s == "memout") { + } + else if (s == "memout") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = MEMOUT; - } else if (s == "interrupted") { + } + else if (s == "interrupted") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = INTERRUPTED; - } else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { + } + else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; - } else { + } + else + { IllegalArgument(s, - "expected satisfiability/validity result, " + "expected satisfiability/entailment result, " "instead got `%s'", s.c_str()); } @@ -142,37 +169,41 @@ bool Result::operator==(const Result& r) const { return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN || d_unknownExplanation == r.d_unknownExplanation); } - if (d_which == TYPE_VALIDITY) { - return d_validity == r.d_validity && - (d_validity != VALIDITY_UNKNOWN || - d_unknownExplanation == r.d_unknownExplanation); + if (d_which == TYPE_ENTAILMENT) + { + return d_entailment == r.d_entailment + && (d_entailment != ENTAILMENT_UNKNOWN + || d_unknownExplanation == r.d_unknownExplanation); } return false; } bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; } -bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; } +bool operator==(enum Result::Entailment e, const Result& r) { return r == e; } bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); } -bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); } +bool operator!=(enum Result::Entailment e, const Result& r) +{ + return !(e == r); +} Result Result::asSatisfiabilityResult() const { if (d_which == TYPE_SAT) { return *this; } - if (d_which == TYPE_VALIDITY) { - switch (d_validity) { - case INVALID: - return Result(SAT, d_inputName); + if (d_which == TYPE_ENTAILMENT) + { + switch (d_entailment) + { + case NOT_ENTAILED: return Result(SAT, d_inputName); - case VALID: - return Result(UNSAT, d_inputName); + case ENTAILED: return Result(UNSAT, d_inputName); - case VALIDITY_UNKNOWN: + case ENTAILMENT_UNKNOWN: return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); - default: Unhandled() << d_validity; + default: Unhandled() << d_entailment; } } @@ -180,28 +211,28 @@ Result Result::asSatisfiabilityResult() const { return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); } -Result Result::asValidityResult() const { - if (d_which == TYPE_VALIDITY) { +Result Result::asEntailmentResult() const +{ + if (d_which == TYPE_ENTAILMENT) + { return *this; } if (d_which == TYPE_SAT) { switch (d_sat) { - case SAT: - return Result(INVALID, d_inputName); + case SAT: return Result(NOT_ENTAILED, d_inputName); - case UNSAT: - return Result(VALID, d_inputName); + case UNSAT: return Result(ENTAILED, d_inputName); case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); + return Result(ENTAILMENT_UNKNOWN, d_unknownExplanation, d_inputName); default: Unhandled() << d_sat; } } // TYPE_NONE - return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName); + return Result(ENTAILMENT_UNKNOWN, NO_STATUS, d_inputName); } string Result::toString() const { @@ -226,18 +257,14 @@ ostream& operator<<(ostream& out, enum Result::Sat s) { return out; } -ostream& operator<<(ostream& out, enum Result::Validity v) { - switch (v) { - case Result::INVALID: - out << "INVALID"; - break; - case Result::VALID: - out << "VALID"; - break; - case Result::VALIDITY_UNKNOWN: - out << "VALIDITY_UNKNOWN"; - break; - default: Unhandled() << v; +ostream& operator<<(ostream& out, enum Result::Entailment e) +{ + switch (e) + { + case Result::NOT_ENTAILED: out << "NOT_ENTAILED"; break; + case Result::ENTAILED: out << "ENTAILED"; break; + case Result::ENTAILMENT_UNKNOWN: out << "ENTAILMENT_UNKNOWN"; break; + default: Unhandled() << e; } return out; } @@ -301,14 +328,11 @@ void Result::toStreamDefault(std::ostream& out) const { break; } } else { - switch (isValid()) { - case Result::INVALID: - out << "invalid"; - break; - case Result::VALID: - out << "valid"; - break; - case Result::VALIDITY_UNKNOWN: + switch (isEntailed()) + { + case Result::NOT_ENTAILED: out << "not_entailed"; break; + case Result::ENTAILED: out << "entailed"; break; + case Result::ENTAILMENT_UNKNOWN: out << "unknown"; if (whyUnknown() != Result::UNKNOWN_REASON) { out << " (" << whyUnknown() << ")"; @@ -332,11 +356,17 @@ void Result::toStreamTptp(std::ostream& out) const { out << "Satisfiable"; } else if (isSat() == Result::UNSAT) { out << "Unsatisfiable"; - } else if (isValid() == Result::VALID) { + } + else if (isEntailed() == Result::ENTAILED) + { out << "Theorem"; - } else if (isValid() == Result::INVALID) { + } + else if (isEntailed() == Result::NOT_ENTAILED) + { out << "CounterSatisfiable"; - } else { + } + else + { out << "GaveUp"; } out << " for " << getInputName(); diff --git a/src/util/result.h b/src/util/result.h index f34a9bb5a..10df05388 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -38,9 +38,19 @@ class CVC4_PUBLIC Result { public: enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 }; - enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 }; + enum Entailment + { + NOT_ENTAILED = 0, + ENTAILED = 1, + ENTAILMENT_UNKNOWN = 2 + }; - enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE }; + enum Type + { + TYPE_SAT, + TYPE_ENTAILMENT, + TYPE_NONE + }; enum UnknownExplanation { REQUIRES_FULL_CHECK, @@ -57,7 +67,7 @@ class CVC4_PUBLIC Result { private: enum Sat d_sat; - enum Validity d_validity; + enum Entailment d_entailment; enum Type d_which; enum UnknownExplanation d_unknownExplanation; std::string d_inputName; @@ -67,12 +77,13 @@ class CVC4_PUBLIC Result { Result(enum Sat s, std::string inputName = ""); - Result(enum Validity v, std::string inputName = ""); + Result(enum Entailment v, std::string inputName = ""); Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = ""); - Result(enum Validity v, enum UnknownExplanation unknownExplanation, + Result(enum Entailment v, + enum UnknownExplanation unknownExplanation, std::string inputName = ""); Result(const std::string& s, std::string inputName = ""); @@ -84,12 +95,13 @@ class CVC4_PUBLIC Result { enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } - enum Validity isValid() const { - return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; + enum Entailment isEntailed() const + { + return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN; } bool isUnknown() const { - return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; + return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN; } Type getType() const { return d_which; } @@ -101,7 +113,7 @@ class CVC4_PUBLIC Result { bool operator==(const Result& r) const; inline bool operator!=(const Result& r) const; Result asSatisfiabilityResult() const; - Result asValidityResult() const; + Result asEntailmentResult() const; std::string toString() const; @@ -128,7 +140,7 @@ class CVC4_PUBLIC Result { * Write a Result out to a stream. * * The default implementation writes a reasonable string in lowercase - * for sat, unsat, valid, invalid, or unknown results. This behavior + * for sat, unsat, entailed, not entailed, or unknown results. This behavior * is overridable by each Printer, since sometimes an output language * has a particular preference for how results should appear. */ @@ -139,15 +151,15 @@ inline bool Result::operator!=(const Result& r) const { return !(*this == r); } std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, - enum Result::Validity v) CVC4_PUBLIC; + enum Result::Entailment e) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) CVC4_PUBLIC; bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC; -bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC; +bool operator==(enum Result::Entailment e, const Result& r) CVC4_PUBLIC; bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC; -bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC; +bool operator!=(enum Result::Entailment e, const Result& r) CVC4_PUBLIC; } /* CVC4 namespace */ diff --git a/src/util/result.i b/src/util/result.i index b77bfd881..cb835fbb0 100644 --- a/src/util/result.i +++ b/src/util/result.i @@ -8,13 +8,13 @@ %ignore CVC4::Result::operator!=(const Result& r) const; %ignore CVC4::operator<<(std::ostream&, enum Result::Sat); -%ignore CVC4::operator<<(std::ostream&, enum Result::Validity); +%ignore CVC4::operator<<(std::ostream&, enum Result::Entailment); %ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); %ignore CVC4::operator==(enum Result::Sat, const Result&); %ignore CVC4::operator!=(enum Result::Sat, const Result&); -%ignore CVC4::operator==(enum Result::Validity, const Result&); -%ignore CVC4::operator!=(enum Result::Validity, const Result&); +%ignore CVC4::operator==(enum Result::Entailment, const Result&); +%ignore CVC4::operator!=(enum Result::Entailment, const Result&); %include "util/result.h" diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc index 1de397ab1..08d591590 100644 --- a/test/regress/regress0/arith/arith.01.cvc +++ b/test/regress/regress0/arith/arith.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc index d7b0291f7..e0a48c357 100644 --- a/test/regress/regress0/arith/arith.02.cvc +++ b/test/regress/regress0/arith/arith.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; z : REAL; diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc index 288c341ef..ce54c8b7e 100644 --- a/test/regress/regress0/arith/arith.03.cvc +++ b/test/regress/regress0/arith/arith.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; diff --git a/test/regress/regress0/arith/bug549.cvc b/test/regress/regress0/arith/bug549.cvc index 54df5e62c..bfb3e75d5 100644 --- a/test/regress/regress0/arith/bug549.cvc +++ b/test/regress/regress0/arith/bug549.cvc @@ -1,3 +1,3 @@ -% EXPECT: valid +% EXPECT: entailed a, b : REAL; -QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
\ No newline at end of file +QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a; diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc index 265d18a84..84954a3ea 100644 --- a/test/regress/regress0/arith/integers/arith-int-014.cvc +++ b/test/regress/regress0/arith/integers/arith-int-014.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ; ASSERT (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3; diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc index d2e2639ab..8f8b01fc9 100644 --- a/test/regress/regress0/arith/integers/arith-int-015.cvc +++ b/test/regress/regress0/arith/integers/arith-int-015.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ; ASSERT (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28; diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc index 345c90899..66f02401b 100644 --- a/test/regress/regress0/arith/integers/arith-int-021.cvc +++ b/test/regress/regress0/arith/integers/arith-int-021.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc index 01d51a226..b3d79e8ff 100644 --- a/test/regress/regress0/arith/integers/arith-int-023.cvc +++ b/test/regress/regress0/arith/integers/arith-int-023.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc index 5a11212d5..e905da9a0 100644 --- a/test/regress/regress0/arith/integers/arith-int-025.cvc +++ b/test/regress/regress0/arith/integers/arith-int-025.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc index c38231695..b6db26e86 100644 --- a/test/regress/regress0/arith/integers/arith-int-042.cvc +++ b/test/regress/regress0/arith/integers/arith-int-042.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ; ASSERT (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ; diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc index 77571e526..3fd20a0b6 100644 --- a/test/regress/regress0/arith/integers/arith-int-042.min.cvc +++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x1: INT; x0: INT; QUERY NOT (((x0 * 6) + (x1 * 32)) = 1); diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc index 7fa2fc937..1739b3364 100644 --- a/test/regress/regress0/arith/integers/arith-int-079.cvc +++ b/test/regress/regress0/arith/integers/arith-int-079.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ; ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ; diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc index d79ec94a7..ed6cb747e 100644 --- a/test/regress/regress0/arith/integers/arith-interval.cvc +++ b/test/regress/regress0/arith/integers/arith-interval.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x: INT; P: INT -> BOOLEAN; diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc index 9d1029cbf..07a2aa2f5 100644 --- a/test/regress/regress0/boolean-prec.cvc +++ b/test/regress/regress0/boolean-prec.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of AND, <=>, NOT. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/bug310.cvc b/test/regress/regress0/bug310.cvc index 0cb6cf0fe..12cb80494 100644 --- a/test/regress/regress0/bug310.cvc +++ b/test/regress/regress0/bug310.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed b : BOOLEAN; DATATYPE D = c(s:INT) END; QUERY c(IF b THEN 1 ELSE 0 ENDIF) = IF b THEN c(1) ELSE c(0) ENDIF; diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc index 304dd6ec4..400f55885 100644 --- a/test/regress/regress0/bug32.cvc +++ b/test/regress/regress0/bug32.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a:BOOLEAN; b:BOOLEAN; ASSERT(a); diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc index fa9462f64..0e06cbc13 100644 --- a/test/regress/regress0/bug322b.cvc +++ b/test/regress/regress0/bug322b.cvc @@ -1,7 +1,7 @@ % COMMAND-LINE: --incremental -% EXPECT: valid -% EXPECT: valid -% EXPECT: valid +% EXPECT: entailed +% EXPECT: entailed +% EXPECT: entailed x : INT; y : INT = x + 1; z : INT = -10; diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc index c51af4e24..665bcdafb 100644 --- a/test/regress/regress0/bug486.cvc +++ b/test/regress/regress0/bug486.cvc @@ -1,6 +1,6 @@ % COMMAND-LINE: --finite-model-find -i -% EXPECT: invalid -% EXPECT: valid +% EXPECT: not_entailed +% EXPECT: entailed prin:TYPE; form:TYPE; diff --git a/test/regress/regress0/bv/bvcomp.cvc b/test/regress/regress0/bv/bvcomp.cvc index b9b4b8e17..17064a2f2 100644 --- a/test/regress/regress0/bv/bvcomp.cvc +++ b/test/regress/regress0/bv/bvcomp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : BITVECTOR(10); diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc index dcacd643a..6bc649a03 100644 --- a/test/regress/regress0/bv/bvsimple.cvc +++ b/test/regress/regress0/bv/bvsimple.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Some tests from the CVC3 user manual. % http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html diff --git a/test/regress/regress0/cvc-rerror-print.cvc b/test/regress/regress0/cvc-rerror-print.cvc index dd05723d2..e134b5666 100644 --- a/test/regress/regress0/cvc-rerror-print.cvc +++ b/test/regress/regress0/cvc-rerror-print.cvc @@ -1,5 +1,5 @@ -% EXPECT: valid -% EXPECT: Cannot get model unless immediately preceded by SAT/INVALID or UNKNOWN response. +% EXPECT: entailed +% EXPECT: Cannot get model unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN response. OPTION "logic" "ALL"; OPTION "produce-models" true; x : INT; diff --git a/test/regress/regress0/cvc3-bug15.cvc b/test/regress/regress0/cvc3-bug15.cvc index 860ce38bd..779a2eab4 100644 --- a/test/regress/regress0/cvc3-bug15.cvc +++ b/test/regress/regress0/cvc3-bug15.cvc @@ -1,5 +1,5 @@ %% This test borrowed from CVC3 regressions, bug15.cvc -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; f : REAL -> REAL; diff --git a/test/regress/regress0/cvc3.userdoc.01.cvc b/test/regress/regress0/cvc3.userdoc.01.cvc index 7c89de4ac..e3e9aaf0a 100644 --- a/test/regress/regress0/cvc3.userdoc.01.cvc +++ b/test/regress/regress0/cvc3.userdoc.01.cvc @@ -1,31 +1,31 @@ % COMMAND-LINE: --incremental -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0000111101010000 = 0hex0f50; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin01@0bin0 = 0bin010; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0011[3:1] = 0bin001; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0011 << 3 = 0bin0011000; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin1000 >> 3 = 0bin0001; -% EXPECT: valid +% EXPECT: entailed QUERY SX(0bin100, 5) = 0bin11100; -% EXPECT: valid +% EXPECT: entailed QUERY BVZEROEXTEND(0bin1,3) = 0bin0001; -% EXPECT: valid +% EXPECT: entailed QUERY BVREPEAT(0bin10,3) = 0bin101010; -% EXPECT: valid +% EXPECT: entailed QUERY BVROTL(0bin101,1) = 0bin011; -% EXPECT: valid +% EXPECT: entailed QUERY BVROTR(0bin101,1) = 0bin110; diff --git a/test/regress/regress0/cvc3.userdoc.02.cvc b/test/regress/regress0/cvc3.userdoc.02.cvc index b6329e953..e143ea275 100644 --- a/test/regress/regress0/cvc3.userdoc.02.cvc +++ b/test/regress/regress0/cvc3.userdoc.02.cvc @@ -2,6 +2,6 @@ x : BITVECTOR(5); y : BITVECTOR(4); yy : BITVECTOR(3); -% EXPECT: valid +% EXPECT: entailed QUERY BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ; diff --git a/test/regress/regress0/cvc3.userdoc.03.cvc b/test/regress/regress0/cvc3.userdoc.03.cvc index 4fc6a5f8c..3b3829ebc 100644 --- a/test/regress/regress0/cvc3.userdoc.03.cvc +++ b/test/regress/regress0/cvc3.userdoc.03.cvc @@ -1,7 +1,7 @@ bv : BITVECTOR(10); a : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] AND diff --git a/test/regress/regress0/cvc3.userdoc.04.cvc b/test/regress/regress0/cvc3.userdoc.04.cvc index 824690bcf..da8b1e82c 100644 --- a/test/regress/regress0/cvc3.userdoc.04.cvc +++ b/test/regress/regress0/cvc3.userdoc.04.cvc @@ -5,5 +5,5 @@ ASSERT x&y&t&z&q = x; ASSERT x|y = t; ASSERT BVXOR(x,~x) = t; -% EXPECT: valid +% EXPECT: entailed QUERY FALSE; diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc b/test/regress/regress0/cvc3.userdoc.05.cvc index 37da96b3c..85e0c2105 100644 --- a/test/regress/regress0/cvc3.userdoc.05.cvc +++ b/test/regress/regress0/cvc3.userdoc.05.cvc @@ -3,7 +3,7 @@ x, y : BITVECTOR(4); ASSERT x = 0hex5; ASSERT y = 0bin0101; -% EXPECT: valid +% EXPECT: entailed QUERY BVMULT(8,x,y)=BVMULT(8,y,x) AND diff --git a/test/regress/regress0/cvc3.userdoc.06.cvc b/test/regress/regress0/cvc3.userdoc.06.cvc index 3801b6d53..3968365ad 100644 --- a/test/regress/regress0/cvc3.userdoc.06.cvc +++ b/test/regress/regress0/cvc3.userdoc.06.cvc @@ -6,8 +6,8 @@ z, t : BITVECTOR(12); ASSERT x = 0hexff; ASSERT z = 0hexff0; -% EXPECT: valid +% EXPECT: entailed QUERY z = x << 4; -% EXPECT: valid +% EXPECT: entailed QUERY (z >> 4)[7:0] = x; diff --git a/test/regress/regress0/datatypes/bug286.cvc b/test/regress/regress0/datatypes/bug286.cvc index 501f5f737..33a320acd 100644 --- a/test/regress/regress0/datatypes/bug286.cvc +++ b/test/regress/regress0/datatypes/bug286.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE foo = f(i:INT) END; x : foo; y : INT; diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc index 8e2818106..e28fc6305 100644 --- a/test/regress/regress0/datatypes/datatype-dump.cvc +++ b/test/regress/regress0/datatypes/datatype-dump.cvc @@ -10,7 +10,7 @@ % EXPECT: END; % EXPECT: x : nat; % EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x)); -% EXPECT: invalid +% EXPECT: not_entailed % DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/datatypes/datatype.cvc b/test/regress/regress0/datatypes/datatype.cvc index 20fec4fdd..6a0e97fc3 100644 --- a/test/regress/regress0/datatypes/datatype.cvc +++ b/test/regress/regress0/datatypes/datatype.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/datatypes/datatype0.cvc b/test/regress/regress0/datatypes/datatype0.cvc index 8fff50a86..0b9e41024 100644 --- a/test/regress/regress0/datatypes/datatype0.cvc +++ b/test/regress/regress0/datatypes/datatype0.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc index 3934959f1..9e746c0e4 100644 --- a/test/regress/regress0/datatypes/datatype1.cvc +++ b/test/regress/regress0/datatypes/datatype1.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype13.cvc b/test/regress/regress0/datatypes/datatype13.cvc index 91e582dbd..78d28be00 100644 --- a/test/regress/regress0/datatypes/datatype13.cvc +++ b/test/regress/regress0/datatypes/datatype13.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE enum = enum1 | enum2 diff --git a/test/regress/regress0/datatypes/datatype2.cvc b/test/regress/regress0/datatypes/datatype2.cvc index 939dff197..64c84de45 100644 --- a/test/regress/regress0/datatypes/datatype2.cvc +++ b/test/regress/regress0/datatypes/datatype2.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc index fff1a5dd7..ce99edbb7 100644 --- a/test/regress/regress0/datatypes/datatype3.cvc +++ b/test/regress/regress0/datatypes/datatype3.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype4.cvc b/test/regress/regress0/datatypes/datatype4.cvc index 217777bdf..83962f49a 100644 --- a/test/regress/regress0/datatypes/datatype4.cvc +++ b/test/regress/regress0/datatypes/datatype4.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE TypeGeneric = generic END; diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc index 4f6320028..b6950845e 100644 --- a/test/regress/regress0/datatypes/empty_tuprec.cvc +++ b/test/regress/regress0/datatypes/empty_tuprec.cvc @@ -7,15 +7,15 @@ b1, b2 : [##]; % empty records (a unit type) c1, c2 : [[]]; % 1-tuples of the empty tuple (a unit type) d1, d2 : [#x:[[##]],y:[#z:[]#]#]; % more complicated records (still a unit type) -% EXPECT: valid +% EXPECT: entailed QUERY a1 = a2; -% EXPECT: valid +% EXPECT: entailed QUERY b1 = b2; -% EXPECT: valid +% EXPECT: entailed QUERY c1 = c2; -% EXPECT: valid +% EXPECT: entailed QUERY d1 = d2; diff --git a/test/regress/regress0/datatypes/mutually-recursive.cvc b/test/regress/regress0/datatypes/mutually-recursive.cvc index b86b647b5..5bd857b6e 100644 --- a/test/regress/regress0/datatypes/mutually-recursive.cvc +++ b/test/regress/regress0/datatypes/mutually-recursive.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat2) | zero, nat2 = succ2(pred2 : nat) | zero2 END; diff --git a/test/regress/regress0/datatypes/rec1.cvc b/test/regress/regress0/datatypes/rec1.cvc index 79c9facda..b3e205985 100644 --- a/test/regress/regress0/datatypes/rec1.cvc +++ b/test/regress/regress0/datatypes/rec1.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed c : BOOLEAN; a17 : BOOLEAN = ((# _a := 2, _b := 2 #) = ( IF c THEN (# _a := 3, _b := 2 #) diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc index 44d523a46..56864c088 100644 --- a/test/regress/regress0/datatypes/rec2.cvc +++ b/test/regress/regress0/datatypes/rec2.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed c : BOOLEAN; a16 : [# _a : INT, _b : INT #] = ( IF c THEN (# _a := 3, _b := 2 #) diff --git a/test/regress/regress0/datatypes/rec4.cvc b/test/regress/regress0/datatypes/rec4.cvc index 08a9988ef..f7f29755f 100644 --- a/test/regress/regress0/datatypes/rec4.cvc +++ b/test/regress/regress0/datatypes/rec4.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a : BOOLEAN; a49 : BOOLEAN = ( IF a THEN (# _a := 1 #) diff --git a/test/regress/regress0/datatypes/rewriter.cvc b/test/regress/regress0/datatypes/rewriter.cvc index 18f8b3441..e9b7662a0 100644 --- a/test/regress/regress0/datatypes/rewriter.cvc +++ b/test/regress/regress0/datatypes/rewriter.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % simple test for rewriter cases diff --git a/test/regress/regress0/datatypes/tuple-record-bug.cvc b/test/regress/regress0/datatypes/tuple-record-bug.cvc index 33c68dece..0e519a64f 100644 --- a/test/regress/regress0/datatypes/tuple-record-bug.cvc +++ b/test/regress/regress0/datatypes/tuple-record-bug.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed Mem_0 : TYPE = ARRAY INT OF INT; diff --git a/test/regress/regress0/datatypes/tuple.cvc b/test/regress/regress0/datatypes/tuple.cvc index 366737525..00ab8d4db 100644 --- a/test/regress/regress0/datatypes/tuple.cvc +++ b/test/regress/regress0/datatypes/tuple.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x: [REAL,INT,REAL] = ( 4/5, 9, 11/9 ); first_elem: REAL = x.0; third_elem: REAL = x.2; diff --git a/test/regress/regress0/datatypes/typed_v10l30054.cvc b/test/regress/regress0/datatypes/typed_v10l30054.cvc index ee414ed65..72c23d888 100644 --- a/test/regress/regress0/datatypes/typed_v10l30054.cvc +++ b/test/regress/regress0/datatypes/typed_v10l30054.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v1l80005.cvc b/test/regress/regress0/datatypes/typed_v1l80005.cvc index 988646f21..95b1a935f 100644 --- a/test/regress/regress0/datatypes/typed_v1l80005.cvc +++ b/test/regress/regress0/datatypes/typed_v1l80005.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v2l30079.cvc b/test/regress/regress0/datatypes/typed_v2l30079.cvc index f32c9e551..2295d1518 100644 --- a/test/regress/regress0/datatypes/typed_v2l30079.cvc +++ b/test/regress/regress0/datatypes/typed_v2l30079.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v3l20092.cvc b/test/regress/regress0/datatypes/typed_v3l20092.cvc index c6260e233..e067852df 100644 --- a/test/regress/regress0/datatypes/typed_v3l20092.cvc +++ b/test/regress/regress0/datatypes/typed_v3l20092.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v5l30069.cvc b/test/regress/regress0/datatypes/typed_v5l30069.cvc index 05d0247cc..f980acc69 100644 --- a/test/regress/regress0/datatypes/typed_v5l30069.cvc +++ b/test/regress/regress0/datatypes/typed_v5l30069.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v10l40099.cvc b/test/regress/regress0/datatypes/v10l40099.cvc index 7b2da4b65..257bf2ccc 100644 --- a/test/regress/regress0/datatypes/v10l40099.cvc +++ b/test/regress/regress0/datatypes/v10l40099.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v2l40025.cvc b/test/regress/regress0/datatypes/v2l40025.cvc index fc466f300..d3411e12e 100644 --- a/test/regress/regress0/datatypes/v2l40025.cvc +++ b/test/regress/regress0/datatypes/v2l40025.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc index b7019e7ae..ea27672d5 100644 --- a/test/regress/regress0/datatypes/v3l60006.cvc +++ b/test/regress/regress0/datatypes/v3l60006.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v5l30058.cvc b/test/regress/regress0/datatypes/v5l30058.cvc index be101b8fb..d3db742ae 100644 --- a/test/regress/regress0/datatypes/v5l30058.cvc +++ b/test/regress/regress0/datatypes/v5l30058.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc index b0dbdc46e..67be78912 100644 --- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/fmf/bug-041417-set-options.cvc b/test/regress/regress0/fmf/bug-041417-set-options.cvc index 16f59f78c..c4e9ba834 100644 --- a/test/regress/regress0/fmf/bug-041417-set-options.cvc +++ b/test/regress/regress0/fmf/bug-041417-set-options.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed OPTION "finite-model-find"; OPTION "fmf-fun"; diff --git a/test/regress/regress0/let.cvc b/test/regress/regress0/let.cvc index 996b09d39..d0f5c5e1f 100644 --- a/test/regress/regress0/let.cvc +++ b/test/regress/regress0/let.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed U: TYPE; a: U; b: U; diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc index 2c2ac2f79..305f2d396 100644 --- a/test/regress/regress0/logops.01.cvc +++ b/test/regress/regress0/logops.01.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc index 67415e95d..c74c11983 100644 --- a/test/regress/regress0/logops.02.cvc +++ b/test/regress/regress0/logops.02.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: invalid +% EXPECT: not_entailed QUERY NOT c AND b; diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc index 42298a8f4..1c86ce594 100644 --- a/test/regress/regress0/logops.03.cvc +++ b/test/regress/regress0/logops.03.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc index 89a9db320..254b0ed87 100644 --- a/test/regress/regress0/logops.04.cvc +++ b/test/regress/regress0/logops.04.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (a => b) <=> (NOT a OR b); diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc index 1ec94e5ae..2897dbc0c 100644 --- a/test/regress/regress0/logops.05.cvc +++ b/test/regress/regress0/logops.05.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY TRUE XOR FALSE; diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc index 5115a90c1..3ede8d211 100644 --- a/test/regress/regress0/precedence/and-not.cvc +++ b/test/regress/regress0/precedence/and-not.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of AND and NOT. A, B: BOOLEAN; diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc index 879becbbf..ec69087d1 100644 --- a/test/regress/regress0/precedence/and-xor.cvc +++ b/test/regress/regress0/precedence/and-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of XOR and AND. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/bool-cmp.cvc b/test/regress/regress0/precedence/bool-cmp.cvc index b8729e92a..4f81c86ad 100644 --- a/test/regress/regress0/precedence/bool-cmp.cvc +++ b/test/regress/regress0/precedence/bool-cmp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of comparisons and booleans x , y, z: INT; diff --git a/test/regress/regress0/precedence/cmp-plus.cvc b/test/regress/regress0/precedence/cmp-plus.cvc index a7c07fe30..54ee7b8f8 100644 --- a/test/regress/regress0/precedence/cmp-plus.cvc +++ b/test/regress/regress0/precedence/cmp-plus.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of comparisons and plus/minus x, y, z: INT; diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc index 9e581d514..af81ea10d 100644 --- a/test/regress/regress0/precedence/eq-fun.cvc +++ b/test/regress/regress0/precedence/eq-fun.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of function application and = T : TYPE; diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc index 745cc7474..4643292b6 100644 --- a/test/regress/regress0/precedence/iff-assoc.cvc +++ b/test/regress/regress0/precedence/iff-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right associativity of <=> A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc index 947433c88..24181487d 100644 --- a/test/regress/regress0/precedence/iff-implies.cvc +++ b/test/regress/regress0/precedence/iff-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of <=> and =>. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc index 1a7cef3b1..c6883c6ad 100644 --- a/test/regress/regress0/precedence/implies-assoc.cvc +++ b/test/regress/regress0/precedence/implies-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right associativity of => A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc index 3de26eb18..9ebed72d4 100644 --- a/test/regress/regress0/precedence/implies-iff.cvc +++ b/test/regress/regress0/precedence/implies-iff.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of <=> and =>. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc index d724d33ef..883e7d4a1 100644 --- a/test/regress/regress0/precedence/implies-or.cvc +++ b/test/regress/regress0/precedence/implies-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of => and OR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc index fc671d7b5..579531ded 100644 --- a/test/regress/regress0/precedence/not-and.cvc +++ b/test/regress/regress0/precedence/not-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of AND and NOT. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc index f658c127e..f8c7366be 100644 --- a/test/regress/regress0/precedence/not-eq.cvc +++ b/test/regress/regress0/precedence/not-eq.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of = and NOT. A, B: INT; diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc index 209df8559..746f142e4 100644 --- a/test/regress/regress0/precedence/or-implies.cvc +++ b/test/regress/regress0/precedence/or-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of => and OR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc index 2a25bac63..405cb68b7 100644 --- a/test/regress/regress0/precedence/or-xor.cvc +++ b/test/regress/regress0/precedence/or-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of OR and XOR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc index 5d980f90d..57b9b99cf 100644 --- a/test/regress/regress0/precedence/plus-mult.cvc +++ b/test/regress/regress0/precedence/plus-mult.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of plus/minus and mult/divide a, b, c, d, e: INT; diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc index 68896db10..08c939c5e 100644 --- a/test/regress/regress0/precedence/xor-and.cvc +++ b/test/regress/regress0/precedence/xor-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of XOR and AND. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc index f31324a53..5f4646b1f 100644 --- a/test/regress/regress0/precedence/xor-assoc.cvc +++ b/test/regress/regress0/precedence/xor-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for left associativity of XOR A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc index 757286764..87abc0e73 100644 --- a/test/regress/regress0/precedence/xor-or.cvc +++ b/test/regress/regress0/precedence/xor-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of OR and XOR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_00.cvc b/test/regress/regress0/preprocess/preprocess_00.cvc index c86843535..2e51a42ad 100644 --- a/test/regress/regress0/preprocess/preprocess_00.cvc +++ b/test/regress/regress0/preprocess/preprocess_00.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_02.cvc b/test/regress/regress0/preprocess/preprocess_02.cvc index e2c93a359..0f94103f6 100644 --- a/test/regress/regress0/preprocess/preprocess_02.cvc +++ b/test/regress/regress0/preprocess/preprocess_02.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_06.cvc b/test/regress/regress0/preprocess/preprocess_06.cvc index 3e45c529a..abcc7a6ac 100644 --- a/test/regress/regress0/preprocess/preprocess_06.cvc +++ b/test/regress/regress0/preprocess/preprocess_06.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc index 8b26c0d08..9a6cd797c 100644 --- a/test/regress/regress0/preprocess/preprocess_13.cvc +++ b/test/regress/regress0/preprocess/preprocess_13.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc index 267a316e8..966668002 100644 --- a/test/regress/regress0/printer/tuples_and_records.cvc +++ b/test/regress/regress0/printer/tuples_and_records.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed % EXPECT: ((r.a, "active")) % EXPECT: ((y.1, 9)) OPTION "produce-models"; diff --git a/test/regress/regress0/push-pop/bug233.cvc b/test/regress/regress0/push-pop/bug233.cvc index 2b9eedcdb..1a6049329 100644 --- a/test/regress/regress0/push-pop/bug233.cvc +++ b/test/regress/regress0/push-pop/bug233.cvc @@ -3,9 +3,9 @@ a, b: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (a AND b) OR NOT (a AND b); -% EXPECT: invalid +% EXPECT: not_entailed QUERY (a OR b); diff --git a/test/regress/regress0/push-pop/incremental-subst-bug.cvc b/test/regress/regress0/push-pop/incremental-subst-bug.cvc index 9b10ef843..657e74486 100644 --- a/test/regress/regress0/push-pop/incremental-subst-bug.cvc +++ b/test/regress/regress0/push-pop/incremental-subst-bug.cvc @@ -1,21 +1,21 @@ % COMMAND-LINE: --incremental U : TYPE; x, y : U; -% EXPECT: invalid +% EXPECT: not_entailed QUERY x = y; ASSERT x = y; -% EXPECT: valid +% EXPECT: entailed QUERY x = y; PUSH; z : U; -% EXPECT: valid +% EXPECT: entailed QUERY x = y; -% EXPECT: invalid +% EXPECT: not_entailed QUERY x = z; -% EXPECT: invalid +% EXPECT: not_entailed QUERY z = x; -% EXPECT: invalid +% EXPECT: not_entailed QUERY z /= x; POP; -% EXPECT: invalid +% EXPECT: not_entailed QUERY z /= x; diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc index 63cf52fd6..d01d7b7d2 100644 --- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc +++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc @@ -1,2 +1,2 @@ -% EXPECT: valid +% EXPECT: entailed QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ; diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc index 6740faa8c..06d2b5049 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc +++ b/test/regress/regress0/sets/cvc-sample.cvc @@ -4,7 +4,7 @@ % EXPECT: unsat % EXPECT: unsat % EXPECT: unsat -% EXPECT: invalid +% EXPECT: not_entailed OPTION "incremental" true; OPTION "logic" "ALL_SUPPORTED"; SetInt : TYPE = SET OF INT; diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc index 83d0225bd..def48254e 100644 --- a/test/regress/regress0/simple.cvc +++ b/test/regress/regress0/simple.cvc @@ -3,5 +3,5 @@ ASSERT x1 OR NOT x0; ASSERT x0 OR NOT x3; ASSERT x3 OR x2; ASSERT x1 AND NOT x1; -% EXPECT: valid +% EXPECT: entailed QUERY x2; diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc index bd732b4dc..dcb7c6f0d 100644 --- a/test/regress/regress0/smallcnf.cvc +++ b/test/regress/regress0/smallcnf.cvc @@ -4,6 +4,6 @@ ASSERT NOT a OR NOT b; ASSERT c OR b OR a; ASSERT b OR NOT a; ASSERT a OR NOT b OR c; -% EXPECT: invalid +% EXPECT: not_entailed QUERY FALSE; diff --git a/test/regress/regress0/smtlib/set-info-status.smt2 b/test/regress/regress0/smtlib/set-info-status.smt2 index 489d686b3..4bfa1766a 100644 --- a/test/regress/regress0/smtlib/set-info-status.smt2 +++ b/test/regress/regress0/smtlib/set-info-status.smt2 @@ -1,4 +1,4 @@ -; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/ENTAILED response.") ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc index 45052deeb..26dda442e 100644 --- a/test/regress/regress0/test11.cvc +++ b/test/regress/regress0/test11.cvc @@ -3,5 +3,5 @@ x, y : BOOLEAN; ASSERT (x OR y); ASSERT NOT (x OR y); -% EXPECT: valid +% EXPECT: entailed QUERY FALSE; diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc index bfe1a3285..7872f5a1a 100644 --- a/test/regress/regress0/test9.cvc +++ b/test/regress/regress0/test9.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed P,Q:BOOLEAN; ASSERT (P OR Q); QUERY (P OR Q); diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc index 42b99cc44..6b0f93324 100644 --- a/test/regress/regress0/uf/simple.01.cvc +++ b/test/regress/regress0/uf/simple.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc index 1dd96fd1c..2bd0b1e1e 100644 --- a/test/regress/regress0/uf/simple.02.cvc +++ b/test/regress/regress0/uf/simple.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc index cc1721ca6..15fe5907c 100644 --- a/test/regress/regress0/uf/simple.03.cvc +++ b/test/regress/regress0/uf/simple.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc index 66223ca7b..0fc52bcca 100644 --- a/test/regress/regress0/uf/simple.04.cvc +++ b/test/regress/regress0/uf/simple.04.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc index 9de754284..b25d8a471 100644 --- a/test/regress/regress0/uf20-03.cvc +++ b/test/regress/regress0/uf20-03.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc index fb38fab65..1516503ff 100644 --- a/test/regress/regress0/wiki.01.cvc +++ b/test/regress/regress0/wiki.01.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR (b OR c) <=> (a OR b) OR c; diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc index 93d555c96..ebeadee14 100644 --- a/test/regress/regress0/wiki.02.cvc +++ b/test/regress/regress0/wiki.02.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND (b AND c) <=> (a AND b) AND c; diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc index 08b049c17..ca0e6a8d1 100644 --- a/test/regress/regress0/wiki.03.cvc +++ b/test/regress/regress0/wiki.03.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR b <=> b OR a; diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc index b88de6144..75fe17238 100644 --- a/test/regress/regress0/wiki.04.cvc +++ b/test/regress/regress0/wiki.04.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND b <=> b AND a; diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index 0fe647f7b..2f87e4ca0 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR (a AND b) <=> a; diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc index 1d466a86e..a4075bda3 100644 --- a/test/regress/regress0/wiki.06.cvc +++ b/test/regress/regress0/wiki.06.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND (a OR b) <=> a; diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc index 146d92832..3b4527bdc 100644 --- a/test/regress/regress0/wiki.07.cvc +++ b/test/regress/regress0/wiki.07.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc index e9c7d3fa3..e15a21412 100644 --- a/test/regress/regress0/wiki.08.cvc +++ b/test/regress/regress0/wiki.08.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc index 478be2db9..5bc5faca5 100644 --- a/test/regress/regress0/wiki.09.cvc +++ b/test/regress/regress0/wiki.09.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR NOT a; diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc index 226a3da82..613022e84 100644 --- a/test/regress/regress0/wiki.10.cvc +++ b/test/regress/regress0/wiki.10.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND NOT a <=> FALSE; diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc index d615fef3b..8debef9cd 100644 --- a/test/regress/regress0/wiki.11.cvc +++ b/test/regress/regress0/wiki.11.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR a <=> a; diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc index 209e512a6..2274fc78e 100644 --- a/test/regress/regress0/wiki.12.cvc +++ b/test/regress/regress0/wiki.12.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND a <=> a; diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc index 2cc69f048..80b95802d 100644 --- a/test/regress/regress0/wiki.13.cvc +++ b/test/regress/regress0/wiki.13.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR FALSE <=> a; diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc index 5a6c16248..7b8a14edb 100644 --- a/test/regress/regress0/wiki.14.cvc +++ b/test/regress/regress0/wiki.14.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND TRUE <=> a; diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc index 6dc84f679..dfb4f13fc 100644 --- a/test/regress/regress0/wiki.15.cvc +++ b/test/regress/regress0/wiki.15.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR TRUE <=> TRUE; diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc index 6b2bf4113..9c69baa52 100644 --- a/test/regress/regress0/wiki.16.cvc +++ b/test/regress/regress0/wiki.16.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND FALSE <=> FALSE; diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc index 7c6701acc..c58160bb9 100644 --- a/test/regress/regress0/wiki.17.cvc +++ b/test/regress/regress0/wiki.17.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT FALSE <=> TRUE; diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc index 7c1b1b8e4..17773b899 100644 --- a/test/regress/regress0/wiki.18.cvc +++ b/test/regress/regress0/wiki.18.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT TRUE <=> FALSE; diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc index d5812b5ea..46b6fc02e 100644 --- a/test/regress/regress0/wiki.19.cvc +++ b/test/regress/regress0/wiki.19.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT (a OR b) <=> NOT a AND NOT b; diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc index 8d2570620..42e114010 100644 --- a/test/regress/regress0/wiki.20.cvc +++ b/test/regress/regress0/wiki.20.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT (a AND b) <=> NOT a OR NOT b; diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc index d65cbcf65..bcc69beea 100644 --- a/test/regress/regress0/wiki.21.cvc +++ b/test/regress/regress0/wiki.21.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT NOT a <=> a; diff --git a/test/regress/regress1/arith/arith-int-001.cvc b/test/regress/regress1/arith/arith-int-001.cvc index 03ed1a6ae..3fd528c11 100644 --- a/test/regress/regress1/arith/arith-int-001.cvc +++ b/test/regress/regress1/arith/arith-int-001.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ; ASSERT (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ; diff --git a/test/regress/regress1/arith/arith-int-002.cvc b/test/regress/regress1/arith/arith-int-002.cvc index 849daba79..6cc4b2c5e 100644 --- a/test/regress/regress1/arith/arith-int-002.cvc +++ b/test/regress/regress1/arith/arith-int-002.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ; ASSERT (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ; diff --git a/test/regress/regress1/arith/arith-int-003.cvc b/test/regress/regress1/arith/arith-int-003.cvc index 9c060c469..f294babe6 100644 --- a/test/regress/regress1/arith/arith-int-003.cvc +++ b/test/regress/regress1/arith/arith-int-003.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ; ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ; diff --git a/test/regress/regress1/arith/arith-int-004.cvc b/test/regress/regress1/arith/arith-int-004.cvc index 314b76d18..15b060d92 100644 --- a/test/regress/regress1/arith/arith-int-004.cvc +++ b/test/regress/regress1/arith/arith-int-004.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ; diff --git a/test/regress/regress1/arith/arith-int-005.cvc b/test/regress/regress1/arith/arith-int-005.cvc index 9b9776ad3..3701d60b4 100644 --- a/test/regress/regress1/arith/arith-int-005.cvc +++ b/test/regress/regress1/arith/arith-int-005.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ; ASSERT (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ; diff --git a/test/regress/regress1/arith/arith-int-006.cvc b/test/regress/regress1/arith/arith-int-006.cvc index 999b4a5b4..53a80310a 100644 --- a/test/regress/regress1/arith/arith-int-006.cvc +++ b/test/regress/regress1/arith/arith-int-006.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ; ASSERT (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ; diff --git a/test/regress/regress1/arith/arith-int-007.cvc b/test/regress/regress1/arith/arith-int-007.cvc index 4cb4d88ef..c0732e2b2 100644 --- a/test/regress/regress1/arith/arith-int-007.cvc +++ b/test/regress/regress1/arith/arith-int-007.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ; ASSERT (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ; diff --git a/test/regress/regress1/arith/arith-int-008.cvc b/test/regress/regress1/arith/arith-int-008.cvc index 1ae22c993..1810d6f28 100644 --- a/test/regress/regress1/arith/arith-int-008.cvc +++ b/test/regress/regress1/arith/arith-int-008.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ; ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ; diff --git a/test/regress/regress1/arith/arith-int-009.cvc b/test/regress/regress1/arith/arith-int-009.cvc index 9bd7a2ce4..14b26da6c 100644 --- a/test/regress/regress1/arith/arith-int-009.cvc +++ b/test/regress/regress1/arith/arith-int-009.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ; ASSERT (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ; diff --git a/test/regress/regress1/arith/arith-int-010.cvc b/test/regress/regress1/arith/arith-int-010.cvc index 4ac85a984..aa649ba4a 100644 --- a/test/regress/regress1/arith/arith-int-010.cvc +++ b/test/regress/regress1/arith/arith-int-010.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ; ASSERT (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ; diff --git a/test/regress/regress1/arith/arith-int-011.cvc b/test/regress/regress1/arith/arith-int-011.cvc index bd2fa2a0d..7de68533f 100644 --- a/test/regress/regress1/arith/arith-int-011.cvc +++ b/test/regress/regress1/arith/arith-int-011.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ; ASSERT (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9; diff --git a/test/regress/regress1/arith/arith-int-012.cvc b/test/regress/regress1/arith/arith-int-012.cvc index 11b0dab27..10922dd89 100644 --- a/test/regress/regress1/arith/arith-int-012.cvc +++ b/test/regress/regress1/arith/arith-int-012.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ; ASSERT (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24; diff --git a/test/regress/regress1/arith/arith-int-013.cvc b/test/regress/regress1/arith/arith-int-013.cvc index 329251cae..8a1f76add 100644 --- a/test/regress/regress1/arith/arith-int-013.cvc +++ b/test/regress/regress1/arith/arith-int-013.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ; ASSERT (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2; diff --git a/test/regress/regress1/arith/arith-int-016.cvc b/test/regress/regress1/arith/arith-int-016.cvc index 6774dd2d1..951650461 100644 --- a/test/regress/regress1/arith/arith-int-016.cvc +++ b/test/regress/regress1/arith/arith-int-016.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ; ASSERT (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ; diff --git a/test/regress/regress1/arith/arith-int-017.cvc b/test/regress/regress1/arith/arith-int-017.cvc index e9a06125a..48287249f 100644 --- a/test/regress/regress1/arith/arith-int-017.cvc +++ b/test/regress/regress1/arith/arith-int-017.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ; ASSERT (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ; diff --git a/test/regress/regress1/arith/arith-int-018.cvc b/test/regress/regress1/arith/arith-int-018.cvc index 4cb97b77e..cae6fed72 100644 --- a/test/regress/regress1/arith/arith-int-018.cvc +++ b/test/regress/regress1/arith/arith-int-018.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ; ASSERT (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ; diff --git a/test/regress/regress1/arith/arith-int-019.cvc b/test/regress/regress1/arith/arith-int-019.cvc index cf9ae2d70..a26bbac01 100644 --- a/test/regress/regress1/arith/arith-int-019.cvc +++ b/test/regress/regress1/arith/arith-int-019.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ; ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ; diff --git a/test/regress/regress1/arith/arith-int-020.cvc b/test/regress/regress1/arith/arith-int-020.cvc index 07a827465..c1416b38f 100644 --- a/test/regress/regress1/arith/arith-int-020.cvc +++ b/test/regress/regress1/arith/arith-int-020.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ; ASSERT (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ; diff --git a/test/regress/regress1/arith/arith-int-022.cvc b/test/regress/regress1/arith/arith-int-022.cvc index 584348da4..4612f72c9 100644 --- a/test/regress/regress1/arith/arith-int-022.cvc +++ b/test/regress/regress1/arith/arith-int-022.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18; QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-024.cvc b/test/regress/regress1/arith/arith-int-024.cvc index f57136dd1..73ae7c4ad 100644 --- a/test/regress/regress1/arith/arith-int-024.cvc +++ b/test/regress/regress1/arith/arith-int-024.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5; QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-026.cvc b/test/regress/regress1/arith/arith-int-026.cvc index 9e69aa2d1..52f2478e0 100644 --- a/test/regress/regress1/arith/arith-int-026.cvc +++ b/test/regress/regress1/arith/arith-int-026.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ; ASSERT (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ; diff --git a/test/regress/regress1/arith/arith-int-027.cvc b/test/regress/regress1/arith/arith-int-027.cvc index b45622fea..6c38642d2 100644 --- a/test/regress/regress1/arith/arith-int-027.cvc +++ b/test/regress/regress1/arith/arith-int-027.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ; ASSERT (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ; diff --git a/test/regress/regress1/arith/arith-int-028.cvc b/test/regress/regress1/arith/arith-int-028.cvc index 61fee4203..7e8b78893 100644 --- a/test/regress/regress1/arith/arith-int-028.cvc +++ b/test/regress/regress1/arith/arith-int-028.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ; ASSERT (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ; diff --git a/test/regress/regress1/arith/arith-int-029.cvc b/test/regress/regress1/arith/arith-int-029.cvc index ee49bbb68..ba49219d8 100644 --- a/test/regress/regress1/arith/arith-int-029.cvc +++ b/test/regress/regress1/arith/arith-int-029.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ; ASSERT (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ; diff --git a/test/regress/regress1/arith/arith-int-030.cvc b/test/regress/regress1/arith/arith-int-030.cvc index 70b6a3785..a6348b107 100644 --- a/test/regress/regress1/arith/arith-int-030.cvc +++ b/test/regress/regress1/arith/arith-int-030.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ; ASSERT (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ; diff --git a/test/regress/regress1/arith/arith-int-031.cvc b/test/regress/regress1/arith/arith-int-031.cvc index 86242f7aa..056ab622e 100644 --- a/test/regress/regress1/arith/arith-int-031.cvc +++ b/test/regress/regress1/arith/arith-int-031.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ; ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ; diff --git a/test/regress/regress1/arith/arith-int-032.cvc b/test/regress/regress1/arith/arith-int-032.cvc index 1ee4c9844..08c29108e 100644 --- a/test/regress/regress1/arith/arith-int-032.cvc +++ b/test/regress/regress1/arith/arith-int-032.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ; ASSERT (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ; diff --git a/test/regress/regress1/arith/arith-int-033.cvc b/test/regress/regress1/arith/arith-int-033.cvc index 599ba4e9a..8259a7725 100644 --- a/test/regress/regress1/arith/arith-int-033.cvc +++ b/test/regress/regress1/arith/arith-int-033.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ; ASSERT (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ; diff --git a/test/regress/regress1/arith/arith-int-034.cvc b/test/regress/regress1/arith/arith-int-034.cvc index ec615a785..2b5ae4f4f 100644 --- a/test/regress/regress1/arith/arith-int-034.cvc +++ b/test/regress/regress1/arith/arith-int-034.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ; ASSERT (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ; diff --git a/test/regress/regress1/arith/arith-int-035.cvc b/test/regress/regress1/arith/arith-int-035.cvc index e7dee2484..1bad259e2 100644 --- a/test/regress/regress1/arith/arith-int-035.cvc +++ b/test/regress/regress1/arith/arith-int-035.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ; ASSERT (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ; diff --git a/test/regress/regress1/arith/arith-int-036.cvc b/test/regress/regress1/arith/arith-int-036.cvc index 9594f9586..0eb783815 100644 --- a/test/regress/regress1/arith/arith-int-036.cvc +++ b/test/regress/regress1/arith/arith-int-036.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ; ASSERT (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ; diff --git a/test/regress/regress1/arith/arith-int-037.cvc b/test/regress/regress1/arith/arith-int-037.cvc index 4d4422d3f..c3ed60011 100644 --- a/test/regress/regress1/arith/arith-int-037.cvc +++ b/test/regress/regress1/arith/arith-int-037.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ; ASSERT (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ; diff --git a/test/regress/regress1/arith/arith-int-038.cvc b/test/regress/regress1/arith/arith-int-038.cvc index 476133b24..52ac2b1e3 100644 --- a/test/regress/regress1/arith/arith-int-038.cvc +++ b/test/regress/regress1/arith/arith-int-038.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ; ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ; diff --git a/test/regress/regress1/arith/arith-int-039.cvc b/test/regress/regress1/arith/arith-int-039.cvc index 9e9235ae8..cecb7f085 100644 --- a/test/regress/regress1/arith/arith-int-039.cvc +++ b/test/regress/regress1/arith/arith-int-039.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ; ASSERT (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-040.cvc b/test/regress/regress1/arith/arith-int-040.cvc index 68502349f..f2dff7796 100644 --- a/test/regress/regress1/arith/arith-int-040.cvc +++ b/test/regress/regress1/arith/arith-int-040.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ; ASSERT (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ; diff --git a/test/regress/regress1/arith/arith-int-041.cvc b/test/regress/regress1/arith/arith-int-041.cvc index a0c2dc0f9..9df03a9bd 100644 --- a/test/regress/regress1/arith/arith-int-041.cvc +++ b/test/regress/regress1/arith/arith-int-041.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ; ASSERT (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ; diff --git a/test/regress/regress1/arith/arith-int-043.cvc b/test/regress/regress1/arith/arith-int-043.cvc index 7efea85e5..7a2d6d6af 100644 --- a/test/regress/regress1/arith/arith-int-043.cvc +++ b/test/regress/regress1/arith/arith-int-043.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ; ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ; diff --git a/test/regress/regress1/arith/arith-int-044.cvc b/test/regress/regress1/arith/arith-int-044.cvc index f933b014b..649532a4b 100644 --- a/test/regress/regress1/arith/arith-int-044.cvc +++ b/test/regress/regress1/arith/arith-int-044.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed %%%% down from 24, up from 6, up from 39 x0, x1, x2, x3 : INT; ASSERT (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0; diff --git a/test/regress/regress1/arith/arith-int-045.cvc b/test/regress/regress1/arith/arith-int-045.cvc index ca1a12ba6..2c552c915 100644 --- a/test/regress/regress1/arith/arith-int-045.cvc +++ b/test/regress/regress1/arith/arith-int-045.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ; ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ; diff --git a/test/regress/regress1/arith/arith-int-046.cvc b/test/regress/regress1/arith/arith-int-046.cvc index d4d206c6e..acf4dc9a9 100644 --- a/test/regress/regress1/arith/arith-int-046.cvc +++ b/test/regress/regress1/arith/arith-int-046.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ; ASSERT (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ; diff --git a/test/regress/regress1/arith/arith-int-047.cvc b/test/regress/regress1/arith/arith-int-047.cvc index 0763e5dc3..bb1225b9d 100644 --- a/test/regress/regress1/arith/arith-int-047.cvc +++ b/test/regress/regress1/arith/arith-int-047.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10; ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ; diff --git a/test/regress/regress1/arith/arith-int-048.cvc b/test/regress/regress1/arith/arith-int-048.cvc index e7c05332d..ccc84f389 100644 --- a/test/regress/regress1/arith/arith-int-048.cvc +++ b/test/regress/regress1/arith/arith-int-048.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ; ASSERT (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ; diff --git a/test/regress/regress1/arith/arith-int-049.cvc b/test/regress/regress1/arith/arith-int-049.cvc index 8eabc78a8..72e3b7f31 100644 --- a/test/regress/regress1/arith/arith-int-049.cvc +++ b/test/regress/regress1/arith/arith-int-049.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ; ASSERT (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ; diff --git a/test/regress/regress1/arith/arith-int-050.cvc b/test/regress/regress1/arith/arith-int-050.cvc index f0ba939b7..21dbfe09a 100644 --- a/test/regress/regress1/arith/arith-int-050.cvc +++ b/test/regress/regress1/arith/arith-int-050.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ; ASSERT (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ; diff --git a/test/regress/regress1/arith/arith-int-051.cvc b/test/regress/regress1/arith/arith-int-051.cvc index 9a2497432..68654a7df 100644 --- a/test/regress/regress1/arith/arith-int-051.cvc +++ b/test/regress/regress1/arith/arith-int-051.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ; ASSERT (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ; diff --git a/test/regress/regress1/arith/arith-int-052.cvc b/test/regress/regress1/arith/arith-int-052.cvc index 83fdc89c8..9c9433ede 100644 --- a/test/regress/regress1/arith/arith-int-052.cvc +++ b/test/regress/regress1/arith/arith-int-052.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ; ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ; diff --git a/test/regress/regress1/arith/arith-int-053.cvc b/test/regress/regress1/arith/arith-int-053.cvc index fa38fa3da..544d53fb9 100644 --- a/test/regress/regress1/arith/arith-int-053.cvc +++ b/test/regress/regress1/arith/arith-int-053.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ; ASSERT (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17; diff --git a/test/regress/regress1/arith/arith-int-054.cvc b/test/regress/regress1/arith/arith-int-054.cvc index 9b0066966..5b4181a11 100644 --- a/test/regress/regress1/arith/arith-int-054.cvc +++ b/test/regress/regress1/arith/arith-int-054.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ; ASSERT (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ; diff --git a/test/regress/regress1/arith/arith-int-055.cvc b/test/regress/regress1/arith/arith-int-055.cvc index 9729fb565..fdfa45848 100644 --- a/test/regress/regress1/arith/arith-int-055.cvc +++ b/test/regress/regress1/arith/arith-int-055.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ; ASSERT (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ; diff --git a/test/regress/regress1/arith/arith-int-056.cvc b/test/regress/regress1/arith/arith-int-056.cvc index e1c3ee1da..394b3dd4e 100644 --- a/test/regress/regress1/arith/arith-int-056.cvc +++ b/test/regress/regress1/arith/arith-int-056.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ; ASSERT (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ; diff --git a/test/regress/regress1/arith/arith-int-057.cvc b/test/regress/regress1/arith/arith-int-057.cvc index 4e7b939b4..252601514 100644 --- a/test/regress/regress1/arith/arith-int-057.cvc +++ b/test/regress/regress1/arith/arith-int-057.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ; ASSERT (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8; diff --git a/test/regress/regress1/arith/arith-int-058.cvc b/test/regress/regress1/arith/arith-int-058.cvc index 4d964f1c6..7e2a04d45 100644 --- a/test/regress/regress1/arith/arith-int-058.cvc +++ b/test/regress/regress1/arith/arith-int-058.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ; ASSERT (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ; diff --git a/test/regress/regress1/arith/arith-int-059.cvc b/test/regress/regress1/arith/arith-int-059.cvc index 841d9c8e1..87773679e 100644 --- a/test/regress/regress1/arith/arith-int-059.cvc +++ b/test/regress/regress1/arith/arith-int-059.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ; ASSERT (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ; diff --git a/test/regress/regress1/arith/arith-int-060.cvc b/test/regress/regress1/arith/arith-int-060.cvc index 227cb49b1..74dd16dca 100644 --- a/test/regress/regress1/arith/arith-int-060.cvc +++ b/test/regress/regress1/arith/arith-int-060.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ; ASSERT (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ; diff --git a/test/regress/regress1/arith/arith-int-061.cvc b/test/regress/regress1/arith/arith-int-061.cvc index 4a3cc28d0..b3bd247b2 100644 --- a/test/regress/regress1/arith/arith-int-061.cvc +++ b/test/regress/regress1/arith/arith-int-061.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ; ASSERT (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ; diff --git a/test/regress/regress1/arith/arith-int-062.cvc b/test/regress/regress1/arith/arith-int-062.cvc index f9a3156a2..0a185eb68 100644 --- a/test/regress/regress1/arith/arith-int-062.cvc +++ b/test/regress/regress1/arith/arith-int-062.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ; ASSERT (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ; diff --git a/test/regress/regress1/arith/arith-int-063.cvc b/test/regress/regress1/arith/arith-int-063.cvc index d88104688..13c4aae2e 100644 --- a/test/regress/regress1/arith/arith-int-063.cvc +++ b/test/regress/regress1/arith/arith-int-063.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ; ASSERT (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ; diff --git a/test/regress/regress1/arith/arith-int-064.cvc b/test/regress/regress1/arith/arith-int-064.cvc index 21ca822e1..f50b3cd97 100644 --- a/test/regress/regress1/arith/arith-int-064.cvc +++ b/test/regress/regress1/arith/arith-int-064.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ; ASSERT (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ; diff --git a/test/regress/regress1/arith/arith-int-065.cvc b/test/regress/regress1/arith/arith-int-065.cvc index b1b9e1b51..354eb981c 100644 --- a/test/regress/regress1/arith/arith-int-065.cvc +++ b/test/regress/regress1/arith/arith-int-065.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ; ASSERT (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ; diff --git a/test/regress/regress1/arith/arith-int-066.cvc b/test/regress/regress1/arith/arith-int-066.cvc index 9532b4198..f53a254bd 100644 --- a/test/regress/regress1/arith/arith-int-066.cvc +++ b/test/regress/regress1/arith/arith-int-066.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ; ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ; diff --git a/test/regress/regress1/arith/arith-int-067.cvc b/test/regress/regress1/arith/arith-int-067.cvc index 5d7b52e69..61159e9aa 100644 --- a/test/regress/regress1/arith/arith-int-067.cvc +++ b/test/regress/regress1/arith/arith-int-067.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ; ASSERT (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ; diff --git a/test/regress/regress1/arith/arith-int-068.cvc b/test/regress/regress1/arith/arith-int-068.cvc index 107a21a12..683d36801 100644 --- a/test/regress/regress1/arith/arith-int-068.cvc +++ b/test/regress/regress1/arith/arith-int-068.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ; ASSERT (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ; diff --git a/test/regress/regress1/arith/arith-int-069.cvc b/test/regress/regress1/arith/arith-int-069.cvc index 3fab229b0..356a28013 100644 --- a/test/regress/regress1/arith/arith-int-069.cvc +++ b/test/regress/regress1/arith/arith-int-069.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ; ASSERT (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ; diff --git a/test/regress/regress1/arith/arith-int-070.cvc b/test/regress/regress1/arith/arith-int-070.cvc index cd828da5f..791b3b8af 100644 --- a/test/regress/regress1/arith/arith-int-070.cvc +++ b/test/regress/regress1/arith/arith-int-070.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ; ASSERT (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ; diff --git a/test/regress/regress1/arith/arith-int-071.cvc b/test/regress/regress1/arith/arith-int-071.cvc index ce5336476..d44b18b45 100644 --- a/test/regress/regress1/arith/arith-int-071.cvc +++ b/test/regress/regress1/arith/arith-int-071.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ; ASSERT (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ; diff --git a/test/regress/regress1/arith/arith-int-072.cvc b/test/regress/regress1/arith/arith-int-072.cvc index 10222deae..fb13a6616 100644 --- a/test/regress/regress1/arith/arith-int-072.cvc +++ b/test/regress/regress1/arith/arith-int-072.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ; ASSERT (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ; diff --git a/test/regress/regress1/arith/arith-int-073.cvc b/test/regress/regress1/arith/arith-int-073.cvc index 98e74be8f..784190cad 100644 --- a/test/regress/regress1/arith/arith-int-073.cvc +++ b/test/regress/regress1/arith/arith-int-073.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ; ASSERT (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ; diff --git a/test/regress/regress1/arith/arith-int-074.cvc b/test/regress/regress1/arith/arith-int-074.cvc index 28cc48186..914cbe8e3 100644 --- a/test/regress/regress1/arith/arith-int-074.cvc +++ b/test/regress/regress1/arith/arith-int-074.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ; ASSERT (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-075.cvc b/test/regress/regress1/arith/arith-int-075.cvc index 3b5131e8b..d3851e284 100644 --- a/test/regress/regress1/arith/arith-int-075.cvc +++ b/test/regress/regress1/arith/arith-int-075.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ; ASSERT (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ; diff --git a/test/regress/regress1/arith/arith-int-076.cvc b/test/regress/regress1/arith/arith-int-076.cvc index 2c8de7cdf..25a3a7d35 100644 --- a/test/regress/regress1/arith/arith-int-076.cvc +++ b/test/regress/regress1/arith/arith-int-076.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ; ASSERT (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ; diff --git a/test/regress/regress1/arith/arith-int-077.cvc b/test/regress/regress1/arith/arith-int-077.cvc index d14da386e..7e4482093 100644 --- a/test/regress/regress1/arith/arith-int-077.cvc +++ b/test/regress/regress1/arith/arith-int-077.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ; ASSERT (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2; diff --git a/test/regress/regress1/arith/arith-int-078.cvc b/test/regress/regress1/arith/arith-int-078.cvc index 3197c6524..eacccc375 100644 --- a/test/regress/regress1/arith/arith-int-078.cvc +++ b/test/regress/regress1/arith/arith-int-078.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ; ASSERT (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ; diff --git a/test/regress/regress1/arith/arith-int-080.cvc b/test/regress/regress1/arith/arith-int-080.cvc index 8be0f9a73..bf6b90c67 100644 --- a/test/regress/regress1/arith/arith-int-080.cvc +++ b/test/regress/regress1/arith/arith-int-080.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ; ASSERT (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14; diff --git a/test/regress/regress1/arith/arith-int-081.cvc b/test/regress/regress1/arith/arith-int-081.cvc index 546148376..47cc66ae2 100644 --- a/test/regress/regress1/arith/arith-int-081.cvc +++ b/test/regress/regress1/arith/arith-int-081.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8; ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ; diff --git a/test/regress/regress1/arith/arith-int-082.cvc b/test/regress/regress1/arith/arith-int-082.cvc index 62bd45de7..a6245f036 100644 --- a/test/regress/regress1/arith/arith-int-082.cvc +++ b/test/regress/regress1/arith/arith-int-082.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ; ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ; diff --git a/test/regress/regress1/arith/arith-int-083.cvc b/test/regress/regress1/arith/arith-int-083.cvc index 6b1084353..3a7c635cc 100644 --- a/test/regress/regress1/arith/arith-int-083.cvc +++ b/test/regress/regress1/arith/arith-int-083.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ; ASSERT (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ; diff --git a/test/regress/regress1/arith/arith-int-084.cvc b/test/regress/regress1/arith/arith-int-084.cvc index 5f0e17afe..d4a0a966c 100644 --- a/test/regress/regress1/arith/arith-int-084.cvc +++ b/test/regress/regress1/arith/arith-int-084.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ; ASSERT (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ; diff --git a/test/regress/regress1/arith/arith-int-085.cvc b/test/regress/regress1/arith/arith-int-085.cvc index 74dd714e8..b1a343e73 100644 --- a/test/regress/regress1/arith/arith-int-085.cvc +++ b/test/regress/regress1/arith/arith-int-085.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed %% down from 3 x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ; diff --git a/test/regress/regress1/arith/arith-int-086.cvc b/test/regress/regress1/arith/arith-int-086.cvc index 64c212b3c..6ee96589b 100644 --- a/test/regress/regress1/arith/arith-int-086.cvc +++ b/test/regress/regress1/arith/arith-int-086.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ; ASSERT (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ; diff --git a/test/regress/regress1/arith/arith-int-087.cvc b/test/regress/regress1/arith/arith-int-087.cvc index 312c08917..b969df1a3 100644 --- a/test/regress/regress1/arith/arith-int-087.cvc +++ b/test/regress/regress1/arith/arith-int-087.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ; ASSERT (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ; diff --git a/test/regress/regress1/arith/arith-int-088.cvc b/test/regress/regress1/arith/arith-int-088.cvc index 5212640be..de0d23844 100644 --- a/test/regress/regress1/arith/arith-int-088.cvc +++ b/test/regress/regress1/arith/arith-int-088.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ; ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ; diff --git a/test/regress/regress1/arith/arith-int-089.cvc b/test/regress/regress1/arith/arith-int-089.cvc index 7ff36d29e..e50daa9de 100644 --- a/test/regress/regress1/arith/arith-int-089.cvc +++ b/test/regress/regress1/arith/arith-int-089.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ; ASSERT (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ; diff --git a/test/regress/regress1/arith/arith-int-090.cvc b/test/regress/regress1/arith/arith-int-090.cvc index 52b9c13f0..74d4ba4db 100644 --- a/test/regress/regress1/arith/arith-int-090.cvc +++ b/test/regress/regress1/arith/arith-int-090.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ; ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ; diff --git a/test/regress/regress1/arith/arith-int-091.cvc b/test/regress/regress1/arith/arith-int-091.cvc index 29a19db39..c03b544a3 100644 --- a/test/regress/regress1/arith/arith-int-091.cvc +++ b/test/regress/regress1/arith/arith-int-091.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ; ASSERT (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ; diff --git a/test/regress/regress1/arith/arith-int-092.cvc b/test/regress/regress1/arith/arith-int-092.cvc index 51c8a6bc4..d080cde0c 100644 --- a/test/regress/regress1/arith/arith-int-092.cvc +++ b/test/regress/regress1/arith/arith-int-092.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ; ASSERT (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ; diff --git a/test/regress/regress1/arith/arith-int-093.cvc b/test/regress/regress1/arith/arith-int-093.cvc index 7d2123d41..e910def47 100644 --- a/test/regress/regress1/arith/arith-int-093.cvc +++ b/test/regress/regress1/arith/arith-int-093.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ; ASSERT (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ; diff --git a/test/regress/regress1/arith/arith-int-094.cvc b/test/regress/regress1/arith/arith-int-094.cvc index a5f1aefce..2204bba4e 100644 --- a/test/regress/regress1/arith/arith-int-094.cvc +++ b/test/regress/regress1/arith/arith-int-094.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ; ASSERT (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-095.cvc b/test/regress/regress1/arith/arith-int-095.cvc index bc47d6f49..e803dbe9b 100644 --- a/test/regress/regress1/arith/arith-int-095.cvc +++ b/test/regress/regress1/arith/arith-int-095.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ; ASSERT (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ; diff --git a/test/regress/regress1/arith/arith-int-096.cvc b/test/regress/regress1/arith/arith-int-096.cvc index 2f6cf3155..354ae180d 100644 --- a/test/regress/regress1/arith/arith-int-096.cvc +++ b/test/regress/regress1/arith/arith-int-096.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ; ASSERT (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28; diff --git a/test/regress/regress1/arith/arith-int-097.cvc b/test/regress/regress1/arith/arith-int-097.cvc index b05061192..67eb614eb 100644 --- a/test/regress/regress1/arith/arith-int-097.cvc +++ b/test/regress/regress1/arith/arith-int-097.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ; ASSERT (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ; diff --git a/test/regress/regress1/arith/arith-int-099.cvc b/test/regress/regress1/arith/arith-int-099.cvc index 0d74dcb39..57a45de03 100644 --- a/test/regress/regress1/arith/arith-int-099.cvc +++ b/test/regress/regress1/arith/arith-int-099.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ; ASSERT (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ; diff --git a/test/regress/regress1/arith/arith-int-100.cvc b/test/regress/regress1/arith/arith-int-100.cvc index 7e07bee14..66be1f8f7 100644 --- a/test/regress/regress1/arith/arith-int-100.cvc +++ b/test/regress/regress1/arith/arith-int-100.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ; ASSERT (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ; diff --git a/test/regress/regress1/boolean.cvc b/test/regress/regress1/boolean.cvc index eb0e7ab52..2c861c0f0 100644 --- a/test/regress/regress1/boolean.cvc +++ b/test/regress/regress1/boolean.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed p : BOOLEAN; q : BOOLEAN; r : BOOLEAN; diff --git a/test/regress/regress1/fmf/ko-bound-set.cvc b/test/regress/regress1/fmf/ko-bound-set.cvc index eebcbc2f8..5306a1513 100644 --- a/test/regress/regress1/fmf/ko-bound-set.cvc +++ b/test/regress/regress1/fmf/ko-bound-set.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed OPTION "finite-model-find"; OPTION "fmf-bound-int"; OPTION "produce-models"; diff --git a/test/regress/regress1/hole6.cvc b/test/regress/regress1/hole6.cvc index dfa9b72d5..5ec31d801 100644 --- a/test/regress/regress1/hole6.cvc +++ b/test/regress/regress1/hole6.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc index f7407a2a5..6f2a8764b 100644 --- a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc +++ b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed OPTION "finite-model-find"; OPTION "fmf-bound-int"; diff --git a/test/regress/regress1/test12.cvc b/test/regress/regress1/test12.cvc index 37687bee1..39ced0428 100644 --- a/test/regress/regress1/test12.cvc +++ b/test/regress/regress1/test12.cvc @@ -1,34 +1,34 @@ % COMMAND-LINE: --incremental -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: valid -% EXPECT: valid +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: entailed +% EXPECT: entailed A: TYPE; P_1: BOOLEAN; P_2: BOOLEAN; diff --git a/test/regress/regress2/arith/arith-int-098.cvc b/test/regress/regress2/arith/arith-int-098.cvc index 08cfd9c9c..cf20f2b61 100644 --- a/test/regress/regress2/arith/arith-int-098.cvc +++ b/test/regress/regress2/arith/arith-int-098.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ; ASSERT (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12; diff --git a/test/regress/regress2/hole7.cvc b/test/regress/regress2/hole7.cvc index 1f762477a..e73588bad 100644 --- a/test/regress/regress2/hole7.cvc +++ b/test/regress/regress2/hole7.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress2/hole8.cvc b/test/regress/regress2/hole8.cvc index 705c95ea6..a46c4da97 100644 --- a/test/regress/regress2/hole8.cvc +++ b/test/regress/regress2/hole8.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress2/typed_v1l50016-simp.cvc b/test/regress/regress2/typed_v1l50016-simp.cvc index b4a1e4b32..1d576ab74 100644 --- a/test/regress/regress2/typed_v1l50016-simp.cvc +++ b/test/regress/regress2/typed_v1l50016-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, diff --git a/test/regress/regress3/hole9.cvc b/test/regress/regress3/hole9.cvc index e60839f7b..b86b3b039 100644 --- a/test/regress/regress3/hole9.cvc +++ b/test/regress/regress3/hole9.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress4/hole10.cvc b/test/regress/regress4/hole10.cvc index ebc8279d3..fb4c41b35 100644 --- a/test/regress/regress4/hole10.cvc +++ b/test/regress/regress4/hole10.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index 141db4eea..2ce50949b 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -29,8 +29,8 @@ int main() { ExprManager em; Options opts; SmtEngine smt(&em); - Result r = smt.query(em.mkConst(true)); + Result r = smt.checkEntailed(em.mkConst(true)); - return (Result::VALID == r) ? 0 : 1; + return (Result::ENTAILED == r) ? 0 : 1; } diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index fb9714d4b..2924359e8 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -35,9 +35,10 @@ int main() { Expr y = em.mkVar("y", em.integerType()); smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5)))); Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0))); - Result r = smt.query(q); + Result r = smt.checkEntailed(q); - if(r != Result::INVALID) { + if (r != Result::NOT_ENTAILED) + { exit(1); } @@ -47,7 +48,7 @@ int main() { } smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5)))); - r = smt.query(q); + r = smt.checkEntailed(q); Statistics stats2 = smt.getStatistics(); bool different = false; for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) { @@ -68,5 +69,5 @@ int main() { } #endif /* CVC4_STATISTICS_ON */ - return r == Result::VALID ? 0 : 1; + return r == Result::ENTAILED ? 0 : 1; } diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp index a7266e0b0..8698fde0e 100644 --- a/test/system/two_smt_engines.cpp +++ b/test/system/two_smt_engines.cpp @@ -28,9 +28,9 @@ int main() { Options opts; SmtEngine smt(&em); SmtEngine smt2(&em); - Result r = smt.query(em.mkConst(true)); - Result r2 = smt2.query(em.mkConst(true)); + Result r = smt.checkEntailed(em.mkConst(true)); + Result r2 = smt2.checkEntailed(em.mkConst(true)); - return r == Result::VALID && r2 == Result::VALID ? 0 : 1; + return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1; } diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h index ab5d65e72..cbfc9cf23 100644 --- a/test/unit/api/result_black.h +++ b/test/unit/api/result_black.h @@ -29,9 +29,8 @@ class ResultBlack : public CxxTest::TestSuite void testIsSat(); void testIsUnsat(); void testIsSatUnknown(); - void testIsValid(); - void testIsInvalid(); - void testIsValidUnknown(); + void testIsEntailed(); + void testIsEntailmentUnknown(); private: std::unique_ptr<Solver> d_solver; @@ -44,9 +43,9 @@ void ResultBlack::testIsNull() TS_ASSERT(!res_null.isSat()); TS_ASSERT(!res_null.isUnsat()); TS_ASSERT(!res_null.isSatUnknown()); - TS_ASSERT(!res_null.isValid()); - TS_ASSERT(!res_null.isInvalid()); - TS_ASSERT(!res_null.isValidUnknown()); + TS_ASSERT(!res_null.isEntailed()); + TS_ASSERT(!res_null.isNotEntailed()); + TS_ASSERT(!res_null.isEntailmentUnknown()); Sort u_sort = d_solver->mkUninterpretedSort("u"); Term x = d_solver->mkVar(u_sort, "x"); d_solver->assertFormula(x.eqTerm(x)); @@ -100,27 +99,24 @@ void ResultBlack::testIsSatUnknown() TS_ASSERT(res.isSatUnknown()); } -void ResultBlack::testIsValid() +void ResultBlack::testIsEntailed() { + d_solver->setOption("incremental", "true"); Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkValid(); - TS_ASSERT(res.isValid()); - TS_ASSERT(!res.isValidUnknown()); -} - -void ResultBlack::testIsInvalid() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkValid(); - TS_ASSERT(res.isInvalid()); - TS_ASSERT(!res.isValidUnknown()); + Term x = d_solver->mkConst(u_sort, "x"); + Term y = d_solver->mkConst(u_sort, "y"); + Term a = x.eqTerm(y).notTerm(); + Term b = x.eqTerm(y); + d_solver->assertFormula(a); + Result entailed = d_solver->checkEntailed(a); + TS_ASSERT(entailed.isEntailed()); + TS_ASSERT(!entailed.isEntailmentUnknown()); + Result not_entailed = d_solver->checkEntailed(b); + TS_ASSERT(not_entailed.isNotEntailed()); + TS_ASSERT(!not_entailed.isEntailmentUnknown()); } -void ResultBlack::testIsValidUnknown() +void ResultBlack::testIsEntailmentUnknown() { d_solver->setLogic("QF_NIA"); d_solver->setOption("incremental", "false"); @@ -128,9 +124,9 @@ void ResultBlack::testIsValidUnknown() Sort int_sort = d_solver->getIntegerSort(); Term x = d_solver->mkVar(int_sort, "x"); d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkValid(); - TS_ASSERT(!res.isValid()); - TS_ASSERT(res.isValidUnknown()); + Result res = d_solver->checkEntailed(x.eqTerm(x)); + TS_ASSERT(!res.isEntailed()); + TS_ASSERT(res.isEntailmentUnknown()); TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON"); } diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 0eefde700..9fd1b7789 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -95,10 +95,9 @@ class SolverBlack : public CxxTest::TestSuite void testPop3(); void testSimplify(); - void testCheckValid1(); - void testCheckValid2(); - void testCheckValidAssuming1(); - void testCheckValidAssuming2(); + void testCheckEntailed(); + void testCheckEntailed1(); + void testCheckEntailed2(); void testSetInfo(); void testSetLogic(); @@ -1104,51 +1103,28 @@ void SolverBlack::testSimplify() TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2)); } -void SolverBlack::testCheckValid1() +void SolverBlack::testCheckEntailed() { d_solver->setOption("incremental", "false"); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValid()); - TS_ASSERT_THROWS(d_solver->checkValid(), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()), + CVC4ApiException&); } -void SolverBlack::testCheckValid2() +void SolverBlack::testCheckEntailed1() { + Sort boolSort = d_solver->getBooleanSort(); + Term x = d_solver->mkConst(boolSort, "x"); + Term y = d_solver->mkConst(boolSort, "y"); + Term z = d_solver->mkTerm(AND, x, y); d_solver->setOption("incremental", "true"); - - Sort realSort = d_solver->getRealSort(); - Sort intSort = d_solver->getIntegerSort(); - - // Constants - Term x = d_solver->mkConst(intSort, "x"); - Term y = d_solver->mkConst(realSort, "y"); - // Values - Term three = d_solver->mkReal(3); - Term neg2 = d_solver->mkReal(-2); - Term two_thirds = d_solver->mkReal(2, 3); - // Terms - Term three_y = d_solver->mkTerm(MULT, three, y); - Term diff = d_solver->mkTerm(MINUS, y, x); - // Formulas - Term x_geq_3y = d_solver->mkTerm(GEQ, x, three_y); - Term x_leq_y = d_solver->mkTerm(LEQ, x, y); - Term neg2_lt_x = d_solver->mkTerm(LT, neg2, x); - // Assertions - Term assertions = d_solver->mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); - - TS_ASSERT_THROWS_NOTHING(d_solver->checkValid()); - d_solver->assertFormula(assertions); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValid()); -} - -void SolverBlack::testCheckValidAssuming1() -{ - d_solver->setOption("incremental", "false"); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue())); - TS_ASSERT_THROWS(d_solver->checkValidAssuming(d_solver->mkTrue()), - CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z)); } -void SolverBlack::testCheckValidAssuming2() +void SolverBlack::testCheckEntailed2() { d_solver->setOption("incremental", "true"); @@ -1185,15 +1161,15 @@ void SolverBlack::testCheckValidAssuming2() p_f_y // p(f(y)) }); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue())); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); d_solver->assertFormula(assertions); TS_ASSERT_THROWS_NOTHING( - d_solver->checkValidAssuming(d_solver->mkTerm(DISTINCT, x, y))); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming( + d_solver->checkEntailed(d_solver->mkTerm(DISTINCT, x, y))); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed( {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)})); - TS_ASSERT_THROWS(d_solver->checkValidAssuming(n), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->checkEntailed(n), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver->checkValidAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}), + d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}), CVC4ApiException&); } |