diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-15 06:41:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-15 06:41:28 -0500 |
| commit | dc2748198fb2c404b31a144fcad67379b3089e3d (patch) | |
| tree | 24b2d5335af2f1c84b8e51ca9284d8a7fde49216 /src/prop/prop_engine.cpp | |
| parent | 3b230077d51c8445328f0b5d5ff94bbd988d1c83 (diff) | |
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.
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
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( |