From c99aa755bd62205b3f7381e6d67c7a1f2d37a3a2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 24 Oct 2021 13:31:56 -0500 Subject: [PATCH] Add new eager conflict detection in strings for integer equivalence classes (#7453) Required to address Zelkova bottlenecks. This generalizes the methods for eager prefix/suffix conflicts for strings to do eager lower/upper bound conflicts for integer equivalence classes based on string-specific reasoning about length terms. This avoids cases where Simplex fails to show a concise conflict due to not having access to string reasoning (e.g. strings::ArithEntail) for arithmetic bounds. The approach can still be improved by inferring fixed length for regular expression memberships, analogous to what is done for prefix/suffix conflicts. It also changes EqcInfo to store (str.len x) instead of x for length terms. --- src/theory/inference_id.cpp | 2 + src/theory/inference_id.h | 6 +- src/theory/strings/arith_entail.cpp | 115 ++++++++++++- src/theory/strings/arith_entail.h | 10 ++ src/theory/strings/core_solver.cpp | 11 +- src/theory/strings/eager_solver.cpp | 175 ++++++++++++++++++-- src/theory/strings/eager_solver.h | 23 ++- src/theory/strings/eqc_info.cpp | 58 ++++--- src/theory/strings/eqc_info.h | 25 ++- src/theory/strings/solver_state.cpp | 13 +- src/theory/strings/solver_state.h | 6 +- src/theory/strings/theory_strings.cpp | 8 +- src/theory/strings/theory_strings.h | 8 +- test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/pattern1.smt2 | 73 ++++++++ 15 files changed, 454 insertions(+), 80 deletions(-) create mode 100644 test/regress/regress1/strings/pattern1.smt2 diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 28557e472..af753dd26 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -429,6 +429,8 @@ const char* toString(InferenceId i) case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS"; case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION"; case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT"; + case InferenceId::STRINGS_ARITH_BOUND_CONFLICT: + return "STRINGS_ARITH_BOUND_CONFLICT"; case InferenceId::STRINGS_REGISTER_TERM_ATOMIC: return "STRINGS_REGISTER_TERM_ATOMIC"; case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 50c063651..70f70e717 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -772,9 +772,11 @@ enum class InferenceId // f(x1, .., xn) and P is the reduction predicate for f // (see theory_strings_preprocess). STRINGS_REDUCTION, - //-------------------- prefix conflict - // prefix conflict (coarse-grained) + //-------------------- merge conflicts + // prefix conflict STRINGS_PREFIX_CONFLICT, + // arithmetic bound conflict + STRINGS_ARITH_BOUND_CONFLICT, //-------------------- other // a lemma added during term registration for an atomic term STRINGS_REGISTER_TERM_ATOMIC, diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 8950ea6fa..9e3d8ad38 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -30,7 +30,10 @@ namespace cvc5 { namespace theory { namespace strings { -ArithEntail::ArithEntail(Rewriter* r) : d_rr(r) {} +ArithEntail::ArithEntail(Rewriter* r) : d_rr(r) +{ + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); +} Node ArithEntail::rewrite(Node a) { return d_rr->rewrite(a); } @@ -197,7 +200,7 @@ bool ArithEntail::checkApprox(Node ar) } // get the current "fixed" sum for the abstraction of ar Node aar = aarSum.empty() - ? nm->mkConst(Rational(0)) + ? d_zero : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(PLUS, aarSum)); aar = d_rr->rewrite(aar); Trace("strings-ent-approx-debug") @@ -709,10 +712,61 @@ bool ArithEntail::checkWithAssumptions(std::vector assumptions, return res; } +struct ArithEntailConstantBoundLowerId +{ +}; +typedef expr::Attribute + ArithEntailConstantBoundLower; + +struct ArithEntailConstantBoundUpperId +{ +}; +typedef expr::Attribute + ArithEntailConstantBoundUpper; + +void ArithEntail::setConstantBoundCache(Node n, Node ret, bool isLower) +{ + if (isLower) + { + ArithEntailConstantBoundLower acbl; + n.setAttribute(acbl, ret); + } + else + { + ArithEntailConstantBoundUpper acbu; + n.setAttribute(acbu, ret); + } +} + +Node ArithEntail::getConstantBoundCache(Node n, bool isLower) +{ + if (isLower) + { + ArithEntailConstantBoundLower acbl; + if (n.hasAttribute(acbl)) + { + return n.getAttribute(acbl); + } + } + else + { + ArithEntailConstantBoundUpper acbu; + if (n.hasAttribute(acbu)) + { + return n.getAttribute(acbu); + } + } + return Node::null(); +} + Node ArithEntail::getConstantBound(Node a, bool isLower) { Assert(d_rr->rewrite(a) == a); - Node ret; + Node ret = getConstantBoundCache(a, isLower); + if (!ret.isNull()) + { + return ret; + } if (a.isConst()) { ret = a; @@ -721,7 +775,7 @@ Node ArithEntail::getConstantBound(Node a, bool isLower) { if (isLower) { - ret = NodeManager::currentNM()->mkConst(Rational(0)); + ret = d_zero; } } else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT) @@ -767,7 +821,7 @@ Node ArithEntail::getConstantBound(Node a, bool isLower) { if (children.empty()) { - ret = NodeManager::currentNM()->mkConst(Rational(0)); + ret = d_zero; } else if (children.size() == 1) { @@ -789,6 +843,55 @@ Node ArithEntail::getConstantBound(Node a, bool isLower) || check(a, false)); Assert(!isLower || ret.isNull() || ret.getConst().sgn() <= 0 || check(a, true)); + // cache + setConstantBoundCache(a, ret, isLower); + return ret; +} + +Node ArithEntail::getConstantBoundLength(Node s, bool isLower) +{ + Assert(s.getType().isStringLike()); + Node ret = getConstantBoundCache(s, isLower); + if (!ret.isNull()) + { + return ret; + } + NodeManager* nm = NodeManager::currentNM(); + if (s.isConst()) + { + ret = nm->mkConst(Rational(Word::getLength(s))); + } + else if (s.getKind() == STRING_CONCAT) + { + Rational sum(0); + bool success = true; + for (const Node& sc : s) + { + Node b = getConstantBoundLength(sc, isLower); + if (b.isNull()) + { + if (isLower) + { + // assume zero and continue + continue; + } + success = false; + break; + } + Assert(b.getKind() == CONST_RATIONAL); + sum = sum + b.getConst(); + } + if (success) + { + ret = nm->mkConst(sum); + } + } + else if (isLower) + { + ret = d_zero; + } + // cache + setConstantBoundCache(s, ret, isLower); return ret; } @@ -853,7 +956,7 @@ bool ArithEntail::inferZerosInSumGeq(Node x, } else { - sum = ys.size() == 1 ? ys[0] : nm->mkConst(Rational(0)); + sum = ys.size() == 1 ? ys[0] : d_zero; } if (check(sum, x)) diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h index 2158b23b0..295afb8c9 100644 --- a/src/theory/strings/arith_entail.h +++ b/src/theory/strings/arith_entail.h @@ -135,6 +135,10 @@ class ArithEntail */ Node getConstantBound(Node a, bool isLower = true); + /** + * get constant bound on the length of s. + */ + Node getConstantBoundLength(Node s, bool isLower = true); /** * Given an inequality y1 + ... + yn >= x, removes operands yi s.t. the * original inequality still holds. Returns true if the original inequality @@ -179,8 +183,14 @@ class ArithEntail void getArithApproximations(Node a, std::vector& approx, bool isOverApprox = false); + /** Set bound cache */ + void setConstantBoundCache(Node n, Node ret, bool isLower); + /** Get bound cache */ + Node getConstantBoundCache(Node n, bool isLower); /** The underlying rewriter */ Rewriter* d_rr; + /** Constant zero */ + Node d_zero; }; } // namespace strings diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index d4d3761d8..b5e15a129 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2550,6 +2550,7 @@ void CoreSolver::checkNormalFormsDeq() const context::CDList& deqs = d_state.getDisequalityList(); + NodeManager* nm = NodeManager::currentNM(); //for each pair of disequal strings, must determine whether their lengths are equal or disequal for (const Node& eq : deqs) { @@ -2564,9 +2565,8 @@ void CoreSolver::checkNormalFormsDeq() EqcInfo* ei = d_state.getOrMakeEqcInfo(n[i], false); lt[i] = ei ? ei->d_lengthTerm : Node::null(); if( lt[i].isNull() ){ - lt[i] = eq[i]; + lt[i] = nm->mkNode(STRING_LENGTH, eq[i]); } - lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] ); } if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1])) { @@ -2642,14 +2642,13 @@ void CoreSolver::checkLengthsEqc() { << "Process length constraints for " << d_strings_eqc[i] << std::endl; // check if there is a length term for this equivalence class EqcInfo* ei = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false); - Node lt = ei ? ei->d_lengthTerm : Node::null(); - if (lt.isNull()) + Node llt = ei ? ei->d_lengthTerm : Node::null(); + if (llt.isNull()) { Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << std::endl; continue; } - Node llt = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, lt); // now, check if length normalization has occurred if (ei->d_normalizedLength.get().isNull()) { @@ -2669,7 +2668,7 @@ void CoreSolver::checkLengthsEqc() { // if not, add the lemma std::vector ant; ant.insert(ant.end(), nfi.d_exp.begin(), nfi.d_exp.end()); - ant.push_back(lt.eqNode(nfi.d_base)); + ant.push_back(llt[0].eqNode(nfi.d_base)); Node lc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nf); Node lcr = rewrite(lc); Trace("strings-process-debug") diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp index 829146f52..21fdd6fa2 100644 --- a/src/theory/strings/eager_solver.cpp +++ b/src/theory/strings/eager_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/eager_solver.h" #include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" using namespace cvc5::kind; @@ -23,7 +24,13 @@ namespace cvc5 { namespace theory { namespace strings { -EagerSolver::EagerSolver(SolverState& state) : d_state(state) {} +EagerSolver::EagerSolver(Env& env, + SolverState& state, + TermRegistry& treg, + ArithEntail& aent) + : EnvObj(env), d_state(state), d_treg(treg), d_aent(aent) +{ +} EagerSolver::~EagerSolver() {} @@ -37,7 +44,30 @@ void EagerSolver::eqNotifyNewClass(TNode t) EqcInfo* ei = d_state.getOrMakeEqcInfo(r); if (k == STRING_LENGTH) { - ei->d_lengthTerm = t[0]; + ei->d_lengthTerm = t; + // also assume it as upper/lower bound as applicable for the equivalence + // class info of t. + EqcInfo* eil = nullptr; + for (size_t i = 0; i < 2; i++) + { + Node b = getBoundForLength(t, i == 0); + if (b.isNull()) + { + continue; + } + if (eil == nullptr) + { + eil = d_state.getOrMakeEqcInfo(t); + } + if (i == 0) + { + eil->d_firstBound = t; + } + else if (i == 1) + { + eil->d_secondBound = t; + } + } } else { @@ -46,11 +76,12 @@ void EagerSolver::eqNotifyNewClass(TNode t) } else if (t.isConst()) { - if (t.getType().isStringLike()) + TypeNode tn = t.getType(); + if (tn.isStringLike() || tn.isInteger()) { EqcInfo* ei = d_state.getOrMakeEqcInfo(t); - ei->d_prefixC = t; - ei->d_suffixC = t; + ei->d_firstBound = t; + ei->d_secondBound = t; } } else if (k == STRING_CONCAT) @@ -66,8 +97,18 @@ void EagerSolver::eqNotifyMerge(TNode t1, TNode t2) { return; } - Assert(t1.getType().isStringLike()); + // always create it if e2 was non-null EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1); + // check for conflict + Node conf = checkForMergeConflict(t1, t2, e1, e2); + if (!conf.isNull()) + { + InferenceId id = t1.getType().isStringLike() + ? InferenceId::STRINGS_PREFIX_CONFLICT + : InferenceId::STRINGS_ARITH_BOUND_CONFLICT; + d_state.setPendingMergeConflict(conf, id); + return; + } // add information from e2 to e1 if (!e2->d_lengthTerm.get().isNull()) { @@ -77,16 +118,6 @@ void EagerSolver::eqNotifyMerge(TNode t1, TNode t2) { e1->d_codeTerm.set(e2->d_codeTerm); } - if (!e2->d_prefixC.get().isNull()) - { - d_state.setPendingPrefixConflictWhen( - e1->addEndpointConst(e2->d_prefixC, Node::null(), false)); - } - if (!e2->d_suffixC.get().isNull()) - { - d_state.setPendingPrefixConflictWhen( - e1->addEndpointConst(e2->d_suffixC, Node::null(), true)); - } if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get()) { e1->d_cardinalityLemK.set(e2->d_cardinalityLemK); @@ -126,9 +157,50 @@ void EagerSolver::addEndpointsToEqcInfo(Node t, Node concat, Node eqc) Trace("strings-eager-pconf-debug") << "New term: " << concat << " for " << t << " with prefix " << c << " (" << (r == 1) << ")" << std::endl; - d_state.setPendingPrefixConflictWhen(ei->addEndpointConst(t, c, r == 1)); + Node conf = ei->addEndpointConst(t, c, r == 1); + if (!conf.isNull()) + { + d_state.setPendingMergeConflict(conf, + InferenceId::STRINGS_PREFIX_CONFLICT); + return; + } + } + } +} + +Node EagerSolver::checkForMergeConflict(Node a, + Node b, + EqcInfo* ea, + EqcInfo* eb) +{ + Assert(eb != nullptr && ea != nullptr); + Assert(a.getType() == b.getType()); + Assert(a.getType().isStringLike() || a.getType().isInteger()); + // check prefix, suffix + for (size_t i = 0; i < 2; i++) + { + Node n = i == 0 ? eb->d_firstBound.get() : eb->d_secondBound.get(); + if (!n.isNull()) + { + Node conf; + if (a.getType().isStringLike()) + { + conf = ea->addEndpointConst(n, Node::null(), i == 1); + } + else + { + Trace("strings-eager-aconf-debug") + << "addArithmeticBound " << n << " into " << a << " from " << b + << std::endl; + conf = addArithmeticBound(ea, n, i == 0); + } + if (!conf.isNull()) + { + return conf; + } } } + return Node::null(); } void EagerSolver::notifyFact(TNode atom, @@ -147,6 +219,75 @@ void EagerSolver::notifyFact(TNode atom, } } +Node EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower) +{ + Assert(e != nullptr); + Assert(!t.isNull()); + Node tb = t.isConst() ? t : getBoundForLength(t, isLower); + Assert(!tb.isNull() && tb.getKind() == CONST_RATIONAL) + << "Unexpected bound " << tb << " from " << t; + Rational br = tb.getConst(); + Node prev = isLower ? e->d_firstBound : e->d_secondBound; + // check if subsumed + if (!prev.isNull()) + { + // convert to bound + Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower); + Assert(!prevb.isNull() && prevb.getKind() == CONST_RATIONAL); + Rational prevbr = prevb.getConst(); + if (prevbr == br || (br < prevbr) == isLower) + { + // subsumed + return Node::null(); + } + } + Node prevo = isLower ? e->d_secondBound : e->d_firstBound; + Trace("strings-eager-aconf-debug") + << "Check conflict for bounds " << t << " " << prevo << std::endl; + if (!prevo.isNull()) + { + // are we in conflict? + Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower); + Assert(!prevob.isNull() && prevob.getKind() == CONST_RATIONAL); + Rational prevobr = prevob.getConst(); + if (prevobr != br && (prevobr < br) == isLower) + { + // conflict + Node ret = EqcInfo::mkMergeConflict(t, prevo); + Trace("strings-eager-aconf") + << "String: eager arithmetic bound conflict: " << ret << std::endl; + return ret; + } + } + if (isLower) + { + e->d_firstBound = t; + } + else + { + e->d_secondBound = t; + } + return Node::null(); +} + +Node EagerSolver::getBoundForLength(Node len, bool isLower) +{ + Assert(len.getKind() == STRING_LENGTH); + // it is prohibitively expensive to convert to original form and rewrite, + // since this may invoke the rewriter on lengths of complex terms. Instead, + // we convert to original term the argument, then call the utility method + // for computing the length of the argument, implicitly under an application + // of length (ArithEntail::getConstantBoundLength). + // convert to original form + Node olent = SkolemManager::getOriginalForm(len[0]); + // get the bound + Node c = d_aent.getConstantBoundLength(olent, isLower); + Trace("strings-eager-aconf-debug") + << "Constant " << (isLower ? "lower" : "upper") << " bound for " << len + << " is " << c << ", from original form " << olent << std::endl; + return c; +} + } // namespace strings } // namespace theory } // namespace cvc5 diff --git a/src/theory/strings/eager_solver.h b/src/theory/strings/eager_solver.h index cf4062bfe..03fb0ff63 100644 --- a/src/theory/strings/eager_solver.h +++ b/src/theory/strings/eager_solver.h @@ -21,8 +21,11 @@ #include #include "expr/node.h" +#include "smt/env_obj.h" +#include "theory/strings/arith_entail.h" #include "theory/strings/eqc_info.h" #include "theory/strings/solver_state.h" +#include "theory/strings/term_registry.h" namespace cvc5 { namespace theory { @@ -32,10 +35,13 @@ namespace strings { * Eager solver, which is responsible for tracking of eager information and * reporting conflicts to the solver state. */ -class EagerSolver +class EagerSolver : protected EnvObj { public: - EagerSolver(SolverState& state); + EagerSolver(Env& env, + SolverState& state, + TermRegistry& treg, + ArithEntail& aent); ~EagerSolver(); /** called when a new equivalence class is created */ void eqNotifyNewClass(TNode t); @@ -58,8 +64,21 @@ class EagerSolver * for some eqc that is currently equal to z. */ void addEndpointsToEqcInfo(Node t, Node concat, Node eqc); + /** + * Check for conflict when merging equivalence classes with the given info, + * return the node corresponding to the conflict if so. + */ + Node checkForMergeConflict(Node a, Node b, EqcInfo* ea, EqcInfo* eb); + /** add arithmetic bound */ + Node addArithmeticBound(EqcInfo* ea, Node t, bool isLower); + /** get bound for length term */ + Node getBoundForLength(Node len, bool isLower); /** Reference to the solver state */ SolverState& d_state; + /** Reference to the term registry */ + TermRegistry& d_treg; + /** Arithmetic entailment */ + ArithEntail& d_aent; }; } // namespace strings 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 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 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 diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h index 1fd430c95..bfc753989 100644 --- a/src/theory/strings/eqc_info.h +++ b/src/theory/strings/eqc_info.h @@ -62,17 +62,34 @@ class EqcInfo context::CDO d_cardinalityLemK; context::CDO d_normalizedLength; /** - * A node that explains the longest constant prefix known of this + * If this is a string equivalence class, this is + * a node that explains the longest constant prefix known of this * equivalence class. This can either be: * (1) A term from this equivalence class, including a constant "ABC" or * concatenation term (str.++ "ABC" ...), or * (2) A membership of the form (str.in.re x R) where x is in this * equivalence class and R is a regular expression of the form * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...). + * + * If this is an integer equivalence class, this is the lower bound + * of the value of this equivalence class. + */ + context::CDO d_firstBound; + /** same as above, for suffix and integer upper bounds. */ + context::CDO d_secondBound; + /** + * Make merge conflict. Let "bound term" refer to a term that is set + * as the data member of this class for d_firstBound or d_secondBound. + * This method is called when this implies that two terms occur in an + * equivalence class that have conflicting properties. For example, + * t may be (str.in_re x (re.++ (str.to_re "A") R2)) and prev may be + * (str.++ "B" y), where the equivalence class of x has merged into + * the equivalence class of (str.++ "B" y). This method would return + * the conflict: + * (and (= x (str.++ "B" y)) (str.in_re x (re.++ (str.to_re "A") R2))) + * for this input. */ - context::CDO d_prefixC; - /** same as above, for suffix. */ - context::CDO d_suffixC; + static Node mkMergeConflict(Node t, Node prev); }; } // namespace strings diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 32ed6896c..28ab63d05 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -90,6 +90,10 @@ Node SolverState::getLengthExp(Node t, std::vector& exp, Node te) // typically shouldnt be necessary lengthTerm = t; } + else + { + lengthTerm = lengthTerm[0]; + } Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm << std::endl; if (te != lengthTerm) @@ -135,13 +139,14 @@ bool SolverState::isEqualEmptyWord(Node s, Node& emps) return false; } -void SolverState::setPendingPrefixConflictWhen(Node conf) +void SolverState::setPendingMergeConflict(Node conf, InferenceId id) { - if (conf.isNull() || d_pendingConflictSet.get()) + if (d_pendingConflictSet.get()) { + // already set conflict return; } - InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT); + InferInfo iiPrefixConf(id); iiPrefixConf.d_conc = d_false; utils::flattenOp(AND, conf, iiPrefixConf.d_premises); setPendingConflict(iiPrefixConf); @@ -188,7 +193,6 @@ void SolverState::separateByLength( // not have an associated length in the mappings above, if the length of // an equivalence class is unknown. std::map > eqc_to_strings; - NodeManager* nm = NodeManager::currentNM(); for (const Node& eqc : n) { Assert(d_ee->getRepresentative(eqc) == eqc); @@ -197,7 +201,6 @@ void SolverState::separateByLength( Node lt = ei ? ei->d_lengthTerm : Node::null(); if (!lt.isNull()) { - lt = nm->mkNode(STRING_LENGTH, lt); Node r = d_ee->getRepresentative(lt); std::pair lkey(r, tnEqc); if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end()) diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index bbeb470f7..061c5cf10 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -64,9 +64,9 @@ class SolverState : public TheoryState void addDisequality(TNode t1, TNode t2); //-------------------------------------- end disequality information //------------------------------------------ conflicts - /** set pending prefix conflict + /** set pending merge conflict * - * If conf is non-null, this is called when conf is a conjunction of literals + * This is called when conf is a conjunction of literals * that hold in the current context that are unsatisfiable. It is set as the * "pending conflict" to be processed as a conflict lemma on the output * channel of this class. It is not sent out immediately since it may require @@ -74,7 +74,7 @@ class SolverState : public TheoryState * during a merge operation, when the equality engine is not in a state to * provide explanations. */ - void setPendingPrefixConflictWhen(Node conf); + void setPendingMergeConflict(Node conf, InferenceId id); /** * Set pending conflict, infer info version. Called when we are in conflict * based on the inference ii. This generalizes the above method. diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 25d0e7336..9a793e14f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,14 +55,14 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_notify(*this), d_statistics(), d_state(env, d_valuation), - d_eagerSolver(d_state), d_termReg(env, d_state, d_statistics, d_pnm), - d_extTheoryCb(), - d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics), - d_extTheory(env, d_extTheoryCb, d_im), d_rewriter(env.getRewriter(), &d_statistics.d_rewrites, d_termReg.getAlphabetCardinality()), + d_eagerSolver(env, d_state, d_termReg, d_rewriter.getArithEntail()), + d_extTheoryCb(), + d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics), + d_extTheory(env, d_extTheoryCb, d_im), // the checker depends on the cardinality of the alphabet d_checker(d_termReg.getAlphabetCardinality()), d_bsolver(env, d_state, d_im), diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index f23b2449f..dbb04580f 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -254,18 +254,18 @@ class TheoryStrings : public Theory { SequencesStatistics d_statistics; /** The solver state object */ SolverState d_state; - /** The eager solver */ - EagerSolver d_eagerSolver; /** The term registry for this theory */ TermRegistry d_termReg; + /** The theory rewriter for this theory. */ + StringsRewriter d_rewriter; + /** The eager solver */ + EagerSolver d_eagerSolver; /** The extended theory callback */ StringsExtfCallback d_extTheoryCb; /** The (custom) output channel of the theory of strings */ InferenceManager d_im; /** Extended theory, responsible for context-dependent simplification. */ ExtTheory d_extTheory; - /** The theory rewriter for this theory. */ - StringsRewriter d_rewriter; /** The proof rule checker */ StringProofRuleChecker d_checker; /** diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5dd456b9f..5b3f3b729 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2280,6 +2280,7 @@ set(regress_1_tests regress1/strings/nt6-dd.smt2 regress1/strings/nterm-re-inter-sigma.smt2 regress1/strings/open-pf-merge.smt2 + regress1/strings/pattern1.smt2 regress1/strings/pierre150331.smt2 regress1/strings/policy_variable.smt2 regress1/strings/pre_ctn_no_skolem_share.smt2 diff --git a/test/regress/regress1/strings/pattern1.smt2 b/test/regress/regress1/strings/pattern1.smt2 new file mode 100644 index 000000000..b75fdb9be --- /dev/null +++ b/test/regress/regress1/strings/pattern1.smt2 @@ -0,0 +1,73 @@ +(set-option :produce-models true) +(set-logic QF_SLIA) +(set-info :status sat) +(declare-const x String) + +(assert + (str.in_re + x + (re.++ + (str.to_re "pref") + (re.* re.allchar) + (str.to_re "a") + (re.* re.allchar) + (str.to_re "b") + (re.* re.allchar) + (str.to_re "c") + (re.* re.allchar) + (str.to_re "d") + (re.* re.allchar) + (str.to_re "e") + (re.* re.allchar) + (str.to_re "f") + (re.* re.allchar) + (str.to_re "g") + (re.* re.allchar) + (str.to_re "h") + (re.* re.allchar) + (str.to_re "i") + (re.* re.allchar) + (str.to_re "j") + (re.* re.allchar) + (str.to_re "k") + (re.* re.allchar) + (str.to_re "l") + (re.* re.allchar) + (str.to_re "m") + (re.* re.allchar) + (str.to_re "n") + (re.* re.allchar) + (str.to_re "o") + (re.* re.allchar) + (str.to_re "p") + (re.* re.allchar) + (str.to_re "q") + (re.* re.allchar) + (str.to_re "r") + (re.* re.allchar) + (str.to_re "s") + (re.* re.allchar) + (str.to_re "t") + (re.* re.allchar) + (str.to_re "u") + (re.* re.allchar) + (str.to_re "v") + (re.* re.allchar) + (str.to_re "w") + (re.* re.allchar) + (str.to_re "x") + (re.* re.allchar) + (str.to_re "y") + (re.* re.allchar) + (str.to_re "z") + (re.* re.allchar)))) + +(assert + (or + (= x "pref0a-b-c-de") + (str.in_re x (re.++ (str.to_re "prefix") (re.* re.allchar))) + (str.in_re x (re.++ (re.* re.allchar) (str.to_re "test") (re.* re.allchar))))) + +(check-sat) + + -- 2.30.2