From: Andrew Reynolds Date: Wed, 18 Nov 2020 14:34:12 +0000 (-0600) Subject: Use symbol manager for get assignment (#5451) X-Git-Tag: cvc5-1.0.0~2588 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c246952ce90ae7c27b4c0646fce05bc69037f46;p=cvc5.git Use symbol manager for get assignment (#5451) 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. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index a7cc8e17f..1112530d3 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5160,11 +5160,11 @@ std::vector Solver::getValue(const std::vector& terms) const { 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 res; for (size_t i = 0, n = terms.size(); i < n; ++i) { @@ -5222,8 +5222,8 @@ Term Solver::getSeparationHeap() const 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; } @@ -5239,8 +5239,8 @@ Term Solver::getSeparationNilTerm() const 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; } @@ -5330,8 +5330,8 @@ void Solver::printModel(std::ostream& out) const 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; } @@ -5343,8 +5343,8 @@ void Solver::blockModel() const 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; } @@ -5355,8 +5355,8 @@ void Solver::blockModelValues(const std::vector& terms) const 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) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 916e20d9b..2b32afa15 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1841,18 +1841,8 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] | 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(), - expr, - SYM_MAN->getGlobalDeclarations()); - c->setMuted(true); - PARSER_STATE->preemptCommand(c); + // notify that expression was given a name + PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue()); } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 892c628dc..b9279fcb0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1218,28 +1218,16 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) 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& es) diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 734b00f92..fd08ab241 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -343,17 +343,11 @@ class Smt2 : public Parser } 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) diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 76549d01d..8bf3bd24e 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -296,18 +296,6 @@ void AstPrinter::toStreamCmdDefineType(std::ostream& out, out << "]," << t << ')' << std::endl; } -void AstPrinter::toStreamCmdDefineNamedFunction( - std::ostream& out, - const std::string& id, - const std::vector& 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; diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index ce621d8e1..ad20ffb79 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -79,13 +79,6 @@ class AstPrinter : public CVC4::Printer TypeNode range, Node formula) const override; - /** Print define-named-fun command */ - void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector& formals, - TypeNode range, - Node formula) const override; - /** Print check-sat command */ void toStreamCmdCheckSat(std::ostream& out, Node n = Node::null()) const override; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8b252d0ea..44ff7be10 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1410,16 +1410,6 @@ void CvcPrinter::toStreamCmdDefineType(std::ostream& out, } } -void CvcPrinter::toStreamCmdDefineNamedFunction( - std::ostream& out, - const std::string& id, - const std::vector& 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; diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 934caf91b..ee4750a61 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -80,13 +80,6 @@ class CvcPrinter : public CVC4::Printer TypeNode range, Node formula) const override; - /** Print define-named-fun command */ - void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector& formals, - TypeNode range, - Node formula) const override; - /** Print check-sat command */ void toStreamCmdCheckSat(std::ostream& out, Node n = Node::null()) const override; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 21eb88c8c..b24025124 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -184,15 +184,6 @@ void Printer::toStreamCmdDefineFunction(std::ostream& out, printUnknownCommand(out, "define-fun"); } -void Printer::toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector& formals, - TypeNode range, - Node formula) const -{ - printUnknownCommand(out, "define-named-function"); -} - void Printer::toStreamCmdDefineFunctionRec( std::ostream& out, const std::vector& funcs, diff --git a/src/printer/printer.h b/src/printer/printer.h index ffacaa5d8..d32418deb 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -103,13 +103,6 @@ class Printer TypeNode range, Node formula) const; - /** Print define-named-fun command */ - virtual void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector& formals, - TypeNode range, - Node formula) const; - /** Print define-fun-rec command */ virtual void toStreamCmdDefineFunctionRec( std::ostream& out, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6628576dd..bed6a890b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1715,20 +1715,6 @@ void Smt2Printer::toStreamCmdDefineType(std::ostream& out, out << ") " << t << ")" << std::endl; } -void Smt2Printer::toStreamCmdDefineNamedFunction( - std::ostream& out, - const std::string& id, - const std::vector& 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; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 3fc144d46..bc8674275 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -92,13 +92,6 @@ class Smt2Printer : public CVC4::Printer TypeNode range, Node formula) const override; - /** Print define-named-fun command */ - void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector& formals, - TypeNode range, - Node formula) const override; - /** Print define-fun-rec command */ void toStreamCmdDefineFunctionRec( std::ostream& out, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 1e7401fa4..c8362fae1 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1277,57 +1277,6 @@ void DefineFunctionCommand::toStream(std::ostream& out, d_formula.getNode()); } -/* -------------------------------------------------------------------------- */ -/* class DefineNamedFunctionCommand */ -/* -------------------------------------------------------------------------- */ - -DefineNamedFunctionCommand::DefineNamedFunctionCommand( - - const std::string& id, - api::Term func, - const std::vector& 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 */ /* -------------------------------------------------------------------------- */ @@ -1663,20 +1612,30 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - std::vector> assignments = - solver->getSmtEngine()->getAssignment(); - vector sexprs; - for (const auto& p : assignments) + std::map enames = sm->getExpressionNames(); + std::vector terms; + std::vector names; + for (const std::pair& e : enames) { - vector 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 values = solver->getValue(terms); + Assert(values.size() == names.size()); + std::vector sexprs; + for (size_t i = 0, nterms = terms.size(); i < nterms; i++) + { + std::vector 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()); } diff --git a/src/smt/command.h b/src/smt/command.h index 7d794cf3f..85897458d 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -495,28 +495,6 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand 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& 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a5861c6b0..9826cd097 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -102,7 +102,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_abductSolver(nullptr), d_interpolSolver(nullptr), d_quantElimSolver(nullptr), - d_assignments(nullptr), d_logic(), d_originalOptions(), d_isInternalSubsolver(false), @@ -176,6 +175,11 @@ size_t SmtEngine::getNumUserLevels() const 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(); @@ -318,10 +322,6 @@ SmtEngine::~SmtEngine() // 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 @@ -1227,99 +1227,6 @@ std::vector SmtEngine::getValues(const std::vector& exprs) 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> 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> 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 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; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0661ae918..7a55d3b74 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -205,6 +205,12 @@ class CVC4_PUBLIC SmtEngine 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). @@ -548,24 +554,6 @@ class CVC4_PUBLIC SmtEngine */ std::vector getValues(const std::vector& 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 > getAssignment(); - /** Print all instantiations made by the quantifiers module. */ void printInstantiations(std::ostream& out); @@ -907,8 +895,6 @@ class CVC4_PUBLIC SmtEngine DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList AssertionList; - /** The type of our internal assignment set */ - typedef context::CDHashSet AssignmentSet; // disallow copy/assignment SmtEngine(const SmtEngine&) = delete; @@ -1145,11 +1131,6 @@ class CVC4_PUBLIC SmtEngine std::unique_ptr d_interpolSolver; /** The solver for quantifier elimination queries */ std::unique_ptr 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. diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5104b07b8..34f5fdcba 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -606,6 +606,7 @@ set(regress_0_tests 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 diff --git a/test/regress/regress0/named-expr-use.smt2 b/test/regress/regress0/named-expr-use.smt2 new file mode 100644 index 000000000..3c520c3a5 --- /dev/null +++ b/test/regress/regress0/named-expr-use.smt2 @@ -0,0 +1,11 @@ +(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)