Create master equality engine at context level 0 (#4081)

Fixes #4077. The master equality engine in `TheoryEngine` was being
created at SAT context level 1. If the context was popped to level zero
by `(reset-assertions)`, `true` and `false` were removed from the master
equality engine, which lead for example to `(= ((_ extract 3 3) x) (_
bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking
at `-t equality`). This commit fixes the issue by postponing the global
context pushes until after the theory engine has been initialized.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5fc0189c33335be00f5715f24476401dd0cd3818..d2919143b4ab6c6c15665cbb88f70c0f86f29d46 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -925,11 +925,6 @@ void SmtEngine::finishInit()
 
   d_private->addUseTheoryListListener(d_theoryEngine);
 
-  // global push/pop around everything, to ensure proper destruction
-  // of context-dependent data structures
-  d_userContext->push();
-  d_context->push();
-
   // ensure that our heuristics are properly set up
   setDefaults();
 
@@ -951,6 +946,11 @@ void SmtEngine::finishInit()
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
 
+  // global push/pop around everything, to ensure proper destruction
+  // of context-dependent data structures
+  d_userContext->push();
+  d_context->push();
+
   Trace("smt-debug") << "Set up assertion list..." << std::endl;
   // [MGD 10/20/2011] keep around in incremental mode, due to a
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 693b7bd66d4a059ce95838c04210ba132a71fbd7..b6896e45d6510259ea6bd91fac9556b020eb5102 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -81,6 +81,11 @@ void EqualityEngine::init() {
   Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl;
   Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl;
 
+  // If we are not at level zero when we initialize this equality engine, we
+  // may remove true/false from the equality engine when we pop to level zero,
+  // which leads to issues.
+  Assert(d_context->getLevel() == 0);
+
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a68c3144116b60bf70695754623466e4eab03c1d..d822ce1572f1b24e5e9712d0f77df912b55f8656 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -898,6 +898,7 @@ set(regress_0_tests
   regress0/smtlib/get-unsat-assumptions.smt2
   regress0/smtlib/global-decls.smt2
   regress0/smtlib/issue4028.smt2
+  regress0/smtlib/issue4077.smt2
   regress0/smtlib/reason-unknown.smt2
   regress0/smtlib/reset.smt2
   regress0/smtlib/reset-assertions1.smt2

diff --git a/test/regress/regress0/smtlib/issue4077.smt2 b/test/regress/regress0/smtlib/issue4077.smt2
new file mode 100644 (file)
index 0000000..76a3788
--- /dev/null
+++ b/test/regress/regress0/smtlib/issue4077.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+
+; Use a quantified logic to make sure that TheoryEngine creates a master
+; equality engine
+(set-logic BV)
+(declare-const x (_ BitVec 4))
+(push)
+(reset-assertions)
+(assert (bvslt (bvsrem (_ bv1 4) x) (_ bv1 4)))
+(check-sat)

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 0460759bc585faad315b028577d67776e4b7f576..2c696af91d59d053cc4ff4eff63d5b81f9d666ac 100644 (file)
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -114,14 +114,10 @@ public:
     // the following call, which constructs its underlying theory engine.
     d_smt->finalOptionsAreSet();
 
-    // guard against duplicate statistics assertion errors
-    delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH];
-    delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH];
-    d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL;
-    d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
-
-    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
-                              d_logicInfo);
+    d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]->setOutputChannel(
+        d_outputChannel);
+    d_arith = static_cast<TheoryArith*>(
+        d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]);
 
     preregistered = new std::set<Node>();
 
@@ -139,7 +135,6 @@ public:
 
     delete preregistered;
 
-    delete d_arith;
     d_outputChannel.clear();
     delete d_scope;
     delete d_smt;