diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-08 20:03:39 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-08 18:03:39 -0700 |
commit | d0559a21f2ca71e8eaf5978e5c0707d7cf11499f (patch) | |
tree | 4846f9bc1469e22699c1ec98aa161d17f73453c6 /src | |
parent | 55acdeb493ee3f9b66ed38f7526670b6e66c46bd (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/ext_theory.cpp | 1 | ||||
-rw-r--r-- | 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; } |