Do not combine theories if theory engine needs check (#5861)

In rare cases, theory combination would be run when theory engine still needs check. This was limited to cases where the output channel is used but no lemmas were sent (TheoryEngine::needCheck() vs. d_lemmasAdded).

This led to problems in the theory of sets, which does not run a full effort check if theory engine needs check (since it knows it will be called to check again). However, running theory combination in these cases is not safe since theory of sets computes information pertaining to the care graph during its full effort check. Running theory combination otherwise would lead to theory of sets using stale data, leading to crashes due to terms not appearing in the equality engine.

This fixes #4124 (which appears not to trigger on master anyways currently).

This bug has also appeared on my sat relevancy development branch, hence fixing on master.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 5558b95d4d0661b482ccb4c8c4df62cd29a75753..0d1206dec9087ff48015f10eec17b5ed4a081528 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -981,7 +981,6 @@ void TheorySetsPrivate::computeCareGraph()
       // populate indices
       for (TNode f1 : it.second)
       {
-        Assert(d_equalityEngine->hasTerm(f1));
         Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
         Assert(d_equalityEngine->hasTerm(f1));
         // break into index based on operator, and type of first argument (since

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0fd8347c86edeb710f31c15003d0efeeaa84e43b..9ba97fa778b096401459f94bb6e2580a65e27d80 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -504,7 +504,9 @@ void TheoryEngine::check(Theory::Effort effort) {
       propagate(effort);
 
       // We do combination if all has been processed and we are in fullcheck
-      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
+      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled()
+          && !d_factsAsserted && !needCheck() && !d_inConflict)
+      {
         // Do the combination
         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
         {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e158f629a0f528c97c33cf5cfa28eead47d41365..82ef8702a481fc566aaeb0fd96e9f0c941eca51f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1953,6 +1953,7 @@ set(regress_1_tests
   regress1/sets/is_singleton1.smt2
   regress1/sets/issue2568.smt2
   regress1/sets/issue2904.smt2
+  regress1/sets/issue4124-need-check.smt2
   regress1/sets/issue4391-card-lasso.smt2
   regress1/sets/issue5271.smt2
   regress1/sets/issue5309.smt2

diff --git a/test/regress/regress1/sets/issue4124-need-check.smt2 b/test/regress/regress1/sets/issue4124-need-check.smt2
new file mode 100644 (file)
index 0000000..3ad43ea
--- /dev/null
+++ b/test/regress/regress1/sets/issue4124-need-check.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --sets-infer-as-lemmas --simplification=none
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun b () (Set (Tuple String Int))) 
+(declare-fun c () (Set (Tuple Int String))) 
+(declare-fun d () (Set (Tuple String String))) 
+(declare-fun f () (Set Int)) 
+(declare-fun e () Int) 
+(assert (= b (insert (mkTuple "" 1)  (mkTuple "" 2) (singleton (mkTuple "" 4))))) 
+(assert (= c (insert (mkTuple 1 "1") (mkTuple 2 "2") (singleton (mkTuple 7 ""))))) 
+(assert (= d (join b c)))    
+(assert (= e (card f))) 
+(check-sat)