Skip to content

Commit

Permalink
Format
Browse files Browse the repository at this point in the history
  • Loading branch information
@ajreynol
ajreynol committed Jan 28, 2025
1 parent 3305380 commit ec7e134
Show file tree
Hide file tree
Showing 6 changed files with 53 additions and 47 deletions.
12 changes: 8 additions & 4 deletions src/api/cpp/cvc5_proof_rule_template.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
35 changes: 17 additions & 18 deletions src/rewriter/basic_rewrite_rcons.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Node> 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]);
Expand Down Expand Up @@ -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<Node> concat;
std::map<Node, Node> 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;
}
Expand Down Expand Up @@ -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<ProofNode> 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;
}

Expand Down
37 changes: 20 additions & 17 deletions src/theory/strings/sequences_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
Expand All @@ -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<Rational>().sgn()!=0)
if (k != Kind::STRING_INDEXOF || n[0].getNumChildren() != 2
|| n[2].isConst() || n[2].getConst<Rational>().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<Node, int>& f : overlap)
{
Expand All @@ -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();
}
Expand Down
2 changes: 1 addition & 1 deletion src/theory/strings/theory_strings.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
12 changes: 6 additions & 6 deletions src/theory/strings/word.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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();
Expand Down
2 changes: 1 addition & 1 deletion src/theory/uf/proof_checker.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
Expand Down

0 comments on commit ec7e134

Please sign in to comment.