Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
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()));
}
}
}
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();
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<Term> 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);
<< 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;
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;
}
{
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;
}
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;
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
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.
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();
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);
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");
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()));
}
}
}
{
Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!");
- System.out.println(helloworld + " is " + slv.checkEntailed(helloworld));
+ System.out.println(
+ helloworld + " is " + slv.checkSatAssuming(helloworld));
}
}
}
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();
System.out.println("Thus the maximum value of (y - x) is 2/3.");
}
}
-}
\ No newline at end of file
+}
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
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.
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()
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)
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")
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()))
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))
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()
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
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.
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;
}
&& 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;
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;
/* 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;
/* 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;
Sort Solver::mkTupleSort(const std::vector<Sort>& 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);
////////
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
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<Term>& 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 */
/* -------------------------------------------------------------------------- */
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
<< "'";
CVC5_API_TRY_CATCH_END;
}
-void Solver::echo(std::ostream& out, const std::string& str) const
-{
- out << str;
-}
-
std::vector<Term> Solver::getAssertions(void) const
{
CVC5_API_TRY_CATCH_BEGIN;
*/
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
*/
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
*/
/* Sort constructor sort ----------------------------------------------- */
- /**
- * @return the name of a sort constructor sort
- */
- std::string getSortConstructorName() const;
-
/**
* @return the arity of a sort constructor sort
*/
*/
Result checkSatAssuming(const std::vector<Term>& 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<Term>& terms) const;
-
/**
* Create datatype sort.
*
const std::vector<Term>& terms,
bool global = false) const;
- /**
- * Echo a given string to the given output stream.
- *
- * SMT-LIB:
- *
- * \verbatim embed:rst:leading-asterisk
- * .. code:: smtlib
- *
- * (echo <string>)
- * \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.
*
* 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 <lbl-option-model-cores>` \endverbatim
- * has been set.
+ * \verbatim embed:rst:inline :ref:`model-cores <lbl-option-model-cores>`
+ * \endverbatim has been set.
*
* @param v The term in question
* @return true if v is a model core symbol
} \
} 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
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
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:
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
*/
/* 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
*/
/* 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
*/
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
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<Solver*>(pointer);
- Term* term = reinterpret_cast<Term*>(termPointer);
- Result* retPointer = new Result(solver->checkEntailed(*term));
- return reinterpret_cast<jlong>(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<Solver*>(pointer);
- std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms);
- Result* retPointer = new Result(solver->checkEntailed(terms));
- return reinterpret_cast<jlong>(retPointer);
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
/*
* Class: io_github_cvc5_api_Solver
* Method: declareDatatype
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Sort*>(pointer);
- return static_cast<jboolean>(current->isFunctionLike());
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Sort*>(pointer);
- Sort* sort = reinterpret_cast<Sort*>(sortPointer);
- return static_cast<jboolean>(current->isSubsortOf(*sort));
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
/*
* Class: io_github_cvc5_api_Sort
* Method: getDatatype
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<Sort*>(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
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<Sort*>(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
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 +
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 +
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 +
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 +
"""
return self.cr.isSatUnknown()
- def isEntailed(self):
- """
- :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query.
- """
- return self.cr.isEntailed()
-
- def isNotEntailed(self):
- """
- :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query that is not entailed.
- """
- return self.cr.isNotEntailed()
-
- def isEntailmentUnknown(self):
- """
- :return: True if query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::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.
r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> 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((<Term?> a).cterm)
- r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v)
- return r
-
@expand_list_arg(num_req_args=1)
def declareDatatype(self, str symbol, *ctors):
"""
"""
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
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
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
{
d_result = res = csa->getResult();
}
- const QueryCommand* q = dynamic_cast<const QueryCommand*>(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) {
}
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());
}
d_assertions.getIteSkolemMap().clear();
}
-void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
- bool isEntailmentCheck)
+void Assertions::initializeCheckSat(const std::vector<Node>& 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)
* 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<Node>& assumptions,
- bool isEntailmentCheck);
+ void initializeCheckSat(const std::vector<Node>& assumptions);
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
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 */
/* -------------------------------------------------------------------------- */
return (res.isSat()
|| (res.isSatUnknown()
&& res.getUnknownExplanation() == api::Result::INCOMPLETE))
- || res.isUnsat() || res.isEntailed();
+ || res.isUnsat();
}
void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
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<Node>{ne}, true);
+ Result r =
+ d_smtSolver.checkSatisfiability(as, std::vector<Node>{ne.notNode()});
Trace("smt-qe") << "Query returned " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
{
}
Result SmtSolver::checkSatisfiability(Assertions& as,
- const std::vector<Node>& assumptions,
- bool isEntailmentCheck)
+ const std::vector<Node>& assumptions)
{
Result result;
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
* 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<Node>& assumptions,
- bool isEntailmentCheck);
+ const std::vector<Node>& 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
{
assump.push_back(assumption);
}
- return checkSatInternal(assump, false);
+ return checkSatInternal(assump);
}
Result SolverEngine::checkSat(const std::vector<Node>& 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<Node>() : std::vector<Node>{node},
- true)
- .asEntailmentResult();
-}
-
-Result SolverEngine::checkEntailed(const std::vector<Node>& nodes)
-{
- ensureWellFormedTerms(nodes, "checkEntailed");
- return checkSatInternal(nodes, true).asEntailmentResult();
-}
-
-Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
- bool isEntailmentCheck)
+Result SolverEngine::checkSatInternal(const std::vector<Node>& 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)
*/
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. */
*/
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;
*/
std::vector<Node> reduceUnsatCore(const std::vector<Node>& 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<Node>& assumptions);
-
/**
* Assert a formula (if provided) to the current context and call
* check(). Returns SAT, UNSAT, or SAT_UNKNOWN result.
/*
* Check satisfiability (used to check satisfiability and entailment).
*/
- Result checkSatInternal(const std::vector<Node>& assumptions,
- bool isEntailmentCheck);
+ Result checkSatInternal(const std::vector<Node>& assumptions);
/**
* Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
{
std::vector<Node> 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
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;
}
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;
}
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());
}
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());
}
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;
}
import cvc5
slv = cvc5.Solver()
-r = slv.checkEntailed(slv.mkBoolean(True))
-r.isEntailed()
+r = slv.checkSatAssuming(slv.mkBoolean(False))
+r.isUnsat()
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())
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()
; EXIT: 0
(set-logic QF_LRA)
-(define-fun x () Real (+ 4 1))
+(define-fun x () Real (+ 4.0 1.0))
% 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)
% 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)
% 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)
% 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)
% 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)
% 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)
% 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)
% states that all reals are not rational (countersatisfiable)
-% Status : CounterSatisfiable
+% Status : Satisfiable
%------------------------------------------------------------------------------
tff(the,conjecture,(
! [X: $real] :
% 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)
% 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 )).
% 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 )).
-% Status: Theorem
+% Status: Unsatisfiable
%--------------------------------------------------------------------------
% COMMAND-LINE: --finite-model-find
-% Status: CounterSatisfiable
+% Status: Satisfiable
%--------------------------------------------------------------------------
(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))
(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))
% 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.
% 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)
% 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)).
% 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.
% 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.
% 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.
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)
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));
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
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<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))
- });
-
- 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");
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)
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);
}
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)
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();
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)
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)
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";
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)
Term t36 = slv.mkTerm(Kind::NOT, {t35});
slv.assertFormula({t36});
slv.assertFormula({t33});
- slv.checkEntailed({t18});
+ slv.checkSatAssuming({t18.notTerm()});
}
} // namespace test
* Blackbox tests using the API targeting UF + higher-order.
*/
-#include "test_api.h"
#include "base/configuration.h"
+#include "test_api.h"
namespace cvc5 {
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
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));
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);
- }
}
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");
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();
@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
@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
== (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";
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")
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))
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
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()
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):
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()
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):
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):
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)
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))
projects / cvc5.git / commitdiff