diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-10-27 16:05:02 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-27 16:05:02 -0700 |
commit | 75f92b54a63f80aabf6591e9033f28c62d9ed030 (patch) | |
tree | 893c423b4f38b6b2a57c6fd386be8e7f702b17df /src/theory/strings/eqc_info.cpp | |
parent | 2519a0ba0491b8500799b56caf952a15bf2d0409 (diff) | |
parent | 95685c06c1c3983bc50a5cf4b4196fc1c5ae2247 (diff) |
Merge branch 'master' into issue7504issue7504
Diffstat (limited to 'src/theory/strings/eqc_info.cpp')
-rw-r--r-- | src/theory/strings/eqc_info.cpp | 58 |
1 files changed, 31 insertions, 27 deletions
diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp index 43636ecea..5fb5e91c3 100644 --- a/src/theory/strings/eqc_info.cpp +++ b/src/theory/strings/eqc_info.cpp @@ -31,15 +31,15 @@ EqcInfo::EqcInfo(context::Context* c) d_codeTerm(c), d_cardinalityLemK(c), d_normalizedLength(c), - d_prefixC(c), - d_suffixC(c) + d_firstBound(c), + d_secondBound(c) { } Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) { // check conflict - Node prev = isSuf ? d_suffixC : d_prefixC; + Node prev = isSuf ? d_secondBound : d_firstBound; if (!prev.isNull()) { Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t @@ -100,28 +100,7 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) { 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); + Node ret = mkMergeConflict(t, prev); Trace("strings-eager-pconf") << "String: eager prefix conflict: " << ret << std::endl; return ret; @@ -129,15 +108,40 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) } if (isSuf) { - d_suffixC = t; + d_secondBound = t; } else { - d_prefixC = t; + d_firstBound = t; } return Node::null(); } +Node EqcInfo::mkMergeConflict(Node t, Node prev) +{ + 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()); + return NodeManager::currentNM()->mkAnd(ccs); +} + } // namespace strings } // namespace theory } // namespace cvc5 |