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.
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";
// 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,
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); }
}
// 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")
return res;
}
+struct ArithEntailConstantBoundLowerId
+{
+};
+typedef expr::Attribute<ArithEntailConstantBoundLowerId, Node>
+ ArithEntailConstantBoundLower;
+
+struct ArithEntailConstantBoundUpperId
+{
+};
+typedef expr::Attribute<ArithEntailConstantBoundUpperId, Node>
+ 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;
{
if (isLower)
{
- ret = NodeManager::currentNM()->mkConst(Rational(0));
+ ret = d_zero;
}
}
else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
{
if (children.empty())
{
- ret = NodeManager::currentNM()->mkConst(Rational(0));
+ ret = d_zero;
}
else if (children.size() == 1)
{
|| check(a, false));
Assert(!isLower || ret.isNull() || ret.getConst<Rational>().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<Rational>();
+ }
+ if (success)
+ {
+ ret = nm->mkConst(sum);
+ }
+ }
+ else if (isLower)
+ {
+ ret = d_zero;
+ }
+ // cache
+ setConstantBoundCache(s, ret, isLower);
return ret;
}
}
else
{
- sum = ys.size() == 1 ? ys[0] : nm->mkConst(Rational(0));
+ sum = ys.size() == 1 ? ys[0] : d_zero;
}
if (check(sum, x))
*/
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
void getArithApproximations(Node a,
std::vector<Node>& 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
const context::CDList<Node>& 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)
{
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]))
{
<< "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())
{
// if not, add the lemma
std::vector<Node> 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")
#include "theory/strings/eager_solver.h"
#include "theory/strings/theory_strings_utils.h"
+#include "util/rational.h"
using namespace cvc5::kind;
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() {}
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
{
}
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)
{
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())
{
{
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);
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,
}
}
+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<Rational>();
+ 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<Rational>();
+ 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<Rational>();
+ 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
#include <map>
#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 {
* 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);
* 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
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
{
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;
}
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
context::CDO<unsigned> d_cardinalityLemK;
context::CDO<Node> 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<Node> d_firstBound;
+ /** same as above, for suffix and integer upper bounds. */
+ context::CDO<Node> 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<Node> d_prefixC;
- /** same as above, for suffix. */
- context::CDO<Node> d_suffixC;
+ static Node mkMergeConflict(Node t, Node prev);
};
} // namespace strings
// typically shouldnt be necessary
lengthTerm = t;
}
+ else
+ {
+ lengthTerm = lengthTerm[0];
+ }
Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm
<< std::endl;
if (te != lengthTerm)
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);
// not have an associated length in the mappings above, if the length of
// an equivalence class is unknown.
std::map<unsigned, std::vector<Node> > eqc_to_strings;
- NodeManager* nm = NodeManager::currentNM();
for (const Node& eqc : n)
{
Assert(d_ee->getRepresentative(eqc) == eqc);
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<Node, TypeNode> lkey(r, tnEqc);
if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
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
* 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.
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),
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;
/**
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
--- /dev/null
+(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)
+
+
projects / cvc5.git / commitdiff