diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 12 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 42 |
2 files changed, 23 insertions, 31 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index ecd3c6f16..b1936d8cc 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1358,8 +1358,7 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) this->DefineFunctionCommand::invoke(smtEngine); if (!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment( - d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + smtEngine->addToAssignment(d_func); } d_commandStatus = CommandSuccess::instance(); } @@ -1751,14 +1750,7 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) for (const auto& p : assignments) { vector<SExpr> v; - if (p.first.getKind() == kind::APPLY) - { - v.emplace_back(SExpr::Keyword(p.first.getOperator().toString())); - } - else - { - v.emplace_back(SExpr::Keyword(p.first.toString())); - } + v.emplace_back(SExpr::Keyword(p.first.toString())); v.emplace_back(SExpr::Keyword(p.second.toString())); sexprs.emplace_back(v); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d035f88c1..66198946f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2734,13 +2734,20 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node if(n.isVar()) { SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n); if(i != d_smt.d_definedFunctions->end()) { + Node f = (*i).second.getFormula(); + // must expand its definition + Node fe = expandDefinitions(f, cache, expandOnly); // replacement must be closed if((*i).second.getFormals().size() > 0) { - result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula())); + result.push(d_smt.d_nodeManager->mkNode( + kind::LAMBDA, + d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, + (*i).second.getFormals()), + fe)); continue; } // don't bother putting in the cache - result.push((*i).second.getFormula()); + result.push(fe); continue; } // don't bother putting in the cache @@ -2758,11 +2765,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node // otherwise expand it bool doExpand = false; - if (k == kind::APPLY) - { - doExpand = true; - } - else if (k == kind::APPLY_UF) + if (k == kind::APPLY_UF) { // Always do beta-reduction here. The reason is that there may be // operators such as INTS_MODULUS in the body of the lambda that would @@ -2775,10 +2778,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node { doExpand = true; } - else if (options::macrosQuant() || options::sygusInference()) + else { - // The above options assign substitutions to APPLY_UF, thus we check - // here and expand if this operator corresponds to a defined function. + // We always check if this operator corresponds to a defined function. doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr()); } } @@ -3969,8 +3971,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv, { children.insert(children.end(), vars.begin(), vars.end()); } - terms[i] = - d_nodeManager->mkNode(i == 0 ? kind::APPLY_UF : kind::APPLY, children); + terms[i] = d_nodeManager->mkNode(kind::APPLY_UF, children); // make application of Inv on primed variables if (i == 0) { @@ -4218,15 +4219,15 @@ bool SmtEngine::addToAssignment(const Expr& ex) { "expected Boolean-typed variable or function application " "in addToAssignment()" ); Node n = e.getNode(); - // must be an APPLY of a zero-ary defined function, or a variable + // must be a defined constant, or a variable PrettyCheckArgument( - ( ( n.getKind() == kind::APPLY && - ( d_definedFunctions->find(n.getOperator()) != - d_definedFunctions->end() ) && - n.getNumChildren() == 0 ) || - n.isVar() ), e, + (((d_definedFunctions->find(n) != d_definedFunctions->end()) + && n.getNumChildren() == 0) + || n.isVar()), + e, "expected variable or defined-function application " - "in addToAssignment(),\ngot %s", e.toString().c_str() ); + "in addToAssignment(),\ngot %s", + e.toString().c_str()); if(!options::produceAssignments()) { return false; } @@ -4295,8 +4296,7 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment() // ensure it's a constant Assert(resultNode.isConst()); - Assert(as.getKind() == kind::APPLY || as.isVar()); - Assert(as.getKind() != kind::APPLY || as.getNumChildren() == 0); + Assert(as.isVar()); res.emplace_back(as.toExpr(), resultNode.toExpr()); } } |