Fix string register extended terms (#2597)

A regress2 benchmark was failing, due to a recent change in our strings rewriter.

The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.

The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.

This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.

diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 7cc8627ebf8ef738f796a943358fbbda62c81c5e..589ec45c0b8fb56cc98207c5e2ecccef6f9d75ab 100644 (file)
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -427,6 +427,7 @@ void ExtTheory::registerTermRec(Node n)
 // mark reduced
 void ExtTheory::markReduced(Node n, bool contextDepend)
 {
+  Trace("extt-debug") << "Mark reduced " << n << std::endl;
   registerTerm(n);
   Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
   d_ext_func_terms[n] = false;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index bc9c198154627f633ad4793104e8493aaff50a16..26ff9188f25acde1f27ad8b31e360e47981d0775 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -266,6 +266,10 @@ void TheoryStrings::addSharedTerm(TNode t) {
   Debug("strings") << "TheoryStrings::addSharedTerm(): "
                      << t << " " << t.getType().isBoolean() << endl;
   d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
+  if (options::stringExp())
+  {
+    getExtTheory()->registerTermRec(t);
+  }
   Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
 }
 
@@ -850,11 +854,6 @@ void TheoryStrings::preRegisterTerm(TNode n) {
         } else {
           // Function applications/predicates
           d_equalityEngine.addTerm(n);
-          if( options::stringExp() ){
-            //collect extended functions here: some may not be asserted to strings (such as those with return type Int),
-            //  but we need to record them so they are treated properly
-            getExtTheory()->registerTermRec( n );
-          }
         }
         //concat terms do not contribute to theory combination?  TODO: verify
         if (n.hasOperator() && kindToTheoryId(k) == THEORY_STRINGS
@@ -1213,7 +1212,9 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
     //getExtTheory()->registerTerm( atom );
   }
   Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
-  //collect extended function terms in the atom
+  // Collect extended function terms in the atom. Notice that we must register
+  // all extended functions occurring in assertions and shared terms. We
+  // make a similar call to registerTermRec in addSharedTerm.
   getExtTheory()->registerTermRec( atom );
   Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
 }