pfn = cdp->getProofFor(children[i]);
pf->addProof(pfn);
// ensure we have a proof of var = subs
- Node veqs = var.eqNode(subs);
- if (veqs != children[index])
- {
- // should be true intro or false intro
- Assert(subs.isConst());
- pf->addStep(veqs,
- subs.getConst<bool>() ? PfRule::TRUE_INTRO
- : PfRule::FALSE_INTRO,
- {children[index]},
- {});
- }
+ Node veqs = addProofForSubsStep(var, subs, children[index], pf.get());
+ // transitivity
pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {});
// add to the substitution
vvec.push_back(var);
continue;
}
}
- // just use equality from CDProof
+ // Just use equality from CDProof, but ensure we have a proof in cdp.
+ // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
+ // uses the assumption children[index] as a Boolean assignment (e.g.
+ // children[index] = true if we are using MethodId::SB_LITERAL).
+ addProofForSubsStep(var, subs, children[index], cdp);
vvec.push_back(var);
svec.push_back(subs);
pgs.push_back(cdp);
return Node::null();
}
+Node ProofPostprocessCallback::addProofForSubsStep(Node var,
+ Node subs,
+ Node assump,
+ CDProof* cdp)
+{
+ // ensure we have a proof of var = subs
+ Node veqs = var.eqNode(subs);
+ if (veqs != assump)
+ {
+ // should be true intro or false intro
+ Assert(subs.isConst());
+ cdp->addStep(
+ veqs,
+ subs.getConst<bool>() ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO,
+ {assump},
+ {});
+ }
+ return veqs;
+}
+
bool ProofPostprocessCallback::addToTransChildren(Node eq,
std::vector<Node>& tchildren,
bool isSymm)
return true;
}
+ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
+ ProofNodeManager* pnm)
+ : d_ruleCount("finalProof::ruleCount"),
+ d_totalRuleCount("finalProof::totalRuleCount", 0),
+ d_pnm(pnm),
+ d_pedanticFailure(false)
+{
+ smtStatisticsRegistry()->registerStat(&d_ruleCount);
+ smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
+}
+
+ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
+ smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
+}
+
+void ProofPostprocessFinalCallback::initializeUpdate()
+{
+ d_pedanticFailure = false;
+ d_pedanticFailureOut.str("");
+}
+
+bool ProofPostprocessFinalCallback::shouldUpdate(ProofNode* pn)
+{
+ PfRule r = pn->getRule();
+ if (Trace.isOn("final-pf-hole"))
+ {
+ if (r == PfRule::THEORY_REWRITE)
+ {
+ Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult()
+ << std::endl;
+ }
+ }
+ // if not doing eager pedantic checking, fail if below threshold
+ if (!options::proofNewPedanticEager())
+ {
+ if (!d_pedanticFailure)
+ {
+ Assert(d_pedanticFailureOut.str().empty());
+ if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
+ {
+ d_pedanticFailure = true;
+ }
+ }
+ }
+ // record stats for the rule
+ d_ruleCount << r;
+ ++d_totalRuleCount;
+ return false;
+}
+
+bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const
+{
+ if (d_pedanticFailure)
+ {
+ out << d_pedanticFailureOut.str();
+ return true;
+ }
+ return false;
+}
+
+ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
+ SmtEngine* smte,
+ ProofGenerator* pppg)
+ : d_cb(pnm, smte, pppg), d_finalCb(pnm), d_pnm(pnm)
+{
+}
+
+ProofPostproccess::~ProofPostproccess() {}
+
+void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
+{
+ // Initialize the callback, which computes necessary static information about
+ // how to process, including how to process assumptions in pf.
+ d_cb.initializeUpdate();
+ // now, process
+ ProofNodeUpdater updater(d_pnm, d_cb);
+ updater.process(pf);
+ // take stats and check pedantic
+ d_finalCb.initializeUpdate();
+ ProofNodeUpdater finalizer(d_pnm, d_finalCb);
+ finalizer.process(pf);
+
+ std::stringstream serr;
+ bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr);
+ if (wasPedanticFailure)
+ {
+ AlwaysAssert(!wasPedanticFailure)
+ << "ProofPostproccess::process: pedantic failure:" << std::endl
+ << serr.str();
+ }
+}
+
+void ProofPostproccess::setEliminateRule(PfRule rule)
+{
+ d_cb.setEliminateRule(rule);
+}
+
} // namespace smt
} // namespace CVC4
* @return The conclusion of the TRANS step.
*/
Node addProofForTrans(const std::vector<Node>& tchildren, CDProof* cdp);
+ /**
+ * Add proof for substitution step. Some substitutions are derived based
+ * on viewing a formula as a Boolean assignment (see MethodId::SB_LITERAL for
+ * example). This method ensures that the proof of var == subs exists
+ * in cdp, where var, subs were derived from BuiltinProofRuleChecker's
+ * getSubstitution method.
+ *
+ * @param var The variable of the substitution
+ * @param subs The substituted term
+ * @param assump The formula the substitution was derived from
+ * @param cdp The proof to add to
+ * @return var == subs, the conclusion of the substitution step.
+ */
+ Node addProofForSubsStep(Node var, Node subs, Node assump, CDProof* cdp);
/** Add eq (or its symmetry) to transivity children, if not reflexive */
bool addToTransChildren(Node eq,
std::vector<Node>& tchildren,
bool isSymm = false);
};
+/** Final callback class, for stats and pedantic checking */
+class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
+{
+ public:
+ ProofPostprocessFinalCallback(ProofNodeManager* pnm);
+ ~ProofPostprocessFinalCallback();
+ /**
+ * Initialize, called once for each new ProofNode to process. This initializes
+ * static information to be used by successive calls to update.
+ */
+ void initializeUpdate();
+ /** Should proof pn be updated? Returns false, adds to stats. */
+ bool shouldUpdate(ProofNode* pn) override;
+ /** was pedantic failure */
+ bool wasPedanticFailure(std::ostream& out) const;
+
+ private:
+ /** Counts number of postprocessed proof nodes for each kind of proof rule */
+ HistogramStat<PfRule> d_ruleCount;
+ /** Total number of postprocessed rule applications */
+ IntStat d_totalRuleCount;
+ /** Proof node manager (used for pedantic checking) */
+ ProofNodeManager* d_pnm;
+ /** Was there a pedantic failure? */
+ bool d_pedanticFailure;
+ /** The pedantic failure string for debugging */
+ std::stringstream d_pedanticFailureOut;
+};
+
+/**
+ * The proof postprocessor module. This postprocesses the final proof
+ * produced by an SmtEngine. Its main two tasks are to:
+ * (1) Connect proofs of preprocessing,
+ * (2) Expand macro PfRule applications.
+ */
+class ProofPostproccess
+{
+ public:
+ ProofPostproccess(ProofNodeManager* pnm,
+ SmtEngine* smte,
+ ProofGenerator* pppg);
+ ~ProofPostproccess();
+ /** post-process */
+ void process(std::shared_ptr<ProofNode> pf);
+ /** set eliminate rule */
+ void setEliminateRule(PfRule rule);
+
+ private:
+ /** The post process callback */
+ ProofPostprocessCallback d_cb;
+ /** The post process callback for finalization */
+ ProofPostprocessFinalCallback d_finalCb;
+ /** The proof node manager */
+ ProofNodeManager* d_pnm;
+};
+
} // namespace smt
} // namespace CVC4
projects / cvc5.git / commitdiff