diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-22 23:41:42 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-22 21:41:42 -0800 |
commit | 6f379f2b83a28995aa77504da1931a598b54bcc0 (patch) | |
tree | 4133e6a9100d2cf68f0b00e10c6492059207d8f0 /src/theory/strings/theory_strings.cpp | |
parent | b70c2eb3fe78f6985fda3086a52d0d74aecb78c2 (diff) |
Minor refactoring of equality notifications (#3798)
Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 54 |
1 files changed, 2 insertions, 52 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d3d75a98d..92af3cc0a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -88,19 +88,6 @@ TheoryStrings::TheoryStrings(context::Context* c, d_esolver.reset(new ExtfSolver( c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt)); d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u)); - getExtTheory()->addFunctionKind(kind::STRING_SUBSTR); - getExtTheory()->addFunctionKind(kind::STRING_STRIDOF); - getExtTheory()->addFunctionKind(kind::STRING_ITOS); - getExtTheory()->addFunctionKind(kind::STRING_STOI); - getExtTheory()->addFunctionKind(kind::STRING_STRREPL); - getExtTheory()->addFunctionKind(kind::STRING_STRREPLALL); - getExtTheory()->addFunctionKind(kind::STRING_STRCTN); - getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP); - getExtTheory()->addFunctionKind(kind::STRING_LEQ); - getExtTheory()->addFunctionKind(kind::STRING_CODE); - getExtTheory()->addFunctionKind(kind::STRING_TOLOWER); - getExtTheory()->addFunctionKind(kind::STRING_TOUPPER); - getExtTheory()->addFunctionKind(kind::STRING_REV); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); @@ -740,52 +727,15 @@ void TheoryStrings::conflict(TNode a, TNode b){ } } -/** called when a new equivalance class is created */ void TheoryStrings::eqNotifyNewClass(TNode t){ Kind k = t.getKind(); - if (k == kind::STRING_LENGTH || k == kind::STRING_CODE) + if (k == STRING_LENGTH || k == STRING_CODE) { Trace("strings-debug") << "New length eqc : " << t << std::endl; - Node r = d_equalityEngine.getRepresentative(t[0]); - EqcInfo* ei = d_state.getOrMakeEqcInfo(r); - if (k == kind::STRING_LENGTH) - { - ei->d_lengthTerm = t[0]; - } - else - { - ei->d_codeTerm = t[0]; - } //we care about the length of this string registerTerm( t[0], 1 ); - return; - } - else if (k == CONST_STRING) - { - EqcInfo* ei = d_state.getOrMakeEqcInfo(t); - ei->d_prefixC = t; - ei->d_suffixC = t; - return; } - else if (k == STRING_CONCAT) - { - d_state.addEndpointsToEqcInfo(t, t, t); - } -} - -/** called when two equivalance classes will merge */ -void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ - d_state.eqNotifyPreMerge(t1, t2); -} - -/** called when two equivalance classes have merged */ -void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) { - -} - -/** called when two equivalance classes are disequal */ -void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - d_state.eqNotifyDisequal(t1, t2, reason); + d_state.eqNotifyNewClass(t); } void TheoryStrings::addCarePairs(TNodeTrie* t1, |