Guard for non-unique skolems in term formula removal (#6179)

In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.

Fixes #6132.

diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 1cb048cf2412e96cd1f0e640f3e695998ad2f45e..44a8f87c2812ac901717489cc480b954e983385b 100644 (file)
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -161,6 +161,15 @@ class SkolemManager
    *
    * Notice that a purification skolem is trivial to justify, and hence it
    * does not require a proof generator.
+   *
+   * Notice that in very rare cases, two different terms may have the
+   * same purification skolem. For example, let k be the skolem introduced to
+   * eliminate (ite A B C). Then, the pair of terms:
+   *  (ite (ite A B C) D E) and (ite k D E)
+   * have the same purification skolem. In the implementation, this is a result
+   * of the fact that the above terms have the same original form. It is sound
+   * to use the same skolem to purify these two terms, since they are
+   * definitionally equivalent.
    */
   Node mkPurifySkolem(Node t,
                       const std::string& prefix,

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index d1bb4f5b8cf7e1f401e71e39b8c88d93444a0cfc..6f2f77a144126c4adabd044ff156009cb4026b74 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -292,6 +292,12 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
           "a variable introduced due to term-level ITE removal");
       d_skolem_cache.insert(node, skolem);
 
+      // Notice that in very rare cases, two different terms may have the
+      // same purification skolem (see SkolemManager::mkPurifySkolem) For such
+      // cases, for simplicity, we repeat the work of constructing the
+      // assertion and proofs below. This is so that the proof for the new form
+      // of the lemma is used.
+
       // The new assertion
       newAssertion = nodeManager->mkNode(
           kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
@@ -497,8 +503,11 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
 
       newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
 
-      // store in the lemma cache
-      d_lemmaCache.insert(skolem, newLem);
+      // store in the lemma cache, if it is not already there.
+      if (d_lemmaCache.find(skolem) == d_lemmaCache.end())
+      {
+        d_lemmaCache.insert(skolem, newLem);
+      }
 
       Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
       newLem.debugCheckClosed("rtf-proof-debug",

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a98ea84bb35d6d0dcfbf362cb9198c4636ed9fa2..6ae77b38b8744ac1d6bd16dca46a65dd357502e9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2038,6 +2038,7 @@ set(regress_1_tests
   regress1/strings/issue5940-2-skc-len-conc.smt2
   regress1/strings/issue6072-inc-no-const-reg.smt2
   regress1/strings/issue6075-repl-len-one-rr.smt2
+  regress1/strings/issue6132-non-unique-skolem.smt2
   regress1/strings/issue6142-repl-inv-rew.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2

diff --git a/test/regress/regress1/strings/issue6132-non-unique-skolem.smt2 b/test/regress/regress1/strings/issue6132-non-unique-skolem.smt2
new file mode 100644 (file)
index 0000000..29d0e94
--- /dev/null
+++ b/test/regress/regress1/strings/issue6132-non-unique-skolem.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun str () String)                                                        
+(assert (= 0 (ite (= str (str.from_code 
+             (ite (= 0 (ite (> (str.len (str.from_int (str.len str))) 1) 1 0)) 1 0))) 1 0)))
+(check-sat)