diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index 7c9823f0812..6881dbca802 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -311,10 +311,14 @@ const char* toString(cvc5::ProofRewriteRule rule) case ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS: return "macro-str-strip-endpoints"; case ProofRewriteRule::MACRO_STR_SPLIT_CTN: return "macro-str-split-ctn"; - case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN: return "str-overlap-split-ctn"; - case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN: return "str-overlap-endpoints-ctn"; - case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF: return "str-overlap-endpoints-indexof"; - case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE: return "str-overlap-endpoints-replace"; + case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN: + return "str-overlap-split-ctn"; + case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN: + return "str-overlap-endpoints-ctn"; + case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF: + return "str-overlap-endpoints-indexof"; + case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE: + return "str-overlap-endpoints-replace"; case ProofRewriteRule::MACRO_STR_COMPONENT_CTN: return "macro-str-component-ctn"; case ProofRewriteRule::MACRO_STR_CONST_NCTN_CONCAT: diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index 7b2c2d268fc..85b82f4f9de 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -889,16 +889,16 @@ bool BasicRewriteRCons::ensureProofMacroStrEqLenUnifyPrefix(CDProof* cdp, NodeManager* nm = nodeManager(); theory::strings::ArithEntail ae(nullptr); theory::strings::StringsEntail sent(nullptr, ae); - - Assert (eq[1].getKind()==Kind::AND); + + Assert(eq[1].getKind() == Kind::AND); Node eq1p = eq[1]; // get the equations equal empty // we group (and (= s t) (= t1 "") ... (= tn "")) to // (and (= s t) (and (= t1 "") ... (= tn ""))) and store in eq1p. std::vector empeqs; - if (eq[1].getNumChildren()>2) + if (eq[1].getNumChildren() > 2) { - empeqs.insert(empeqs.end(), eq[1].begin()+1, eq[1].end()); + empeqs.insert(empeqs.end(), eq[1].begin() + 1, eq[1].end()); Node eq1g = nm->mkAnd(empeqs); eq1p = nm->mkNode(Kind::AND, eq[1][0], eq1g); Node eqg = eq1p.eqNode(eq[1]); @@ -979,15 +979,13 @@ bool BasicRewriteRCons::ensureProofMacroStrEqLenUnifyPrefix(CDProof* cdp, cdfwd.addStep(diffneqz, ProofRule::EQ_RESOLVE, {leneqi, equiv}, {}); Trace("brc-macro") << "...have " << diffneqz << std::endl; - // get the concatenation term corresponding to the components equated to empty std::vector concat; std::map empMap; - Assert(eq1p.getKind() == Kind::AND && eq1p.getNumChildren()==2); + Assert(eq1p.getKind() == Kind::AND && eq1p.getNumChildren() == 2); for (const Node& ee : empeqs) { - Assert(ee.getKind() == Kind::EQUAL - && ee[0].getType().isStringLike()); + Assert(ee.getKind() == Kind::EQUAL && ee[0].getType().isStringLike()); concat.push_back(ee[0]); empMap[ee[0]] = ee; } @@ -1085,39 +1083,40 @@ bool BasicRewriteRCons::ensureProofMacroStrEqLenUnifyPrefix(CDProof* cdp, cdmid.addStep(implMid, ProofRule::SCOPE, {eqqeq}, empeqs); Trace("brc-macro") << "...intermediate result: " << implMid << std::endl; std::shared_ptr pfmid = cdmid.getProofFor(implMid); - Assert (implMid[1][0]==eq[0]); - Assert (implMid[1][1]==eq1p[0]); - + Assert(implMid[1][0] == eq[0]); + Assert(implMid[1][1] == eq1p[0]); + // finish the forward proof cdfwd.addProof(pfmid); cdfwd.addStep(implMid[1], ProofRule::MODUS_PONENS, {eq1p[1], implMid}, {}); cdfwd.addStep(eq1p[0], ProofRule::EQ_RESOLVE, {eq[0], implMid[1]}, {}); - cdfwd.addStep(eq1p, ProofRule::AND_INTRO, {eq1p[0], eq1p[1]}, {}); + cdfwd.addStep(eq1p, ProofRule::AND_INTRO, {eq1p[0], eq1p[1]}, {}); Node impl = nm->mkNode(Kind::IMPLIES, eq[0], eq1p); cdfwd.addStep(impl, ProofRule::SCOPE, {eq1p}, {eq[0]}); cdp->addProof(cdfwd.getProofFor(impl)); - + // reverse proof is easy CDProof cdrev(d_env); cdrev.addProof(pfmid); cdrev.addStep(implMid[1], ProofRule::MODUS_PONENS, {eq1p[1], implMid}, {}); Node equivs = implMid[1][1].eqNode(implMid[1][0]); cdrev.addStep(equivs, ProofRule::SYMM, {implMid[1]}, {}); - cdrev.addStep(implMid[1][0], ProofRule::EQ_RESOLVE, {implMid[1][1], equivs}, {}); + cdrev.addStep( + implMid[1][0], ProofRule::EQ_RESOLVE, {implMid[1][1], equivs}, {}); Node implrev = nm->mkNode(Kind::IMPLIES, eq1p, eq[0]); cdrev.addStep(implrev, ProofRule::SCOPE, {eq[0]}, {eq1p[0], eq1p[1]}); cdp->addProof(cdrev.getProofFor(implrev)); - + // dual implication Node eqfinal = proveDualImplication(cdp, impl, implrev); - + // if we grouped the empty equations, we close with a transitive step // which we added via ACI_NORM above - if (eq1p!=eq[1]) + if (eq1p != eq[1]) { cdp->addStep(eq, ProofRule::TRANS, {eqfinal, eq1p.eqNode(eq[1])}, {}); } - + return true; } diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 0bfac9546d5..2761734164e 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1799,7 +1799,7 @@ Node SequencesRewriter::rewriteViaStrReplaceReAllEval(const Node& n) Node SequencesRewriter::rewriteViaOverlap(ProofRewriteRule id, const Node& n) { - if (n.getNumChildren()<2 || !n[1].isConst()) + if (n.getNumChildren() < 2 || !n[1].isConst()) { return Node::null(); } @@ -1809,44 +1809,44 @@ Node SequencesRewriter::rewriteViaOverlap(ProofRewriteRule id, const Node& n) { case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN: { - if (k!=Kind::STRING_CONTAINS || n[0].getNumChildren()!=3) + if (k != Kind::STRING_CONTAINS || n[0].getNumChildren() != 3) { return Node::null(); } overlap.emplace_back(n[0][1], 0); } - break; + break; case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN: { - if (k!=Kind::STRING_CONTAINS || n[0].getNumChildren()!=3) + if (k != Kind::STRING_CONTAINS || n[0].getNumChildren() != 3) { return Node::null(); } overlap.emplace_back(n[0][0], 1); overlap.emplace_back(n[0][2], -1); } - break; + break; case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF: { - if (k!=Kind::STRING_INDEXOF || n[0].getNumChildren()!=2 || n[2].isConst() || n[2].getConst().sgn()!=0) + if (k != Kind::STRING_INDEXOF || n[0].getNumChildren() != 2 + || n[2].isConst() || n[2].getConst().sgn() != 0) { return Node::null(); } overlap.emplace_back(n[0][1], -1); } - break; + break; case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE: { - if (k!=Kind::STRING_REPLACE || n[0].getNumChildren()!=3) + if (k != Kind::STRING_REPLACE || n[0].getNumChildren() != 3) { return Node::null(); } overlap.emplace_back(n[0][0], 1); overlap.emplace_back(n[0][2], -1); } - break; - default: - return Node::null(); + break; + default: return Node::null(); } for (const std::pair& f : overlap) { @@ -1861,20 +1861,23 @@ Node SequencesRewriter::rewriteViaOverlap(ProofRewriteRule id, const Node& n) return Node::null(); } } - - NodeManager * nm = nodeManager(); + + NodeManager* nm = nodeManager(); switch (id) { case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN: - return nm->mkNode(Kind::OR, nm->mkNode(k, n[0][0], n[1]), nm->mkNode(k, n[0][2], n[1])); + return nm->mkNode( + Kind::OR, nm->mkNode(k, n[0][0], n[1]), nm->mkNode(k, n[0][2], n[1])); case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN: return nm->mkNode(k, n[0][1], n[1]); case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF: return nm->mkNode(k, n[0][0], n[1], n[2]); case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE: - return nm->mkNode(Kind::STRING_CONCAT, n[0][0], nm->mkNode(k, n[0][1], n[1], n[2]), n[0][2]); - default: - break; + return nm->mkNode(Kind::STRING_CONCAT, + n[0][0], + nm->mkNode(k, n[0][1], n[1], n[2]), + n[0][2]); + default: break; } return Node::null(); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3330b8d6c0a..ebc2efd6e15 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -59,7 +59,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_termReg(env, *this, d_state, d_statistics), d_arithEntail( options().strings.stringRecArithApprox ? env.getRewriter() : nullptr, - options().strings.stringRecArithApprox), + options().strings.stringRecArithApprox), d_strEntail(d_env.getRewriter(), d_arithEntail), d_rewriter(env.getNodeManager(), d_arithEntail, diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index fbe4a99e000..b4b43a177d5 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -388,9 +388,9 @@ bool Word::noOverlapWith(TNode x, TNode y, int dir) switch (dir) { case 0: return sx.noOverlapWith(sy); - case -1: return sx.find(sy)==std::string::npos && sx.roverlap(sy)==0; - case 1: return sx.find(sy)==std::string::npos && sx.overlap(sy)==0; - default:break; + case -1: return sx.find(sy) == std::string::npos && sx.roverlap(sy) == 0; + case 1: return sx.find(sy) == std::string::npos && sx.overlap(sy) == 0; + default: break; } } else if (k == Kind::CONST_SEQUENCE) @@ -401,9 +401,9 @@ bool Word::noOverlapWith(TNode x, TNode y, int dir) switch (dir) { case 0: return sx.noOverlapWith(sy); - case -1: return sx.find(sy)==std::string::npos && sx.roverlap(sy)==0; - case 1: return sx.find(sy)==std::string::npos && sx.overlap(sy)==0; - default:break; + case -1: return sx.find(sy) == std::string::npos && sx.roverlap(sy) == 0; + case 1: return sx.find(sy) == std::string::npos && sx.overlap(sy) == 0; + default: break; } } Unimplemented(); diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp index d91b0b2045e..6e6630e8625 100644 --- a/src/theory/uf/proof_checker.cpp +++ b/src/theory/uf/proof_checker.cpp @@ -127,7 +127,7 @@ Node UfProofRuleChecker::checkInternal(ProofRule id, } NodeManager* nm = nodeManager(); Node l = nm->mkNode(k, lchildren); - if (l!=args[0]) + if (l != args[0]) { return Node::null(); }