Add finishInit method to PropEngine (#4895)

This changes an initialization issue in regarding PropEngine and TheoryEngine.

In the constructor for PropEngine, we convert and assert literals for true and false to CNF stream. Doing so triggers several things, including calls that preregister these literals with the associated TheoryEngine. This means that literals are preregistered to TheoryEngine before it has been fully initialized (TheoryEngine::finishInit). This is not currently an issue since this only involves modules that are constructed statically (e.g. SharedTermsDatabase), but this will lead to issues when the TheoryEngine is more configurable.

The solution is to additionally have a PropEngine::finishInit, which is called after TheoryEngine::finishInit, which does this step. The PropEngine should not assert anything to CNF before this method is called.

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c9d0b95b5e7c3bffdca5b64a486fc69bace9fa17..f74e525092130d38faf99757d0b6ecbfcbb43933 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -102,7 +102,10 @@ PropEngine::PropEngine(TheoryEngine* te,
   PROOF (
          ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
          );
+}
 
+void PropEngine::finishInit()
+{
   NodeManager* nm = NodeManager::currentNM();
   d_cnfStream->convertAndAssert(nm->mkConst(true), false, false, RULE_GIVEN);
   d_cnfStream->convertAndAssert(

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 7f1d5ef65bd4d3838de46d30d44d4c2476a349a3..9a2daee49ab4f5a06bbe342d8db82940b50cbf7c 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -69,6 +69,13 @@ class PropEngine
    */
   CVC4_PUBLIC ~PropEngine();
 
+  /**
+   * Finish initialize. Call this after construction just before we are
+   * ready to use this class. Should be called after TheoryEngine::finishInit.
+   * This method converts and asserts true and false into the CNF stream.
+   */
+  void finishInit();
+
   /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index e0837c7cfe6142224bdc418778a655169a6af1d0..a31d84587782ba49b5197afd0d5bba68c46fa89a 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -77,6 +77,7 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
   d_theoryEngine->setPropEngine(getPropEngine());
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
+  d_propEngine->finishInit();
 }
 
 void SmtSolver::resetAssertions()
@@ -92,6 +93,7 @@ void SmtSolver::resetAssertions()
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
   // depend on knowing the associated PropEngine.
+  d_propEngine->finishInit();
 }
 
 void SmtSolver::interrupt()