diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-13 23:43:10 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-13 23:43:10 -0700 |
commit | ffb7947f8e3709eaf73de5d0f6f97379a90ecc57 (patch) | |
tree | 8e26068cc9dad41d4d7cb1fa360f4bc0dde8b96e | |
parent | 442ab0cdd8578631974318c17dd8ace59d145839 (diff) |
Create master equality engine at context level 0
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.
-rw-r--r-- | src/smt/smt_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 5 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/smtlib/issue4077.smt2 | 11 |
4 files changed, 22 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5fc0189c3..d2919143b 100644 --- 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 693b7bd66..b6896e45d 100644 --- 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 a68c31441..d822ce157 100644 --- 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 index 000000000..76a37886b --- /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) |