{
Trace("strings-ipc-debug") << "InferProofCons::convert: " << infer
<< (isRev ? " :rev " : " ") << conc << std::endl;
- for (const Node& ec : exp)
+ for (const Node& ec : ps.d_children)
{
Trace("strings-ipc-debug") << " e: " << ec << std::endl;
}
case InferenceId::STRINGS_NORMAL_FORM:
case InferenceId::STRINGS_CODE_PROXY:
{
- ps.d_args.push_back(conc);
- // will attempt this rule
- ps.d_rule = PfRule::MACRO_SR_PRED_INTRO;
+ std::vector<Node> pcs = ps.d_children;
+ Node pconc = conc;
+ // purify core substitution proves conc from pconc if necessary,
+ // we apply MACRO_SR_PRED_INTRO to prove pconc
+ if (purifyCoreSubstitution(pconc, pcs, psb, false))
+ {
+ if (psb.applyPredIntro(pconc, pcs))
+ {
+ useBuffer = true;
+ }
+ }
}
break;
// ========================== substitution + rewriting
break;
}
// apply MACRO_SR_PRED_ELIM using equalities up to the main eq
+ // we purify the core substitution
+ std::vector<Node> pcsr(ps.d_children.begin(),
+ ps.d_children.begin() + mainEqIndex);
+ Node pmainEq = mainEq;
+ // we transform mainEq to pmainEq and then use this as the first
+ // argument to MACRO_SR_PRED_ELIM.
+ if (!purifyCoreSubstitution(pmainEq, pcsr, psb, true))
+ {
+ break;
+ }
std::vector<Node> childrenSRew;
- childrenSRew.push_back(mainEq);
- childrenSRew.insert(childrenSRew.end(),
- ps.d_children.begin(),
- ps.d_children.begin() + mainEqIndex);
+ childrenSRew.push_back(pmainEq);
+ childrenSRew.insert(childrenSRew.end(), pcsr.begin(), pcsr.end());
+ // now, conclude the proper equality
Node mainEqSRew =
psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {});
- if (CDProof::isSame(mainEqSRew, mainEq))
+ if (CDProof::isSame(mainEqSRew, pmainEq))
{
Trace("strings-ipc-core") << "...undo step" << std::endl;
// the rule added above was not necessary
return "strings::InferProofCons";
}
+bool InferProofCons::purifyCoreSubstitution(Node& tgt,
+ std::vector<Node>& children,
+ TheoryProofStepBuffer& psb,
+ bool concludeTgtNew) const
+{
+ // collect the terms to purify, which are the LHS of the substitution
+ std::unordered_set<Node> termsToPurify;
+ for (const Node& nc : children)
+ {
+ Assert(nc.getKind() == EQUAL && nc[0].getType().isStringLike());
+ termsToPurify.insert(nc[0]);
+ }
+ // now, purify each of the children of the substitution
+ for (size_t i = 0, nchild = children.size(); i < nchild; i++)
+ {
+ Node pnc = purifyCorePredicate(children[i], true, psb, termsToPurify);
+ if (pnc.isNull())
+ {
+ return false;
+ }
+ if (children[i] != pnc)
+ {
+ Trace("strings-ipc-pure-subs")
+ << "Converted: " << children[i] << " to " << pnc << std::endl;
+ children[i] = pnc;
+ }
+ // we now should have a substitution with only atomic terms
+ Assert(children[i][0].getNumChildren() == 0);
+ }
+ // now, purify the target predicate
+ tgt = purifyCorePredicate(tgt, concludeTgtNew, psb, termsToPurify);
+ return !tgt.isNull();
+}
+
+Node InferProofCons::purifyCorePredicate(
+ Node lit,
+ bool concludeNew,
+ TheoryProofStepBuffer& psb,
+ std::unordered_set<Node>& termsToPurify) const
+{
+ bool pol = lit.getKind() != NOT;
+ Node atom = pol ? lit : lit[0];
+ if (atom.getKind() != EQUAL || !atom[0].getType().isStringLike())
+ {
+ // we only purify string (dis)equalities
+ return lit;
+ }
+ // purify both sides of the equality
+ std::vector<Node> pcs;
+ bool childChanged = false;
+ for (const Node& lc : atom)
+ {
+ Node plc = purifyCoreTerm(lc, termsToPurify);
+ childChanged = childChanged || plc != lc;
+ pcs.push_back(plc);
+ }
+ if (!childChanged)
+ {
+ return lit;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ Node newLit = nm->mkNode(EQUAL, pcs);
+ if (!pol)
+ {
+ newLit = newLit.notNode();
+ }
+ Assert(lit != newLit);
+ // prove by transformation, should always succeed
+ if (!psb.applyPredTransform(
+ concludeNew ? lit : newLit, concludeNew ? newLit : lit, {}))
+ {
+ // failed, return null
+ return Node::null();
+ }
+ return newLit;
+}
+
+Node InferProofCons::purifyCoreTerm(
+ Node n, std::unordered_set<Node>& termsToPurify) const
+{
+ Assert(n.getType().isStringLike());
+ if (n.getNumChildren() == 0)
+ {
+ return n;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ if (n.getKind() == STRING_CONCAT)
+ {
+ std::vector<Node> pcs;
+ for (const Node& nc : n)
+ {
+ pcs.push_back(purifyCoreTerm(nc, termsToPurify));
+ }
+ return nm->mkNode(STRING_CONCAT, pcs);
+ }
+ if (termsToPurify.find(n) == termsToPurify.end())
+ {
+ // did not need to purify
+ return n;
+ }
+ SkolemManager* sm = nm->getSkolemManager();
+ Node k = sm->mkPurifySkolem(n, "k");
+ return k;
+}
+
} // namespace strings
} // namespace theory
} // namespace cvc5
* conclusion, or null if we were not able to construct a TRANS step.
*/
Node convertTrans(Node eqa, Node eqb, TheoryProofStepBuffer& psb);
+ /**
+ * Purify core substitution.
+ *
+ * When reconstructing proofs for the core strings calculus, we rely on
+ * sequential substitutions for constructing proofs involving recursive
+ * computation of normal forms. However, this can be incorrect in cases where
+ * a term like (str.replace x a b) is being treated as an atomic term,
+ * and a substitution applied over (str.replace x a b) -> c, x -> d.
+ * This can lead to the term (str.replace d a b) being generated instead of
+ * c.
+ *
+ * As an example of this method, given input:
+ * tgt = (= x (str.++ (f x) c))
+ * children = { (= (f x) a), (= x (str.++ b (f x))) }
+ * concludeTgtNew = true
+ * This method updates:
+ * tgt = (= x (str.++ k c))
+ * children = { (= k a), (= x (str.++ b k)) }
+ * where k is the purification skolem for (f x). Additionally, it ensures
+ * that psb has a proof of:
+ * (= x (str.++ k c)) from (= x (str.++ (f x) c))
+ * ...note the direction, since concludeTgtNew = true
+ * (= k a) from (= (f x) a)
+ * (= x (str.++ b k)) from (= x (str.++ b (f x)))
+ * Notice that the resulting substitution can now be safely used as a
+ * sequential substution, since (f x) has been purified with k. The proofs
+ * in psb ensure that a proof step involving the purified substitution will
+ * have the same net effect as a proof step using the original substitution.
+ *
+ * @param tgt The term we were originally going to apply the substitution to.
+ * @param children The premises corresponding to the substitution.
+ * @param psb The proof step buffer
+ * @param concludeTgtNew Whether we require proving the purified form of
+ * tgt from tgt or vice versa.
+ * @return true if we successfully purified the substitution and the target
+ * term. Additionally, if successful, we ensure psb contains proofs of
+ * children'[i] from children[i] for all i, and tgt' from tgt (or vice versa
+ * based on concludeTgtNew).
+ */
+ bool purifyCoreSubstitution(Node& tgt,
+ std::vector<Node>& children,
+ TheoryProofStepBuffer& psb,
+ bool concludeTgtNew = false) const;
+ /**
+ * Return the purified form of the predicate lit with respect to a set of
+ * terms to purify, call the returned literal lit'.
+ * If concludeNew is true, then we add a proof of lit' from lit in psb;
+ * otherwise we add a proof of lit from lit'.
+ * Note that string predicates that require purification are string
+ * (dis)equalities only.
+ */
+ Node purifyCorePredicate(Node lit,
+ bool concludeNew,
+ TheoryProofStepBuffer& psb,
+ std::unordered_set<Node>& termsToPurify) const;
+ /**
+ * Purify term with respect to a set of terms to purify. This replaces
+ * all terms to purify with their purification variables that occur in
+ * positions that are relevant for the core calculus of strings (direct
+ * children of concat or equal).
+ */
+ Node purifyCoreTerm(Node n, std::unordered_set<Node>& termsToPurify) const;
/** the proof node manager */
ProofNodeManager* d_pnm;
/** The lazy fact map */
projects / cvc5.git / commitdiff