From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 15 Aug 2020 11:41:28 +0000 (-0500)
Subject: Add finishInit method to PropEngine (#4895)
X-Git-Tag: cvc5-1.0.0~2999
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc2748198fb2c404b31a144fcad67379b3089e3d;p=cvc5.git

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 c9d0b95b5..f74e52509 100644
--- 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 7f1d5ef65..9a2daee49 100644
--- 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 e0837c7cf..a31d84587 100644
--- 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()