}
traversing.push_back(cur);
visit.push_back(cur);
- if (d_mergeSubproofs)
+ // If we are not the top-level proof, we were a scope, or became a scope
+ // after updating, we do a separate recursive call to this method. This
+ // allows us to properly track the assumptions in scope, which is
+ // important for example to merge or to determine updates based on free
+ // assumptions.
+ if (cur->getRule() == PfRule::SCOPE && cur != pf)
{
- // If we are not the top-level proof, we were a scope, or became a
- // scope after updating, we need to make a separate recursive call to
- // this method. This is not necessary if we are not merging subproofs.
- if (cur->getRule() == PfRule::SCOPE && cur != pf)
- {
- std::vector<Node> nfa;
- // if we are debugging free assumptions, update the set
- if (d_debugFreeAssumps)
- {
- nfa.insert(nfa.end(), fa.begin(), fa.end());
- const std::vector<Node>& args = cur->getArguments();
- nfa.insert(nfa.end(), args.begin(), args.end());
- Trace("pfnu-debug2")
- << "Process new scope with " << args << std::endl;
- }
- // Process in new call separately, since we should not cache
- // the results of proofs that have a different scope.
- processInternal(cur, nfa, traversing);
- continue;
- }
+ std::vector<Node> nfa;
+ nfa.insert(nfa.end(), fa.begin(), fa.end());
+ const std::vector<Node>& args = cur->getArguments();
+ nfa.insert(nfa.end(), args.begin(), args.end());
+ Trace("pfnu-debug2") << "Process new scope with " << args << std::endl;
+ // Process in new call separately
+ processInternal(cur, nfa, traversing);
+ continue;
}
const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
// now, process children
bool& continueUpdate)
{
// should it be updated?
- if (!d_cb.shouldUpdate(cur, continueUpdate))
+ if (!d_cb.shouldUpdate(cur, fa, continueUpdate))
{
return false;
}
// store in the proof
cpf.addProof(cp);
}
- Trace("pf-process-debug")
- << "Updating (" << cur->getRule() << ")..." << std::endl;
Node res = cur->getResult();
+ Trace("pf-process-debug")
+ << "Updating (" << cur->getRule() << "): " << res << std::endl;
// only if the callback updated the node
if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
{
/** Should proof pn be updated?
*
* @param pn the proof node that maybe should be updated
+ * @param fa the assumptions in scope
* @param continueUpdate whether we should continue recursively updating pn
* @return whether we should run the update method on pn
*/
virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa,
bool& continueUpdate) = 0;
/**
* Update the proof rule application, store steps in cdp. Return true if
[[option.mode.DOT]]
name = "dot"
help = "Output DOT proof"
-
+[[option.mode.VERIT]]
+ name = "verit"
+ help = "Output veriT proof"
+
[[option]]
name = "proofPrintConclusion"
category = "regular"
void ProofPostprocessCallback::initializeUpdate() { d_assumpToProof.clear(); }
bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa,
bool& continueUpdate)
{
bool result = pn->getRule() == PfRule::ASSUME
* cancelled, i.e., continueUpdate is set to false.
*/
bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa,
bool& continueUpdate) override;
/** Update the proof rule application.
*
d_pnm(new ProofNodeManager(d_pchecker.get())),
d_pppg(new PreprocessProofGenerator(
d_pnm.get(), u, "smt::PreprocessProofGenerator")),
- d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
+ d_pfpp(new ProofPostproccess(
+ d_pnm.get(),
+ smte,
+ d_pppg.get(),
+ // by default the post-processor will update all assumptions, which
+ // can lead to SCOPE subproofs of the form
+ // A
+ // ...
+ // B1 B2
+ // ... ...
+ // ------------
+ // C
+ // ------------- SCOPE [B1, B2]
+ // B1 ^ B2 => C
+ //
+ // where A is an available assumption from outside the scope (note
+ // that B1 was an assumption of this SCOPE subproof but since it could
+ // be inferred from A, it was updated). This shape is problematic for
+ // the veriT reconstruction, so we disable the update of scoped
+ // assumptions (which would disable the update of B1 in this case).
+ options::proofFormatMode() != options::ProofFormatMode::VERIT)),
d_finalProof(nullptr)
{
// add rules to eliminate here
}
// TODO (proj #37) according to the proof format, post process the proof node
// TODO (proj #37) according to the proof format, print the proof node
-
+
if (options::proofFormatMode() == options::ProofFormatMode::DOT)
{
proof::DotPrinter::print(out, fp.get());
ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm,
SmtEngine* smte,
- ProofGenerator* pppg)
- : d_pnm(pnm), d_smte(smte), d_pppg(pppg), d_wfpm(pnm)
+ ProofGenerator* pppg,
+ bool updateScopedAssumptions)
+ : d_pnm(pnm),
+ d_smte(smte),
+ d_pppg(pppg),
+ d_wfpm(pnm),
+ d_updateScopedAssumptions(updateScopedAssumptions)
{
d_true = NodeManager::currentNM()->mkConst(true);
- // always check whether to update ASSUME
- d_elimRules.insert(PfRule::ASSUME);
}
void ProofPostprocessCallback::initializeUpdate()
}
bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa,
bool& continueUpdate)
{
- return d_elimRules.find(pn->getRule()) != d_elimRules.end();
+ PfRule id = pn->getRule();
+ if (d_elimRules.find(id) != d_elimRules.end())
+ {
+ return true;
+ }
+ // other than elimination rules, we always update assumptions as long as
+ // d_updateScopedAssumptions is true or they are *not* in scope, i.e., not in
+ // fa
+ if (id != PfRule::ASSUME
+ || (!d_updateScopedAssumptions
+ && std::find(fa.begin(), fa.end(), pn->getResult()) != fa.end()))
+ {
+ Trace("smt-proof-pp-debug")
+ << "... not updating in-scope assumption " << pn->getResult() << "\n";
+ return false;
+ }
+ return true;
}
bool ProofPostprocessCallback::update(Node res,
}
bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa,
bool& continueUpdate)
{
PfRule r = pn->getRule();
ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
SmtEngine* smte,
- ProofGenerator* pppg)
+ ProofGenerator* pppg,
+ bool updateScopedAssumptions)
: d_pnm(pnm),
- d_cb(pnm, smte, pppg),
+ d_cb(pnm, smte, pppg, updateScopedAssumptions),
// the update merges subproofs
d_updater(d_pnm, d_cb, true),
d_finalCb(pnm),
public:
ProofPostprocessCallback(ProofNodeManager* pnm,
SmtEngine* smte,
- ProofGenerator* pppg);
+ ProofGenerator* pppg,
+ bool updateScopedAssumptions);
~ProofPostprocessCallback() {}
/**
* Initialize, called once for each new ProofNode to process. This initializes
void setEliminateRule(PfRule rule);
/** Should proof pn be updated? */
bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa,
bool& continueUpdate) override;
/** Update the proof rule application. */
bool update(Node res,
std::vector<Node> d_wfAssumptions;
/** Kinds of proof rules we are eliminating */
std::unordered_set<PfRule, PfRuleHashFunction> d_elimRules;
+ /** Whether we post-process assumptions in scope. */
+ bool d_updateScopedAssumptions;
//---------------------------------reset at the begining of each update
/** Mapping assumptions to their proof from preprocessing */
std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
void initializeUpdate();
/** Should proof pn be updated? Returns false, adds to stats. */
bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa,
bool& continueUpdate) override;
/** was pedantic failure */
bool wasPedanticFailure(std::ostream& out) const;
class ProofPostproccess
{
public:
+ /**
+ * @param pnm The proof node manager we are using
+ * @param smte The SMT engine whose proofs are being post-processed
+ * @param pppg The proof generator for pre-processing proofs
+ * @param updateScopedAssumptions Whether we post-process assumptions in
+ * scope. Since doing so is sound and only problematic depending on who is
+ * consuming the proof, it's true by default.
+ */
ProofPostproccess(ProofNodeManager* pnm,
SmtEngine* smte,
- ProofGenerator* pppg);
+ ProofGenerator* pppg,
+ bool updateScopedAssumptions = true);
~ProofPostproccess();
/** post-process */
void process(std::shared_ptr<ProofNode> pf);
regress0/printer/let_shadowing.smt2
regress0/printer/symbol_starting_w_digit.smt2
regress0/printer/tuples_and_records.cvc
+ regress0/proofs/scope.smt2
regress0/push-pop/boolean/fuzz_12.smt2
regress0/push-pop/boolean/fuzz_13.smt2
regress0/push-pop/boolean/fuzz_14.smt2
--- /dev/null
+; COMMAND-LINE: --produce-proofs
+; EXIT: 0
+; SCRUBBER: grep -v -E '.*'
+(set-logic AUFLIA)
+(declare-sort A$ 0)
+(declare-sort B$ 0)
+(declare-sort C$ 0)
+(declare-sort D$ 0)
+(declare-sort E$ 0)
+(declare-sort F$ 0)
+(declare-sort G$ 0)
+(declare-sort H$ 0)
+(declare-sort I$ 0)
+(declare-sort J$ 0)
+(declare-sort K$ 0)
+(declare-sort L$ 0)
+(declare-sort M$ 0)
+(declare-sort N$ 0)
+(declare-sort O$ 0)
+(declare-sort P$ 0)
+(declare-fun f1$ (M$ J$) L$)
+(declare-fun f2$ (N$ C$) L$)
+(declare-fun f3$ (C$ A$) B$)
+(declare-fun f4$ (D$ E$) B$)
+(declare-fun f5$ (F$ G$) D$)
+(declare-fun f6$ (A$) F$)
+(declare-fun f7$ (A$) G$)
+(declare-fun f8$ (A$) E$)
+(declare-fun f9$ (A$) E$)
+(declare-fun x1$ () M$)
+(declare-fun x2$ () N$)
+(declare-fun x3$ () C$)
+(declare-fun x4$ () C$)
+(declare-fun x5$ () D$)
+(declare-fun x6$ () J$)
+(declare-fun x7$ () J$)
+(declare-fun x8$ () M$)
+(declare-fun x9$ () O$)
+(declare-fun f10$ (H$ A$) K$)
+(declare-fun f3a$ (E$ H$) I$)
+(declare-fun f3b$ (J$ K$) I$)
+(declare-fun f5a$ (O$ P$) N$)
+(declare-fun x10$ () P$)
+(assert (! (forall ((?v0 A$)) (not (= (f3$ x3$ ?v0) (f4$ (f5$ (f6$ ?v0) (f7$ ?v0)) (f8$ ?v0))))) :named a0))
+(assert (! (forall ((?v0 A$)) (not (= (f3$ x4$ ?v0) (f4$ x5$ (f9$ ?v0))))) :named a1))
+(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f8$ ?v0) ?v1) (f3b$ x6$ (f10$ ?v1 ?v0))))) :named a2))
+(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f9$ ?v0) ?v1) (f3b$ x7$ (f10$ ?v1 ?v0))))) :named a3))
+(assert (! (not (= (f1$ x8$ x6$) (f2$ (f5a$ x9$ x10$) x3$))) :named a4))
+(assert (! (= (f1$ x1$ x7$) (f1$ x8$ x6$)) :named a5))
+(assert (! (= (f1$ x1$ x7$) (f2$ x2$ x4$)) :named a6))
+(assert (! (= (f2$ x2$ x4$) (f2$ (f5a$ x9$ x10$) x3$)) :named a7))
+(assert (! (not false) :named a8))
+(check-sat)
+(get-proof)
\ No newline at end of file
projects / cvc5.git / commitdiff