From c5eb77b96cd67b8d80ee8901a3f0b5ae7d54aab2 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 25 Aug 2020 15:00:11 -0300 Subject: Eliminating spurious replay of commands for define funs expansion when checking unsat cores (#4941) Doing it via commands being added to the coreChecker SMT engine is not necessary since we can directly add assertions after expansion from the original SMT engine. --- src/smt/smt_engine.cpp | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) (limited to 'src/smt/smt_engine.cpp') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 59df10195..98e865478 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -157,7 +157,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_abductSolver(nullptr), d_quantElimSolver(nullptr), d_assignments(nullptr), - d_defineCommands(), d_logic(), d_originalOptions(), d_isInternalSubsolver(false), @@ -714,10 +713,6 @@ void SmtEngine::defineFunction(Expr func, d_dumpm->addToModelCommandAndDump( c, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); - PROOF(if (options::checkUnsatCores()) { - d_defineCommands.push_back(c.clone()); - }); - // type check body debugCheckFunctionBody(formula, formals, func); @@ -1555,17 +1550,12 @@ void SmtEngine::checkUnsatCore() { coreChecker.getOptions().set(options::checkUnsatCores, false); coreChecker.getOptions().set(options::checkProofs, false); - PROOF( - std::vector::const_iterator itg = d_defineCommands.begin(); - for (; itg != d_defineCommands.end(); ++itg) { - (*itg)->invoke(&coreChecker); - } - ); - 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(Node::fromExpr(*i)); + Node assertionAfterExpansion = expandDefinitions(Node::fromExpr(*i)); + Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i + << ", expanded to " << assertionAfterExpansion << "\n"; + coreChecker.assertFormula(assertionAfterExpansion); } Result r; try { @@ -1618,7 +1608,7 @@ void SmtEngine::checkModel(bool hardFailure) { Assert(te != nullptr); te->checkTheoryAssertionsWithModel(hardFailure); } - + // Output the model Notice() << *m; -- cgit v1.2.3