diff options
| -rw-r--r-- | src/theory/strings/base_solver.cpp | 38 | ||||
| -rw-r--r-- | src/theory/strings/base_solver.h | 5 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
3 files changed, 24 insertions, 21 deletions
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 4a03637d0..e2d1fbb3e 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -27,11 +27,8 @@ namespace CVC4 { namespace theory { namespace strings { -BaseSolver::BaseSolver(context::Context* c, - context::UserContext* u, - SolverState& s, - InferenceManager& im) - : d_state(s), d_im(im), d_congruent(c) +BaseSolver::BaseSolver(SolverState& s, InferenceManager& im) + : d_state(s), d_im(im), d_congruent(s.getSatContext()) { d_false = NodeManager::currentNM()->mkConst(false); d_cardSize = utils::getAlphabetCardinality(); @@ -323,8 +320,10 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, Node nrr = d_state.getRepresentative(n[count]); Assert(!d_eqcInfo[nrr].d_bestContent.isNull() && d_eqcInfo[nrr].d_bestContent.isConst()); + // must flatten to avoid nested AND in explanations + utils::flattenOp(AND, d_eqcInfo[nrr].d_exp, exp); + // now explain equality to base d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp); - exp.push_back(d_eqcInfo[nrr].d_exp); } else { @@ -353,9 +352,13 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, Assert(!nct.isConst()); bei.d_bestContent = nct; bei.d_base = n; - bei.d_exp = utils::mkAnd(exp); + if (!exp.empty()) + { + bei.d_exp = utils::mkAnd(exp); + } Trace("strings-debug") - << "Set eqc best content " << n << " to " << nct << std::endl; + << "Set eqc best content " << n << " to " << nct + << ", explanation = " << bei.d_exp << std::endl; } } } @@ -370,11 +373,12 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, BaseEqcInfo& bei = d_eqcInfo[nr]; if (!bei.d_bestContent.isConst()) { - Trace("strings-debug") - << "Set eqc const " << n << " to " << c << std::endl; bei.d_bestContent = c; bei.d_base = n; bei.d_exp = utils::mkAnd(exp); + Trace("strings-debug") + << "Set eqc const " << n << " to " << c + << ", explanation = " << bei.d_exp << std::endl; } else if (c != bei.d_bestContent) { @@ -487,8 +491,10 @@ void BaseSolver::checkCardinalityType(TypeNode tn, else { // find the minimimum constant that we are unknown to be disequal from, or - // otherwise stop if we increment such that cardinality does not apply - unsigned r = 0; + // otherwise stop if we increment such that cardinality does not apply. + // We always start with r=1 since by the invariants of our term registry, + // a term is either equal to the empty string, or has length >= 1. + unsigned r = 1; bool success = true; while (r < card_need && success) { @@ -545,8 +551,8 @@ void BaseSolver::checkCardinalityType(TypeNode tn, Node k_node = nm->mkConst(Rational(int_k)); // add cardinality lemma Node dist = nm->mkNode(DISTINCT, cols[i]); - std::vector<Node> vec_node; - vec_node.push_back(dist); + std::vector<Node> expn; + expn.push_back(dist); for (std::vector<Node>::iterator itr1 = cols[i].begin(); itr1 != cols[i].end(); ++itr1) @@ -555,7 +561,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, if (len != lr) { Node len_eq_lr = len.eqNode(lr); - vec_node.push_back(len_eq_lr); + expn.push_back(len_eq_lr); } } Node len = nm->mkNode(STRING_LENGTH, cols[i][0]); @@ -566,7 +572,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, { std::vector<Node> emptyVec; d_im.sendInference( - emptyVec, vec_node, cons, Inference::CARDINALITY, true); + emptyVec, expn, cons, Inference::CARDINALITY, true); return; } } diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 334fdf596..b8fb71dd3 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -41,10 +41,7 @@ class BaseSolver using NodeSet = context::CDHashSet<Node, NodeHashFunction>; public: - BaseSolver(context::Context* c, - context::UserContext* u, - SolverState& s, - InferenceManager& im); + BaseSolver(SolverState& s, InferenceManager& im); ~BaseSolver(); //-----------------------inference steps diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5ac8b8f7e..61980be3e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -88,7 +88,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_im.reset( new InferenceManager(c, u, d_state, d_termReg, *extt, out, d_statistics)); // initialize the solvers - d_bsolver.reset(new BaseSolver(c, u, d_state, *d_im)); + d_bsolver.reset(new BaseSolver(d_state, *d_im)); d_csolver.reset(new CoreSolver(c, u, d_state, *d_im, d_termReg, *d_bsolver)); d_esolver.reset(new ExtfSolver(c, u, |