Fix caching in TheoryEngine::getExplanation() (#4736)

Commit 64a7db86206aa0993f75446a3e7f77f3c0c023c6 introduced a caching
mechanism in `TheoryEngine::getExplanation()`. However, there seem to be
issues related to the timestamps of the explanations. This commit fixes
the issue by making the timestamp part of the cache. The change ensures
that explanations for a certain node never rely on other explanations
for that node with a later timestamp.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2bbdcceb311bbea1ebec6daaff94b79bc6035999..4bca07170bc46b386d4853b0db7fd68cf5683494 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1788,7 +1788,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     }
   });
   // cache of nodes we have already explained by some theory
-  std::unordered_set<Node, NodeHashFunction> cache;
+  std::unordered_map<Node, size_t, NodeHashFunction> cache;
 
   while (i < explanationVector.size()) {
     // Get the current literal to explain
@@ -1799,6 +1799,14 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
         << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
         << toExplain.d_theory << endl;
 
+    if (cache.find(toExplain.d_node) != cache.end()
+        && cache[toExplain.d_node] < toExplain.d_timestamp)
+    {
+      ++i;
+      continue;
+    }
+    cache[toExplain.d_node] = toExplain.d_timestamp;
+
     // If a true constant or a negation of a false constant we can ignore it
     if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
     {
@@ -1870,16 +1878,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
         continue;
       }
     }
-    // We must cache after checking the timestamp in the block of code above.
-    // Afterwards, we can ignore this timestamp, as well as caching the Node,
-    // since any theory's explanation will suffice.
-    if (cache.find(toExplain.d_node) != cache.end())
-    {
-      ++i;
-      continue;
-    }
-    cache.insert(toExplain.d_node);
-    // It was produced by the theory, so ask for an explanation
+
     Node explanation;
     if (toExplain.d_theory == THEORY_BUILTIN)
     {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 18bf6d104eba66ecab2174281cb03a630d4d3187..5072e5a176eaeab3bc9e4c83757c3e861e61d3ab 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1801,6 +1801,8 @@ set(regress_1_tests
   regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
   regress1/strings/issue4379.smt2
   regress1/strings/issue4608-re-derive.smt2
+  regress1/strings/issue4735.smt2
+  regress1/strings/issue4735_2.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
index 65e705fa3769b3f560bb84f259731df265f0cf62..2ec7d76f07975962d1fc7b4a0b8e05d2c1b40bb2 100644 (file)
--- a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
+++ b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE: --no-check-models --nl-ext-tplanes
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_NRA)

diff --git a/test/regress/regress1/strings/issue4735.smt2 b/test/regress/regress1/strings/issue4735.smt2
new file mode 100644 (file)
index 0000000..d0c9aee
--- /dev/null
+++ b/test/regress/regress1/strings/issue4735.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE: --strings-fmf
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun a () String)
+(declare-fun b () Int)
+(declare-fun c () String)
+(declare-fun d () String)
+(declare-fun e () String)
+(declare-fun f () String)
+(declare-fun g () String)
+(declare-fun h () String)
+(declare-fun i () Bool)
+(declare-fun j () String)
+(declare-fun k () String)
+(assert (= e "0000000000"))
+(assert (distinct a d))
+(assert
+ (ite (distinct b 0)
+ (and (= (str.++ d e) (str.++ c j))
+  (= (str.len c) 2)
+  (= j (str.++ f k))
+  (= f (str.++ g h))
+  (str.in_re g (str.to_re "A")))
+ (str.in_re j (str.to_re ""))))
+(assert (distinct i (= b 0)))
+(assert i)
+(check-sat)

diff --git a/test/regress/regress1/strings/issue4735_2.smt2 b/test/regress/regress1/strings/issue4735_2.smt2
new file mode 100644 (file)
index 0000000..2c92a51
--- /dev/null
+++ b/test/regress/regress1/strings/issue4735_2.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-fmf
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (distinct b (str.++ a a)))
+(assert (str.in_re (str.++ b "\x2f" b) (re.++ (re.opt re.allchar) (str.to_re "\x2f\x65") re.all)))
+(check-sat)