new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
impExpr(new Expr(twox_plus_y_geq_3));
- System.out.println("Checking validity of formula " + formula + " with CVC4.");
- System.out.println("CVC4 should report VALID.");
- System.out.println("Result from CVC4 is: " + smt.query(formula));
+ System.out.println(
+ "Checking entailment of formula " + formula + " with CVC4.");
+ System.out.println("CVC4 should report ENTAILED.");
+ System.out.println("Result from CVC4 is: " + smt.checkEntailed(formula));
}
}
let bformula = new_Expr(formula) in
-print_string "Checking validity of formula " ;
+print_string "Checking entailment of formula " ;
print_string (get_string (formula->toString ())) ;
print_string " with CVC4." ;
print_newline () ;
-print_string "CVC4 should report VALID." ;
+print_string "CVC4 should report ENTAILED." ;
print_newline () ;
print_string "Result from CVC4 is: " ;
-print_string (get_string (smt->query(bformula)->toString ())) ;
+print_string (get_string (smt->checkEntailed(bformula)->toString ())) ;
print_newline ()
;;
my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
-print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
-print "CVC4 should report VALID.\n";
-print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n";
+print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n";
+print "CVC4 should report ENTAILED.\n";
+print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n";
my $formula = new CVC4::Expr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::Expr($twox_plus_y_geq_3));
-print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
-print "CVC4 should report VALID.\n";
-print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n";
+print "Checking entailment of formula " . $formula->toString() . " with CVC4.\n";
+print "CVC4 should report ENTAILED.\n";
+print "Result from CVC4 is: " . $smt->checkEntailed($formula)->toString() . "\n";
formula = Expr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(Expr(twox_plus_y_geq_3))
- print("Checking validity of formula " + formula.toString() + " with CVC4.")
- print("CVC4 should report VALID.")
- print("Result from CVC4 is: " + smt.query(formula).toString())
+ print("Checking entailment of formula " + formula.toString() + " with CVC4.")
+ print("CVC4 should report ENTAILED .")
+ print("Result from CVC4 is: " + smt.checkEntailed(formula).toString())
return 0
formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3))
-puts "Checking validity of formula " + formula.toString + " with CVC4."
-puts "CVC4 should report VALID."
-puts "Result from CVC4 is: " + smt.query(formula).toString
+puts "Checking entailment of formula " + formula.toString + " with CVC4."
+puts "CVC4 should report ENTAILED."
+puts "Result from CVC4 is: " + smt.checkEntailed(formula).toString
exit
set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]]
-puts "Checking validity of formula [Expr_toString $formula] with CVC4."
-puts "CVC4 should report VALID."
-puts "Result from CVC4 is: [Result_toString [SmtEngine_query smt $formula]]"
+puts "Checking entailment of formula [Expr_toString $formula] with CVC4."
+puts "CVC4 should report ENTAILED."
+puts "Result from CVC4 is: [Result_toString [SmtEngine_checkEntailed smt $formula]]"
slv.assertFormula(assignment1);
Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_);
- cout << " Check validity assuming: " << new_x_eq_new_x_ << endl;
- cout << " Expect valid. " << endl;
- cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl;
+ cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl;
+ cout << " Expect ENTAILED. " << endl;
+ cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
cout << " Popping context. " << endl;
slv.pop();
cout << "Asserting " << assignment2 << " to CVC4 " << endl;
slv.assertFormula(assignment2);
- cout << " Check validity assuming: " << new_x_eq_new_x_ << endl;
- cout << " Expect valid. " << endl;
- cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl;
+ cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl;
+ cout << " Expect ENTAILED. " << endl;
+ cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl;
Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm();
std::vector<Term> v{new_x_eq_new_x_, x_neq_x};
- cout << " Check Validity Assuming: " << v << endl;
- cout << " Expect invalid. " << endl;
- cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
+ cout << " Check entailment assuming: " << v << endl;
+ cout << " Expect NOT_ENTAILED. " << endl;
+ cout << " CVC4: " << slv.checkEntailed(v) << endl;
// Assert that a is odd
Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
Expr new_x_eq_new_x_ = em.mkExpr(kind::EQUAL, new_x, new_x_);
cout << " Querying: " << new_x_eq_new_x_ << endl;
- cout << " Expect valid. " << endl;
- cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
+ cout << " Expect entailed. " << endl;
+ cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl;
cout << " Popping context. " << endl;
smt.pop();
smt.assertFormula(assignment2);
cout << " Querying: " << new_x_eq_new_x_ << endl;
- cout << " Expect valid. " << endl;
- cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
+ cout << " Expect ENTAILED. " << endl;
+ cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl;
Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr();
std::vector<Expr> v{new_x_eq_new_x_, x_neq_x};
cout << " Querying: " << v << endl;
- cout << " Expect invalid. " << endl;
- cout << " CVC4: " << smt.query(v) << endl;
+ cout << " Expect NOT_ENTAILED. " << endl;
+ cout << " CVC4: " << smt.checkEntailed(v) << endl;
// Assert that a is odd
Expr extract_op = em.mkConst(BitVectorExtract(0, 0));
cout << "Given the following assertions:" << endl
<< assertions << endl << endl;
- cout << "Prove x /= y is valid. " << endl
- << "CVC4: " << slv.checkValidAssuming(slv.mkTerm(DISTINCT, x, y))
- << "." << endl << endl;
+ cout << "Prove x /= y is entailed. " << endl
+ << "CVC4: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "."
+ << endl
+ << endl;
cout << "Call checkSat to show that the assertions are satisfiable. "
<< endl
cout << "Given the following assumptions:" << endl
<< assumptions << endl
- << "Prove x /= y is valid. "
- << "CVC4 says: " << smt.query(em.mkExpr(kind::DISTINCT, x, y))
+ << "Prove x /= y is entailed. "
+ << "CVC4 says: " << smt.checkEntailed(em.mkExpr(kind::DISTINCT, x, y))
<< "." << endl;
cout << "Now we call checksat on a trivial query to show that" << endl
slv.assertFormula(eq);
Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0);
- cout << " Check validity assuming: " << eq2 << endl;
- cout << " Expect valid. " << endl;
- cout << " CVC4: " << slv.checkValidAssuming(eq2) << endl;
+ cout << " Check entailment assuming: " << eq2 << endl;
+ cout << " Expect ENTAILED. " << endl;
+ cout << " CVC4: " << slv.checkEntailed(eq2) << endl;
return 0;
}
Expr eq2 = em.mkExpr(kind::EQUAL, x_31_31, x_0_0);
cout << " Querying: " << eq2 << endl;
- cout << " Expect valid. " << endl;
- cout << " CVC4: " << smt.query(eq2) << endl;
+ cout << " Expect entailed. " << endl;
+ cout << " CVC4: " << smt.checkEntailed(eq2) << endl;
return 0;
}
{
Solver slv;
Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
- std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld)
+ std::cout << helloworld << " is " << slv.checkEntailed(helloworld)
<< std::endl;
return 0;
}
ExprManager em;
Expr helloworld = em.mkVar("Hello World!", em.booleanType());
SmtEngine smt(&em);
- std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;
+ std::cout << helloworld << " is " << smt.checkEntailed(helloworld)
+ << std::endl;
return 0;
}
Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_);
System.out.println(" Querying: " + new_x_eq_new_x_);
- System.out.println(" Expect valid. ");
- System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_));
+ System.out.println(" Expect entailed. ");
+ System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_));
System.out.println(" Popping context. ");
smt.pop();
smt.assertFormula(assignment2);
System.out.println(" Querying: " + new_x_eq_new_x_);
- System.out.println(" Expect valid. ");
- System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_));
+ System.out.println(" Expect entailed. ");
+ System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_));
}
}
System.out.println("Given the following assumptions:");
System.out.println(assumptions);
- System.out.println("Prove x /= y is valid. " +
- "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) +
- ".");
-
+ System.out.println("Prove x /= y is entailed. "
+ + "CVC4 says: " + smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y))
+ + ".");
System.out.println("Now we call checksat on a trivial query to show that");
System.out.println("the assumptions are satisfiable: " +
Expr helloworld = em.mkVar("Hello World!", em.booleanType());
SmtEngine smt = new SmtEngine(em);
- System.out.println(helloworld + " is " + smt.query(helloworld));
+ System.out.println(helloworld + " is " + smt.checkEntailed(helloworld));
}
}
smt.push();
Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds);
System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4.");
- System.out.println("CVC4 should report VALID.");
- System.out.println("Result from CVC4 is: " + smt.query(diff_leq_two_thirds));
+ System.out.println("CVC4 should report ENTAILED.");
+ System.out.println(
+ "Result from CVC4 is: " + smt.checkEntailed(diff_leq_two_thirds));
smt.pop();
System.out.println();
slv.push();
Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds);
cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl;
- cout << "CVC4 should report VALID." << endl;
- cout << "Result from CVC4 is: "
- << slv.checkValidAssuming(diff_leq_two_thirds) << endl;
+ cout << "CVC4 should report ENTAILED." << endl;
+ cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds)
+ << endl;
slv.pop();
cout << endl;
smt.push();
Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds);
cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl;
- cout << "CVC4 should report VALID." << endl;
- cout << "Result from CVC4 is: " << smt.query(diff_leq_two_thirds) << endl;
+ cout << "CVC4 should report ENTAILED." << endl;
+ cout << "Result from CVC4 is: " << smt.checkEntailed(diff_leq_two_thirds)
+ << endl;
smt.pop();
cout << endl;
#! \file bitvectors.py
## \verbatim
## Top contributors (to current version):
- ## Makai Mann
+ ## Makai Mann, Aina Niemetz
## This file is part of the CVC4 project.
## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
slv.assertFormula(assignment1)
new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_)
- print("Checking validity assuming:", new_x_eq_new_x_)
- print("Expect valid.")
- print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_))
+ print("Checking entailment assuming:", new_x_eq_new_x_)
+ print("Expect ENTAILED.")
+ print("CVC4:", slv.checkEntailment(new_x_eq_new_x_))
print("Popping context.")
slv.pop()
print("Asserting {} to CVC4".format(assignment2))
slv.assertFormula(assignment2)
- print("Checking validity assuming:", new_x_eq_new_x_)
- print("Expect valid.")
- print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_))
+ print("Checking entailment assuming:", new_x_eq_new_x_)
+ print("Expect ENTAILED.")
+ print("CVC4:", slv.checkEntailed(new_x_eq_new_x_))
x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm()
v = [new_x_eq_new_x_, x_neq_x]
- print("Check Validity Assuming: ", v)
- print("Expect invalid.")
- print("CVC4:", slv.checkValidAssuming(v))
+ print("Check entailment assuming: ", v)
+ print("Expect NOT_ENTAILED.")
+ print("CVC4:", slv.checkEntailed(v))
# Assert that a is odd
extract_op = slv.mkOp(kinds.BVExtract, 0, 0)
#! \file combination.py
## \verbatim
## Top contributors (to current version):
- ## Makai Mann
+ ## Makai Mann, Aina Niemetz
## This file is part of the CVC4 project.
## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
slv.assertFormula(assertions)
print("Given the following assertions:", assertions, "\n")
- print("Prove x /= y is valid.\nCVC4: ",
- slv.checkValidAssuming(slv.mkTerm(kinds.Distinct, x, y)), "\n")
+ print("Prove x /= y is entailed.\nCVC4: ",
+ slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n")
print("Call checkSat to show that the assertions are satisfiable")
print("CVC4:", slv.checkSat(), "\n")
#! \file extract.py
## \verbatim
## Top contributors (to current version):
- ## Makai Mann
+ ## Makai Mann, Aina Niemetz
## This file is part of the CVC4 project.
## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
slv.assertFormula(eq)
eq2 = slv.mkTerm(Equal, x_31_31, x_0_0)
- print("Check validity assuming:", eq2)
- print("Expect valid")
- print("CVC4:", slv.checkValidAssuming(eq2))
+ print("Check entailment assuming:", eq2)
+ print("Expect ENTAILED")
+ print("CVC4:", slv.checkEntailed(eq2))
#! \file helloworld.py
## \verbatim
## Top contributors (to current version):
-## Makai Mann
+## Makai Mann, Aina Niemetz
## This file is part of the CVC4 project.
## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
if __name__ == "__main__":
slv = pycvc4.Solver()
helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!")
- print(helloworld, "is", slv.checkValidAssuming(helloworld))
+ print(helloworld, "is", slv.checkEntailed(helloworld))
#! \file linear_arith.py
## \verbatim
## Top contributors (to current version):
-## Makai Mann
+## Makai Mann, Aina Niemetz
## This file is part of the CVC4 project.
## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
slv.push()
diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds)
print("Prove that", diff_leq_two_thirds, "with CVC4")
- print("CVC4 should report VALID")
+ print("CVC4 should report ENTAILED")
print("Result from CVC4 is:",
- slv.checkValidAssuming(diff_leq_two_thirds))
+ slv.checkEntailed(diff_leq_two_thirds))
slv.pop()
print()
#! \file sets.py
## \verbatim
## Top contributors (to current version):
-## Makai Mann
+## Makai Mann, Aina Niemetz
## This file is part of the CVC4 project.
## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
theorem = slv.mkTerm(kinds.Equal, lhs, rhs)
print("CVC4 reports: {} is {}".format(theorem,
- slv.checkValidAssuming(theorem)))
+ slv.checkEntailed(theorem)))
# Verify emptset is a subset of any set
theorem = slv.mkTerm(kinds.Subset, emptyset, A)
print("CVC4 reports: {} is {}".format(theorem,
- slv.checkValidAssuming(theorem)))
+ slv.checkEntailed(theorem)))
# Find me an element in 1, 2 intersection 2, 3, if there is one.
Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
- cout << "CVC4 reports: " << theorem << " is "
- << slv.checkValidAssuming(theorem) << "." << endl;
+ cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+ << "." << endl;
}
// Verify emptset is a subset of any set
Term theorem = slv.mkTerm(SUBSET, emptyset, A);
- cout << "CVC4 reports: " << theorem << " is "
- << slv.checkValidAssuming(theorem) << "." << endl;
+ cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem)
+ << "." << endl;
}
// Find me an element in {1, 2} intersection {2, 3}, if there is one.
Expr theorem = em.mkExpr(kind::EQUAL, lhs, rhs);
- cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl;
+ cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem)
+ << "." << endl;
}
// Verify emptset is a subset of any set
Expr theorem = em.mkExpr(kind::SUBSET, emptyset, A);
- cout << "CVC4 reports: " << theorem << " is " << smt.query(theorem) << "." << endl;
+ cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem)
+ << "." << endl;
}
// Find me an element in {1, 2} intersection {2, 3}, if there is one.
em.mkExpr(kind::AND, x_positive, y_positive).
impExpr(twox_plus_y_geq_3);
- cout << "Checking validity of formula " << formula << " with CVC4." << endl;
- cout << "CVC4 should report VALID." << endl;
- cout << "Result from CVC4 is: " << smt.query(formula) << endl;
+ cout << "Checking entailment of formula " << formula << " with CVC4." << endl;
+ cout << "CVC4 should report ENTAILED." << endl;
+ cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl;
return 0;
}
&& d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
}
-bool Result::isValid(void) const
+bool Result::isEntailed(void) const
{
- return d_result->getType() == CVC4::Result::TYPE_VALIDITY
- && d_result->isValid() == CVC4::Result::VALID;
+ return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+ && d_result->isEntailed() == CVC4::Result::ENTAILED;
}
-bool Result::isInvalid(void) const
+bool Result::isNotEntailed(void) const
{
- return d_result->getType() == CVC4::Result::TYPE_VALIDITY
- && d_result->isValid() == CVC4::Result::INVALID;
+ return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+ && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED;
}
-bool Result::isValidUnknown(void) const
+bool Result::isEntailmentUnknown(void) const
{
- return d_result->getType() == CVC4::Result::TYPE_VALIDITY
- && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN;
+ return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+ && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN;
}
bool Result::operator==(const Result& r) const
CVC4_API_SOLVER_TRY_CATCH_END;
}
-Result Solver::checkValid(void) const
+Result Solver::checkEntailed(Term term) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
|| CVC4::options::incrementalSolving())
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
+ CVC4_API_ARG_CHECK_NOT_NULL(term);
- CVC4::Result r = d_smtEngine->query();
+ CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr);
return Result(r);
CVC4_API_SOLVER_TRY_CATCH_END;
}
-Result Solver::checkValidAssuming(Term assumption) const
+Result Solver::checkEntailed(const std::vector<Term>& terms) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
|| CVC4::options::incrementalSolving())
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
- CVC4_API_ARG_CHECK_NOT_NULL(assumption);
-
- CVC4::Result r = d_smtEngine->query(*assumption.d_expr);
- return Result(r);
-
- CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
-Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const
-{
- CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(!d_smtEngine->isQueryMade()
- || CVC4::options::incrementalSolving())
- << "Cannot make multiple queries unless incremental solving is enabled "
- "(try --incremental)";
- for (const Term& assumption : assumptions)
+ for (const Term& term : terms)
{
- CVC4_API_ARG_CHECK_NOT_NULL(assumption);
+ CVC4_API_ARG_CHECK_NOT_NULL(term);
}
- std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
- CVC4::Result r = d_smtEngine->query(eassumptions);
+ std::vector<Expr> exprs = termVectorToExprs(terms);
+ CVC4::Result r = d_smtEngine->checkEntailed(exprs);
return Result(r);
CVC4_API_SOLVER_TRY_CATCH_END;
bool isSatUnknown() const;
/**
- * Return true if corresponding query was a valid checkValid() or
- * checkValidAssuming() query.
+ * Return true if corresponding query was an entailed checkEntailed() query.
*/
- bool isValid() const;
+ bool isEntailed() const;
/**
- * Return true if corresponding query was an invalid checkValid() or
- * checkValidAssuming() query.
+ * Return true if corresponding query was a checkEntailed() query that is
+ * not entailed.
*/
- bool isInvalid() const;
+ bool isNotEntailed() const;
/**
- * Return true if query was a checkValid() or checkValidAssuming() query
- * and CVC4 was not able to determine (in)validity.
+ * Return true if query was a checkEntailed() () query and CVC4 was not able
+ * to determine if it is entailed.
*/
- bool isValidUnknown() const;
+ bool isEntailmentUnknown() const;
/**
* Operator overloading for equality of two results.
Result checkSatAssuming(const std::vector<Term>& assumptions) const;
/**
- * Check validity.
- * @return the result of the validity check.
+ * Check entailment of the given formula w.r.t. the current set of assertions.
+ * @param term the formula to check entailment for
+ * @return the result of the entailment check.
*/
- Result checkValid() const;
+ Result checkEntailed(Term term) const;
/**
- * Check validity assuming the given formula.
- * @param assumption the formula to assume
- * @return the result of the validity check.
- */
- Result checkValidAssuming(Term assumption) const;
-
- /**
- * Check validity assuming the given formulas.
- * @param assumptions the formulas to assume
- * @return the result of the validity check.
+ * Check entailment of the given set of given formulas w.r.t. the current
+ * set of assertions.
+ * @param terms the terms to check entailment for
+ * @return the result of the entailmentcheck.
*/
- Result checkValidAssuming(const std::vector<Term>& assumptions) const;
+ Result checkEntailed(const std::vector<Term>& terms) const;
/**
* Create datatype sort.
bint isSat() except +
bint isUnsat() except +
bint isSatUnknown() except +
- bint isValid() except +
- bint isInvalid() except +
- bint isValidUnknown() except +
+ bint isEntailed() except +
+ bint isNotEntailed() except +
+ bint isEntailmentUnknown() except +
string getUnknownExplanation() except +
string toString() except +
void assertFormula(Term term) except +
Result checkSat() except +
Result checkSatAssuming(const vector[Term]& assumptions) except +
- Result checkValid() except +
- Result checkValidAssuming(const vector[Term]& assumptions) except +
+ Result checkEntailed(const vector[Term]& assumptions) except +
Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors)
Term declareFun(const string& symbol, Sort sort) except +
Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except +
explanation = r.getUnknownExplanation().decode()
return Result(name, explanation)
- def checkValid(self):
- cdef c_Result r = self.csolver.checkValid()
- name = r.toString().decode()
- explanation = ""
- if r.isValidUnknown():
- explanation = r.getUnknownExplanation().decode()
- return Result(name, explanation)
-
@expand_list_arg(num_req_args=0)
- def checkValidAssuming(self, *assumptions):
+ def checkEntailed(self, *assumptions):
'''
Supports the following arguments:
- Result checkValidAssuming(List[Term] assumptions)
+ Result checkEntailed(List[Term] assumptions)
where assumptions can also be comma-separated arguments of
type (boolean) Term
cdef vector[c_Term] v
for a in assumptions:
v.push_back((<Term?> a).cterm)
- r = self.csolver.checkValidAssuming(<const vector[c_Term]&> v)
+ r = self.csolver.checkEntailed(<const vector[c_Term]&> v)
name = r.toString().decode()
explanation = ""
- if r.isValidUnknown():
+ if r.isEntailmentUnknown():
explanation = r.getUnknownExplanation().decode()
return Result(name, explanation)
{
try
{
- d_result = smtEngine->query(d_expr);
+ d_result = smtEngine->checkEntailed(d_expr);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
resourceManager->out()) {
Result::UnknownExplanation why = resourceManager->outOfResources() ?
Result::RESOURCEOUT : Result::TIMEOUT;
- return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
+ return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename);
}
// Make sure the prop layer has all of the assertions
Result SmtEngine::quickCheck() {
Assert(d_fullyInited);
Trace("smt") << "SMT quickCheck()" << endl;
- return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
+ return Result(
+ Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
}
theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
{
std::stringstream ss;
ss << "Cannot " << c
- << " unless immediately preceded by SAT/INVALID or UNKNOWN response.";
+ << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
+ "response.";
throw RecoverableModalException(ss.str().c_str());
}
return checkSatisfiability(assumptions, inUnsatCore, false);
}
-Result SmtEngine::query(const Expr& assumption, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore)
{
- Dump("benchmark") << QueryCommand(assumption, inUnsatCore);
- return checkSatisfiability(assumption.isNull()
- ? std::vector<Expr>()
- : std::vector<Expr>{assumption},
- inUnsatCore,
- true)
- .asValidityResult();
+ Dump("benchmark") << QueryCommand(expr, inUnsatCore);
+ return checkSatisfiability(
+ expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
+ inUnsatCore,
+ true)
+ .asEntailmentResult();
}
-Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore)
{
- return checkSatisfiability(assumptions, inUnsatCore, true).asValidityResult();
+ return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult();
}
Result SmtEngine::checkSatisfiability(const Expr& expr,
bool inUnsatCore,
- bool isQuery)
+ bool isEntailmentCheck)
{
return checkSatisfiability(
expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
inUnsatCore,
- isQuery);
+ isEntailmentCheck);
}
Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
bool inUnsatCore,
- bool isQuery)
+ bool isEntailmentCheck)
{
try
{
finalOptionsAreSet();
doPendingPops();
- Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
+ Trace("smt") << "SmtEngine::"
+ << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
<< assumptions << ")" << endl;
if(d_queryMade && !options::incrementalSolving()) {
setProblemExtended();
- if (isQuery)
+ if (isEntailmentCheck)
{
size_t size = assumptions.size();
if (size > 1)
d_smtMode = SMT_MODE_SAT_UNKNOWN;
}
- Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
- << assumptions << ") => " << r << endl;
+ Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
+ << "(" << assumptions << ") => " << r << endl;
// Check that SAT results generate a model correctly.
if(options::checkModels()) {
{
throw RecoverableModalException(
"Cannot get unsat assumptions unless immediately preceded by "
- "UNSAT/VALID response.");
+ "UNSAT/ENTAILED.");
}
finalOptionsAreSet();
if (Dump.isOn("benchmark"))
}
bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv);
- return quickCheck().asValidityResult();
+ return quickCheck().asEntailmentResult();
}/* SmtEngine::assertFormula() */
/*
Expr heap;
Expr nil;
Model* m = getAvailableModel("get separation logic heap and nil");
- if (m->getHeapModel(heap, nil))
+ if (!m->getHeapModel(heap, nil))
{
- return std::make_pair(heap, nil);
+ InternalError()
+ << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
+ "expressions from theory model.";
}
- InternalError()
- << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
- "expressions from theory model.";
+ return std::make_pair(heap, nil);
}
std::vector<Expr> SmtEngine::getExpandedAssertions()
if (d_smtMode != SMT_MODE_UNSAT)
{
throw RecoverableModalException(
- "Cannot get an unsat core unless immediately preceded by UNSAT/VALID "
- "response.");
+ "Cannot get an unsat core unless immediately preceded by "
+ "UNSAT/ENTAILED response.");
}
d_proofManager->traceUnsatCore(); // just to trigger core creation
if (d_smtMode != SMT_MODE_UNSAT)
{
throw RecoverableModalException(
- "Cannot get a proof unless immediately preceded by UNSAT/VALID "
+ "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
"response.");
}
*/
bool isFullyInited() { return d_fullyInited; }
- /** Return true if a query() or checkSat() has already been made. */
+ /**
+ * Return true if a checkEntailed() or checkSatisfiability() has been made.
+ */
bool isQueryMade() { return d_queryMade; }
/** Return the user context level. */
std::string getFilename() const;
/**
- * Get the model (only if immediately preceded by a SAT
- * or INVALID query). Only permitted if produce-models is on.
+ * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
+ * query). Only permitted if produce-models is on.
*/
Model* getModel();
/**
* Block the current model values of (at least) the values in exprs.
- * Can be called only if immediately preceded by a SAT or INVALID query. Only
- * permitted if produce-models is on, and the block-models option is set to a
- * mode other than "none".
+ * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query.
+ * Only permitted if produce-models is on, and the block-models option is set
+ * to a mode other than "none".
*
* This adds an assertion to the assertion stack of the form:
* (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
Result assertFormula(const Expr& e, bool inUnsatCore = true);
/**
- * Check validity of an expression with respect to the current set
- * of assertions by asserting the query expression's negation and
- * calling check(). Returns valid, invalid, or unknown result.
+ * Check if a given (set of) expression(s) is entailed with respect to the
+ * current set of assertions. We check this by asserting the negation of
+ * the (big AND over the) given (set of) expression(s).
+ * Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result.
*
* @throw Exception
*/
- Result query(const Expr& assumption = Expr(), bool inUnsatCore = true);
- Result query(const std::vector<Expr>& assumptions, bool inUnsatCore = true);
+ Result checkEntailed(const Expr& assumption = Expr(),
+ bool inUnsatCore = true);
+ Result checkEntailed(const std::vector<Expr>& assumptions,
+ bool inUnsatCore = true);
/**
* Assert a formula (if provided) to the current context and call
- * check(). Returns sat, unsat, or unknown result.
+ * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result.
*
* @throw Exception
*/
Expr expandDefinitions(const Expr& e);
/**
- * Get the assigned value of an expr (only if immediately preceded
- * by a SAT or INVALID query). Only permitted if the SmtEngine is
- * set to operate interactively and produce-models is on.
+ * Get the assigned value of an expr (only if immediately preceded by a SAT
+ * or NOT_ENTAILED query). Only permitted if the SmtEngine is set to operate
+ * interactively and produce-models is on.
*
* @throw ModalException, TypeCheckingException, LogicException,
* UnsafeInterruptException
/**
* Get the assignment (only if immediately preceded by a SAT or
- * INVALID query). Only permitted if the SmtEngine is set to
+ * NOT_ENTAILED query). Only permitted if the SmtEngine is set to
* operate interactively and produce-assignments is on.
*/
std::vector<std::pair<Expr, Expr> > getAssignment();
/**
- * Get the last proof (only if immediately preceded by an UNSAT
- * or VALID query). Only permitted if CVC4 was built with proof
- * support and produce-proofs is on.
+ * Get the last proof (only if immediately preceded by an UNSAT or ENTAILED
+ * query). Only permitted if CVC4 was built with proof support and
+ * produce-proofs is on.
*
* The Proof object is owned by this SmtEngine until the SmtEngine is
* destroyed.
std::vector<std::vector<Expr> >& tvecs);
/**
- * Get an unsatisfiable core (only if immediately preceded by an
- * UNSAT or VALID query). Only permitted if CVC4 was built with
- * unsat-core support and produce-unsat-cores is on.
+ * Get an unsatisfiable core (only if immediately preceded by an UNSAT or
+ * ENTAILED query). Only permitted if CVC4 was built with unsat-core support
+ * and produce-unsat-cores is on.
*/
UnsatCore getUnsatCore();
*
* Note that the cumulative timer only ticks away when one of the
* SmtEngine's workhorse functions (things like assertFormula(),
- * query(), checkSat(), and simplify()) are running. Between calls,
- * the timer is still.
+ * checkEntailed(), checkSat(), and simplify()) are running.
+ * Between calls, the timer is still.
*
* When an SmtEngine is first created, it has no time or resource
* limits.
/** Flush statistic from this SmtEngine. Safe to use in a signal handler. */
void safeFlushStatistics(int fd) const;
- /** Returns the most recent result of checkSat/query or (set-info :status). */
+ /**
+ * Returns the most recent result of checkSat/checkEntailed or
+ * (set-info :status).
+ */
Result getStatusOfLastCommand() const { return d_status; }
/**
/**
* Internal method to get an unsatisfiable core (only if immediately preceded
- * by an UNSAT or VALID query). Only permitted if CVC4 was built with
+ * by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with
* unsat-core support and produce-unsat-cores is on. Does not dump the
* command.
*/
bool userVisible = true,
const char* dumpTag = "declarations");
- /* Check satisfiability (used for query and check-sat). */
+ /* Check satisfiability (used to check satisfiability and entailment). */
Result checkSatisfiability(const Expr& assumption,
bool inUnsatCore,
- bool isQuery);
+ bool isEntailmentCheck);
Result checkSatisfiability(const std::vector<Expr>& assumptions,
bool inUnsatCore,
- bool isQuery);
+ bool isEntailmentCheck);
/**
* Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
/**
* The list of assumptions from the previous call to checkSatisfiability.
- * Note that if the last call to checkSatisfiability was a validity check,
- * i.e., a call to query(a1, ..., an), then d_assumptions contains one single
- * assumption ~(a1 AND ... AND an).
+ * Note that if the last call to checkSatisfiability was an entailment check,
+ * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains
+ * one single assumption ~(a1 AND ... AND an).
*/
std::vector<Expr> d_assumptions;
bool d_fullyInited;
/**
- * Whether or not a query() or checkSat() has already been made through
- * this SmtEngine. If true, and incrementalSolving is false, then
- * attempting an additional query() or checkSat() will fail with a
- * ModalException.
+ * Whether or not a checkEntailed() or checkSatisfiability() has already been
+ * made through this SmtEngine. If true, and incrementalSolving is false,
+ * then attempting an additional checkEntailed() or checkSat() will fail with
+ * a ModalException.
*/
bool d_queryMade;
bool d_globalNegation;
/**
- * Most recent result of last checkSat/query or (set-info :status).
+ * Most recent result of last checkSatisfiability/checkEntailed or
+ * (set-info :status).
*/
Result d_status;
Result::Result()
: d_sat(SAT_UNKNOWN),
- d_validity(VALIDITY_UNKNOWN),
+ d_entailment(ENTAILMENT_UNKNOWN),
d_which(TYPE_NONE),
d_unknownExplanation(UNKNOWN_REASON),
- d_inputName("") {}
+ d_inputName("")
+{
+}
Result::Result(enum Sat s, std::string inputName)
: d_sat(s),
- d_validity(VALIDITY_UNKNOWN),
+ d_entailment(ENTAILMENT_UNKNOWN),
d_which(TYPE_SAT),
d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName) {
+ d_inputName(inputName)
+{
PrettyCheckArgument(s != SAT_UNKNOWN,
"Must provide a reason for satisfiability being unknown");
}
-Result::Result(enum Validity v, std::string inputName)
+Result::Result(enum Entailment e, std::string inputName)
: d_sat(SAT_UNKNOWN),
- d_validity(v),
- d_which(TYPE_VALIDITY),
+ d_entailment(e),
+ d_which(TYPE_ENTAILMENT),
d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName) {
- PrettyCheckArgument(v != VALIDITY_UNKNOWN,
- "Must provide a reason for validity being unknown");
+ d_inputName(inputName)
+{
+ PrettyCheckArgument(e != ENTAILMENT_UNKNOWN,
+ "Must provide a reason for entailment being unknown");
}
-Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
+Result::Result(enum Sat s,
+ enum UnknownExplanation unknownExplanation,
std::string inputName)
: d_sat(s),
- d_validity(VALIDITY_UNKNOWN),
+ d_entailment(ENTAILMENT_UNKNOWN),
d_which(TYPE_SAT),
d_unknownExplanation(unknownExplanation),
- d_inputName(inputName) {
+ d_inputName(inputName)
+{
PrettyCheckArgument(s == SAT_UNKNOWN,
"improper use of unknown-result constructor");
}
-Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+Result::Result(enum Entailment e,
+ enum UnknownExplanation unknownExplanation,
std::string inputName)
: d_sat(SAT_UNKNOWN),
- d_validity(v),
- d_which(TYPE_VALIDITY),
+ d_entailment(e),
+ d_which(TYPE_ENTAILMENT),
d_unknownExplanation(unknownExplanation),
- d_inputName(inputName) {
- PrettyCheckArgument(v == VALIDITY_UNKNOWN,
+ d_inputName(inputName)
+{
+ PrettyCheckArgument(e == ENTAILMENT_UNKNOWN,
"improper use of unknown-result constructor");
}
Result::Result(const std::string& instr, std::string inputName)
: d_sat(SAT_UNKNOWN),
- d_validity(VALIDITY_UNKNOWN),
+ d_entailment(ENTAILMENT_UNKNOWN),
d_which(TYPE_NONE),
d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName) {
+ d_inputName(inputName)
+{
string s = instr;
transform(s.begin(), s.end(), s.begin(), ::tolower);
if (s == "sat" || s == "satisfiable") {
} else if (s == "unsat" || s == "unsatisfiable") {
d_which = TYPE_SAT;
d_sat = UNSAT;
- } else if (s == "valid") {
- d_which = TYPE_VALIDITY;
- d_validity = VALID;
- } else if (s == "invalid") {
- d_which = TYPE_VALIDITY;
- d_validity = INVALID;
- } else if (s == "incomplete") {
+ }
+ else if (s == "entailed")
+ {
+ d_which = TYPE_ENTAILMENT;
+ d_entailment = ENTAILED;
+ }
+ else if (s == "not_entailed")
+ {
+ d_which = TYPE_ENTAILMENT;
+ d_entailment = NOT_ENTAILED;
+ }
+ else if (s == "incomplete")
+ {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = INCOMPLETE;
- } else if (s == "timeout") {
+ }
+ else if (s == "timeout")
+ {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = TIMEOUT;
- } else if (s == "resourceout") {
+ }
+ else if (s == "resourceout")
+ {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = RESOURCEOUT;
- } else if (s == "memout") {
+ }
+ else if (s == "memout")
+ {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = MEMOUT;
- } else if (s == "interrupted") {
+ }
+ else if (s == "interrupted")
+ {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = INTERRUPTED;
- } else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
+ }
+ else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0)
+ {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
- } else {
+ }
+ else
+ {
IllegalArgument(s,
- "expected satisfiability/validity result, "
+ "expected satisfiability/entailment result, "
"instead got `%s'",
s.c_str());
}
return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN ||
d_unknownExplanation == r.d_unknownExplanation);
}
- if (d_which == TYPE_VALIDITY) {
- return d_validity == r.d_validity &&
- (d_validity != VALIDITY_UNKNOWN ||
- d_unknownExplanation == r.d_unknownExplanation);
+ if (d_which == TYPE_ENTAILMENT)
+ {
+ return d_entailment == r.d_entailment
+ && (d_entailment != ENTAILMENT_UNKNOWN
+ || d_unknownExplanation == r.d_unknownExplanation);
}
return false;
}
bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; }
-bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; }
+bool operator==(enum Result::Entailment e, const Result& r) { return r == e; }
bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); }
-bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); }
+bool operator!=(enum Result::Entailment e, const Result& r)
+{
+ return !(e == r);
+}
Result Result::asSatisfiabilityResult() const {
if (d_which == TYPE_SAT) {
return *this;
}
- if (d_which == TYPE_VALIDITY) {
- switch (d_validity) {
- case INVALID:
- return Result(SAT, d_inputName);
+ if (d_which == TYPE_ENTAILMENT)
+ {
+ switch (d_entailment)
+ {
+ case NOT_ENTAILED: return Result(SAT, d_inputName);
- case VALID:
- return Result(UNSAT, d_inputName);
+ case ENTAILED: return Result(UNSAT, d_inputName);
- case VALIDITY_UNKNOWN:
+ case ENTAILMENT_UNKNOWN:
return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
- default: Unhandled() << d_validity;
+ default: Unhandled() << d_entailment;
}
}
return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
}
-Result Result::asValidityResult() const {
- if (d_which == TYPE_VALIDITY) {
+Result Result::asEntailmentResult() const
+{
+ if (d_which == TYPE_ENTAILMENT)
+ {
return *this;
}
if (d_which == TYPE_SAT) {
switch (d_sat) {
- case SAT:
- return Result(INVALID, d_inputName);
+ case SAT: return Result(NOT_ENTAILED, d_inputName);
- case UNSAT:
- return Result(VALID, d_inputName);
+ case UNSAT: return Result(ENTAILED, d_inputName);
case SAT_UNKNOWN:
- return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
+ return Result(ENTAILMENT_UNKNOWN, d_unknownExplanation, d_inputName);
default: Unhandled() << d_sat;
}
}
// TYPE_NONE
- return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
+ return Result(ENTAILMENT_UNKNOWN, NO_STATUS, d_inputName);
}
string Result::toString() const {
return out;
}
-ostream& operator<<(ostream& out, enum Result::Validity v) {
- switch (v) {
- case Result::INVALID:
- out << "INVALID";
- break;
- case Result::VALID:
- out << "VALID";
- break;
- case Result::VALIDITY_UNKNOWN:
- out << "VALIDITY_UNKNOWN";
- break;
- default: Unhandled() << v;
+ostream& operator<<(ostream& out, enum Result::Entailment e)
+{
+ switch (e)
+ {
+ case Result::NOT_ENTAILED: out << "NOT_ENTAILED"; break;
+ case Result::ENTAILED: out << "ENTAILED"; break;
+ case Result::ENTAILMENT_UNKNOWN: out << "ENTAILMENT_UNKNOWN"; break;
+ default: Unhandled() << e;
}
return out;
}
break;
}
} else {
- switch (isValid()) {
- case Result::INVALID:
- out << "invalid";
- break;
- case Result::VALID:
- out << "valid";
- break;
- case Result::VALIDITY_UNKNOWN:
+ switch (isEntailed())
+ {
+ case Result::NOT_ENTAILED: out << "not_entailed"; break;
+ case Result::ENTAILED: out << "entailed"; break;
+ case Result::ENTAILMENT_UNKNOWN:
out << "unknown";
if (whyUnknown() != Result::UNKNOWN_REASON) {
out << " (" << whyUnknown() << ")";
out << "Satisfiable";
} else if (isSat() == Result::UNSAT) {
out << "Unsatisfiable";
- } else if (isValid() == Result::VALID) {
+ }
+ else if (isEntailed() == Result::ENTAILED)
+ {
out << "Theorem";
- } else if (isValid() == Result::INVALID) {
+ }
+ else if (isEntailed() == Result::NOT_ENTAILED)
+ {
out << "CounterSatisfiable";
- } else {
+ }
+ else
+ {
out << "GaveUp";
}
out << " for " << getInputName();
public:
enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 };
- enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 };
+ enum Entailment
+ {
+ NOT_ENTAILED = 0,
+ ENTAILED = 1,
+ ENTAILMENT_UNKNOWN = 2
+ };
- enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE };
+ enum Type
+ {
+ TYPE_SAT,
+ TYPE_ENTAILMENT,
+ TYPE_NONE
+ };
enum UnknownExplanation {
REQUIRES_FULL_CHECK,
private:
enum Sat d_sat;
- enum Validity d_validity;
+ enum Entailment d_entailment;
enum Type d_which;
enum UnknownExplanation d_unknownExplanation;
std::string d_inputName;
Result(enum Sat s, std::string inputName = "");
- Result(enum Validity v, std::string inputName = "");
+ Result(enum Entailment v, std::string inputName = "");
Result(enum Sat s, enum UnknownExplanation unknownExplanation,
std::string inputName = "");
- Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+ Result(enum Entailment v,
+ enum UnknownExplanation unknownExplanation,
std::string inputName = "");
Result(const std::string& s, std::string inputName = "");
enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; }
- enum Validity isValid() const {
- return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
+ enum Entailment isEntailed() const
+ {
+ return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN;
}
bool isUnknown() const {
- return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
+ return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN;
}
Type getType() const { return d_which; }
bool operator==(const Result& r) const;
inline bool operator!=(const Result& r) const;
Result asSatisfiabilityResult() const;
- Result asValidityResult() const;
+ Result asEntailmentResult() const;
std::string toString() const;
* Write a Result out to a stream.
*
* The default implementation writes a reasonable string in lowercase
- * for sat, unsat, valid, invalid, or unknown results. This behavior
+ * for sat, unsat, entailed, not entailed, or unknown results. This behavior
* is overridable by each Printer, since sometimes an output language
* has a particular preference for how results should appear.
*/
std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream& out,
- enum Result::Validity v) CVC4_PUBLIC;
+ enum Result::Entailment e) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream& out,
enum Result::UnknownExplanation e) CVC4_PUBLIC;
bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
-bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC;
+bool operator==(enum Result::Entailment e, const Result& r) CVC4_PUBLIC;
bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
-bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC;
+bool operator!=(enum Result::Entailment e, const Result& r) CVC4_PUBLIC;
} /* CVC4 namespace */
%ignore CVC4::Result::operator!=(const Result& r) const;
%ignore CVC4::operator<<(std::ostream&, enum Result::Sat);
-%ignore CVC4::operator<<(std::ostream&, enum Result::Validity);
+%ignore CVC4::operator<<(std::ostream&, enum Result::Entailment);
%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
%ignore CVC4::operator==(enum Result::Sat, const Result&);
%ignore CVC4::operator!=(enum Result::Sat, const Result&);
-%ignore CVC4::operator==(enum Result::Validity, const Result&);
-%ignore CVC4::operator!=(enum Result::Validity, const Result&);
+%ignore CVC4::operator==(enum Result::Entailment, const Result&);
+%ignore CVC4::operator!=(enum Result::Entailment, const Result&);
%include "util/result.h"
-% EXPECT: valid
+% EXPECT: entailed
x : REAL;
y : REAL;
-% EXPECT: valid
+% EXPECT: entailed
x : REAL;
y : REAL;
z : REAL;
-% EXPECT: valid
+% EXPECT: entailed
x : REAL;
y : REAL;
-% EXPECT: valid
+% EXPECT: entailed
a, b : REAL;
-QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
\ No newline at end of file
+QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ;
ASSERT (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ;
ASSERT (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12;
QUERY FALSE;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9;
QUERY FALSE;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3;
QUERY FALSE;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ;
ASSERT (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ;
-% EXPECT: valid
+% EXPECT: entailed
x1: INT;
x0: INT;
QUERY NOT (((x0 * 6) + (x1 * 32)) = 1);
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ;
ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ;
-% EXPECT: valid
+% EXPECT: entailed
x: INT;
P: INT -> BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of AND, <=>, NOT.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
b : BOOLEAN;
DATATYPE D = c(s:INT) END;
QUERY c(IF b THEN 1 ELSE 0 ENDIF) = IF b THEN c(1) ELSE c(0) ENDIF;
-% EXPECT: valid
+% EXPECT: entailed
a:BOOLEAN;
b:BOOLEAN;
ASSERT(a);
% COMMAND-LINE: --incremental
-% EXPECT: valid
-% EXPECT: valid
-% EXPECT: valid
+% EXPECT: entailed
+% EXPECT: entailed
+% EXPECT: entailed
x : INT;
y : INT = x + 1;
z : INT = -10;
% COMMAND-LINE: --finite-model-find -i
-% EXPECT: invalid
-% EXPECT: valid
+% EXPECT: not_entailed
+% EXPECT: entailed
prin:TYPE;
form:TYPE;
-% EXPECT: valid
+% EXPECT: entailed
x : BITVECTOR(10);
-% EXPECT: valid
+% EXPECT: entailed
% Some tests from the CVC3 user manual.
% http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html
-% EXPECT: valid
-% EXPECT: Cannot get model unless immediately preceded by SAT/INVALID or UNKNOWN response.
+% EXPECT: entailed
+% EXPECT: Cannot get model unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN response.
OPTION "logic" "ALL";
OPTION "produce-models" true;
x : INT;
%% This test borrowed from CVC3 regressions, bug15.cvc
-% EXPECT: valid
+% EXPECT: entailed
x : REAL;
y : REAL;
f : REAL -> REAL;
% COMMAND-LINE: --incremental
-% EXPECT: valid
+% EXPECT: entailed
QUERY 0bin0000111101010000 = 0hex0f50;
-% EXPECT: valid
+% EXPECT: entailed
QUERY 0bin01@0bin0 = 0bin010;
-% EXPECT: valid
+% EXPECT: entailed
QUERY 0bin0011[3:1] = 0bin001;
-% EXPECT: valid
+% EXPECT: entailed
QUERY 0bin0011 << 3 = 0bin0011000;
-% EXPECT: valid
+% EXPECT: entailed
QUERY 0bin1000 >> 3 = 0bin0001;
-% EXPECT: valid
+% EXPECT: entailed
QUERY SX(0bin100, 5) = 0bin11100;
-% EXPECT: valid
+% EXPECT: entailed
QUERY BVZEROEXTEND(0bin1,3) = 0bin0001;
-% EXPECT: valid
+% EXPECT: entailed
QUERY BVREPEAT(0bin10,3) = 0bin101010;
-% EXPECT: valid
+% EXPECT: entailed
QUERY BVROTL(0bin101,1) = 0bin011;
-% EXPECT: valid
+% EXPECT: entailed
QUERY BVROTR(0bin101,1) = 0bin110;
y : BITVECTOR(4);
yy : BITVECTOR(3);
-% EXPECT: valid
+% EXPECT: entailed
QUERY
BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ;
bv : BITVECTOR(10);
a : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY
0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2]
AND
ASSERT x|y = t;
ASSERT BVXOR(x,~x) = t;
-% EXPECT: valid
+% EXPECT: entailed
QUERY FALSE;
ASSERT x = 0hex5;
ASSERT y = 0bin0101;
-% EXPECT: valid
+% EXPECT: entailed
QUERY
BVMULT(8,x,y)=BVMULT(8,y,x)
AND
ASSERT x = 0hexff;
ASSERT z = 0hexff0;
-% EXPECT: valid
+% EXPECT: entailed
QUERY z = x << 4;
-% EXPECT: valid
+% EXPECT: entailed
QUERY (z >> 4)[7:0] = x;
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE foo = f(i:INT) END;
x : foo;
y : INT;
% EXPECT: END;
% EXPECT: x : nat;
% EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x));
-% EXPECT: invalid
+% EXPECT: not_entailed
%
DATATYPE nat = succ(pred : nat) | zero END;
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE nat = succ(pred : nat) | zero END;
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE nat = succ(pred : nat) | zero END;
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
tree = node(left : tree, right : tree) | leaf
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE enum = enum1
| enum2
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE
nat = succ(pred : nat) | zero,
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
tree = node(left : tree, right : tree) | leaf
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
TypeGeneric = generic
END;
c1, c2 : [[]]; % 1-tuples of the empty tuple (a unit type)
d1, d2 : [#x:[[##]],y:[#z:[]#]#]; % more complicated records (still a unit type)
-% EXPECT: valid
+% EXPECT: entailed
QUERY a1 = a2;
-% EXPECT: valid
+% EXPECT: entailed
QUERY b1 = b2;
-% EXPECT: valid
+% EXPECT: entailed
QUERY c1 = c2;
-% EXPECT: valid
+% EXPECT: entailed
QUERY d1 = d2;
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE nat = succ(pred : nat2) | zero,
nat2 = succ2(pred2 : nat) | zero2 END;
-% EXPECT: valid
+% EXPECT: entailed
c : BOOLEAN;
a17 : BOOLEAN = ((# _a := 2, _b := 2 #) = (
IF c THEN (# _a := 3, _b := 2 #)
-% EXPECT: valid
+% EXPECT: entailed
c : BOOLEAN;
a16 : [# _a : INT, _b : INT #] = (
IF c THEN (# _a := 3, _b := 2 #)
-% EXPECT: valid
+% EXPECT: entailed
a : BOOLEAN;
a49 : BOOLEAN = (
IF a THEN (# _a := 1 #)
-% EXPECT: valid
+% EXPECT: entailed
% simple test for rewriter cases
-% EXPECT: invalid
+% EXPECT: not_entailed
Mem_0 : TYPE = ARRAY INT OF INT;
-% EXPECT: valid
+% EXPECT: entailed
x: [REAL,INT,REAL] = ( 4/5, 9, 11/9 );
first_elem: REAL = x.0;
third_elem: REAL = x.2;
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: valid
+% EXPECT: entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
nat = succ(pred : nat) | zero,
list = cons(car : tree, cdr : list) | null,
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
nat = succ(pred : nat) | zero
END;
-% EXPECT: invalid
+% EXPECT: not_entailed
OPTION "finite-model-find";
OPTION "fmf-fun";
-% EXPECT: valid
+% EXPECT: entailed
U: TYPE;
a: U;
b: U;
a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
a, b, c: BOOLEAN;
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY NOT c AND b;
a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY (a => b) <=> (NOT a OR b);
a, b, c: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY TRUE XOR FALSE;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of AND and NOT.
A, B: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of XOR and AND.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of comparisons and booleans
x , y, z: INT;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of comparisons and plus/minus
x, y, z: INT;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of function application and =
T : TYPE;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right associativity of <=>
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of <=> and =>.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right associativity of =>
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of <=> and =>.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of => and OR.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of AND and NOT.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of = and NOT.
A, B: INT;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of => and OR.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of OR and XOR.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of plus/minus and mult/divide
a, b, c, d, e: INT;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of XOR and AND.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for left associativity of XOR
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
% Simple test for right precedence of OR and XOR.
A, B, C: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
a0, a1, a2, a3, a4, a5: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
-% EXPECT: invalid
+% EXPECT: not_entailed
% EXPECT: ((r.a, "active"))
% EXPECT: ((y.1, 9))
OPTION "produce-models";
a, b: BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY (a AND b) OR NOT (a AND b);
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY (a OR b);
% COMMAND-LINE: --incremental
U : TYPE;
x, y : U;
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY x = y;
ASSERT x = y;
-% EXPECT: valid
+% EXPECT: entailed
QUERY x = y;
PUSH;
z : U;
-% EXPECT: valid
+% EXPECT: entailed
QUERY x = y;
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY x = z;
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY z = x;
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY z /= x;
POP;
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY z /= x;
-% EXPECT: valid
+% EXPECT: entailed
QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ;
% EXPECT: unsat
% EXPECT: unsat
% EXPECT: unsat
-% EXPECT: invalid
+% EXPECT: not_entailed
OPTION "incremental" true;
OPTION "logic" "ALL_SUPPORTED";
SetInt : TYPE = SET OF INT;
ASSERT x0 OR NOT x3;
ASSERT x3 OR x2;
ASSERT x1 AND NOT x1;
-% EXPECT: valid
+% EXPECT: entailed
QUERY x2;
ASSERT c OR b OR a;
ASSERT b OR NOT a;
ASSERT a OR NOT b OR c;
-% EXPECT: invalid
+% EXPECT: not_entailed
QUERY FALSE;
-; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
+; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/ENTAILED response.")
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
ASSERT (x OR y);
ASSERT NOT (x OR y);
-% EXPECT: valid
+% EXPECT: entailed
QUERY FALSE;
-% EXPECT: valid
+% EXPECT: entailed
P,Q:BOOLEAN;
ASSERT (P OR Q);
QUERY (P OR Q);
-% EXPECT: valid
+% EXPECT: entailed
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: invalid
+% EXPECT: not_entailed
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: valid
+% EXPECT: entailed
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: invalid
+% EXPECT: not_entailed
A: TYPE;
B: TYPE;
x, y: A;
-% EXPECT: invalid
+% EXPECT: not_entailed
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR (b OR c) <=> (a OR b) OR c;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND (b AND c) <=> (a AND b) AND c;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR b <=> b OR a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND b <=> b AND a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR (a AND b) <=> a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND (a OR b) <=> a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR NOT a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND NOT a <=> FALSE;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR a <=> a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND a <=> a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR FALSE <=> a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND TRUE <=> a;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a OR TRUE <=> TRUE;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY a AND FALSE <=> FALSE;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY NOT FALSE <=> TRUE;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY NOT TRUE <=> FALSE;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY NOT (a OR b) <=> NOT a AND NOT b;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY NOT (a AND b) <=> NOT a OR NOT b;
a, b, c : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
QUERY NOT NOT a <=> a;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ;
ASSERT (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ;
ASSERT (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ;
ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ;
ASSERT (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ;
ASSERT (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ;
ASSERT (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ;
ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ;
ASSERT (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ;
ASSERT (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ;
ASSERT (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ;
ASSERT (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ;
ASSERT (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ;
ASSERT (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ;
ASSERT (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ;
ASSERT (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ;
ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ;
ASSERT (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18;
QUERY FALSE;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5;
QUERY FALSE;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ;
ASSERT (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ;
ASSERT (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ;
ASSERT (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ;
ASSERT (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ;
ASSERT (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ;
ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ;
ASSERT (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ;
ASSERT (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ;
ASSERT (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ;
ASSERT (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ;
ASSERT (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ;
ASSERT (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ;
ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ;
ASSERT (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ;
ASSERT (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ;
ASSERT (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ;
ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ;
-% EXPECT: valid
+% EXPECT: entailed
%%%% down from 24, up from 6, up from 39
x0, x1, x2, x3 : INT;
ASSERT (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ;
ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ;
ASSERT (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10;
ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ;
ASSERT (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ;
ASSERT (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ;
ASSERT (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ;
ASSERT (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ;
ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ;
ASSERT (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ;
ASSERT (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ;
ASSERT (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ;
ASSERT (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ;
ASSERT (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ;
ASSERT (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ;
ASSERT (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ;
ASSERT (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ;
ASSERT (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ;
ASSERT (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ;
ASSERT (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ;
ASSERT (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ;
ASSERT (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ;
ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ;
ASSERT (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ;
ASSERT (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ;
ASSERT (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ;
ASSERT (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ;
ASSERT (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ;
ASSERT (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ;
ASSERT (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ;
ASSERT (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ;
ASSERT (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ;
ASSERT (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ;
ASSERT (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ;
ASSERT (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ;
ASSERT (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8;
ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ;
ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ;
ASSERT (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ;
ASSERT (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
%% down from 3
x0, x1, x2, x3 : INT;
ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ;
ASSERT (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ;
ASSERT (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ;
ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ;
ASSERT (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ;
ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ;
ASSERT (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ;
ASSERT (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ;
ASSERT (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ;
ASSERT (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ;
-% EXPECT: valid
+% EXPECT: entailed
x0, x1, x2, x3 : INT;
ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ;
ASSERT (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ;
ASSERT (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ;
ASSERT (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ;
ASSERT (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ;
ASSERT (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ;
-% EXPECT: valid
+% EXPECT: entailed
p : BOOLEAN;
q : BOOLEAN;
r : BOOLEAN;
-% EXPECT: invalid
+% EXPECT: not_entailed
OPTION "finite-model-find";
OPTION "fmf-bound-int";
OPTION "produce-models";
-% EXPECT: valid
+% EXPECT: entailed
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
OPTION "finite-model-find";
OPTION "fmf-bound-int";
% COMMAND-LINE: --incremental
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: valid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: valid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: invalid
-% EXPECT: valid
-% EXPECT: valid
-% EXPECT: valid
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: not_entailed
+% EXPECT: entailed
+% EXPECT: entailed
+% EXPECT: entailed
A: TYPE;
P_1: BOOLEAN;
P_2: BOOLEAN;
-% EXPECT: invalid
+% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ;
ASSERT (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12;
-% EXPECT: valid
+% EXPECT: entailed
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: invalid
+% EXPECT: not_entailed
DATATYPE
nat = succ(pred : nat) | zero,
-% EXPECT: valid
+% EXPECT: entailed
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
-% EXPECT: valid
+% EXPECT: entailed
x_1 : BOOLEAN;
x_2 : BOOLEAN;
x_3 : BOOLEAN;
ExprManager em;
Options opts;
SmtEngine smt(&em);
- Result r = smt.query(em.mkConst(true));
+ Result r = smt.checkEntailed(em.mkConst(true));
- return (Result::VALID == r) ? 0 : 1;
+ return (Result::ENTAILED == r) ? 0 : 1;
}
Expr y = em.mkVar("y", em.integerType());
smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5))));
Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0)));
- Result r = smt.query(q);
+ Result r = smt.checkEntailed(q);
- if(r != Result::INVALID) {
+ if (r != Result::NOT_ENTAILED)
+ {
exit(1);
}
}
smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5))));
- r = smt.query(q);
+ r = smt.checkEntailed(q);
Statistics stats2 = smt.getStatistics();
bool different = false;
for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
}
#endif /* CVC4_STATISTICS_ON */
- return r == Result::VALID ? 0 : 1;
+ return r == Result::ENTAILED ? 0 : 1;
}
Options opts;
SmtEngine smt(&em);
SmtEngine smt2(&em);
- Result r = smt.query(em.mkConst(true));
- Result r2 = smt2.query(em.mkConst(true));
+ Result r = smt.checkEntailed(em.mkConst(true));
+ Result r2 = smt2.checkEntailed(em.mkConst(true));
- return r == Result::VALID && r2 == Result::VALID ? 0 : 1;
+ return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1;
}
void testIsSat();
void testIsUnsat();
void testIsSatUnknown();
- void testIsValid();
- void testIsInvalid();
- void testIsValidUnknown();
+ void testIsEntailed();
+ void testIsEntailmentUnknown();
private:
std::unique_ptr<Solver> d_solver;
TS_ASSERT(!res_null.isSat());
TS_ASSERT(!res_null.isUnsat());
TS_ASSERT(!res_null.isSatUnknown());
- TS_ASSERT(!res_null.isValid());
- TS_ASSERT(!res_null.isInvalid());
- TS_ASSERT(!res_null.isValidUnknown());
+ TS_ASSERT(!res_null.isEntailed());
+ TS_ASSERT(!res_null.isNotEntailed());
+ TS_ASSERT(!res_null.isEntailmentUnknown());
Sort u_sort = d_solver->mkUninterpretedSort("u");
Term x = d_solver->mkVar(u_sort, "x");
d_solver->assertFormula(x.eqTerm(x));
TS_ASSERT(res.isSatUnknown());
}
-void ResultBlack::testIsValid()
+void ResultBlack::testIsEntailed()
{
+ d_solver->setOption("incremental", "true");
Sort u_sort = d_solver->mkUninterpretedSort("u");
- Term x = d_solver->mkVar(u_sort, "x");
- d_solver->assertFormula(x.eqTerm(x).notTerm());
- Result res = d_solver->checkValid();
- TS_ASSERT(res.isValid());
- TS_ASSERT(!res.isValidUnknown());
-}
-
-void ResultBlack::testIsInvalid()
-{
- Sort u_sort = d_solver->mkUninterpretedSort("u");
- Term x = d_solver->mkVar(u_sort, "x");
- d_solver->assertFormula(x.eqTerm(x));
- Result res = d_solver->checkValid();
- TS_ASSERT(res.isInvalid());
- TS_ASSERT(!res.isValidUnknown());
+ Term x = d_solver->mkConst(u_sort, "x");
+ Term y = d_solver->mkConst(u_sort, "y");
+ Term a = x.eqTerm(y).notTerm();
+ Term b = x.eqTerm(y);
+ d_solver->assertFormula(a);
+ Result entailed = d_solver->checkEntailed(a);
+ TS_ASSERT(entailed.isEntailed());
+ TS_ASSERT(!entailed.isEntailmentUnknown());
+ Result not_entailed = d_solver->checkEntailed(b);
+ TS_ASSERT(not_entailed.isNotEntailed());
+ TS_ASSERT(!not_entailed.isEntailmentUnknown());
}
-void ResultBlack::testIsValidUnknown()
+void ResultBlack::testIsEntailmentUnknown()
{
d_solver->setLogic("QF_NIA");
d_solver->setOption("incremental", "false");
Sort int_sort = d_solver->getIntegerSort();
Term x = d_solver->mkVar(int_sort, "x");
d_solver->assertFormula(x.eqTerm(x).notTerm());
- Result res = d_solver->checkValid();
- TS_ASSERT(!res.isValid());
- TS_ASSERT(res.isValidUnknown());
+ Result res = d_solver->checkEntailed(x.eqTerm(x));
+ TS_ASSERT(!res.isEntailed());
+ TS_ASSERT(res.isEntailmentUnknown());
TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON");
}
void testPop3();
void testSimplify();
- void testCheckValid1();
- void testCheckValid2();
- void testCheckValidAssuming1();
- void testCheckValidAssuming2();
+ void testCheckEntailed();
+ void testCheckEntailed1();
+ void testCheckEntailed2();
void testSetInfo();
void testSetLogic();
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
}
-void SolverBlack::testCheckValid1()
+void SolverBlack::testCheckEntailed()
{
d_solver->setOption("incremental", "false");
- TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
- TS_ASSERT_THROWS(d_solver->checkValid(), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+ TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()),
+ CVC4ApiException&);
}
-void SolverBlack::testCheckValid2()
+void SolverBlack::testCheckEntailed1()
{
+ Sort boolSort = d_solver->getBooleanSort();
+ Term x = d_solver->mkConst(boolSort, "x");
+ Term y = d_solver->mkConst(boolSort, "y");
+ Term z = d_solver->mkTerm(AND, x, y);
d_solver->setOption("incremental", "true");
-
- Sort realSort = d_solver->getRealSort();
- Sort intSort = d_solver->getIntegerSort();
-
- // Constants
- Term x = d_solver->mkConst(intSort, "x");
- Term y = d_solver->mkConst(realSort, "y");
- // Values
- Term three = d_solver->mkReal(3);
- Term neg2 = d_solver->mkReal(-2);
- Term two_thirds = d_solver->mkReal(2, 3);
- // Terms
- Term three_y = d_solver->mkTerm(MULT, three, y);
- Term diff = d_solver->mkTerm(MINUS, y, x);
- // Formulas
- Term x_geq_3y = d_solver->mkTerm(GEQ, x, three_y);
- Term x_leq_y = d_solver->mkTerm(LEQ, x, y);
- Term neg2_lt_x = d_solver->mkTerm(LT, neg2, x);
- // Assertions
- Term assertions = d_solver->mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x);
-
- TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
- d_solver->assertFormula(assertions);
- TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
-}
-
-void SolverBlack::testCheckValidAssuming1()
-{
- d_solver->setOption("incremental", "false");
- TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue()));
- TS_ASSERT_THROWS(d_solver->checkValidAssuming(d_solver->mkTrue()),
- CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+ TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z));
}
-void SolverBlack::testCheckValidAssuming2()
+void SolverBlack::testCheckEntailed2()
{
d_solver->setOption("incremental", "true");
p_f_y // p(f(y))
});
- TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue()));
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
d_solver->assertFormula(assertions);
TS_ASSERT_THROWS_NOTHING(
- d_solver->checkValidAssuming(d_solver->mkTerm(DISTINCT, x, y)));
- TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(
+ d_solver->checkEntailed(d_solver->mkTerm(DISTINCT, x, y)));
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(
{d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
- TS_ASSERT_THROWS(d_solver->checkValidAssuming(n), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->checkEntailed(n), CVC4ApiException&);
TS_ASSERT_THROWS(
- d_solver->checkValidAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}),
+ d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}),
CVC4ApiException&);
}
projects / cvc5.git / commitdiff