From: Andrew Reynolds Date: Mon, 14 Mar 2022 18:29:30 +0000 (-0500) Subject: Remove unecessary methods from the API (#8260) X-Git-Tag: cvc5-1.0.0~262 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f1483e2e3e61c50e8bf6d7b7d86ea49f69371c6;p=cvc5.git Remove unecessary methods from the API (#8260) Removes checkEntailed from Solver. Removes isEntailed, isNotEntailed, isEntailedUnknown from Result. Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort. Updates examples and unit tests. --- diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 3a9eaf77d..dc1a6de1c 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -52,8 +52,9 @@ public class SimpleVC Term formula = slv.mkTerm(Kind.AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3); System.out.println("Checking entailment of formula " + formula + " with cvc5."); - System.out.println("cvc5 should report ENTAILED."); - System.out.println("Result from cvc5 is: " + slv.checkEntailed(formula)); + System.out.println("cvc5 should report UNSAT."); + System.out.println( + "Result from cvc5 is: " + slv.checkSatAssuming(formula.notTerm())); } } } diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp index 51f438a2d..3aa9ca8ad 100644 --- a/examples/api/cpp/bitvectors.cpp +++ b/examples/api/cpp/bitvectors.cpp @@ -88,9 +88,9 @@ int main() slv.assertFormula(assignment1); Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); - cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect ENTAILED. " << endl; - cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl; + cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl; + cout << " Expect UNSAT. " << endl; + cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl; cout << " Popping context. " << endl; slv.pop(); @@ -104,15 +104,16 @@ int main() cout << "Asserting " << assignment2 << " to cvc5 " << endl; slv.assertFormula(assignment2); - cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect ENTAILED. " << endl; - cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl; + cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl; + cout << " Expect UNSAT. " << endl; + cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl; Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); std::vector v{new_x_eq_new_x_, x_neq_x}; - cout << " Check entailment assuming: " << v << endl; - cout << " Expect NOT_ENTAILED. " << endl; - cout << " cvc5: " << slv.checkEntailed(v) << endl; + Term query = slv.mkTerm(AND, v); + cout << " Check sat assuming: " << query.notTerm() << endl; + cout << " Expect SAT. " << endl; + cout << " cvc5: " << slv.checkSatAssuming(query.notTerm()) << endl; // Assert that a is odd Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); diff --git a/examples/api/cpp/combination.cpp b/examples/api/cpp/combination.cpp index 98393abe1..c3847e51e 100644 --- a/examples/api/cpp/combination.cpp +++ b/examples/api/cpp/combination.cpp @@ -83,7 +83,7 @@ int main() << assertions << endl << endl; cout << "Prove x /= y is entailed. " << endl - << "cvc5: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." + << "cvc5: " << slv.checkSatAssuming(slv.mkTerm(EQUAL, x, y)) << "." << endl << endl; diff --git a/examples/api/cpp/extract.cpp b/examples/api/cpp/extract.cpp index b5de58d26..9b036caa4 100644 --- a/examples/api/cpp/extract.cpp +++ b/examples/api/cpp/extract.cpp @@ -48,9 +48,9 @@ int main() slv.assertFormula(eq); Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); - cout << " Check entailment assuming: " << eq2 << endl; - cout << " Expect ENTAILED. " << endl; - cout << " cvc5: " << slv.checkEntailed(eq2) << endl; + cout << " Check sat assuming: " << eq2.notTerm() << endl; + cout << " Expect UNSAT. " << endl; + cout << " cvc5: " << slv.checkSatAssuming(eq2.notTerm()) << endl; return 0; } diff --git a/examples/api/cpp/helloworld.cpp b/examples/api/cpp/helloworld.cpp index d8c9327b8..957cc8937 100644 --- a/examples/api/cpp/helloworld.cpp +++ b/examples/api/cpp/helloworld.cpp @@ -23,7 +23,7 @@ int main() { Solver slv; Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!"); - std::cout << helloworld << " is " << slv.checkEntailed(helloworld) + std::cout << helloworld << " is " << slv.checkSatAssuming(helloworld) << std::endl; return 0; } diff --git a/examples/api/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp index 9b027844a..3a8879813 100644 --- a/examples/api/cpp/linear_arith.cpp +++ b/examples/api/cpp/linear_arith.cpp @@ -61,9 +61,9 @@ int main() slv.push(); Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); cout << "Prove that " << diff_leq_two_thirds << " with cvc5." << endl; - cout << "cvc5 should report ENTAILED." << endl; - cout << "Result from cvc5 is: " << slv.checkEntailed(diff_leq_two_thirds) - << endl; + cout << "cvc5 should report UNSAT." << endl; + cout << "Result from cvc5 is: " + << slv.checkSatAssuming(diff_leq_two_thirds.notTerm()) << endl; slv.pop(); cout << endl; diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index ff3546b6f..8cd643908 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -51,8 +51,8 @@ int main() Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem) - << "." << endl; + cout << "cvc5 reports: " << theorem << " is " + << slv.checkSatAssuming(theorem.notTerm()) << "." << endl; } // Verify emptset is a subset of any set @@ -62,8 +62,8 @@ int main() Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A); - cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem) - << "." << endl; + cout << "cvc5 reports: " << theorem << " is " + << slv.checkSatAssuming(theorem.notTerm()) << "." << endl; } // Find me an element in {1, 2} intersection {2, 3}, if there is one. diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 4d1d9e169..e5a78e86c 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -86,9 +86,10 @@ public class BitVectors slv.assertFormula(assignment1); Term new_x_eq_new_x_ = slv.mkTerm(Kind.EQUAL, new_x, new_x_); - System.out.println(" Check entailment assuming: " + new_x_eq_new_x_); - System.out.println(" Expect ENTAILED. "); - System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_)); + System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm()); + System.out.println(" Expect UNSAT. "); + System.out.println( + " cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm())); System.out.println(" Popping context. "); slv.pop(); @@ -102,15 +103,17 @@ public class BitVectors System.out.println("Asserting " + assignment2 + " to cvc5 "); slv.assertFormula(assignment2); - System.out.println(" Check entailment assuming: " + new_x_eq_new_x_); - System.out.println(" Expect ENTAILED. "); - System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_)); + System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm()); + System.out.println(" Expect UNSAT. "); + System.out.println( + " cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm())); Term x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm(); Term[] v = new Term[] {new_x_eq_new_x_, x_neq_x}; - System.out.println(" Check entailment assuming: " + v); - System.out.println(" Expect NOT_ENTAILED. "); - System.out.println(" cvc5: " + slv.checkEntailed(v)); + Term query = slv.mkTerm(Kind.AND, v); + System.out.println(" Check sat assuming: " + query.notTerm()); + System.out.println(" Expect SAT. "); + System.out.println(" cvc5: " + slv.checkSatAssuming(query.notTerm())); // Assert that a is odd Op extract_op = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0); diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index e1eb77968..f2c6d046b 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -86,7 +86,8 @@ public class Combination System.out.println("Given the following assertions:\n" + assertions + "\n"); System.out.println("Prove x /= y is entailed. \n" - + "cvc5: " + slv.checkEntailed(slv.mkTerm(Kind.DISTINCT, x, y)) + ".\n"); + + "cvc5: " + slv.checkSatAssuming(slv.mkTerm(Kind.EQUAL, x, y)) + + ".\n"); System.out.println("Call checkSat to show that the assertions are satisfiable. \n" + "cvc5: " + slv.checkSat() + ".\n"); diff --git a/examples/api/java/Extract.java b/examples/api/java/Extract.java index 4ec0c100f..c9c325bb0 100644 --- a/examples/api/java/Extract.java +++ b/examples/api/java/Extract.java @@ -47,8 +47,8 @@ public class Extract Term eq2 = slv.mkTerm(Kind.EQUAL, x_31_31, x_0_0); System.out.println(" Check entailment assuming: " + eq2); - System.out.println(" Expect ENTAILED. "); - System.out.println(" cvc5: " + slv.checkEntailed(eq2)); + System.out.println(" Expect UNSAT. "); + System.out.println(" cvc5: " + slv.checkSatAssuming(eq2.notTerm())); } } } diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 3c2de1e2d..b222a57e1 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -23,7 +23,8 @@ public class HelloWorld { Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!"); - System.out.println(helloworld + " is " + slv.checkEntailed(helloworld)); + System.out.println( + helloworld + " is " + slv.checkSatAssuming(helloworld)); } } } diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 980ec712f..0e59b7109 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -56,8 +56,9 @@ public class LinearArith slv.push(); Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds); System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5."); - System.out.println("cvc5 should report ENTAILED."); - System.out.println("Result from cvc5 is: " + slv.checkEntailed(diff_leq_two_thirds)); + System.out.println("cvc5 should report UNSAT."); + System.out.println("Result from cvc5 is: " + + slv.checkSatAssuming(diff_leq_two_thirds.notTerm())); slv.pop(); System.out.println(); @@ -74,4 +75,4 @@ public class LinearArith System.out.println("Thus the maximum value of (y - x) is 2/3."); } } -} \ No newline at end of file +} diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java index 7eaa3a256..b7b20905c 100644 --- a/examples/api/java/Sets.java +++ b/examples/api/java/Sets.java @@ -50,7 +50,8 @@ public class Sets Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); + System.out.println("cvc5 reports: " + theorem + " is " + + slv.checkSatAssuming(theorem.notTerm()) + "."); } // Verify set.empty is a subset of any set @@ -60,7 +61,8 @@ public class Sets Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A); - System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); + System.out.println("cvc5 reports: " + theorem + " is " + + slv.checkSatAssuming(theorem.notTerm()) + "."); } // Find me an element in {1, 2} intersection {2, 3}, if there is one. diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 0a56783d9..49816ead6 100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -84,9 +84,9 @@ if __name__ == "__main__": slv.assertFormula(assignment1) new_x_eq_new_x_ = slv.mkTerm(Kind.Equal, new_x, new_x_) - print("Checking entailment assuming:", new_x_eq_new_x_) - print("Expect ENTAILED.") - print("cvc5:", slv.checkEntailed(new_x_eq_new_x_)) + print("Checking sat assuming:", new_x_eq_new_x_.notTerm()) + print("Expect UNSAT.") + print("cvc5:", slv.checkSatAssuming(new_x_eq_new_x_.notTerm())) print("Popping context.") slv.pop() @@ -100,16 +100,17 @@ if __name__ == "__main__": print("Asserting {} to cvc5".format(assignment2)) slv.assertFormula(assignment2) - print("Checking entailment assuming:", new_x_eq_new_x_) - print("Expect ENTAILED.") - print("cvc5:", slv.checkEntailed(new_x_eq_new_x_)) + print("Checking sat assuming:", new_x_eq_new_x_.notTerm()) + print("Expect UNSAT.") + print("cvc5:", slv.checkSatAssuming(new_x_eq_new_x_.notTerm())) x_neq_x = slv.mkTerm(Kind.Equal, x, x).notTerm() v = [new_x_eq_new_x_, x_neq_x] - print("Check entailment assuming: ", v) - print("Expect NOT_ENTAILED.") - print("cvc5:", slv.checkEntailed(v)) + query = slv.mkTerm(Kind.And, v) + print("Check sat assuming: ", query.notTerm()) + print("Expect SAT.") + print("cvc5:", slv.checkSatAssuming(query.notTerm())) # Assert that a is odd extract_op = slv.mkOp(Kind.BVExtract, 0, 0) diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index 1f41c6913..d787d14d9 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -71,7 +71,7 @@ if __name__ == "__main__": print("Given the following assertions:", assertions, "\n") print("Prove x /= y is entailed.\ncvc5: ", - slv.checkEntailed(slv.mkTerm(Kind.Distinct, x, y)), "\n") + slv.checkSatAssuming(slv.mkTerm(Kind.Equal, x, y)), "\n") print("Call checkSat to show that the assertions are satisfiable") print("cvc5:", slv.checkSat(), "\n") diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index 2770284e2..3c93e407e 100644 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -46,6 +46,6 @@ if __name__ == "__main__": slv.assertFormula(eq) eq2 = slv.mkTerm(Kind.Equal, x_31_31, x_0_0) - print("Check entailment assuming:", eq2) - print("Expect ENTAILED") - print("cvc5:", slv.checkEntailed(eq2)) + print("Check sat assuming:", eq2.notTerm()) + print("Expect UNSAT") + print("cvc5:", slv.checkSatAssuming(eq2.notTerm())) diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py index cd2f61025..4dfa3a18d 100644 --- a/examples/api/python/helloworld.py +++ b/examples/api/python/helloworld.py @@ -20,4 +20,4 @@ from cvc5 import Kind if __name__ == "__main__": slv = cvc5.Solver() helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!") - print(helloworld, "is", slv.checkEntailed(helloworld)) + print(helloworld, "is", slv.checkSatAssuming(helloworld)) diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index 301939719..4f01acb15 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -56,9 +56,9 @@ if __name__ == "__main__": slv.push() diff_leq_two_thirds = slv.mkTerm(Kind.Leq, diff, two_thirds) print("Prove that", diff_leq_two_thirds, "with cvc5") - print("cvc5 should report ENTAILED") + print("cvc5 should report UNSAT") print("Result from cvc5 is:", - slv.checkEntailed(diff_leq_two_thirds)) + slv.checkSatAssuming(diff_leq_two_thirds.notTerm())) slv.pop() print() diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 88742095b..ebc856d30 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -49,7 +49,7 @@ if __name__ == "__main__": theorem = slv.mkTerm(Kind.Equal, lhs, rhs) print("cvc5 reports: {} is {}".format(theorem, - slv.checkEntailed(theorem))) + slv.checkSatAssuming(theorem.notTerm()))) # Verify emptset is a subset of any set @@ -59,7 +59,7 @@ if __name__ == "__main__": theorem = slv.mkTerm(Kind.SetSubset, emptyset, A) print("cvc5 reports: {} is {}".format(theorem, - slv.checkEntailed(theorem))) + slv.checkSatAssuming(theorem.notTerm()))) # 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 fa3602540..e440c09a0 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -49,9 +49,9 @@ int main() { std::cout << "Checking entailment of formula " << formula << " with cvc5." << std::endl; - std::cout << "cvc5 should report ENTAILED." << std::endl; - std::cout << "Result from cvc5 is: " << slv.checkEntailed(formula) - << std::endl; + std::cout << "cvc5 should report UNSAT." << std::endl; + std::cout << "Result from cvc5 is: " + << slv.checkSatAssuming(formula.notTerm()) << std::endl; return 0; } diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index a54588b11..1dffd5776 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -937,24 +937,6 @@ bool Result::isSatUnknown(void) const && d_result->isSat() == cvc5::Result::SAT_UNKNOWN; } -bool Result::isEntailed(void) const -{ - return d_result->getType() == cvc5::Result::TYPE_ENTAILMENT - && d_result->isEntailed() == cvc5::Result::ENTAILED; -} - -bool Result::isNotEntailed(void) const -{ - return d_result->getType() == cvc5::Result::TYPE_ENTAILMENT - && d_result->isEntailed() == cvc5::Result::NOT_ENTAILED; -} - -bool Result::isEntailmentUnknown(void) const -{ - return d_result->getType() == cvc5::Result::TYPE_ENTAILMENT - && d_result->isEntailed() == cvc5::Result::ENTAILMENT_UNKNOWN; -} - bool Result::operator==(const Result& r) const { return *d_result == *r.d_result; @@ -1375,25 +1357,6 @@ bool Sort::isFirstClass() const CVC5_API_TRY_CATCH_END; } -bool Sort::isFunctionLike() const -{ - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return d_type->isFunctionLike(); - //////// - CVC5_API_TRY_CATCH_END; -} - -bool Sort::isSubsortOf(const Sort& s) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_ARG_CHECK_SOLVER("sort", s); - //////// all checks before this line - return d_type->isSubtypeOf(*s.d_type); - //////// - CVC5_API_TRY_CATCH_END; -} - Datatype Sort::getDatatype() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1656,17 +1619,6 @@ Sort Sort::getSequenceElementSort() const /* Uninterpreted sort -------------------------------------------------- */ -std::string Sort::getUninterpretedSortName() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - //////// all checks before this line - return d_type->getName(); - //////// - CVC5_API_TRY_CATCH_END; -} - bool Sort::isUninterpretedSortParameterized() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1702,17 +1654,6 @@ std::vector Sort::getUninterpretedSortParamSorts() const /* Sort constructor sort ----------------------------------------------- */ -std::string Sort::getSortConstructorName() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; - //////// all checks before this line - return d_type->getName(); - //////// - CVC5_API_TRY_CATCH_END; -} - size_t Sort::getSortConstructorArity() const { CVC5_API_TRY_CATCH_BEGIN; @@ -5801,7 +5742,7 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol, Sort Solver::mkTupleSort(const std::vector& sorts) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts); + CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts); //////// all checks before this line return mkTupleSortHelper(sorts); //////// @@ -6064,7 +6005,7 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const CVC5_API_SOLVER_CHECK_SORT(sort); CVC5_API_SOLVER_CHECK_TERM(val); CVC5_API_ARG_CHECK_EXPECTED(sort.isArray(), sort) << "an array sort"; - CVC5_API_CHECK(val.getSort().isSubsortOf(sort.getArrayElementSort())) + CVC5_API_CHECK(val.getSort() == sort.getArrayElementSort()) << "Value does not match element sort"; //////// all checks before this line @@ -6672,36 +6613,6 @@ Term Solver::simplify(const Term& term) CVC5_API_TRY_CATCH_END; } -Result Solver::checkEntailed(const Term& term) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_slv->isQueryMade() - || d_slv->getOptions().base.incrementalSolving) - << "Cannot make multiple queries unless incremental solving is enabled " - "(try --incremental)"; - CVC5_API_SOLVER_CHECK_TERM(term); - ensureWellFormedTerm(term); - //////// all checks before this line - return d_slv->checkEntailed(*term.d_node); - //////// - CVC5_API_TRY_CATCH_END; -} - -Result Solver::checkEntailed(const std::vector& terms) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(!d_slv->isQueryMade() - || d_slv->getOptions().base.incrementalSolving) - << "Cannot make multiple queries unless incremental solving is enabled " - "(try --incremental)"; - CVC5_API_SOLVER_CHECK_TERMS(terms); - ensureWellFormedTerms(terms); - //////// all checks before this line - return d_slv->checkEntailed(Term::termVectorToNodes(terms)); - //////// - CVC5_API_TRY_CATCH_END; -} - /* SMT-LIB commands */ /* -------------------------------------------------------------------------- */ @@ -6831,7 +6742,7 @@ Term Solver::defineFun(const std::string& symbol, CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort); CVC5_API_SOLVER_CHECK_TERM(term); - CVC5_API_CHECK(term.getSort().isSubsortOf(sort)) + CVC5_API_CHECK(term.getSort() == sort) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -7004,11 +6915,6 @@ void Solver::defineFunsRec(const std::vector& funs, CVC5_API_TRY_CATCH_END; } -void Solver::echo(std::ostream& out, const std::string& str) const -{ - out << str; -} - std::vector Solver::getAssertions(void) const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 95c2d73b1..3a10aa0a6 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -224,23 +224,6 @@ class CVC5_EXPORT Result */ bool isSatUnknown() const; - /** - * Return true if corresponding query was an entailed checkEntailed() query. - */ - bool isEntailed() const; - - /** - * Return true if corresponding query was a checkEntailed() query that is - * not entailed. - */ - bool isNotEntailed() const; - - /** - * Return true if query was a checkEntailed() query and cvc5 was not able to - * determine if it is entailed. - */ - bool isEntailmentUnknown() const; - /** * Operator overloading for equality of two results. * @param r the result to compare to for equality @@ -553,26 +536,6 @@ class CVC5_EXPORT Sort */ bool isFirstClass() const; - /** - * Is this a function-LIKE sort? - * - * Anything function-like except arrays (e.g., datatype selectors) is - * considered a function here. Function-like terms can not be the argument - * or return value for any term that is function-like. - * This is mainly to avoid higher order. - * - * @note Arrays are explicitly not considered function-like here. - * - * @return true if this is a function-like sort - */ - bool isFunctionLike() const; - - /** - * Is this sort a subsort of the given sort? - * @return true if this sort is a subsort of s - */ - bool isSubsortOf(const Sort& s) const; - /** * @return the underlying datatype of a datatype sort */ @@ -736,11 +699,6 @@ class CVC5_EXPORT Sort /* Sort constructor sort ----------------------------------------------- */ - /** - * @return the name of a sort constructor sort - */ - std::string getSortConstructorName() const; - /** * @return the arity of a sort constructor sort */ @@ -3865,21 +3823,6 @@ class CVC5_EXPORT Solver */ Result checkSatAssuming(const std::vector& assumptions) const; - /** - * 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 checkEntailed(const Term& term) const; - - /** - * 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 checkEntailed(const std::vector& terms) const; - /** * Create datatype sort. * @@ -4036,22 +3979,6 @@ class CVC5_EXPORT Solver const std::vector& terms, bool global = false) const; - /** - * Echo a given string to the given output stream. - * - * SMT-LIB: - * - * \verbatim embed:rst:leading-asterisk - * .. code:: smtlib - * - * (echo ) - * \endverbatim - * - * @param out the output stream - * @param str the string to echo - */ - void echo(std::ostream& out, const std::string& str) const; - /** * Get the list of asserted formulas. * @@ -4246,8 +4173,8 @@ class CVC5_EXPORT Solver * for showing the satisfiability of the last call to checkSat using the * current model. This method will only return false (for any v) if * option - * \verbatim embed:rst:inline :ref:`model-cores ` \endverbatim - * has been set. + * \verbatim embed:rst:inline :ref:`model-cores ` + * \endverbatim has been set. * * @param v The term in question * @return true if v is a model core symbol diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h index db628e1b6..e0ab5cfb8 100644 --- a/src/api/cpp/cvc5_checks.h +++ b/src/api/cpp/cvc5_checks.h @@ -399,28 +399,6 @@ namespace api { } \ } while (0) -/** - * Sort checks for member functions of class Solver. - * Check if each sort in the given container of sorts is not null, associated - * with this solver, and not function-like. - */ -#define CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts) \ - do \ - { \ - size_t i = 0; \ - for (const auto& s : sorts) \ - { \ - CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \ - CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - this == s.d_solver, "sort", sorts, i) \ - << "a sorts associated with this solver"; \ - CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - !s.getTypeNode().isFunctionLike(), "sort", sorts, i) \ - << "non-function-like sort"; \ - i += 1; \ - } \ - } while (0) - /** * Domain sort check for member functions of class Solver. * Check if domain sort is not null, associated with this solver, and a diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java index 3a34fbda6..1657d4a13 100644 --- a/src/api/java/io/github/cvc5/api/Result.java +++ b/src/api/java/io/github/cvc5/api/Result.java @@ -124,38 +124,6 @@ public class Result extends AbstractPointer private native boolean isSatUnknown(long pointer); - /** - * Return true if corresponding query was an entailed checkEntailed() query. - */ - public boolean isEntailed() - { - return isEntailed(pointer); - } - - private native boolean isEntailed(long pointer); - - /** - * Return true if corresponding query was a checkEntailed() query that is - * not entailed. - */ - public boolean isNotEntailed() - { - return isNotEntailed(pointer); - } - - private native boolean isNotEntailed(long pointer); - - /** - * Return true if query was a checkEntailed() query and cvc5 was not able to - * determine if it is entailed. - */ - public boolean isEntailmentUnknown() - { - return isEntailmentUnknown(pointer); - } - - private native boolean isEntailmentUnknown(long pointer); - /** * Operator overloading for equality of two results. * @param r the result to compare to for equality diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 5b985c4cb..6e73b3300 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -1485,34 +1485,6 @@ public class Solver implements IPointer, AutoCloseable private native long checkSatAssuming(long pointer, long[] assumptionPointers); - /** - * 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. - */ - public Result checkEntailed(Term term) - { - long resultPointer = checkEntailed(pointer, term.getPointer()); - return new Result(this, resultPointer); - } - - private native long checkEntailed(long pointer, long termPointer); - - /** - * 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. - */ - public Result checkEntailed(Term[] terms) - { - long[] pointers = Utils.getPointers(terms); - long resultPointer = checkEntailed(pointer, pointers); - return new Result(this, resultPointer); - } - - private native long checkEntailed(long pointer, long[] termPointers); - /** * Create datatype sort. * SMT-LIB: diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index 549ad6c25..967f0ea1e 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -385,36 +385,6 @@ public class Sort extends AbstractPointer implements Comparable private native boolean isFirstClass(long pointer); - /** - * Is this a function-LIKE sort? - * - * Anything function-like except arrays (e.g., datatype selectors) is - * considered a function here. Function-like terms can not be the argument - * or return value for any term that is function-like. - * This is mainly to avoid higher order. - * - * @apiNote Arrays are explicitly not considered function-like here. - * - * @return true if this is a function-like sort - */ - public boolean isFunctionLike() - { - return isFunctionLike(pointer); - } - - private native boolean isFunctionLike(long pointer); - - /** - * Is this sort a subsort of the given sort? - * @return true if this sort is a subsort of s - */ - public boolean isSubsortOf(Sort s) - { - return isSubsortOf(pointer, s.getPointer()); - } - - private native boolean isSubsortOf(long pointer, long sortPointer); - /** * @return the underlying datatype of a datatype sort */ @@ -683,16 +653,6 @@ public class Sort extends AbstractPointer implements Comparable /* Uninterpreted sort -------------------------------------------------- */ - /** - * @return the name of an uninterpreted sort - */ - public String getUninterpretedSortName() - { - return getUninterpretedSortName(pointer); - } - - private native String getUninterpretedSortName(long pointer); - /** * @return true if an uninterpreted sort is parameterezied */ @@ -716,16 +676,6 @@ public class Sort extends AbstractPointer implements Comparable /* Sort constructor sort ----------------------------------------------- */ - /** - * @return the name of a sort constructor sort - */ - public String getSortConstructorName() - { - return getSortConstructorName(pointer); - } - - private native String getSortConstructorName(long pointer); - /** * @return the arity of a sort constructor sort */ diff --git a/src/api/java/jni/result.cpp b/src/api/java/jni/result.cpp index 0534f240e..98bdcc765 100644 --- a/src/api/java/jni/result.cpp +++ b/src/api/java/jni/result.cpp @@ -89,48 +89,6 @@ Java_io_github_cvc5_api_Result_isSatUnknown(JNIEnv* env, jobject, jlong pointer) CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); } -/* - * Class: io_github_cvc5_api_Result - * Method: isEntailed - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_api_Result_isEntailed(JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Result* current = (Result*)pointer; - return (jboolean)current->isEntailed(); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); -} - -/* - * Class: io_github_cvc5_api_Result - * Method: isNotEntailed - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isNotEntailed( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Result* current = (Result*)pointer; - return (jboolean)current->isNotEntailed(); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); -} - -/* - * Class: io_github_cvc5_api_Result - * Method: isEntailmentUnknown - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isEntailmentUnknown( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Result* current = (Result*)pointer; - return (jboolean)current->isEntailmentUnknown(); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); -} - /* * Class: io_github_cvc5_api_Result * Method: equals diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 7d4d2acd6..4544ca2a7 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -1568,38 +1568,6 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSatAssuming__J_3J( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } -/* - * Class: io_github_cvc5_api_Solver - * Method: checkEntailed - * Signature: (JJ)J - */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkEntailed__JJ( - JNIEnv* env, jobject, jlong pointer, jlong termPointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast(pointer); - Term* term = reinterpret_cast(termPointer); - Result* retPointer = new Result(solver->checkEntailed(*term)); - return reinterpret_cast(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - -/* - * Class: io_github_cvc5_api_Solver - * Method: checkEntailed - * Signature: (J[J)J - */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkEntailed__J_3J( - JNIEnv* env, jobject, jlong pointer, jlongArray jTerms) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast(pointer); - std::vector terms = getObjectsFromPointers(env, jTerms); - Result* retPointer = new Result(solver->checkEntailed(terms)); - return reinterpret_cast(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - /* * Class: io_github_cvc5_api_Solver * Method: declareDatatype diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index 689b26e53..a3570dc86 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -480,35 +480,6 @@ Java_io_github_cvc5_api_Sort_isFirstClass(JNIEnv* env, jobject, jlong pointer) CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } -/* - * Class: io_github_cvc5_api_Sort - * Method: isFunctionLike - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_api_Sort_isFunctionLike(JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - return static_cast(current->isFunctionLike()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); -} - -/* - * Class: io_github_cvc5_api_Sort - * Method: isSubsortOf - * Signature: (JJ)Z - */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSubsortOf( - JNIEnv* env, jobject, jlong pointer, jlong sortPointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - Sort* sort = reinterpret_cast(sortPointer); - return static_cast(current->isSubsortOf(*sort)); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); -} - /* * Class: io_github_cvc5_api_Sort * Method: getDatatype @@ -881,20 +852,6 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSequenceElementSort( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } -/* - * Class: io_github_cvc5_api_Sort - * Method: getUninterpretedSortName - * Signature: (J)Ljava/lang/String; - */ -JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Sort_getUninterpretedSortName( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - return env->NewStringUTF(current->getUninterpretedSortName().c_str()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} - /* * Class: io_github_cvc5_api_Sort * Method: isUninterpretedSortParameterized @@ -935,20 +892,6 @@ Java_io_github_cvc5_api_Sort_getUninterpretedSortParamSorts(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } -/* - * Class: io_github_cvc5_api_Sort - * Method: getSortConstructorName - * Signature: (J)Ljava/lang/String; - */ -JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Sort_getSortConstructorName( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - return env->NewStringUTF(current->getSortConstructorName().c_str()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} - /* * Class: io_github_cvc5_api_Sort * Method: getSortConstructorArity diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index adad1467b..1e2c1c93e 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -142,9 +142,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isSat() except + bint isUnsat() except + bint isSatUnknown() except + - bint isEntailed() except + - bint isNotEntailed() except + - bint isEntailmentUnknown() except + bint operator==(const Result& r) except + bint operator!=(const Result& r) except + UnknownExplanation getUnknownExplanation() except + @@ -260,7 +257,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": void assertFormula(Term term) except + Result checkSat() except + Result checkSatAssuming(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 + @@ -351,8 +347,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isUninterpretedSort() except + bint isSortConstructor() except + bint isFirstClass() except + - bint isFunctionLike() except + - bint isSubsortOf(Sort s) except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except + @@ -371,10 +365,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort getSetElementSort() except + Sort getBagElementSort() except + Sort getSequenceElementSort() except + - string getUninterpretedSortName() except + bint isUninterpretedSortParameterized() except + vector[Sort] getUninterpretedSortParamSorts() except + - string getSortConstructorName() except + size_t getSortConstructorArity() except + uint32_t getBitVectorSize() except + uint32_t getFloatingPointExponentSize() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index b5b101231..53b3f643d 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -603,24 +603,6 @@ cdef class Result: """ return self.cr.isSatUnknown() - def isEntailed(self): - """ - :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() ` query. - """ - return self.cr.isEntailed() - - def isNotEntailed(self): - """ - :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() ` query that is not entailed. - """ - return self.cr.isNotEntailed() - - def isEntailmentUnknown(self): - """ - :return: True if query was a :cpp:func:`Solver::checkEntailed() ` query query and cvc5 was not able to determine if it is entailed. - """ - return self.cr.isEntailmentUnknown() - def getUnknownExplanation(self): """ :return: an explanation for an unknown query result. @@ -1761,21 +1743,6 @@ cdef class Solver: r.cr = self.csolver.checkSatAssuming( v) return r - @expand_list_arg(num_req_args=0) - def checkEntailed(self, *assumptions): - """Check entailment of the given formula w.r.t. the current set of assertions. - - :param terms: the formulas to check entailment for, as a list or as distinct arguments - :return: the result of the entailment check. - """ - cdef Result r = Result() - # used if assumptions is a list of terms - cdef vector[c_Term] v - for a in assumptions: - v.push_back(( a).cterm) - r.cr = self.csolver.checkEntailed( v) - return r - @expand_list_arg(num_req_args=1) def declareDatatype(self, str symbol, *ctors): """ @@ -2694,29 +2661,6 @@ cdef class Sort: """ return self.csort.isFirstClass() - def isFunctionLike(self): - """ - Is this a function-LIKE sort? - - Anything function-like except arrays (e.g., datatype selectors) is - considered a function here. Function-like terms can not be the argument - or return value for any term that is function-like. - This is mainly to avoid higher order. - - .. note:: Arrays are explicitly not considered function-like here. - - :return: True if this is a function-like sort - """ - return self.csort.isFunctionLike() - - def isSubsortOf(self, Sort sort): - """ - Is this sort a subsort of the given sort? - - :return: True if this sort is a subsort of s - """ - return self.csort.isSubsortOf(sort.csort) - def getDatatype(self): """ :return: the underlying datatype of a datatype sort @@ -2908,12 +2852,6 @@ cdef class Sort: sort.csort = self.csort.getSequenceElementSort() return sort - def getUninterpretedSortName(self): - """ - :return: the name of an uninterpreted sort - """ - return self.csort.getUninterpretedSortName().decode() - def isUninterpretedSortParameterized(self): """ :return: True if an uninterpreted sort is parameterized @@ -2931,12 +2869,6 @@ cdef class Sort: param_sorts.append(sort) return param_sorts - def getSortConstructorName(self): - """ - :return: the name of a sort constructor sort - """ - return self.csort.getSortConstructorName().decode() - def getSortConstructorArity(self): """ :return: the arity of a sort constructor sort diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 34175f8f8..efd092c5b 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -132,13 +132,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) { d_result = res = csa->getResult(); } - const QueryCommand* q = dynamic_cast(cmd); - if(q != nullptr) { - d_result = res = q->getResult(); - } - bool isResultUnsat = res.isUnsat() || res.isEntailed(); - bool isResultSat = res.isSat() || res.isNotEntailed(); + bool isResultUnsat = res.isUnsat(); + bool isResultSat = res.isSat(); // dump the model/proof/unsat core if option is set if (status) { diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 45e71b271..c78494e2c 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -258,7 +258,8 @@ parseCommand returns [cvc5::Command* cmd = NULL] } seq->addCommand(new SetInfoCommand("filename", filename)); if(PARSER_STATE->hasConjecture()) { - seq->addCommand(new QueryCommand(SOLVER->mkFalse())); + // note this does not impact how the TPTP status is reported currently + seq->addCommand(new CheckSatAssumingCommand(SOLVER->mkTrue())); } else { seq->addCommand(new CheckSatCommand()); } diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 188c5046b..3d7cb0601 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -68,33 +68,14 @@ void Assertions::clearCurrent() d_assertions.getIteSkolemMap().clear(); } -void Assertions::initializeCheckSat(const std::vector& assumptions, - bool isEntailmentCheck) +void Assertions::initializeCheckSat(const std::vector& assumptions) { - NodeManager* nm = NodeManager::currentNM(); // reset global negation d_globalNegation = false; // clear the assumptions d_assumptions.clear(); - if (isEntailmentCheck) - { - size_t size = assumptions.size(); - if (size > 1) - { - /* Assume: not (BIGAND assumptions) */ - d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode()); - } - else if (size == 1) - { - /* Assume: not expr */ - d_assumptions.push_back(assumptions[0].notNode()); - } - } - else - { - /* Assume: BIGAND assumptions */ - d_assumptions = assumptions; - } + /* Assume: BIGAND assumptions */ + d_assumptions = assumptions; Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); for (const Node& e : d_assumptions) diff --git a/src/smt/assertions.h b/src/smt/assertions.h index ade5bbc81..2f80c645c 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -69,11 +69,8 @@ class Assertions : protected EnvObj * upcoming check-sat call. * * @param assumptions The assumptions of the upcoming check-sat call. - * @param isEntailmentCheck Whether we are checking entailment of assumptions - * in the upcoming check-sat call. */ - void initializeCheckSat(const std::vector& assumptions, - bool isEntailmentCheck); + void initializeCheckSat(const std::vector& assumptions); /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 1474ed240..5535cd0c2 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -544,56 +544,6 @@ void CheckSatAssumingCommand::toStream(std::ostream& out, out, termVectorToNodes(d_terms)); } -/* -------------------------------------------------------------------------- */ -/* class QueryCommand */ -/* -------------------------------------------------------------------------- */ - -QueryCommand::QueryCommand(const api::Term& t) : d_term(t) {} - -api::Term QueryCommand::getTerm() const { return d_term; } -void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm) -{ - try - { - d_result = solver->checkEntailed(d_term); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -api::Result QueryCommand::getResult() const { return d_result; } -void QueryCommand::printResult(std::ostream& out) const -{ - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_result << endl; - } -} - -Command* QueryCommand::clone() const -{ - QueryCommand* c = new QueryCommand(d_term); - c->d_result = d_result; - return c; -} - -std::string QueryCommand::getCommandName() const { return "query"; } - -void QueryCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const -{ - Printer::getPrinter(language)->toStreamCmdQuery(out, termToNode(d_term)); -} - /* -------------------------------------------------------------------------- */ /* class DeclareSygusVarCommand */ /* -------------------------------------------------------------------------- */ @@ -1891,7 +1841,7 @@ bool GetInstantiationsCommand::isEnabled(api::Solver* solver, return (res.isSat() || (res.isSatUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE)) - || res.isUnsat() || res.isEntailed(); + || res.isUnsat(); } void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm) { diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 1b84e0c74..8d41be049 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -72,9 +72,8 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Trace("smt-qe-debug") << "Query for quantifier elimination : " << ne << std::endl; Assert(ne.getNumChildren() == 3); - // We consider this to be an entailment check, which also avoids incorrect - // status reporting (see SolverEngineState::d_expectedStatus). - Result r = d_smtSolver.checkSatisfiability(as, std::vector{ne}, true); + Result r = + d_smtSolver.checkSatisfiability(as, std::vector{ne.notNode()}); Trace("smt-qe") << "Query returned " << r << std::endl; if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 2151dc03e..cf3c40ac0 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -113,8 +113,7 @@ void SmtSolver::interrupt() } Result SmtSolver::checkSatisfiability(Assertions& as, - const std::vector& assumptions, - bool isEntailmentCheck) + const std::vector& assumptions) { Result result; @@ -126,7 +125,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, d_state.notifyCheckSat(hasAssumptions); // then, initialize the assertions - as.initializeCheckSat(assumptions, isEntailmentCheck); + as.initializeCheckSat(assumptions); // make the check, where notice smt engine should be fully inited by now diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 4ee4b0139..10625f4bd 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -93,12 +93,9 @@ class SmtSolver * during this call. * @param assumptions The assumptions for this check-sat call, which are * temporary assertions. - * @param isEntailmentCheck Whether this is an entailment check (assumptions - * are negated in this case). */ Result checkSatisfiability(Assertions& as, - const std::vector& assumptions, - bool isEntailmentCheck); + const std::vector& assumptions); /** * Process the assertions that have been asserted in as. This moves the set of * assertions that have been buffered into as, preprocesses them, pushes them diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 9d8311392..7cefea507 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -746,48 +746,28 @@ Result SolverEngine::checkSat(const Node& assumption) { assump.push_back(assumption); } - return checkSatInternal(assump, false); + return checkSatInternal(assump); } Result SolverEngine::checkSat(const std::vector& assumptions) { ensureWellFormedTerms(assumptions, "checkSat"); - return checkSatInternal(assumptions, false); + return checkSatInternal(assumptions); } -Result SolverEngine::checkEntailed(const Node& node) -{ - ensureWellFormedTerm(node, "checkEntailed"); - return checkSatInternal( - node.isNull() ? std::vector() : std::vector{node}, - true) - .asEntailmentResult(); -} - -Result SolverEngine::checkEntailed(const std::vector& nodes) -{ - ensureWellFormedTerms(nodes, "checkEntailed"); - return checkSatInternal(nodes, true).asEntailmentResult(); -} - -Result SolverEngine::checkSatInternal(const std::vector& assumptions, - bool isEntailmentCheck) +Result SolverEngine::checkSatInternal(const std::vector& assumptions) { Result r; SolverEngineScope smts(this); finishInit(); - Trace("smt") << "SolverEngine::" - << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" - << assumptions << ")" << endl; + Trace("smt") << "SolverEngine::checkSat(" << assumptions << ")" << endl; // check the satisfiability with the solver object - r = d_smtSolver->checkSatisfiability( - *d_asserts.get(), assumptions, isEntailmentCheck); + r = d_smtSolver->checkSatisfiability(*d_asserts.get(), assumptions); - Trace("smt") << "SolverEngine::" - << (isEntailmentCheck ? "query" : "checkSat") << "(" - << assumptions << ") => " << r << endl; + Trace("smt") << "SolverEngine::checkSat(" << assumptions << ") => " << r + << endl; // Check that SAT results generate a model correctly. if (d_env->getOptions().smt.checkModels) diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index ae8013965..824f67dbd 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -149,7 +149,7 @@ class CVC5_EXPORT SolverEngine */ bool isFullyInited() const; /** - * Return true if a checkEntailed() or checkSatisfiability() has been made. + * Return true if a checkSatisfiability() has been made. */ bool isQueryMade() const; /** Return the user context level. */ @@ -163,7 +163,7 @@ class CVC5_EXPORT SolverEngine */ bool isSmtModeSat() const; /** - * Returns the most recent result of checkSat/checkEntailed or + * Returns the most recent result of checkSat or * (set-info :status). */ Result getStatusOfLastCommand() const; @@ -349,17 +349,6 @@ class CVC5_EXPORT SolverEngine */ std::vector reduceUnsatCore(const std::vector& core); - /** - * 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 checkEntailed(const Node& assumption); - Result checkEntailed(const std::vector& assumptions); - /** * Assert a formula (if provided) to the current context and call * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result. @@ -1017,8 +1006,7 @@ class CVC5_EXPORT SolverEngine /* * Check satisfiability (used to check satisfiability and entailment). */ - Result checkSatInternal(const std::vector& assumptions, - bool isEntailmentCheck); + Result checkSatInternal(const std::vector& assumptions); /** * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 692a123db..e3844ab46 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -259,7 +259,7 @@ Result SygusSolver::checkSynth(Assertions& as, bool isNext) { std::vector query; query.push_back(d_conj); - r = d_smtSolver.checkSatisfiability(as, query, false); + r = d_smtSolver.checkSatisfiability(as, query); } // The result returned by the above call is typically "unknown", which may // or may not correspond to a state in which we solved the conjecture diff --git a/test/api/cpp/boilerplate.cpp b/test/api/cpp/boilerplate.cpp index 0f561e7cf..a57a6a895 100644 --- a/test/api/cpp/boilerplate.cpp +++ b/test/api/cpp/boilerplate.cpp @@ -27,7 +27,7 @@ using namespace std; int main() { Solver slv; - Result r = slv.checkEntailed(slv.mkBoolean(true)); - return r.isEntailed() ? 0 : 1; + Result r = slv.checkSatAssuming(slv.mkBoolean(false)); + return r.isUnsat() ? 0 : 1; } diff --git a/test/api/cpp/issue5074.cpp b/test/api/cpp/issue5074.cpp index a4f07a581..a8e91c27a 100644 --- a/test/api/cpp/issue5074.cpp +++ b/test/api/cpp/issue5074.cpp @@ -25,7 +25,7 @@ int main() Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, t6); Term t14 = slv.mkTerm(Kind::STRING_REPLACE_RE, {t6, t12, t6}); Term t16 = slv.mkTerm(Kind::STRING_CONTAINS, {t14, t14}); - slv.checkEntailed(t16); + slv.checkSatAssuming(t16.notTerm()); return 0; } diff --git a/test/api/cpp/proj-issue344.cpp b/test/api/cpp/proj-issue344.cpp index 5f486706c..3d0f43777 100644 --- a/test/api/cpp/proj-issue344.cpp +++ b/test/api/cpp/proj-issue344.cpp @@ -29,5 +29,6 @@ int main(void) Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13}); Term t66 = slv.mkTerm(Kind::BITVECTOR_ULTBV, {t25, t25}); Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66}); - slv.checkEntailed({t154, t154, t154, t154}); + Term query = slv.mkTerm(Kind::AND, {t154, t154, t154, t154}); + slv.checkSatAssuming(query.notTerm()); } diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/proj-issue345.cpp index c33e9e5b8..95b93952e 100644 --- a/test/api/cpp/proj-issue345.cpp +++ b/test/api/cpp/proj-issue345.cpp @@ -29,6 +29,7 @@ int main(void) Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13}); Term t66 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t25, t25}); Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66}); - slv.checkEntailed({t154, t154, t154, t154}); + Term query = slv.mkTerm(Kind::AND, {t154, t154, t154, t154}); + slv.checkSatAssuming(query.notTerm()); } diff --git a/test/api/cpp/two_solvers.cpp b/test/api/cpp/two_solvers.cpp index 150da1e9e..a052094b4 100644 --- a/test/api/cpp/two_solvers.cpp +++ b/test/api/cpp/two_solvers.cpp @@ -24,8 +24,8 @@ using namespace std; int main() { Solver s1; Solver s2; - Result r = s1.checkEntailed(s1.mkBoolean(true)); - Result r2 = s2.checkEntailed(s2.mkBoolean(true)); - return r.isEntailed() && r2.isEntailed() ? 0 : 1; + Result r = s1.checkSatAssuming(s1.mkBoolean(false)); + Result r2 = s2.checkSatAssuming(s2.mkBoolean(false)); + return r.isUnsat() && r2.isUnsat() ? 0 : 1; } diff --git a/test/api/python/boilerplate.py b/test/api/python/boilerplate.py index fc0d50a86..ee3e6ca57 100644 --- a/test/api/python/boilerplate.py +++ b/test/api/python/boilerplate.py @@ -20,5 +20,5 @@ import cvc5 slv = cvc5.Solver() -r = slv.checkEntailed(slv.mkBoolean(True)) -r.isEntailed() +r = slv.checkSatAssuming(slv.mkBoolean(False)) +r.isUnsat() diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py index 84a200f84..f41ebb16a 100644 --- a/test/api/python/issue5074.py +++ b/test/api/python/issue5074.py @@ -22,4 +22,4 @@ t6 = slv.mkTerm(Kind.StringFromCode, c1) t12 = slv.mkTerm(Kind.StringToRegexp, t6) t14 = slv.mkTerm(Kind.StringReplaceRe, [t6, t12, t6]) t16 = slv.mkTerm(Kind.StringContains, [t14, t14]) -slv.checkEntailed(t16) +slv.checkSatAssuming(t16.notTerm()) diff --git a/test/api/python/two_solvers.py b/test/api/python/two_solvers.py index 2e458ed32..7692d907c 100644 --- a/test/api/python/two_solvers.py +++ b/test/api/python/two_solvers.py @@ -17,6 +17,6 @@ import cvc5 s1 = cvc5.Solver() s2 = cvc5.Solver() -r1 = s1.checkEntailed(s1.mkBoolean(True)) -r2 = s2.checkEntailed(s2.mkBoolean(True)) -assert r1.isEntailed() and r2.isEntailed() +r1 = s1.checkSatAssuming(s1.mkBoolean(False)) +r2 = s2.checkSatAssuming(s2.mkBoolean(False)) +assert r1.isUnsat() and r2.isUnsat() diff --git a/test/regress/regress0/bug398.smt2 b/test/regress/regress0/bug398.smt2 index 3e4a1faca..6e59b0564 100644 --- a/test/regress/regress0/bug398.smt2 +++ b/test/regress/regress0/bug398.smt2 @@ -1,3 +1,3 @@ ; EXIT: 0 (set-logic QF_LRA) -(define-fun x () Real (+ 4 1)) +(define-fun x () Real (+ 4.0 1.0)) diff --git a/test/regress/regress0/tptp/ARI086=1.p b/test/regress/regress0/tptp/ARI086=1.p index f6d2fcb28..7b6d1518a 100644 --- a/test/regress/regress0/tptp/ARI086=1.p +++ b/test/regress/regress0/tptp/ARI086=1.p @@ -9,7 +9,7 @@ % Source : [TPTP] % Names : -% Status : CounterSatisfiable +% Status : Satisfiable % Rating : 0.00 v5.2.0, 1.00 v5.0.0 % Syntax : Number of formulae : 1 ( 1 unit; 0 type) % Number of atoms : 1 ( 1 equality) diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p index f30db563a..16d58b687 100644 --- a/test/regress/regress0/tptp/DAT001=1.p +++ b/test/regress/regress0/tptp/DAT001=1.p @@ -10,7 +10,7 @@ % Source : [TPTP] % Names : -% Status : Theorem +% Status : Unsatisfiable % Rating : 0.12 v5.5.0, 0.25 v5.4.0, 0.38 v5.3.0, 0.29 v5.2.0, 0.20 v5.1.0, 0.25 v5.0.0 % Syntax : Number of formulae : 8 ( 5 unit; 4 type) % Number of atoms : 13 ( 0 equality) diff --git a/test/regress/regress0/tptp/MGT019+2.p b/test/regress/regress0/tptp/MGT019+2.p index 7bebdc095..83e7a2d76 100644 --- a/test/regress/regress0/tptp/MGT019+2.p +++ b/test/regress/regress0/tptp/MGT019+2.p @@ -15,7 +15,7 @@ % Names : LEMMA 1 [PM93] % : L1 [PB+94] -% Status : CounterSatisfiable +% Status : Satisfiable % Rating : 0.00 v4.1.0, 0.20 v4.0.1, 0.00 v3.5.0, 0.33 v3.4.0, 0.00 v2.1.0 % Syntax : Number of formulae : 5 ( 0 unit) % Number of atoms : 21 ( 1 equality) diff --git a/test/regress/regress0/tptp/PUZ131_1.p b/test/regress/regress0/tptp/PUZ131_1.p index b9e1c648b..c60038357 100644 --- a/test/regress/regress0/tptp/PUZ131_1.p +++ b/test/regress/regress0/tptp/PUZ131_1.p @@ -15,7 +15,7 @@ % Source : [TPTP] % Names : -% Status : Theorem +% Status : Unsatisfiable % Rating : 0.00 v5.0.0 % Syntax : Number of formulae : 19 ( 14 unit; 10 type) % Number of atoms : 28 ( 1 equality) diff --git a/test/regress/regress0/tptp/SYN000+1.p b/test/regress/regress0/tptp/SYN000+1.p index 682c11b69..bc0a7bef8 100644 --- a/test/regress/regress0/tptp/SYN000+1.p +++ b/test/regress/regress0/tptp/SYN000+1.p @@ -9,7 +9,7 @@ % Source : [TPTP] % Names : -% Status : Theorem +% Status : Unsatisfiable % Rating : 0.43 v5.5.0, 0.48 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0 % Syntax : Number of formulae : 12 ( 5 unit) % Number of atoms : 31 ( 3 equality) diff --git a/test/regress/regress0/tptp/SYN000=2.p b/test/regress/regress0/tptp/SYN000=2.p index 802613f4b..a34357130 100644 --- a/test/regress/regress0/tptp/SYN000=2.p +++ b/test/regress/regress0/tptp/SYN000=2.p @@ -9,7 +9,7 @@ % Source : [TPTP] % Names : -% Status : Theorem +% Status : Unsatisfiable % Rating : ? v5.5.1 % Syntax : Number of formulae : 83 ( 73 unit; 6 type) % Number of atoms : 100 ( 4 equality) diff --git a/test/regress/regress0/tptp/SYN000_1.p b/test/regress/regress0/tptp/SYN000_1.p index ed683c070..48703c459 100644 --- a/test/regress/regress0/tptp/SYN000_1.p +++ b/test/regress/regress0/tptp/SYN000_1.p @@ -9,7 +9,7 @@ % Source : [TPTP] % Names : -% Status : Theorem +% Status : Unsatisfiable % Rating : 0.40 v5.5.0, 0.25 v5.4.0, 0.33 v5.2.0, 0.67 v5.0.0 % Syntax : Number of formulae : 38 ( 21 unit; 25 type) % Number of atoms : 74 ( 3 equality) diff --git a/test/regress/regress0/tptp/is_rat_simple.p b/test/regress/regress0/tptp/is_rat_simple.p index c983033b9..747ce9007 100644 --- a/test/regress/regress0/tptp/is_rat_simple.p +++ b/test/regress/regress0/tptp/is_rat_simple.p @@ -1,5 +1,5 @@ % states that all reals are not rational (countersatisfiable) -% Status : CounterSatisfiable +% Status : Satisfiable %------------------------------------------------------------------------------ tff(the,conjecture,( ! [X: $real] : diff --git a/test/regress/regress0/tptp/parse-neg-rational.p b/test/regress/regress0/tptp/parse-neg-rational.p index 9e892a3b7..7b20c09df 100644 --- a/test/regress/regress0/tptp/parse-neg-rational.p +++ b/test/regress/regress0/tptp/parse-neg-rational.p @@ -9,7 +9,7 @@ % Source : [TPTP] % Names : -% Status : Theorem +% Status : Unsatisfiable % Rating : 0.00 v6.2.0, 0.20 v6.1.0, 0.22 v6.0.0, 0.25 v5.3.0, 0.14 v5.2.0, 0.20 v5.1.0, 0.25 v5.0.0 % Syntax : Number of formulae : 1 ( 1 unit; 0 type) % Number of atoms : 1 ( 0 equality) diff --git a/test/regress/regress0/tptp/tff0-arith.p b/test/regress/regress0/tptp/tff0-arith.p index c0e9af25a..8f759cce7 100644 --- a/test/regress/regress0/tptp/tff0-arith.p +++ b/test/regress/regress0/tptp/tff0-arith.p @@ -1,7 +1,7 @@ % example from the TFF0 paper % see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa % -% Status : Theorem +% Status : Unsatisfiable % tff(list_type,type, ( list: $tType )). tff(nil_type,type, ( nil: list )). diff --git a/test/regress/regress0/tptp/tff0.p b/test/regress/regress0/tptp/tff0.p index 0402687bc..2374cb07a 100644 --- a/test/regress/regress0/tptp/tff0.p +++ b/test/regress/regress0/tptp/tff0.p @@ -1,7 +1,7 @@ % example from the TFF0 paper % see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa % -% Status : Theorem +% Status : Unsatisfiable % tff(student_type,type, ( student: $tType )). tff(professor_type,type,( professor: $tType )). diff --git a/test/regress/regress0/tptp/tptp_parser10.p b/test/regress/regress0/tptp/tptp_parser10.p index d6a257121..5b47adbdc 100644 --- a/test/regress/regress0/tptp/tptp_parser10.p +++ b/test/regress/regress0/tptp/tptp_parser10.p @@ -1,4 +1,4 @@ -% Status: Theorem +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/tptp_parser9.p b/test/regress/regress0/tptp/tptp_parser9.p index 4ce2e0227..32c0f71cb 100644 --- a/test/regress/regress0/tptp/tptp_parser9.p +++ b/test/regress/regress0/tptp/tptp_parser9.p @@ -1,5 +1,5 @@ % COMMAND-LINE: --finite-model-find -% Status: CounterSatisfiable +% Status: Satisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress1/bug800.smt2 b/test/regress/regress1/bug800.smt2 index b62be95bd..1315c81fc 100644 --- a/test/regress/regress1/bug800.smt2 +++ b/test/regress/regress1/bug800.smt2 @@ -25,7 +25,7 @@ (declare-fun |main::__CPAchecker_TMP_0@3| () Real) (declare-fun |__ADDRESS_OF_main::d1| () Real) (declare-fun |main::d2@2| () Real) -(define-fun _7 () Real 0) +(define-fun _7 () Real 0.0) (define-fun _8 () Real |__ADDRESS_OF_main::x1|) (define-fun _9 () Real (__BASE_ADDRESS_OF__ _8)) (define-fun _10 () Bool (= _8 _9)) @@ -40,7 +40,7 @@ (define-fun _19 () Real |__ADDRESS_OF_main::d1|) (define-fun _20 () Real (__BASE_ADDRESS_OF__ _19)) (define-fun _21 () Bool (= _19 _20)) -(define-fun _22 () Real 1) +(define-fun _22 () Real 1.0) (define-fun _23 () Real |main::d1@2|) (define-fun _24 () Bool (= _23 _22)) (define-fun _25 () Bool (and _21 _24)) diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p index e07ad784f..f1dcadf00 100644 --- a/test/regress/regress1/ho/NUM925^1.p +++ b/test/regress/regress1/ho/NUM925^1.p @@ -1,5 +1,5 @@ % COMMAND-LINE: --ho-elim -% EXPECT: % SZS status Theorem for NUM925^1 +% EXPECT: % SZS status Unsatisfiable for NUM925^1 %------------------------------------------------------------------------------ % File : NUM925^1 : TPTP v7.2.0. Released v5.3.0. diff --git a/test/regress/regress1/ho/fta0328.lfho.p b/test/regress/regress1/ho/fta0328.lfho.p index f67c6db58..0756a4414 100644 --- a/test/regress/regress1/ho/fta0328.lfho.p +++ b/test/regress/regress1/ho/fta0328.lfho.p @@ -1,5 +1,5 @@ % COMMAND-LINE: --finite-model-find -% EXPECT: % SZS status CounterSatisfiable for fta0328.lfho +% EXPECT: % SZS status Satisfiable for fta0328.lfho % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/.isabelle/contrib/e-2.0-2/x86_64-darwin/eprover --auto-schedule --tstp-in --tstp-out --silent --cpu-limit=2 --proof-object=1 /Users/blanchette/hgs/matryoshka/papers/2019-TACAS-ehoh/eval/judgment_day/judgment_day_lifting_32/fta/prob_804__4064966_1 ) ; } % This file was generated by Isabelle (most likely Sledgehammer) diff --git a/test/regress/regress1/ho/store-ax-min.p b/test/regress/regress1/ho/store-ax-min.p index d000a17d0..2f1cb6b03 100644 --- a/test/regress/regress1/ho/store-ax-min.p +++ b/test/regress/regress1/ho/store-ax-min.p @@ -1,6 +1,6 @@ % COMMAND-LINE: --full-saturate-quant --ho-elim-store-ax % COMMAND-LINE: --full-saturate-quant --ho-elim -% EXPECT: % SZS status Theorem for store-ax-min +% EXPECT: % SZS status Unsatisfiable for store-ax-min thf(a, type, (a: $i)). thf(b, type, (b: $i)). diff --git a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p index bf58b95d8..594a0953f 100644 --- a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p +++ b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p @@ -1,5 +1,5 @@ % COMMAND-LINE: --full-saturate-quant --ho-elim -% EXPECT: % SZS status Theorem for bug_instfalse_SEU882^5 +% EXPECT: % SZS status Unsatisfiable for bug_instfalse_SEU882^5 %------------------------------------------------------------------------------ % File : SEU882^5 : TPTP v7.2.0. Released v4.0.0. diff --git a/test/regress/regress2/ho/involved_parsing_ALG248^3.p b/test/regress/regress2/ho/involved_parsing_ALG248^3.p index 47a89143d..2c7ab5549 100644 --- a/test/regress/regress2/ho/involved_parsing_ALG248^3.p +++ b/test/regress/regress2/ho/involved_parsing_ALG248^3.p @@ -1,5 +1,5 @@ % COMMAND-LINE: --ho-elim -% EXPECT: % SZS status Theorem for involved_parsing_ALG248^3 +% EXPECT: % SZS status Unsatisfiable for involved_parsing_ALG248^3 %------------------------------------------------------------------------------ % File : ALG248^3 : TPTP v7.2.0. Bugfixed v5.2.0. diff --git a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p index 5f87519d1..dc7e0c483 100644 --- a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p +++ b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p @@ -1,5 +1,5 @@ % COMMAND-LINE: --full-saturate-quant --ho-elim -% EXPECT: % SZS status Theorem for partial_app_interpreted_SWW474^2 +% EXPECT: % SZS status Unsatisfiable for partial_app_interpreted_SWW474^2 %------------------------------------------------------------------------------ % File : SWW474^2 : TPTP v7.2.0. Released v5.3.0. diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index b06e20fbf..c783f2fa2 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -301,23 +301,6 @@ TEST_F(TestApiBlackDatatype, parametricDatatype) ASSERT_NE(pairIntInt, pairIntReal); ASSERT_NE(pairIntInt, pairRealInt); ASSERT_NE(pairIntReal, pairRealInt); - - ASSERT_TRUE(pairRealReal.isSubsortOf(pairRealReal)); - ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealReal)); - ASSERT_FALSE(pairRealInt.isSubsortOf(pairRealReal)); - ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealReal)); - ASSERT_FALSE(pairRealReal.isSubsortOf(pairRealInt)); - ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealInt)); - ASSERT_TRUE(pairRealInt.isSubsortOf(pairRealInt)); - ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealInt)); - ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntReal)); - ASSERT_TRUE(pairIntReal.isSubsortOf(pairIntReal)); - ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntReal)); - ASSERT_FALSE(pairIntInt.isSubsortOf(pairIntReal)); - ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntInt)); - ASSERT_FALSE(pairIntReal.isSubsortOf(pairIntInt)); - ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntInt)); - ASSERT_TRUE(pairIntInt.isSubsortOf(pairIntInt)); } TEST_F(TestApiBlackDatatype, isFinite) diff --git a/test/unit/api/cpp/result_black.cpp b/test/unit/api/cpp/result_black.cpp index 23f48caa2..9606a2540 100644 --- a/test/unit/api/cpp/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp @@ -32,9 +32,6 @@ TEST_F(TestApiBlackResult, isNull) ASSERT_FALSE(res_null.isSat()); ASSERT_FALSE(res_null.isUnsat()); ASSERT_FALSE(res_null.isSatUnknown()); - ASSERT_FALSE(res_null.isEntailed()); - ASSERT_FALSE(res_null.isNotEntailed()); - ASSERT_FALSE(res_null.isEntailmentUnknown()); Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); @@ -88,35 +85,5 @@ TEST_F(TestApiBlackResult, isSatUnknown) ASSERT_TRUE(res.isSatUnknown()); } -TEST_F(TestApiBlackResult, isEntailed) -{ - d_solver.setOption("incremental", "true"); - Sort u_sort = d_solver.mkUninterpretedSort("u"); - 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); - cvc5::api::Result entailed = d_solver.checkEntailed(a); - ASSERT_TRUE(entailed.isEntailed()); - ASSERT_FALSE(entailed.isEntailmentUnknown()); - cvc5::api::Result not_entailed = d_solver.checkEntailed(b); - ASSERT_TRUE(not_entailed.isNotEntailed()); - ASSERT_FALSE(not_entailed.isEntailmentUnknown()); -} - -TEST_F(TestApiBlackResult, isEntailmentUnknown) -{ - d_solver.setLogic("QF_NIA"); - d_solver.setOption("incremental", "false"); - d_solver.setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver.getIntegerSort(); - Term x = d_solver.mkConst(int_sort, "x"); - d_solver.assertFormula(x.eqTerm(x).notTerm()); - cvc5::api::Result res = d_solver.checkEntailed(x.eqTerm(x)); - ASSERT_FALSE(res.isEntailed()); - ASSERT_TRUE(res.isEntailmentUnknown()); - ASSERT_EQ(res.getUnknownExplanation(), api::Result::UNKNOWN_REASON); -} } // namespace test } // namespace cvc5 diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 4ea0b7ff1..b07b3eaa7 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2264,79 +2264,6 @@ TEST_F(TestApiBlackSolver, assertFormula) ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC5ApiException); } -TEST_F(TestApiBlackSolver, checkEntailed) -{ - d_solver.setOption("incremental", "false"); - ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue())); - ASSERT_THROW(d_solver.checkEntailed(d_solver.mkTrue()), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException); -} - -TEST_F(TestApiBlackSolver, checkEntailed1) -{ - 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"); - ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue())); - ASSERT_THROW(d_solver.checkEntailed(Term()), CVC5ApiException); - ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue())); - ASSERT_NO_THROW(d_solver.checkEntailed(z)); - Solver slv; - ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException); -} - -TEST_F(TestApiBlackSolver, checkEntailed2) -{ - d_solver.setOption("incremental", "true"); - - Sort uSort = d_solver.mkUninterpretedSort("u"); - Sort intSort = d_solver.getIntegerSort(); - Sort boolSort = d_solver.getBooleanSort(); - Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort); - Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort); - - Term n = Term(); - // Constants - Term x = d_solver.mkConst(uSort, "x"); - Term y = d_solver.mkConst(uSort, "y"); - // Functions - Term f = d_solver.mkConst(uToIntSort, "f"); - Term p = d_solver.mkConst(intPredSort, "p"); - // Values - Term zero = d_solver.mkInteger(0); - Term one = d_solver.mkInteger(1); - // Terms - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(ADD, f_x, f_y); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); - Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); - // Assertions - Term assertions = - d_solver.mkTerm(AND, - std::vector{ - d_solver.mkTerm(LEQ, zero, f_x), // 0 <= f(x) - d_solver.mkTerm(LEQ, zero, f_y), // 0 <= f(y) - d_solver.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notTerm(), // not p(0) - p_f_y // p(f(y)) - }); - - ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue())); - d_solver.assertFormula(assertions); - ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y))); - ASSERT_NO_THROW(d_solver.checkEntailed( - {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)})); - ASSERT_THROW(d_solver.checkEntailed(n), CVC5ApiException); - ASSERT_THROW(d_solver.checkEntailed({n, d_solver.mkTerm(DISTINCT, x, y)}), - CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException); -} - TEST_F(TestApiBlackSolver, checkSat) { d_solver.setOption("incremental", "false"); @@ -2802,8 +2729,9 @@ TEST_F(TestApiBlackSolver, issue7000) Term t59 = d_solver.mkConst(s2, "_x51"); Term t72 = d_solver.mkTerm(EQUAL, t37, t59); Term t74 = d_solver.mkTerm(GT, t4, t7); + Term query = d_solver.mkTerm(AND, {t72, t74, t72, t72}); // throws logic exception since logic is not higher order by default - ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException); + ASSERT_THROW(d_solver.checkSatAssuming(query.notTerm()), CVC5ApiException); } TEST_F(TestApiBlackSolver, issue5893) @@ -3009,7 +2937,7 @@ TEST_F(TestApiBlackSolver, proj_issue383) Term t3 = d_solver.mkConst(s4, "_x25"); Term t13 = d_solver.mkConst(s1, "_x34"); - d_solver.checkEntailed(t13); + d_solver.checkSatAssuming(t13.notTerm()); ASSERT_THROW(d_solver.getValue(t3), CVC5ApiException); } @@ -3178,7 +3106,7 @@ TEST_F(TestApiBlackSolver, proj_issue429) Term t111 = slv.mkTerm(Kind::SEQ_UNIT, {t16}); Term t119 = slv.mkTerm(slv.mkOp(Kind::SEQ_UNIT), {t6}); Term t126 = slv.mkTerm(Kind::SEQ_PREFIX, {t111, t119}); - slv.checkEntailed({t126}); + slv.checkSatAssuming({t126.notTerm()}); } TEST_F(TestApiBlackSolver, proj_issue422) diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 4b2c2ae0b..a7192d78e 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -271,30 +271,6 @@ TEST_F(TestApiBlackSort, isFirstClass) ASSERT_NO_THROW(Sort().isFirstClass()); } -TEST_F(TestApiBlackSort, isFunctionLike) -{ - Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), - d_solver.getIntegerSort()); - ASSERT_FALSE(d_solver.getIntegerSort().isFunctionLike()); - ASSERT_TRUE(fun_sort.isFunctionLike()); - - Sort dt_sort = create_datatype_sort(); - Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt[0][1].getSelectorTerm().getSort(); - ASSERT_TRUE(cons_sort.isFunctionLike()); - - ASSERT_NO_THROW(Sort().isFunctionLike()); -} - -TEST_F(TestApiBlackSort, isSubsortOf) -{ - ASSERT_TRUE(d_solver.getIntegerSort().isSubsortOf(d_solver.getIntegerSort())); - ASSERT_TRUE(d_solver.getIntegerSort().isSubsortOf(d_solver.getRealSort())); - ASSERT_FALSE( - d_solver.getIntegerSort().isSubsortOf(d_solver.getBooleanSort())); - ASSERT_NO_THROW(Sort().isSubsortOf(Sort())); -} - TEST_F(TestApiBlackSort, getDatatype) { Sort dtypeSort = create_datatype_sort(); @@ -443,9 +419,9 @@ TEST_F(TestApiBlackSort, getSequenceElementSort) TEST_F(TestApiBlackSort, getUninterpretedSortName) { Sort uSort = d_solver.mkUninterpretedSort("u"); - ASSERT_NO_THROW(uSort.getUninterpretedSortName()); + ASSERT_NO_THROW(uSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC5ApiException); + ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException); } TEST_F(TestApiBlackSort, isUninterpretedSortParameterized) @@ -473,9 +449,9 @@ TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) { Sort sSort = d_solver.mkSortConstructorSort("s", 2); - ASSERT_NO_THROW(sSort.getSortConstructorName()); + ASSERT_NO_THROW(sSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getSortConstructorName(), CVC5ApiException); + ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException); } TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) @@ -580,23 +556,6 @@ TEST_F(TestApiBlackSort, sortCompare) ASSERT_TRUE((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort)); } -TEST_F(TestApiBlackSort, sortSubtyping) -{ - Sort intSort = d_solver.getIntegerSort(); - Sort realSort = d_solver.getRealSort(); - ASSERT_TRUE(intSort.isSubsortOf(realSort)); - ASSERT_FALSE(realSort.isSubsortOf(intSort)); - - Sort arraySortII = d_solver.mkArraySort(intSort, intSort); - Sort arraySortIR = d_solver.mkArraySort(intSort, realSort); - - Sort setSortI = d_solver.mkSetSort(intSort); - Sort setSortR = d_solver.mkSetSort(realSort); - // we don't support subtyping for sets - ASSERT_FALSE(setSortI.isSubsortOf(setSortR)); - ASSERT_FALSE(setSortR.isSubsortOf(setSortI)); -} - TEST_F(TestApiBlackSort, sortScopedToString) { std::string name = "uninterp-sort"; diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp index f902378cd..8a56c032c 100644 --- a/test/unit/api/cpp/theory_arith_nl_black.cpp +++ b/test/unit/api/cpp/theory_arith_nl_black.cpp @@ -85,7 +85,7 @@ TEST_F(TestTheoryBlackArithNl, proj_issue421) Term t77 = slv.mkTerm(Kind::LEQ, {t69, t10}); Term t128 = slv.mkTerm(Kind::SEQ_PREFIX, {t65, t8}); slv.assertFormula({t77}); - slv.checkEntailed({1, t128}); + slv.checkSatAssuming(t128.notTerm()); } TEST_F(TestTheoryBlackArithNl, cvc5Projects455) @@ -139,7 +139,7 @@ TEST_F(TestTheoryBlackArithNl, cvc5Projects455) Term t36 = slv.mkTerm(Kind::NOT, {t35}); slv.assertFormula({t36}); slv.assertFormula({t33}); - slv.checkEntailed({t18}); + slv.checkSatAssuming({t18.notTerm()}); } } // namespace test diff --git a/test/unit/api/cpp/theory_uf_ho_black.cpp b/test/unit/api/cpp/theory_uf_ho_black.cpp index 03eb4304a..c672b12aa 100644 --- a/test/unit/api/cpp/theory_uf_ho_black.cpp +++ b/test/unit/api/cpp/theory_uf_ho_black.cpp @@ -13,8 +13,8 @@ * Blackbox tests using the API targeting UF + higher-order. */ -#include "test_api.h" #include "base/configuration.h" +#include "test_api.h" namespace cvc5 { diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 0867ad6b5..74e4e1ceb 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -274,23 +274,6 @@ class DatatypeTest assertNotEquals(pairIntInt, pairIntReal); assertNotEquals(pairIntInt, pairRealInt); assertNotEquals(pairIntReal, pairRealInt); - - assertTrue(pairRealReal.isSubsortOf(pairRealReal)); - assertFalse(pairIntReal.isSubsortOf(pairRealReal)); - assertFalse(pairRealInt.isSubsortOf(pairRealReal)); - assertFalse(pairIntInt.isSubsortOf(pairRealReal)); - assertFalse(pairRealReal.isSubsortOf(pairRealInt)); - assertFalse(pairIntReal.isSubsortOf(pairRealInt)); - assertTrue(pairRealInt.isSubsortOf(pairRealInt)); - assertFalse(pairIntInt.isSubsortOf(pairRealInt)); - assertFalse(pairRealReal.isSubsortOf(pairIntReal)); - assertTrue(pairIntReal.isSubsortOf(pairIntReal)); - assertFalse(pairRealInt.isSubsortOf(pairIntReal)); - assertFalse(pairIntInt.isSubsortOf(pairIntReal)); - assertFalse(pairRealReal.isSubsortOf(pairIntInt)); - assertFalse(pairIntReal.isSubsortOf(pairIntInt)); - assertFalse(pairRealInt.isSubsortOf(pairIntInt)); - assertTrue(pairIntInt.isSubsortOf(pairIntInt)); } @Test void datatypeIsFinite() throws CVC5ApiException diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index 96266bce9..5f149dd8a 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -43,9 +43,6 @@ class ResultTest assertFalse(res_null.isSat()); assertFalse(res_null.isUnsat()); assertFalse(res_null.isSatUnknown()); - assertFalse(res_null.isEntailed()); - assertFalse(res_null.isNotEntailed()); - assertFalse(res_null.isEntailmentUnknown()); Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); @@ -98,35 +95,4 @@ class ResultTest assertFalse(res.isSat()); assertTrue(res.isSatUnknown()); } - - @Test void isEntailed() - { - d_solver.setOption("incremental", "true"); - Sort u_sort = d_solver.mkUninterpretedSort("u"); - 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); - assertTrue(entailed.isEntailed()); - assertFalse(entailed.isEntailmentUnknown()); - Result not_entailed = d_solver.checkEntailed(b); - assertTrue(not_entailed.isNotEntailed()); - assertFalse(not_entailed.isEntailmentUnknown()); - } - - @Test void isEntailmentUnknown() throws CVC5ApiException - { - d_solver.setLogic("QF_NIA"); - d_solver.setOption("incremental", "false"); - d_solver.setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver.getIntegerSort(); - Term x = d_solver.mkConst(int_sort, "x"); - d_solver.assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver.checkEntailed(x.eqTerm(x)); - assertFalse(res.isEntailed()); - assertTrue(res.isEntailmentUnknown()); - assertEquals(res.getUnknownExplanation(), Result.UnknownExplanation.UNKNOWN_REASON); - } } diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index f4b3f7f91..ba93ed102 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -2242,83 +2242,6 @@ class SolverTest slv.close(); } - @Test void checkEntailed() - { - d_solver.setOption("incremental", "false"); - assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue())); - assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.mkTrue())); - Solver slv = new Solver(); - assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue())); - slv.close(); - } - - @Test void checkEntailed1() - { - 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"); - assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue())); - assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.getNullTerm())); - assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue())); - assertDoesNotThrow(() -> d_solver.checkEntailed(z)); - Solver slv = new Solver(); - assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue())); - slv.close(); - } - - @Test void checkEntailed2() - { - d_solver.setOption("incremental", "true"); - - Sort uSort = d_solver.mkUninterpretedSort("u"); - Sort intSort = d_solver.getIntegerSort(); - Sort boolSort = d_solver.getBooleanSort(); - Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort); - Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort); - - Term n = d_solver.getNullTerm(); - // Constants - Term x = d_solver.mkConst(uSort, "x"); - Term y = d_solver.mkConst(uSort, "y"); - // Functions - Term f = d_solver.mkConst(uToIntSort, "f"); - Term p = d_solver.mkConst(intPredSort, "p"); - // Values - Term zero = d_solver.mkInteger(0); - Term one = d_solver.mkInteger(1); - // Terms - Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(ADD, f_x, f_y); - Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); - Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); - // Assertions - Term assertions = d_solver.mkTerm(AND, - new Term[] { - d_solver.mkTerm(LEQ, zero, f_x), // 0 <= f(x) - d_solver.mkTerm(LEQ, zero, f_y), // 0 <= f(y) - d_solver.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notTerm(), // not p(0) - p_f_y // p(f(y)) - }); - - assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue())); - d_solver.assertFormula(assertions); - assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y))); - assertDoesNotThrow(() - -> d_solver.checkEntailed( - new Term[] {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)})); - assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(n)); - assertThrows(CVC5ApiException.class, - () -> d_solver.checkEntailed(new Term[] {n, d_solver.mkTerm(DISTINCT, x, y)})); - - Solver slv = new Solver(); - assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue())); - slv.close(); - } - @Test void checkSat() throws CVC5ApiException { d_solver.setOption("incremental", "false"); diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 3022af024..37e62e5bd 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -262,28 +262,6 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isFirstClass()); } - @Test void isFunctionLike() throws CVC5ApiException - { - Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort()); - assertFalse(d_solver.getIntegerSort().isFunctionLike()); - assertTrue(fun_sort.isFunctionLike()); - - Sort dt_sort = create_datatype_sort(); - Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt.getConstructor(0).getSelector(1).getSelectorTerm().getSort(); - assertTrue(cons_sort.isFunctionLike()); - - assertDoesNotThrow(() -> d_solver.getNullSort().isFunctionLike()); - } - - @Test void isSubsortOf() - { - assertTrue(d_solver.getIntegerSort().isSubsortOf(d_solver.getIntegerSort())); - assertTrue(d_solver.getIntegerSort().isSubsortOf(d_solver.getRealSort())); - assertFalse(d_solver.getIntegerSort().isSubsortOf(d_solver.getBooleanSort())); - assertDoesNotThrow(() -> d_solver.getNullSort().isSubsortOf(d_solver.getNullSort())); - } - @Test void getDatatype() throws CVC5ApiException { Sort dtypeSort = create_datatype_sort(); @@ -430,9 +408,9 @@ class SortTest @Test void getUninterpretedSortName() throws CVC5ApiException { Sort uSort = d_solver.mkUninterpretedSort("u"); - assertDoesNotThrow(() -> uSort.getUninterpretedSortName()); + assertDoesNotThrow(() -> uSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); - assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortName()); + assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); } @Test void isUninterpretedSortParameterized() throws CVC5ApiException @@ -460,9 +438,9 @@ class SortTest @Test void getUninterpretedSortConstructorName() throws CVC5ApiException { Sort sSort = d_solver.mkSortConstructorSort("s", 2); - assertDoesNotThrow(() -> sSort.getSortConstructorName()); + assertDoesNotThrow(() -> sSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); - assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorName()); + assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); } @Test void getUninterpretedSortConstructorArity() throws CVC5ApiException @@ -567,23 +545,6 @@ class SortTest == (intSort.compareTo(bvSort) >= 0)); } - @Test void sortSubtyping() - { - Sort intSort = d_solver.getIntegerSort(); - Sort realSort = d_solver.getRealSort(); - assertTrue(intSort.isSubsortOf(realSort)); - assertFalse(realSort.isSubsortOf(intSort)); - - Sort arraySortII = d_solver.mkArraySort(intSort, intSort); - Sort arraySortIR = d_solver.mkArraySort(intSort, realSort); - - Sort setSortI = d_solver.mkSetSort(intSort); - Sort setSortR = d_solver.mkSetSort(realSort); - // we don't support subtyping for sets - assertFalse(setSortI.isSubsortOf(setSortR)); - assertFalse(setSortR.isSubsortOf(setSortI)); - } - @Test void sortScopedToString() throws CVC5ApiException { String name = "uninterp-sort"; diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index efd67ab29..89b307bf7 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -300,23 +300,6 @@ def test_parametric_datatype(solver): assert pairIntInt != pairRealInt assert pairIntReal != pairRealInt - assert pairRealReal.isSubsortOf(pairRealReal) - assert not pairIntReal.isSubsortOf(pairRealReal) - assert not pairRealInt.isSubsortOf(pairRealReal) - assert not pairIntInt.isSubsortOf(pairRealReal) - assert not pairRealReal.isSubsortOf(pairRealInt) - assert not pairIntReal.isSubsortOf(pairRealInt) - assert pairRealInt.isSubsortOf(pairRealInt) - assert not pairIntInt.isSubsortOf(pairRealInt) - assert not pairRealReal.isSubsortOf(pairIntReal) - assert pairIntReal.isSubsortOf(pairIntReal) - assert not pairRealInt.isSubsortOf(pairIntReal) - assert not pairIntInt.isSubsortOf(pairIntReal) - assert not pairRealReal.isSubsortOf(pairIntInt) - assert not pairIntReal.isSubsortOf(pairIntInt) - assert not pairRealInt.isSubsortOf(pairIntInt) - assert pairIntInt.isSubsortOf(pairIntInt) - def test_is_finite(solver): dtypedecl = solver.mkDatatypeDecl("dt", []) ctordecl = solver.mkDatatypeConstructorDecl("cons") diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index 247451756..86f2ab8a7 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -32,9 +32,6 @@ def test_is_null(solver): assert not res_null.isSat() assert not res_null.isUnsat() assert not res_null.isSatUnknown() - assert not res_null.isEntailed() - assert not res_null.isNotEntailed() - assert not res_null.isEntailmentUnknown() u_sort = solver.mkUninterpretedSort("u") x = solver.mkConst(u_sort, "x") solver.assertFormula(x.eqTerm(x)) @@ -81,34 +78,3 @@ def test_is_sat_unknown(solver): res = solver.checkSat() assert not res.isSat() assert res.isSatUnknown() - - -def test_is_entailed(solver): - solver.setOption("incremental", "true") - u_sort = solver.mkUninterpretedSort("u") - x = solver.mkConst(u_sort, "x") - y = solver.mkConst(u_sort, "y") - a = x.eqTerm(y).notTerm() - b = x.eqTerm(y) - solver.assertFormula(a) - entailed = solver.checkEntailed(a) - assert entailed.isEntailed() - assert not entailed.isEntailmentUnknown() - not_entailed = solver.checkEntailed(b) - assert not_entailed.isNotEntailed() - assert not not_entailed.isEntailmentUnknown() - - -def test_is_entailment_unknown(solver): - solver.setLogic("QF_NIA") - solver.setOption("incremental", "false") - solver.setOption("solve-int-as-bv", "32") - int_sort = solver.getIntegerSort() - x = solver.mkConst(int_sort, "x") - solver.assertFormula(x.eqTerm(x).notTerm()) - res = solver.checkEntailed(x.eqTerm(x)) - assert not res.isEntailed() - assert res.isEntailmentUnknown() - print(type(cvc5.RoundTowardZero)) - print(type(cvc5.UnknownReason)) - assert res.getUnknownExplanation() == cvc5.UnknownReason diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 5125b2e00..aca628d28 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -1687,81 +1687,6 @@ def test_assert_formula(solver): slv.assertFormula(solver.mkTrue()) -def test_check_entailed(solver): - solver.setOption("incremental", "false") - solver.checkEntailed(solver.mkTrue()) - with pytest.raises(RuntimeError): - solver.checkEntailed(solver.mkTrue()) - slv = cvc5.Solver() - with pytest.raises(RuntimeError): - slv.checkEntailed(solver.mkTrue()) - - -def test_check_entailed1(solver): - boolSort = solver.getBooleanSort() - x = solver.mkConst(boolSort, "x") - y = solver.mkConst(boolSort, "y") - z = solver.mkTerm(Kind.And, x, y) - solver.setOption("incremental", "true") - solver.checkEntailed(solver.mkTrue()) - with pytest.raises(RuntimeError): - solver.checkEntailed(cvc5.Term(solver)) - solver.checkEntailed(solver.mkTrue()) - solver.checkEntailed(z) - slv = cvc5.Solver() - with pytest.raises(RuntimeError): - slv.checkEntailed(solver.mkTrue()) - - -def test_check_entailed2(solver): - solver.setOption("incremental", "true") - - uSort = solver.mkUninterpretedSort("u") - intSort = solver.getIntegerSort() - boolSort = solver.getBooleanSort() - uToIntSort = solver.mkFunctionSort(uSort, intSort) - intPredSort = solver.mkFunctionSort(intSort, boolSort) - - n = cvc5.Term(solver) - # Constants - x = solver.mkConst(uSort, "x") - y = solver.mkConst(uSort, "y") - # Functions - f = solver.mkConst(uToIntSort, "f") - p = solver.mkConst(intPredSort, "p") - # Values - zero = solver.mkInteger(0) - one = solver.mkInteger(1) - # Terms - f_x = solver.mkTerm(Kind.ApplyUf, f, x) - f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Add, f_x, f_y) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) - p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) - # Assertions - assertions =\ - solver.mkTerm(Kind.And,\ - [solver.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x) - solver.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y) - solver.mkTerm(Kind.Leq, summ, one), # f(x) + f(y) <= 1 - p_0.notTerm(), # not p(0) - p_f_y # p(f(y)) - ]) - - solver.checkEntailed(solver.mkTrue()) - solver.assertFormula(assertions) - solver.checkEntailed(solver.mkTerm(Kind.Distinct, x, y)) - solver.checkEntailed(\ - [solver.mkFalse(), solver.mkTerm(Kind.Distinct, x, y)]) - with pytest.raises(RuntimeError): - solver.checkEntailed(n) - with pytest.raises(RuntimeError): - solver.checkEntailed([n, solver.mkTerm(Kind.Distinct, x, y)]) - slv = cvc5.Solver() - with pytest.raises(RuntimeError): - slv.checkEntailed(solver.mkTrue()) - - def test_check_sat(solver): solver.setOption("incremental", "false") solver.checkSat() @@ -2440,9 +2365,10 @@ def test_issue7000(solver): t59 = solver.mkConst(s2, "_x51") t72 = solver.mkTerm(Kind.Equal, t37, t59) t74 = solver.mkTerm(Kind.Gt, t4, t7) + query = solver.mkTerm(Kind.And, t72, t74, t72, t72) # throws logic exception since logic is not higher order by default with pytest.raises(RuntimeError): - solver.checkEntailed(t72, t74, t72, t72) + solver.checkSatAssuming(query.notTerm()) def test_mk_sygus_var(solver): diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 6214a58a1..1a71461b5 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -243,27 +243,6 @@ def test_is_first_class(solver): Sort(solver).isFirstClass() -def test_is_function_like(solver): - fun_sort = solver.mkFunctionSort(solver.getRealSort(), - solver.getIntegerSort()) - assert not solver.getIntegerSort().isFunctionLike() - assert fun_sort.isFunctionLike() - - dt_sort = create_datatype_sort(solver) - dt = dt_sort.getDatatype() - cons_sort = dt[0][1].getSelectorTerm().getSort() - assert cons_sort.isFunctionLike() - - Sort(solver).isFunctionLike() - - -def test_is_subsort_of(solver): - assert solver.getIntegerSort().isSubsortOf(solver.getIntegerSort()) - assert solver.getIntegerSort().isSubsortOf(solver.getRealSort()) - assert not solver.getIntegerSort().isSubsortOf(solver.getBooleanSort()) - Sort(solver).isSubsortOf(Sort(solver)) - - def test_get_datatype(solver): dtypeSort = create_datatype_sort(solver) dtypeSort.getDatatype() @@ -415,10 +394,10 @@ def test_get_sequence_element_sort(solver): def test_get_uninterpreted_sort_name(solver): uSort = solver.mkUninterpretedSort("u") - uSort.getUninterpretedSortName() + uSort.getSymbol() bvSort = solver.mkBitVectorSort(32) with pytest.raises(RuntimeError): - bvSort.getUninterpretedSortName() + bvSort.getSymbol() def test_is_uninterpreted_sort_parameterized(solver): @@ -445,10 +424,10 @@ def test_get_uninterpreted_sort_paramsorts(solver): def test_get_uninterpreted_sort_constructor_name(solver): sSort = solver.mkSortConstructorSort("s", 2) - sSort.getSortConstructorName() + sSort.getSymbol() bvSort = solver.mkBitVectorSort(32) with pytest.raises(RuntimeError): - bvSort.getSortConstructorName() + bvSort.getSymbol() def test_get_uninterpreted_sort_constructor_arity(solver): @@ -553,22 +532,6 @@ def test_sort_compare(solver): assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort) -def test_sort_subtyping(solver): - intSort = solver.getIntegerSort() - realSort = solver.getRealSort() - assert intSort.isSubsortOf(realSort) - assert not realSort.isSubsortOf(intSort) - - arraySortII = solver.mkArraySort(intSort, intSort) - arraySortIR = solver.mkArraySort(intSort, realSort) - - setSortI = solver.mkSetSort(intSort) - setSortR = solver.mkSetSort(realSort) - # we don't support subtyping for sets - assert not setSortI.isSubsortOf(setSortR) - assert not setSortR.isSubsortOf(setSortI) - - def test_sort_scoped_tostring(solver): name = "uninterp-sort" bvsort8 = solver.mkBitVectorSort(8) diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index d1c195c4f..69de847ca 100644 --- a/test/unit/api/python/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py @@ -52,7 +52,7 @@ def testGetBV(): def testGetArray(): solver = cvc5.Solver() - arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) + arrsort = solver.mkArraySort(solver.getIntegerSort(), solver.getIntegerSort()) zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) stores = solver.mkTerm(Kind.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) stores = solver.mkTerm(Kind.Store, stores, solver.mkInteger(2), solver.mkInteger(3))