This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine.
Note: we now limit :named terms to those not beneath quantifiers and let-bindings.
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+ CVC4_API_RECOVERABLE_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_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Cannot get value unless after a SAT or unknown response.";
std::vector<Term> res;
for (size_t i = 0, n = terms.size(); i < n; ++i)
{
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation heap term unless model generation is enabled "
"(try --produce-models)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
- << "Cannot get separtion heap term when in unsat mode.";
+ CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Can only get separtion heap term after sat or unknown response.";
return Term(this, d_smtEngine->getSepHeapExpr());
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation nil term unless model generation is enabled "
"(try --produce-models)";
- CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
- << "Cannot get separtion nil term when in unsat mode.";
+ CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Can only get separtion nil term after sat or unknown response.";
return Term(this, d_smtEngine->getSepNilExpr());
CVC4_API_SOLVER_TRY_CATCH_END;
}
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_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Can only get value after sat or unknown response.";
out << *d_smtEngine->getModel();
CVC4_API_SOLVER_TRY_CATCH_END;
}
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_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Can only block model after sat or unknown response.";
d_smtEngine->blockModel();
CVC4_API_SOLVER_TRY_CATCH_END;
}
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_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Can only block model values after sat or unknown response.";
CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
<< "a non-empty set of terms";
for (size_t i = 0, tsize = terms.size(); i < tsize; ++i)
| ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
{
attr = std::string(":named");
- api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
- std::string name = sexpr.getValue();
- // bind name to expr with define-fun
- // TODO (projects-248) SYM_MAN->setExpressionName(func, name, false);
- Command* c =
- new DefineNamedFunctionCommand(name,
- func,
- std::vector<api::Term>(),
- expr,
- SYM_MAN->getGlobalDeclarations());
- c->setMuted(true);
- PARSER_STATE->preemptCommand(c);
+ // notify that expression was given a name
+ PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue());
}
;
return ret;
}
-api::Term Smt2::setNamedAttribute(api::Term& expr, const SExpr& sexpr)
+void Smt2::notifyNamedExpression(api::Term& expr, std::string name)
{
- if (!sexpr.isKeyword())
- {
- parseError("improperly formed :named annotation");
- }
- std::string name = sexpr.getValue();
checkUserSymbol(name);
- // ensure expr is a closed subterm
- if (expr.getExpr().hasFreeVariable())
- {
- std::stringstream ss;
- ss << ":named annotations can only name terms that are closed";
- parseError(ss.str());
- }
- // check that sexpr is a fresh function symbol, and reserve it
- reserveSymbolAtAssertionLevel(name);
- // define it
- api::Term func = bindVar(name, expr.getSort(), ExprManager::VAR_FLAG_DEFINED);
- // remember the last term to have been given a :named attribute
+ // remember the expression name in the symbol manager
+ getSymbolManager()->setExpressionName(expr, name, false);
+ // define the variable
+ defineVar(name, expr);
+ // set the last named term, which ensures that we catch when assertions are
+ // named
setLastNamedTerm(expr, name);
- return func;
}
api::Term Smt2::mkAnd(const std::vector<api::Term>& es)
}
this->Parser::checkDeclaration(name, check, type, notes);
}
- /** Set named attribute
- *
- * This is called when expression expr is annotated with a name, i.e.
- * (! expr :named sexpr). It sets up the necessary information to process
- * this naming, including marking that expr is the last named term.
- *
- * We construct an expression symbol whose name is the name of s-expression
- * which is used later for tracking assertions in unsat cores. This
- * symbol is returned by this method.
+ /**
+ * Notify that expression expr was given name std::string via a :named
+ * attribute.
*/
- api::Term setNamedAttribute(api::Term& expr, const SExpr& sexpr);
+ void notifyNamedExpression(api::Term& expr, std::string name);
// Throw a ParserException with msg appended with the current logic.
inline void parseErrorLogic(const std::string& msg)
out << "]," << t << ')' << std::endl;
}
-void AstPrinter::toStreamCmdDefineNamedFunction(
- std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const
-{
- out << "DefineNamedFunction( ";
- toStreamCmdDefineFunction(out, id, formals, range, formula);
- out << " )" << std::endl;
-}
-
void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
out << "Simplify( << " << n << " >> )" << std::endl;
TypeNode range,
Node formula) const override;
- /** Print define-named-fun command */
- void toStreamCmdDefineNamedFunction(std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const override;
-
/** Print check-sat command */
void toStreamCmdCheckSat(std::ostream& out,
Node n = Node::null()) const override;
}
}
-void CvcPrinter::toStreamCmdDefineNamedFunction(
- std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const
-{
- toStreamCmdDefineFunction(out, id, formals, range, formula);
-}
-
void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
out << "TRANSFORM " << n << ';' << std::endl;
TypeNode range,
Node formula) const override;
- /** Print define-named-fun command */
- void toStreamCmdDefineNamedFunction(std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const override;
-
/** Print check-sat command */
void toStreamCmdCheckSat(std::ostream& out,
Node n = Node::null()) const override;
printUnknownCommand(out, "define-fun");
}
-void Printer::toStreamCmdDefineNamedFunction(std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const
-{
- printUnknownCommand(out, "define-named-function");
-}
-
void Printer::toStreamCmdDefineFunctionRec(
std::ostream& out,
const std::vector<Node>& funcs,
TypeNode range,
Node formula) const;
- /** Print define-named-fun command */
- virtual void toStreamCmdDefineNamedFunction(std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const;
-
/** Print define-fun-rec command */
virtual void toStreamCmdDefineFunctionRec(
std::ostream& out,
out << ") " << t << ")" << std::endl;
}
-void Smt2Printer::toStreamCmdDefineNamedFunction(
- std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const
-{
- out << "DefineNamedFunction( ";
- toStreamCmdDefineFunction(out, id, formals, range, formula);
- out << " )" << std::endl;
-
- printUnknownCommand(out, "define-named-function");
-}
-
void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
{
out << "(simplify " << n << ')' << std::endl;
TypeNode range,
Node formula) const override;
- /** Print define-named-fun command */
- void toStreamCmdDefineNamedFunction(std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const override;
-
/** Print define-fun-rec command */
void toStreamCmdDefineFunctionRec(
std::ostream& out,
d_formula.getNode());
}
-/* -------------------------------------------------------------------------- */
-/* class DefineNamedFunctionCommand */
-/* -------------------------------------------------------------------------- */
-
-DefineNamedFunctionCommand::DefineNamedFunctionCommand(
-
- const std::string& id,
- api::Term func,
- const std::vector<api::Term>& formals,
- api::Term formula,
- bool global)
- : DefineFunctionCommand(id, func, formals, formula, global)
-{
-}
-
-void DefineNamedFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
- this->DefineFunctionCommand::invoke(solver, sm);
- if (!d_func.isNull() && d_func.getSort().isBoolean())
- {
- solver->getSmtEngine()->addToAssignment(d_func.getExpr());
- }
- d_commandStatus = CommandSuccess::instance();
-}
-
-Command* DefineNamedFunctionCommand::clone() const
-{
- return new DefineNamedFunctionCommand(
- d_symbol, d_func, d_formals, d_formula, d_global);
-}
-
-void DefineNamedFunctionCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- OutputLanguage language) const
-{
- // get the range type of the function, or the type itself
- // if its not a function
- TypeNode range = d_func.getSort().getTypeNode();
- if (range.isFunction())
- {
- range = range.getRangeType();
- }
- Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
- out,
- d_func.toString(),
- api::termVectorToNodes(d_formals),
- range,
- d_formula.getNode());
-}
-
/* -------------------------------------------------------------------------- */
/* class DefineFunctionRecCommand */
/* -------------------------------------------------------------------------- */
{
try
{
- std::vector<std::pair<Expr, Expr>> assignments =
- solver->getSmtEngine()->getAssignment();
- vector<SExpr> sexprs;
- for (const auto& p : assignments)
+ std::map<api::Term, std::string> enames = sm->getExpressionNames();
+ std::vector<api::Term> terms;
+ std::vector<std::string> names;
+ for (const std::pair<const api::Term, std::string>& e : enames)
{
- vector<SExpr> v;
- v.emplace_back(SExpr::Keyword(p.first.toString()));
- v.emplace_back(SExpr::Keyword(p.second.toString()));
- sexprs.emplace_back(v);
+ terms.push_back(e.first);
+ names.push_back(e.second);
+ }
+ // Must use vector version of getValue to ensure error is thrown regardless
+ // of whether terms is empty.
+ std::vector<api::Term> values = solver->getValue(terms);
+ Assert(values.size() == names.size());
+ std::vector<SExpr> sexprs;
+ for (size_t i = 0, nterms = terms.size(); i < nterms; i++)
+ {
+ std::vector<SExpr> ss;
+ ss.emplace_back(SExpr::Keyword(names[i]));
+ ss.emplace_back(SExpr::Keyword(values[i].toString()));
+ sexprs.emplace_back(ss);
}
d_result = SExpr(sexprs);
d_commandStatus = CommandSuccess::instance();
}
- catch (RecoverableModalException& e)
+ catch (api::CVC4ApiRecoverableException& e)
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
bool d_global;
}; /* class DefineFunctionCommand */
-/**
- * This differs from DefineFunctionCommand only in that it instructs
- * the SmtEngine to "remember" this function for later retrieval with
- * getAssignment(). Used for :named attributes in SMT-LIBv2.
- */
-class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
-{
- public:
- DefineNamedFunctionCommand(const std::string& id,
- api::Term func,
- const std::vector<api::Term>& formals,
- api::Term formula,
- bool global);
- void invoke(api::Solver* solver, SymbolManager* sm) override;
- Command* clone() const override;
- void toStream(
- std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class DefineNamedFunctionCommand */
-
/**
* The command when parsing define-fun-rec or define-funs-rec.
* This command will assert a set of quantified formulas that specify
d_abductSolver(nullptr),
d_interpolSolver(nullptr),
d_quantElimSolver(nullptr),
- d_assignments(nullptr),
d_logic(),
d_originalOptions(),
d_isInternalSubsolver(false),
return d_state->getNumUserLevels();
}
SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); }
+bool SmtEngine::isSmtModeSat() const
+{
+ SmtMode mode = getSmtMode();
+ return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN;
+}
Result SmtEngine::getStatusOfLastCommand() const
{
return d_state->getStatus();
// of context-dependent data structures
d_state->cleanup();
- if(d_assignments != NULL) {
- d_assignments->deleteSelf();
- }
-
d_definedFunctions->deleteSelf();
//destroy all passes before destroying things that they refer to
return result;
}
-bool SmtEngine::addToAssignment(const Expr& ex) {
- SmtScope smts(this);
- finishInit();
- d_state->doPendingPops();
- // Substitute out any abstract values in ex
- Node n = d_absValues->substituteAbstractValues(Node::fromExpr(ex));
- TypeNode type = n.getType(options::typeChecking());
- // must be Boolean
- PrettyCheckArgument(type.isBoolean(),
- n,
- "expected Boolean-typed variable or function application "
- "in addToAssignment()");
- // must be a defined constant, or a variable
- PrettyCheckArgument(
- (((d_definedFunctions->find(n) != d_definedFunctions->end())
- && n.getNumChildren() == 0)
- || n.isVar()),
- n,
- "expected variable or defined-function application "
- "in addToAssignment(),\ngot %s",
- n.toString().c_str());
- if(!options::produceAssignments()) {
- return false;
- }
- if(d_assignments == NULL) {
- d_assignments = new (true) AssignmentSet(getContext());
- }
- d_assignments->insert(n);
-
- return true;
-}
-
-// TODO(#1108): Simplify the error reporting of this method.
-vector<pair<Expr, Expr>> SmtEngine::getAssignment()
-{
- Trace("smt") << "SMT getAssignment()" << endl;
- SmtScope smts(this);
- finishInit();
- if(Dump.isOn("benchmark")) {
- getOutputManager().getPrinter().toStreamCmdGetAssignment(
- getOutputManager().getDumpOut());
- }
- if(!options::produceAssignments()) {
- const char* msg =
- "Cannot get the current assignment when "
- "produce-assignments option is off.";
- throw ModalException(msg);
- }
-
- // Get the model here, regardless of whether d_assignments is null, since
- // we should throw errors related to model availability whether or not
- // assignments is null.
- Model* m = getAvailableModel("get assignment");
-
- vector<pair<Expr,Expr>> res;
- if (d_assignments != nullptr)
- {
- TypeNode boolType = d_nodeManager->booleanType();
- for (AssignmentSet::key_iterator i = d_assignments->key_begin(),
- iend = d_assignments->key_end();
- i != iend;
- ++i)
- {
- Node as = *i;
- Assert(as.getType() == boolType);
-
- Trace("smt") << "--- getting value of " << as << endl;
-
- // Expand, then normalize
- std::unordered_map<Node, Node, NodeHashFunction> cache;
- Node n = d_pp->expandDefinitions(as, cache);
- n = Rewriter::rewrite(n);
-
- Trace("smt") << "--- getting value of " << n << endl;
- Node resultNode;
- if (m != nullptr)
- {
- resultNode = m->getValue(n);
- }
-
- // type-check the result we got
- Assert(resultNode.isNull() || resultNode.getType() == boolType);
-
- // ensure it's a constant
- Assert(resultNode.isConst());
-
- Assert(as.isVar());
- res.emplace_back(as.toExpr(), resultNode.toExpr());
- }
- }
- return res;
-}
-
// TODO(#1108): Simplify the error reporting of this method.
Model* SmtEngine::getModel() {
Trace("smt") << "SMT getModel()" << endl;
size_t getNumUserLevels() const;
/** Return the current mode of the solver. */
SmtMode getSmtMode() const;
+ /**
+ * Whether the SmtMode allows for get-value, get-model, get-assignment, etc.
+ * This is equivalent to:
+ * getSmtMode()==SmtMode::SAT || getSmtMode()==SmtMode::SAT_UNKNOWN
+ */
+ bool isSmtModeSat() const;
/**
* Returns the most recent result of checkSat/checkEntailed or
* (set-info :status).
*/
std::vector<Node> getValues(const std::vector<Node>& exprs);
- /**
- * Add a function to the set of expressions whose value is to be
- * later returned by a call to getAssignment(). The expression
- * should be a Boolean zero-ary defined function or a Boolean
- * variable. Rather than throwing a ModalException on modal
- * failures (not in interactive mode or not producing assignments),
- * this function returns true if the expression was added and false
- * if this request was ignored.
- */
- bool addToAssignment(const Expr& e);
-
- /**
- * Get the assignment (only if immediately preceded by a SAT or
- * 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();
-
/** Print all instantiations made by the quantifiers module. */
void printInstantiations(std::ostream& out);
DefinedFunctionMap;
/** The type of our internal assertion list */
typedef context::CDList<Node> AssertionList;
- /** The type of our internal assignment set */
- typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
// disallow copy/assignment
SmtEngine(const SmtEngine&) = delete;
std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
/** The solver for quantifier elimination queries */
std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
- /**
- * List of items for which to retrieve values using getAssignment().
- */
- AssignmentSet* d_assignments;
-
/**
* The logic we're in. This logic may be an extension of the logic set by the
* user.
regress0/logops.04.cvc
regress0/logops.05.cvc
regress0/model-core.smt2
+ regress0/named-expr-use.smt2
regress0/nl/coeff-sat.smt2
regress0/nl/ext-rew-aggr-test.smt2
regress0/nl/iand-no-init.smt2
--- /dev/null
+(set-logic QF_LIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (or (= x 5) (= x 7)))
+(assert (or (! (= x 5) :named foo) (= x y)))
+
+(assert (= foo (= x 7)))
+
+(check-sat)
projects / cvc5.git / commitdiff