From 80493d9fa63169f02ff8b3c71622c49c6e068357 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 12 Jun 2020 12:57:05 -0500 Subject: [PATCH] (proof-new) Minor updates to strings base solver (#4606) In preparation for proofs, this PR involves flattening AND and removing spurious true literals in conjunctions. This also updates our policy for applying cardinality, where in some rare cases we were applying cardinality for pairs of string terms for length 0 (e.g. "there is at most 1 eqc of length 0"), which is spurious due to our term registry which always splits on emptiness. --- src/theory/strings/base_solver.cpp | 38 ++++++++++++++++----------- src/theory/strings/base_solver.h | 5 +--- 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 vec_node; - vec_node.push_back(dist); + std::vector expn; + expn.push_back(dist); for (std::vector::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 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; 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, -- 2.30.2