diff options
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; } |