From 9e6ca7166cc2c3444429ee691f7b0c32281eddf1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Feb 2021 19:14:01 -0600 Subject: [PATCH] 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. --- src/theory/sets/theory_sets_private.cpp | 1 - src/theory/theory_engine.cpp | 4 +++- test/regress/CMakeLists.txt | 1 + .../regress/regress1/sets/issue4124-need-check.smt2 | 13 +++++++++++++ 4 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/sets/issue4124-need-check.smt2 diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5558b95d4..0d1206dec 100644 --- 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 0fd8347c8..9ba97fa77 100644 --- 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 e158f629a..82ef8702a 100644 --- 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 index 000000000..3ad43ea98 --- /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) -- 2.30.2