diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 10:17:30 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 10:17:30 -0600 |
commit | 9b09505bb2a8ed50622b9442700e7f98d010b955 (patch) | |
tree | cdc9b8fe22178cf96346b068eef3377067f92f59 /src/theory/strings/solver_state.cpp | |
parent | abd0048cdb6cf4d2ee0a096c9f7a63a1f7f1d9c8 (diff) |
Move equivalence class info to its own file in strings (#3799)
Code move only, no updates to behavior or content of code in this PR.
Diffstat (limited to 'src/theory/strings/solver_state.cpp')
-rw-r--r-- | src/theory/strings/solver_state.cpp | 114 |
1 files changed, 0 insertions, 114 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 5eb0818b7..422c9e58b 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -24,120 +24,6 @@ namespace CVC4 { namespace theory { namespace strings { -EqcInfo::EqcInfo(context::Context* c) - : d_lengthTerm(c), - d_codeTerm(c), - d_cardinalityLemK(c), - d_normalizedLength(c), - d_prefixC(c), - d_suffixC(c) -{ -} - -Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) -{ - // check conflict - Node prev = isSuf ? d_suffixC : d_prefixC; - if (!prev.isNull()) - { - Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t - << " post=" << isSuf << std::endl; - Node prevC = utils::getConstantEndpoint(prev, isSuf); - Assert(!prevC.isNull()); - Assert(prevC.getKind() == CONST_STRING); - if (c.isNull()) - { - c = utils::getConstantEndpoint(t, isSuf); - Assert(!c.isNull()); - } - Assert(c.getKind() == CONST_STRING); - bool conflict = false; - // if the constant prefixes are different - if (c != prevC) - { - // conflicts between constants should be handled by equality engine - Assert(!t.isConst() || !prev.isConst()); - Trace("strings-eager-pconf-debug") - << "Check conflict constants " << prevC << ", " << c << std::endl; - const String& ps = prevC.getConst<String>(); - const String& cs = c.getConst<String>(); - unsigned pvs = ps.size(); - unsigned cvs = cs.size(); - if (pvs == cvs || (pvs > cvs && t.isConst()) - || (cvs > pvs && prev.isConst())) - { - // If equal length, cannot be equal due to node check above. - // If one is fully constant and has less length than the other, then the - // other will not fit and we are in conflict. - conflict = true; - } - else - { - const String& larges = pvs > cvs ? ps : cs; - const String& smalls = pvs > cvs ? cs : ps; - if (isSuf) - { - conflict = !larges.hasSuffix(smalls); - } - else - { - conflict = !larges.hasPrefix(smalls); - } - } - if (!conflict && (pvs > cvs || prev.isConst())) - { - // current is subsumed, either shorter prefix or the other is a full - // constant - return Node::null(); - } - } - else if (!t.isConst()) - { - // current is subsumed since the other may be a full constant - return Node::null(); - } - if (conflict) - { - Trace("strings-eager-pconf") - << "Conflict for " << prevC << ", " << c << std::endl; - std::vector<Node> ccs; - Node r[2]; - for (unsigned i = 0; i < 2; i++) - { - Node tp = i == 0 ? t : prev; - if (tp.getKind() == STRING_IN_REGEXP) - { - ccs.push_back(tp); - r[i] = tp[0]; - } - else - { - r[i] = tp; - } - } - if (r[0] != r[1]) - { - ccs.push_back(r[0].eqNode(r[1])); - } - Assert(!ccs.empty()); - Node ret = - ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs); - Trace("strings-eager-pconf") - << "String: eager prefix conflict: " << ret << std::endl; - return ret; - } - } - if (isSuf) - { - d_suffixC = t; - } - else - { - d_prefixC = t; - } - return Node::null(); -} - SolverState::SolverState(context::Context* c, eq::EqualityEngine& ee, Valuation& v) |