Fixes cvc5/cvc5-projects#439.
This extended (theory) proof step buffer with options for discarding duplicate conclusions. This option is now used in the strings theory proof construction, which may have duplication of conclusions due to purification. It simplifies some of the logic regarding popStep in this utility which is required due to the new policy.
#include "proof/proof_step_buffer.h"
+#include "proof/proof.h"
#include "proof/proof_checker.h"
using namespace cvc5::kind;
return out;
}
-ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {}
+ProofStepBuffer::ProofStepBuffer(ProofChecker* pc,
+ bool ensureUnique,
+ bool autoSym)
+ : d_autoSym(autoSym), d_checker(pc), d_ensureUnique(ensureUnique)
+{
+}
Node ProofStepBuffer::tryStep(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
Node expected)
+{
+ bool added;
+ return tryStep(added, id, children, args, expected);
+}
+
+Node ProofStepBuffer::tryStep(bool& added,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args,
+ Node expected)
{
if (d_checker == nullptr)
{
+ added = false;
Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker.";
return Node::null();
}
if (!res.isNull())
{
// add proof step
- d_steps.push_back(
- std::pair<Node, ProofStep>(res, ProofStep(id, children, args)));
+ added = addStep(id, children, args, res);
+ }
+ else
+ {
+ added = false;
}
return res;
}
-void ProofStepBuffer::addStep(PfRule id,
+bool ProofStepBuffer::addStep(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
Node expected)
{
+ if (d_ensureUnique)
+ {
+ if (d_allSteps.find(expected) != d_allSteps.end())
+ {
+ Trace("psb-debug") << "Discard " << expected << " from " << id
+ << std::endl;
+ return false;
+ }
+ d_allSteps.insert(expected);
+ // if we are automatically considering symmetry, we also add the symmetric
+ // fact here
+ if (d_autoSym)
+ {
+ Node sexpected = CDProof::getSymmFact(expected);
+ if (!sexpected.isNull())
+ {
+ d_allSteps.insert(sexpected);
+ }
+ }
+ Trace("psb-debug") << "Add " << expected << " from " << id << std::endl;
+ }
d_steps.push_back(
std::pair<Node, ProofStep>(expected, ProofStep(id, children, args)));
+ return true;
}
void ProofStepBuffer::addSteps(ProofStepBuffer& psb)
Assert(!d_steps.empty());
if (!d_steps.empty())
{
+ if (d_ensureUnique)
+ {
+ d_allSteps.erase(d_steps.back().first);
+ }
d_steps.pop_back();
}
}
return d_steps;
}
-void ProofStepBuffer::clear() { d_steps.clear(); }
+void ProofStepBuffer::clear()
+{
+ d_steps.clear();
+ d_allSteps.clear();
+}
} // namespace cvc5
class ProofStepBuffer
{
public:
- ProofStepBuffer(ProofChecker* pc = nullptr);
+ /**
+ * @param pc The proof checker we are using
+ * @param ensureUnique Whether we ensure that the conclusions of steps
+ * added to this buffer are unique. Later steps with the same conclusion as
+ * a previous one are discarded.
+ * @param autoSym Whether this proof step buffer is considering symmetry
+ * automatically. For example, this should be true if the steps of this buffer
+ * are being added to a CDProof with automatic symmetry. This impacts
+ * uniqueness of conclusions and whether certain steps are necessary.
+ */
+ ProofStepBuffer(ProofChecker* pc = nullptr,
+ bool ensureUnique = false,
+ bool autoSym = true);
~ProofStepBuffer() {}
/**
* Returns the conclusion of the proof step, as determined by the proof
const std::vector<Node>& children,
const std::vector<Node>& args,
Node expected = Node::null());
- /** Same as above, without checking */
- void addStep(PfRule id,
+ /** Same as try step, but tracks whether a step was added */
+ Node tryStep(bool& added,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args,
+ Node expected = Node::null());
+ /**
+ * Same as above, without checking
+ * @return true if a step was added. This may return false if e.g. expected
+ * was a duplicate conclusion.
+ */
+ bool addStep(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
Node expected);
/** Clear */
void clear();
+ protected:
+ /**
+ * Whether this proof step buffer is being added to a CDProof with automatic
+ * symmetry. This impacts uniqueness of conclusions and whether certain
+ * steps are necessary.
+ */
+ bool d_autoSym;
+
private:
/** The proof checker*/
ProofChecker* d_checker;
/** the queued proof steps */
std::vector<std::pair<Node, ProofStep>> d_steps;
+ /** Whether we are ensuring the conclusions in the buffer are unique */
+ bool d_ensureUnique;
+ /** The set of conclusions in steps */
+ std::unordered_set<Node> d_allSteps;
};
} // namespace cvc5
namespace cvc5 {
-TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
- : ProofStepBuffer(pc)
+TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc,
+ bool ensureUnique,
+ bool autoSym)
+ : ProofStepBuffer(pc, ensureUnique, autoSym)
{
}
std::vector<Node> args;
args.push_back(src);
addMethodIds(args, ids, ida, idr);
- Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
+ bool added;
+ Node res = tryStep(added, PfRule::MACRO_SR_EQ_INTRO, exp, args);
if (res.isNull())
{
// failed to apply
if (res != expected)
{
// did not provide the correct target
- popStep();
+ if (added)
+ {
+ popStep();
+ }
return false;
}
// successfully proved src == tgt.
MethodId idr)
{
// symmetric equalities
- if (CDProof::isSame(src, tgt))
+ if (d_autoSym && CDProof::isSame(src, tgt))
{
return true;
}
children.insert(children.end(), exp.begin(), exp.end());
std::vector<Node> args;
addMethodIds(args, ids, ida, idr);
- Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
- if (CDProof::isSame(src, srcRew))
+ bool added;
+ Node srcRew = tryStep(added, PfRule::MACRO_SR_PRED_ELIM, children, args);
+ if (d_autoSym && added && CDProof::isSame(src, srcRew))
{
popStep();
}
class TheoryProofStepBuffer : public ProofStepBuffer
{
public:
- TheoryProofStepBuffer(ProofChecker* pc = nullptr);
+ TheoryProofStepBuffer(ProofChecker* pc = nullptr,
+ bool ensureUnique = false,
+ bool autoSym = true);
~TheoryProofStepBuffer() {}
//---------------------------- utilities builtin proof rules
/**
// now go back and convert it to proof steps and add to proof
bool useBuffer = false;
ProofStep ps;
- TheoryProofStepBuffer psb(pf->getManager()->getChecker());
+ // ensure proof steps are unique
+ TheoryProofStepBuffer psb(pf->getManager()->getChecker(), true);
// run the conversion
convert(infer, isRev, conc, exp, ps, psb, useBuffer);
// make the proof based on the step or the buffer
}
// try to find a set of proof steps to incorporate into the buffer
psb.clear();
+ // explicitly add ASSUME steps to the proof step buffer for premises of the
+ // inference, so that they will not be overwritten in the reconstruction
+ // below
+ for (const Node& ec : ps.d_children)
+ {
+ Trace("strings-ipc-debug") << "Explicit add " << ec << std::endl;
+ psb.addStep(PfRule::ASSUME, {}, {ec}, ec);
+ }
NodeManager* nm = NodeManager::currentNM();
Node nodeIsRev = nm->mkConst(isRev);
switch (infer)
{
break;
}
+ Trace("strings-ipc-core")
+ << "Main equality after purify " << pmainEq << std::endl;
std::vector<Node> childrenSRew;
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, pmainEq))
- {
- Trace("strings-ipc-core") << "...undo step" << std::endl;
- // the rule added above was not necessary
- psb.popStep();
- }
- else if (mainEqSRew == conc)
+ if (mainEqSRew == conc)
{
Trace("strings-ipc-core") << "...success after rewrite!" << std::endl;
useBuffer = true;
// fail
break;
}
- else if (mainEqCeq == mainEqSRew)
- {
- Trace("strings-ipc-core") << "...undo step" << std::endl;
- // not necessary, probably first component of equality
- psb.popStep();
- }
// Now, mainEqCeq is an equality t ++ ... == s ++ ... where the
// inference involved t and s.
if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ
Node mainEqMain = psb.tryStep(rule, childrenMain, argsMain);
Trace("strings-ipc-core") << "Main equality after " << rule << " "
<< mainEqMain << std::endl;
- if (mainEqMain == mainEqCeq)
- {
- Trace("strings-ipc-core") << "...undo step" << std::endl;
- // not necessary, probably first component of equality
- psb.popStep();
- }
// either equal or rewrites to it
std::vector<Node> cexp;
if (psb.applyPredTransform(mainEqMain, conc, cexp))
* true. In this case, the argument psb is updated to contain (possibly
* multiple) proof steps for how to construct a proof for the given inference.
* In particular, psb will contain a set of steps that form a proof
- * whose conclusion is ii.d_conc and whose free assumptions are ii.d_ant.
+ * whose conclusion is conc and whose free assumptions are exp.
*/
static void convert(InferenceId infer,
bool isRev,
regress2/strings/issue6639-replace-re-all.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
+ regress2/strings/proj-439-cyclic-str-ipc.smt2
regress2/strings/proof-fail-083021-delta.smt2
regress2/strings/range-perf.smt2
regress2/strings/repl-repl-i-no-push.smt2
--- /dev/null
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-const x Int)
+(declare-fun u () String)
+(assert (and (not (= 0 (ite (str.prefixof "mo" u) 1 0))) (not (= 0 (ite (str.contains (str.substr (str.substr u 10 (str.len u)) 0 (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0))) "W") 1 0))) (= 0 (ite (not (= "aost" (str.++ (str.substr (str.substr u 1 (str.len u)) 0 (str.indexof (str.substr (str.substr u 10 (str.len u)) (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0)) (str.len (str.substr u 0 (str.len u)))) "W" 0)) (str.substr (str.++ (str.replace (str.substr (str.substr u 10 (str.len u)) 0 (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0))) "A" "a") (str.substr u 0 x)) (+ 1 (str.indexof (str.substr (str.substr u 10 (str.len u)) (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0)) (str.len (str.substr u 0 (str.len u)))) "W" 0)) (str.len (str.substr u 0 (str.len u))))))) 1 0))))
+(check-sat)
projects / cvc5.git / commitdiff