From 6476c8c75ed7fd584b5afa658dd2c8ba277c59e2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 6 Nov 2020 13:47:22 -0600 Subject: [PATCH] (proof-new) Miscellaneous changes to strings for proofs (#5362) This includes all minor remaining changes from proof-new for strings that were not merged to master. This includes mostly minor changes to make proofs pass, including reordering assertions. It also removes some non-standard pedantic checks as these are now subsumed by standard ones. It also makes the strings rewriter slightly more safe when checking arithmetic entailment under assumptions. This code used substitution, which was not safe when quantifiers were involved. This is replaced by capture avoiding substitution here. --- src/theory/strings/arith_entail.cpp | 8 +++++++- src/theory/strings/base_solver.cpp | 7 +++---- src/theory/strings/infer_proof_cons.cpp | 11 ----------- src/theory/strings/normal_form.cpp | 9 ++++----- src/theory/strings/term_registry.cpp | 10 ---------- src/theory/strings/theory_strings_preprocess.cpp | 10 ++++++---- 6 files changed, 20 insertions(+), 35 deletions(-) diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index cc2c7a2e6..3c58767b3 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -15,6 +15,7 @@ #include "theory/strings/arith_entail.h" #include "expr/attribute.h" +#include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" @@ -555,6 +556,8 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict) { Assert(assumption.getKind() == kind::EQUAL); Assert(Rewriter::rewrite(assumption) == assumption); + Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a + << ", strict=" << strict << std::endl; // Find candidates variables to compute substitutions for std::unordered_set candVars; @@ -615,8 +618,11 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict) // Could not solve for v return false; } + Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> " + << solution << std::endl; - a = a.substitute(TNode(v), TNode(solution)); + // use capture avoiding substitution + a = expr::substituteCaptureAvoiding(a, v, solution); return check(a, strict); } diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index d33a7f902..451c01f8c 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -638,9 +638,8 @@ void BaseSolver::checkCardinalityType(TypeNode tn, ei->d_cardinalityLemK.set(int_k + 1); if (!cons.isConst() || !cons.getConst()) { - std::vector emptyVec; d_im.sendInference( - emptyVec, expn, cons, Inference::CARDINALITY, true); + expn, expn, cons, Inference::CARDINALITY, false, true); return; } } @@ -675,7 +674,7 @@ Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector& exp) } if (!bei.d_exp.isNull()) { - exp.push_back(bei.d_exp); + utils::flattenOp(AND, bei.d_exp, exp); } if (!bei.d_base.isNull()) { @@ -695,7 +694,7 @@ Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector& exp) Assert(!bei.d_bestContent.isNull()); if (!bei.d_exp.isNull()) { - exp.push_back(bei.d_exp); + utils::flattenOp(AND, bei.d_exp, exp); } if (!bei.d_base.isNull()) { diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index c5275cc43..66f71bf14 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -878,17 +878,6 @@ void InferProofCons::convert(Inference infer, ps.d_rule = PfRule::STRING_TRUST; // add to stats d_statistics.d_inferencesNoPf << infer; - if (options::proofNewPedantic() > 0) - { - std::stringstream serr; - serr << "InferProofCons::convert: Failed " << infer - << (isRev ? " :rev " : " ") << conc << std::endl; - for (const Node& ec : exp) - { - serr << " e: " << ec << std::endl; - } - Unhandled() << serr.str(); - } } if (Trace.isOn("strings-ipc-debug")) { diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp index 372b07f56..7724b5137 100644 --- a/src/theory/strings/normal_form.cpp +++ b/src/theory/strings/normal_form.cpp @@ -83,6 +83,7 @@ void NormalForm::addToExplanation(Node exp, unsigned new_val, unsigned new_rev_val) { + Assert(!exp.isConst()); if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end()) { d_exp.push_back(exp); @@ -177,11 +178,9 @@ void NormalForm::getExplanationForPrefixEq(NormalForm& nfi, Trace("strings-explain-prefix") << "Included " << curr_exp.size() << " / " << (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl; - if (nfi.d_base != nfj.d_base) - { - Node eq = nfi.d_base.eqNode(nfj.d_base); - curr_exp.push_back(eq); - } + // add explanation for why they are equal + Node eq = nfi.d_base.eqNode(nfj.d_base); + curr_exp.push_back(eq); } } // namespace strings diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 76230bcff..8274b7dc0 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -462,11 +462,6 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma( Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one << std::endl; Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl; - if (options::proofNewPedantic() > 0) - { - Unhandled() << "Unhandled lemma Strings::Lemma SK-GEQ-ONE : " - << len_geq_one << std::endl; - } return TrustNode::mkTrustLemma(len_geq_one, nullptr); } @@ -476,11 +471,6 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma( Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one << std::endl; Trace("strings-assert") << "(assert " << len_one << ")" << std::endl; - if (options::proofNewPedantic() > 0) - { - Unhandled() << "Unhandled lemma Strings::Lemma SK-ONE : " << len_one - << std::endl; - } return TrustNode::mkTrustLemma(len_one, nullptr); } Assert(s == LENGTH_SPLIT); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a8c1a6573..936f60ed2 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -875,7 +875,7 @@ Node StringsPreprocess::reduce(Node t, { Node ltp = sc->mkTypedSkolemCached( nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp"); - Node k = nm->mkSkolem("k", nm->integerType()); + Node k = SkolemCache::mkIndexVar(t); std::vector conj; conj.push_back(nm->mkNode(GEQ, k, zero)); @@ -899,6 +899,8 @@ Node StringsPreprocess::reduce(Node t, } conj.push_back(nm->mkNode(ITE, ite_ch)); + Node conjn = nm->mkNode( + EXISTS, nm->mkNode(BOUND_VAR_LIST, k), nm->mkNode(AND, conj)); // Intuitively, the reduction says either x and y are equal, or they have // some (maximal) common prefix after which their characters at position k // are distinct, and the comparison of their code matches the return value @@ -912,13 +914,13 @@ Node StringsPreprocess::reduce(Node t, // assert: // IF x=y // THEN: ltp - // ELSE: k >= 0 AND k <= len( x ) AND k <= len( y ) AND + // ELSE: exists k. + // k >= 0 AND k <= len( x ) AND k <= len( y ) AND // substr( x, 0, k ) = substr( y, 0, k ) AND // IF ltp // THEN: str.code(substr( x, k, 1 )) < str.code(substr( y, k, 1 )) // ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 )) - Node assert = - nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj)); + Node assert = nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, conjn); asserts.push_back(assert); // Thus, str.<=( x, y ) = ltp -- 2.30.2