diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-08-25 15:00:11 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-25 15:00:11 -0300 |
commit | c5eb77b96cd67b8d80ee8901a3f0b5ae7d54aab2 (patch) | |
tree | 24ca2e0802a18c5ec27d50dd793a2b3a6ccf5a41 | |
parent | 16578fca1c50d2ca9fce45c9c262db7ff6e2fd92 (diff) |
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.
-rw-r--r-- | src/smt/smt_engine.cpp | 20 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 6 |
2 files changed, 5 insertions, 21 deletions
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<Command*>::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; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 28dc8726b..99c4a67d3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1115,12 +1115,6 @@ class CVC4_PUBLIC SmtEngine AssignmentSet* d_assignments; /** - * A vector of command definitions to be imported in the new - * SmtEngine when checking unsat-cores. - */ - std::vector<Command*> d_defineCommands; - - /** * The logic we're in. This logic may be an extension of the logic set by the * user. */ |