From: Andrew Reynolds Date: Sun, 23 Feb 2020 05:41:42 +0000 (-0600) Subject: Minor refactoring of equality notifications (#3798) X-Git-Tag: cvc5-1.0.0~3615 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6f379f2b83a28995aa77504da1931a598b54bcc0;p=cvc5.git 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. --- diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 2fc49d8b7..5eb0818b7 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -206,6 +206,35 @@ const context::CDList& SolverState::getDisequalityList() const return d_eeDisequalities; } +void SolverState::eqNotifyNewClass(TNode t) +{ + Kind k = t.getKind(); + if (k == STRING_LENGTH || k == STRING_CODE) + { + Node r = d_ee.getRepresentative(t[0]); + EqcInfo* ei = getOrMakeEqcInfo(r); + if (k == STRING_LENGTH) + { + ei->d_lengthTerm = t[0]; + } + else + { + ei->d_codeTerm = t[0]; + } + } + else if (k == CONST_STRING) + { + EqcInfo* ei = getOrMakeEqcInfo(t); + ei->d_prefixC = t; + ei->d_suffixC = t; + return; + } + else if (k == STRING_CONCAT) + { + addEndpointsToEqcInfo(t, t, t); + } +} + void SolverState::eqNotifyPreMerge(TNode t1, TNode t2) { EqcInfo* e2 = getOrMakeEqcInfo(t2, false); diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 28dfbfd09..b295ba12d 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -121,6 +121,8 @@ class SolverState const context::CDList& getDisequalityList() const; //-------------------------------------- end equality information //-------------------------------------- notifications for equalities + /** called when a new equivalence class is created */ + void eqNotifyNewClass(TNode t); /** called when two equivalence classes will merge */ void eqNotifyPreMerge(TNode t1, TNode t2); /** called when two equivalence classes are made disequal */ 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, diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index e0fca1b2e..79681a5f9 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -124,18 +124,21 @@ class TheoryStrings : public Theory { // NotifyClass for equality engine class NotifyClass : public eq::EqualityEngineNotify { - TheoryStrings& d_str; public: - NotifyClass(TheoryStrings& t_str): d_str(t_str) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) override - { - Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_str.propagate(equality); - } else { - // We use only literal triggers so taking not is safe - return d_str.propagate(equality.notNode()); - } + NotifyClass(TheoryStrings& ts) : d_str(ts), d_state(ts.d_state) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { + Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality + << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) + { + return d_str.propagate(equality); + } + else + { + // We use only literal triggers so taking not is safe + return d_str.propagate(equality.notNode()); + } } bool eqNotifyTriggerPredicate(TNode predicate, bool value) override { @@ -143,7 +146,7 @@ class TheoryStrings : public Theory { if (value) { return d_str.propagate(predicate); } else { - return d_str.propagate(predicate.notNode()); + return d_str.propagate(predicate.notNode()); } } bool eqNotifyTriggerTermEquality(TheoryId tag, @@ -153,9 +156,9 @@ class TheoryStrings : public Theory { { Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { - return d_str.propagate(t1.eqNode(t2)); + return d_str.propagate(t1.eqNode(t2)); } else { - return d_str.propagate(t1.eqNode(t2).notNode()); + return d_str.propagate(t1.eqNode(t2).notNode()); } } void eqNotifyConstantTermMerge(TNode t1, TNode t2) override @@ -171,18 +174,23 @@ class TheoryStrings : public Theory { void eqNotifyPreMerge(TNode t1, TNode t2) override { Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; - d_str.eqNotifyPreMerge(t1, t2); + d_state.eqNotifyPreMerge(t1, t2); } void eqNotifyPostMerge(TNode t1, TNode t2) override { Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; - d_str.eqNotifyPostMerge(t1, t2); } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override { Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; - d_str.eqNotifyDisequal(t1, t2, reason); + d_state.eqNotifyDisequal(t1, t2, reason); } + + private: + /** The theory of strings object to notify */ + TheoryStrings& d_str; + /** The solver state of the theory of strings */ + SolverState& d_state; };/* class TheoryStrings::NotifyClass */ //--------------------------- helper functions @@ -280,12 +288,6 @@ private: void conflict(TNode a, TNode b); /** called when a new equivalence class is created */ void eqNotifyNewClass(TNode t); - /** called when two equivalence classes will merge */ - void eqNotifyPreMerge(TNode t1, TNode t2); - /** called when two equivalence classes have merged */ - void eqNotifyPostMerge(TNode t1, TNode t2); - /** called when two equivalence classes are made disequal */ - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); protected: /** compute care graph */