Eliminating spurious replay of commands for define funs expansion when checking unsat...

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.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 59df10195650497d91ef90bfcd2bf6df6bb7f890..98e86547831e906a955e4adc827889637df47c4e 100644 (file)
--- 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 28dc8726bab127f313b95628ac3b6f6233d43b37..99c4a67d3f09d069ca6cfa8b65f994a94dd6a495 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1114,12 +1114,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.