From d0559a21f2ca71e8eaf5978e5c0707d7cf11499f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 8 Oct 2018 20:03:39 -0500 Subject: [PATCH] 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. --- src/theory/ext_theory.cpp | 1 + src/theory/strings/theory_strings.cpp | 13 +++++++------ 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index 7cc8627eb..589ec45c0 100644 --- 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 bc9c19815..26ff9188f 100644 --- 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; } -- 2.30.2