From 245e6dad30c9077e3212fa5fcfbe3f7dd8b35bd6 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 11 Jul 2020 16:45:06 -0700 Subject: Towards Node-level SmtEngine --- src/api/cvc4cpp.cpp | 2 +- src/preprocessing/passes/sygus_inference.cpp | 2 +- src/smt/smt_engine.cpp | 117 ++++++++++----------- src/smt/smt_engine.h | 6 +- .../quantifiers/sygus/cegis_core_connective.cpp | 2 +- src/theory/smt_engine_subsolver.cpp | 2 +- 6 files changed, 65 insertions(+), 66 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 3439fd1d0..0619d7878 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4220,7 +4220,7 @@ void Solver::assertFormula(Term term) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_NOT_NULL(term); - d_smtEngine->assertFormula(*term.d_expr); + d_smtEngine->assertFormula(Node::fromExpr(*term.d_expr)); CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 4500c7880..2ffe7e0ce 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -303,7 +303,7 @@ bool SygusInference::solveSygus(std::vector& assertions, SmtEngine* currSmt = smt::currentSmtEngine(); SmtEngine rrSygus(nm->toExprManager(), &currSmt->getOptions()); rrSygus.setLogic(currSmt->getLogicInfo()); - rrSygus.assertFormula(body.toExpr()); + rrSygus.assertFormula(body); Trace("sygus-infer") << "*** Check sat..." << std::endl; Result r = rrSygus.checkSat(); Trace("sygus-infer") << "...result : " << r << std::endl; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0d8189aa4..e94520021 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1263,8 +1263,7 @@ void SmtEngine::defineFunction(Expr func, debugCheckFunctionBody(formula, formals, func); // Substitute out any abstract values in formula - Expr form = - d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr(); + Node formNode = d_private->substituteAbstractValues(Node::fromExpr(formula)); TNode funcNode = func.getTNode(); vector formalsNodes; @@ -1274,7 +1273,6 @@ void SmtEngine::defineFunction(Expr func, ++i) { formalsNodes.push_back((*i).getNode()); } - TNode formNode = form.getTNode(); DefinedFunction def(funcNode, formalsNodes, formNode); // Permit (check-sat) (define-fun ...) (get-value ...) sequences. // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks @@ -1371,21 +1369,21 @@ void SmtEngine::defineFunctionsRec( // assert the quantified formula // notice we don't call assertFormula directly, since this would // duplicate the output on raw-benchmark. - Expr e = d_private->substituteAbstractValues(Node::fromExpr(lem)).toExpr(); + Node n = d_private->substituteAbstractValues(Node::fromExpr(lem)); if (d_assertionList != nullptr) { - d_assertionList->push_back(e); + d_assertionList->push_back(n); } if (global && d_globalDefineFunRecLemmas != nullptr) { // Global definitions are asserted at check-sat-time because we have to // make sure that they are always present Assert(!language::isInputLangSygus(options::inputLanguage())); - d_globalDefineFunRecLemmas->emplace_back(Node::fromExpr(e)); + d_globalDefineFunRecLemmas->emplace_back(n); } else { - d_private->addFormula(e.getNode(), false, true, false, maybeHasFv); + d_private->addFormula(n, false, true, false, maybeHasFv); } } } @@ -1609,16 +1607,16 @@ void SmtEnginePrivate::addFormula( //d_assertions.push_back(Rewriter::rewrite(n)); } -void SmtEngine::ensureBoolean(const Expr& e) +void SmtEngine::ensureBoolean(const Node& n) { - Type type = e.getType(options::typeChecking()); - Type boolType = d_exprManager->booleanType(); + TypeNode type = n.getType(options::typeChecking()); + TypeNode boolType = NodeManager::currentNM()->booleanType(); if(type != boolType) { stringstream ss; ss << "Expected " << boolType << "\n" - << "The assertion : " << e << "\n" + << "The assertion : " << n << "\n" << "Its type : " << type; - throw TypeCheckingException(e, ss.str()); + throw TypeCheckingException(n.toExpr(), ss.str()); } } @@ -1727,17 +1725,16 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, for (Expr e : d_assumptions) { // Substitute out any abstract values in ex. - e = d_private->substituteAbstractValues(Node::fromExpr(e)).toExpr(); - Assert(e.getExprManager() == d_exprManager); + Node n = d_private->substituteAbstractValues(Node::fromExpr(e)); // Ensure expr is type-checked at this point. - ensureBoolean(e); + ensureBoolean(n); /* Add assumption */ if (d_assertionList != NULL) { - d_assertionList->push_back(e); + d_assertionList->push_back(n); } - d_private->addFormula(e.getNode(), inUnsatCore, true, true); + d_private->addFormula(n, inUnsatCore, true, true); } if (d_globalDefineFunRecLemmas != nullptr) @@ -1877,28 +1874,27 @@ vector SmtEngine::getUnsatAssumptions(void) return res; } -Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) +Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) { - Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; + Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl; if (Dump.isOn("raw-benchmark")) { - Dump("raw-benchmark") << AssertCommand(ex); + Dump("raw-benchmark") << AssertCommand(formula.toExpr()); } // Substitute out any abstract values in ex - Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + Node n = d_private->substituteAbstractValues(formula); - ensureBoolean(e); + ensureBoolean(n); if(d_assertionList != NULL) { - d_assertionList->push_back(e); + d_assertionList->push_back(n); } bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); - d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv); + d_private->addFormula(n, inUnsatCore, true, false, maybeHasFv); return quickCheck().asEntailmentResult(); }/* SmtEngine::assertFormula() */ @@ -2108,7 +2104,7 @@ Result SmtEngine::checkSynth() // we push a context so that this conjecture is removed if we modify it // later internalPush(); - assertFormula(body.toExpr(), true); + assertFormula(body, true); } else { @@ -2271,23 +2267,22 @@ bool SmtEngine::addToAssignment(const Expr& ex) { finalOptionsAreSet(); doPendingPops(); // Substitute out any abstract values in ex - Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - Type type = e.getType(options::typeChecking()); + Node n = d_private->substituteAbstractValues(Node::fromExpr(ex)); + TypeNode type = n.getType(options::typeChecking()); // must be Boolean - PrettyCheckArgument( - type.isBoolean(), e, - "expected Boolean-typed variable or function application " - "in addToAssignment()" ); - Node n = e.getNode(); + 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()), - e, + n, "expected variable or defined-function application " "in addToAssignment(),\ngot %s", - e.toString().c_str()); + n.toString().c_str()); if(!options::produceAssignments()) { return false; } @@ -2443,7 +2438,7 @@ Result SmtEngine::blockModel() std::vector eassertsProc = getExpandedAssertions(); Expr eblocker = ModelBlocker::getModelBlocker( eassertsProc, m, options::blockModelsMode()); - return assertFormula(eblocker); + return assertFormula(Node::fromExpr(eblocker)); } Result SmtEngine::blockModelValues(const std::vector& exprs) @@ -2468,7 +2463,7 @@ Result SmtEngine::blockModelValues(const std::vector& exprs) // we always do block model values mode here Expr eblocker = ModelBlocker::getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); - return assertFormula(eblocker); + return assertFormula(Node::fromExpr(eblocker)); } std::pair SmtEngine::getSepHeapAndNilExpr(void) @@ -2596,7 +2591,7 @@ void SmtEngine::checkUnsatCore() { Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl; for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl; - coreChecker.assertFormula(*i); + coreChecker.assertFormula(Node::fromExpr(*i)); } Result r; try { @@ -2739,9 +2734,11 @@ void SmtEngine::checkModel(bool hardFailure) { } // Now go through all our user assertions checking if they're satisfied. - for(AssertionList::const_iterator i = d_assertionList->begin(); i != d_assertionList->end(); ++i) { - Notice() << "SmtEngine::checkModel(): checking assertion " << *i << endl; - Node n = Node::fromExpr(*i); + for (const Node& assertion : *d_assertionList) + { + Notice() << "SmtEngine::checkModel(): checking assertion " << assertion + << endl; + Node n = assertion; // Apply any define-funs from the problem. { @@ -2820,7 +2817,7 @@ void SmtEngine::checkModel(bool hardFailure) { stringstream ss; ss << "SmtEngine::checkModel(): " << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl - << "assertion: " << *i << endl + << "assertion: " << assertion << endl << "simplifies to: " << n << endl << "expected `true'." << endl << "Run with `--check-models -v' for additional diagnostics."; @@ -2893,23 +2890,20 @@ void SmtEngine::checkSynthSolution() std::vector auxAssertions; // expand definitions cache std::unordered_map cache; - for (AssertionList::const_iterator i = d_assertionList->begin(); - i != d_assertionList->end(); - ++i) + for (const Node& assertion : *d_assertionList) { - Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i << endl; - Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n"; - Node assertion = Node::fromExpr(*i); + Notice() << "SmtEngine::checkSynthSolution(): checking assertion " + << assertion << endl; + Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n"; // Apply any define-funs from the problem. - assertion = + Node n = d_private->getProcessAssertions()->expandDefinitions(assertion, cache); - Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << assertion - << endl; - Trace("check-synth-sol") << "Expanded assertion " << assertion << "\n"; - if (conjs.find(assertion) == conjs.end()) + Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << n << endl; + Trace("check-synth-sol") << "Expanded assertion " << n << "\n"; + if (conjs.find(n) == conjs.end()) { Trace("check-synth-sol") << "It is an auxiliary assertion\n"; - auxAssertions.push_back(assertion); + auxAssertions.push_back(n); } else { @@ -2953,12 +2947,12 @@ void SmtEngine::checkSynthSolution() << conjBody << endl; Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody << "\n"; - solChecker.assertFormula(conjBody.toExpr()); + solChecker.assertFormula(conjBody); // Assert all auxiliary assertions. This may include recursive function // definitions that were added as assertions to the sygus problem. for (const Node& a : auxAssertions) { - solChecker.assertFormula(a.toExpr()); + solChecker.assertFormula(a); } Result r = solChecker.checkSat(); Notice() << "SmtEngine::checkSynthSolution(): result is " << r << endl; @@ -3008,7 +3002,7 @@ void SmtEngine::checkAbduct(Expr a) << ": asserting formulas" << std::endl; for (const Expr& e : asserts) { - abdChecker.assertFormula(e); + abdChecker.assertFormula(Node::fromExpr(e)); } Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j << ": check the assertions" << std::endl; @@ -3263,7 +3257,7 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) l.enableSygus(); d_subsolver->setLogic(l); // assert the abduction query - d_subsolver->assertFormula(aconj.toExpr()); + d_subsolver->assertFormula(aconj); if (getAbductInternal(abd)) { // successfully generated an abduct, update to abduct state @@ -3398,8 +3392,13 @@ vector SmtEngine::getAssertions() { throw ModalException(msg); } Assert(d_assertionList != NULL); + std::vector res; + for (const Node& n : *d_assertionList) + { + res.emplace_back(n.toExpr()); + } // copy the result out - return vector(d_assertionList->begin(), d_assertionList->end()); + return res; } void SmtEngine::push() diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8db8eadd5..783748c47 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -369,7 +369,7 @@ class CVC4_PUBLIC SmtEngine * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Result assertFormula(const Expr& e, bool inUnsatCore = true); + Result assertFormula(const Node& formula, bool inUnsatCore = true); /** * Check if a given (set of) expression(s) is entailed with respect to the @@ -906,7 +906,7 @@ class CVC4_PUBLIC SmtEngine typedef context::CDHashMap DefinedFunctionMap; /** The type of our internal assertion list */ - typedef context::CDList AssertionList; + typedef context::CDList AssertionList; /** The type of our internal assignment set */ typedef context::CDHashSet AssignmentSet; @@ -1063,7 +1063,7 @@ class CVC4_PUBLIC SmtEngine * * throw@ TypeCheckingException */ - void ensureBoolean(const Expr& e); + void ensureBoolean(const Node& n); void internalPush(); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index de75af083..f1086749e 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -745,7 +745,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts); for (const Node& a : rasserts) { - checkSol->assertFormula(a.toExpr()); + checkSol->assertFormula(a); } Result r = checkSol->checkSat(); Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl; diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 45c115524..747923a17 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -59,7 +59,7 @@ void initializeSubsolver(std::unique_ptr& smte, smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); if (!query.isNull()) { - smte->assertFormula(query.toExpr()); + smte->assertFormula(query); } } -- cgit v1.2.3