{DISTINCT, CVC4::Kind::DISTINCT},
{CONSTANT, CVC4::Kind::VARIABLE},
{VARIABLE, CVC4::Kind::BOUND_VARIABLE},
+ {SEXPR, CVC4::Kind::SEXPR},
{LAMBDA, CVC4::Kind::LAMBDA},
{WITNESS, CVC4::Kind::WITNESS},
/* Boolean ------------------------------------------------------------- */
d_ctor->getConstructor());
(void)ret.getType(true); /* kick off type checking */
// apply type ascription to the operator
- Term sctor =
- api::Term(d_solver,
- ret);
+ Term sctor = api::Term(d_solver, ret);
return sctor;
-
+
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_END;
}
+Term Solver::getQuantifierElimination(api::Term q) const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_ARG_CHECK_NOT_NULL(q);
+ CVC4_API_SOLVER_CHECK_TERM(q);
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ return Term(this,
+ d_smtEngine->getQuantifierElimination(q.getNode(), true, true));
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::getQuantifierEliminationDisjunct(api::Term q) const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_ARG_CHECK_NOT_NULL(q);
+ CVC4_API_SOLVER_CHECK_TERM(q);
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ return Term(
+ this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true));
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
Term Solver::getSeparationHeap() const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_SOLVER_TRY_CATCH_END;
}
+void Solver::blockModel() const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+ << "Cannot get value unless model generation is enabled "
+ "(try --produce-models)";
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
+ << "Cannot get value when in unsat mode.";
+ d_smtEngine->blockModel();
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+void Solver::blockModelValues(const std::vector<Term>& terms) const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+ << "Cannot get value unless model generation is enabled "
+ "(try --produce-models)";
+ CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
+ << "Cannot get value when in unsat mode.";
+ CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
+ << "a non-empty set of terms";
+ for (int i = 0; i < terms.size(); ++i)
+ {
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !terms[i].isNull(), "term", terms[i], i)
+ << "a non-null term";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == terms[i].d_solver, "term", terms[i], i)
+ << "a term associated to this solver object";
+ }
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ d_smtEngine->blockModelValues(termVectorToExprs(terms));
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+void Solver::printInstantiations(std::ostream& out) const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ d_smtEngine->printInstantiations(out);
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
/**
* ( push <numeral> )
*/
*/
std::vector<Term> getValue(const std::vector<Term>& terms) const;
+ /**
+ * Do quantifier elimination.
+ * SMT-LIB: ( get-qe <q> )
+ * Requires a logic that supports quantifier elimination. Currently, the only
+ * logics supported by quantifier elimination is LRA and LIA.
+ * @param q a quantified formula of the form:
+ * Q x1...xn. P( x1...xn, y1...yn )
+ * where P( x1...xn, y1...yn ) is a quantifier-free formula
+ * @return a formula ret such that, given the current set of formulas A
+ * asserted to this solver:
+ * - ( A ^ q ) and ( A ^ ret ) are equivalent
+ * - ret is quantifier-free formula containing only free variables in
+ * y1...yn.
+ */
+ Term getQuantifierElimination(api::Term q) const;
+
+ /**
+ * Do partial quantifier elimination, which can be used for incrementally
+ * computing the result of a quantifier elimination.
+ * SMT-LIB: ( get-qe-disjunct <q> )
+ * Requires a logic that supports quantifier elimination. Currently, the only
+ * logics supported by quantifier elimination is LRA and LIA.
+ * @param q a quantified formula of the form:
+ * Q x1...xn. P( x1...xn, y1...yn )
+ * where P( x1...xn, y1...yn ) is a quantifier-free formula
+ * @return a formula ret such that, given the current set of formulas A
+ * asserted to this solver:
+ * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
+ * exists,
+ * - ret is quantifier-free formula containing only free variables in
+ * y1...yn,
+ * - If Q is exists, let A^Q_n be the formula
+ * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
+ * where for each i=1,...n, formula ret^Q_i is the result of calling
+ * getQuantifierEliminationDisjunct for q with the set of assertions
+ * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
+ * A ^ ret^Q_1 ^ ... ^ ret^Q_n
+ * where ret^Q_i is the same as above. In either case, we have
+ * that ret^Q_j will eventually be true or false, for some finite j.
+ */
+ Term getQuantifierEliminationDisjunct(api::Term q) const;
+
/**
* When using separation logic, obtain the term for the heap.
* @return The term for the heap
*/
void printModel(std::ostream& out) const;
+ /**
+ * Block the current model. Can be called only if immediately preceded by a
+ * SAT or INVALID query.
+ * SMT-LIB: ( block-model )
+ * Requires enabling 'produce-models' option and setting 'block-models' option
+ * to a mode other than "none".
+ */
+ void blockModel() const;
+
+ /**
+ * Block the current model values of (at least) the values in terms. Can be
+ * called only if immediately preceded by a SAT or NOT_ENTAILED query.
+ * SMT-LIB: ( block-model-values ( <terms>+ ) )
+ * Requires enabling 'produce-models' option and setting 'block-models' option
+ * to a mode other than "none".
+ */
+ void blockModelValues(const std::vector<Term>& terms) const;
+
+ /**
+ * Print all instantiations made by the quantifiers module.
+ * @param out the output stream
+ */
+ void printInstantiations(std::ostream& out) const;
+
/**
* Push (a) level(s) to the assertion stack.
* SMT-LIB: ( push <numeral> )
#if 0
/* Skolem variable (internal only) */
SKOLEM,
- /* Symbolic expression (any arity) */
- SEXPR,
#endif
+ /*
+ * Symbolic expression.
+ * Parameters: n > 0
+ * -[1]..[n]: terms
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ * mkTerm(Kind kind, Term child1, Term child2)
+ * mkTerm(Kind kind, Term child1, Term child2, Term child3)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ SEXPR,
/**
* Lambda expression.
* Parameters: 2
{
try
{
- solver->getSmtEngine()->assertFormula(d_term.getExpr(), d_inUnsatCore);
+ solver->getSmtEngine()->assertFormula(d_term.getNode(), d_inUnsatCore);
d_commandStatus = CommandSuccess::instance();
}
catch (UnsafeInterruptException& e)
api::Term ExpandDefinitionsCommand::getTerm() const { return d_term; }
void ExpandDefinitionsCommand::invoke(api::Solver* solver)
{
- Node t = d_term.getNode();
- d_result = api::Term(solver, solver->getSmtEngine()->expandDefinitions(t));
- d_commandStatus = CommandSuccess::instance();
+ try
+ {
+ d_result = api::Term(
+ solver, solver->getSmtEngine()->expandDefinitions(d_term.getNode()));
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
}
api::Term ExpandDefinitionsCommand::getResult() const { return d_result; }
{
try
{
- NodeManager* nm = solver->getNodeManager();
- smt::SmtScope scope(solver->getSmtEngine());
- std::vector<Node> result =
- api::termVectorToNodes(solver->getValue(d_terms));
+ std::vector<api::Term> result = solver->getValue(d_terms);
Assert(result.size() == d_terms.size());
for (int i = 0, size = d_terms.size(); i < size; i++)
{
- api::Term t = d_terms[i];
- Node tNode = t.getNode();
- Node request = options::expandDefinitions()
- ? solver->getSmtEngine()->expandDefinitions(tNode)
- : tNode;
- Node value = result[i];
- if (value.getType().isInteger() && request.getType() == nm->realType())
+ api::Term request = d_terms[i];
+ api::Term value = result[i];
+ if (value.getSort().isInteger()
+ && request.getSort() == solver->getRealSort())
{
// Need to wrap in division-by-one so that output printers know this
// is an integer-looking constant that really should be output as
// a rational. Necessary for SMT-LIB standards compliance.
- value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
+ value = solver->mkTerm(api::DIVISION, value, solver->mkReal(1));
}
- result[i] = nm->mkNode(kind::SEXPR, request, value);
+ result[i] = solver->mkTerm(api::SEXPR, request, value);
}
- d_result = api::Term(solver, nm->mkNode(kind::SEXPR, result));
+ d_result = solver->mkTerm(api::SEXPR, result);
d_commandStatus = CommandSuccess::instance();
}
catch (api::CVC4ApiRecoverableException& e)
{
try
{
- solver->getSmtEngine()->blockModel();
+ solver->blockModel();
d_commandStatus = CommandSuccess::instance();
}
- catch (RecoverableModalException& e)
+ catch (api::CVC4ApiRecoverableException& e)
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
{
try
{
- solver->getSmtEngine()->blockModelValues(api::termVectorToExprs(d_terms));
+ solver->blockModelValues(d_terms);
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
/* class GetInstantiationsCommand */
/* -------------------------------------------------------------------------- */
-GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
+GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
void GetInstantiationsCommand::invoke(api::Solver* solver)
{
try
{
- d_smtEngine = solver->getSmtEngine();
+ d_solver = solver;
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
}
else
{
- d_smtEngine->printInstantiations(out);
+ d_solver->printInstantiations(out);
}
}
{
GetInstantiationsCommand* c = new GetInstantiationsCommand();
// c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
+ c->d_solver = d_solver;
return c;
}
{
try
{
- d_result = api::Term(solver,
- solver->getSmtEngine()->getQuantifierElimination(
- d_term.getNode(), d_doFull));
+ if (d_doFull)
+ {
+ d_result = solver->getQuantifierElimination(d_term);
+ }
+ else
+ {
+ d_result = solver->getQuantifierEliminationDisjunct(d_term);
+ }
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
- SmtEngine* d_smtEngine;
+ api::Solver* d_solver;
}; /* class GetInstantiationsCommand */
class CVC4_PUBLIC GetSynthSolutionCommand : public Command
finishInit();
- PrettyCheckArgument(
- !exprs.empty(),
- "block model values must be called on non-empty set of terms");
if (Dump.isOn("benchmark"))
{
getOutputManager().getPrinter().toStreamCmdBlockModelValues(
void testGetValue1();
void testGetValue2();
void testGetValue3();
+ void testGetQuantifierElimination();
+ void testGetQuantifierEliminationDisjunct();
void testGetSeparationHeapTerm1();
void testGetSeparationHeapTerm2();
void testGetSeparationHeapTerm3();
void testPrintModel2();
void testPrintModel3();
+ void testBlockModel1();
+ void testBlockModel2();
+ void testBlockModel3();
+ void testBlockModel4();
+ void testBlockModelValues1();
+ void testBlockModelValues2();
+ void testBlockModelValues3();
+ void testBlockModelValues4();
+ void testBlockModelValues5();
+
void testSimplify();
void testAssertFormula();
TS_ASSERT_THROWS(slv.getValue(x), CVC4ApiException&);
}
+void SolverBlack::testGetQuantifierElimination()
+{
+ Term x = d_solver->mkVar(d_solver->getBooleanSort(), "x");
+ Term forall =
+ d_solver->mkTerm(FORALL,
+ d_solver->mkTerm(BOUND_VAR_LIST, x),
+ d_solver->mkTerm(OR, x, d_solver->mkTerm(NOT, x)));
+ TS_ASSERT_THROWS(d_solver->getQuantifierElimination(Term()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver->getQuantifierElimination(Solver().mkBoolean(false)),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierElimination(forall));
+}
+
+void SolverBlack::testGetQuantifierEliminationDisjunct()
+{
+ Term x = d_solver->mkVar(d_solver->getBooleanSort(), "x");
+ Term forall =
+ d_solver->mkTerm(FORALL,
+ d_solver->mkTerm(BOUND_VAR_LIST, x),
+ d_solver->mkTerm(OR, x, d_solver->mkTerm(NOT, x)));
+ TS_ASSERT_THROWS(d_solver->getQuantifierEliminationDisjunct(Term()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver->getQuantifierEliminationDisjunct(Solver().mkBoolean(false)),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierEliminationDisjunct(forall));
+}
+
namespace {
/**
* Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
TS_ASSERT_THROWS_NOTHING(d_solver->printModel(std::cout));
}
+void SolverBlack::testBlockModel1()
+{
+ d_solver->setOption("produce-models", "true");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ d_solver->checkSat();
+ TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&);
+}
+
+void SolverBlack::testBlockModel2()
+{
+ d_solver->setOption("block-models", "literals");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ d_solver->checkSat();
+ TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&);
+}
+
+void SolverBlack::testBlockModel3()
+{
+ d_solver->setOption("produce-models", "true");
+ d_solver->setOption("block-models", "literals");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&);
+}
+
+void SolverBlack::testBlockModel4()
+{
+ d_solver->setOption("produce-models", "true");
+ d_solver->setOption("block-models", "literals");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ d_solver->checkSat();
+ TS_ASSERT_THROWS_NOTHING(d_solver->blockModel());
+}
+
+void SolverBlack::testBlockModelValues1()
+{
+ d_solver->setOption("produce-models", "true");
+ d_solver->setOption("block-models", "literals");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ d_solver->checkSat();
+ TS_ASSERT_THROWS(d_solver->blockModelValues({}), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->blockModelValues({Term()}), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->blockModelValues({Solver().mkBoolean(false)}),
+ CVC4ApiException&);
+}
+
+void SolverBlack::testBlockModelValues2()
+{
+ d_solver->setOption("produce-models", "true");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ d_solver->checkSat();
+ TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&);
+}
+
+void SolverBlack::testBlockModelValues3()
+{
+ d_solver->setOption("block-models", "literals");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ d_solver->checkSat();
+ TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&);
+}
+
+void SolverBlack::testBlockModelValues4()
+{
+ d_solver->setOption("produce-models", "true");
+ d_solver->setOption("block-models", "literals");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&);
+}
+
+void SolverBlack::testBlockModelValues5()
+{
+ d_solver->setOption("produce-models", "true");
+ d_solver->setOption("block-models", "literals");
+ Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+ d_solver->assertFormula(x.eqTerm(x));
+ d_solver->checkSat();
+ TS_ASSERT_THROWS_NOTHING(d_solver->blockModelValues({x}));
+}
+
void SolverBlack::testSetInfo()
{
TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&);
projects / cvc5.git / commitdiff