5511800a13340cba87c34468229145ccf656d3e0
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Gereon Kremer
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
13 * The implementation of the module for proofs for preprocessing in an
17 #include "smt/preprocess_proof_generator.h"
21 #include "options/proof_options.h"
22 #include "proof/proof.h"
23 #include "proof/proof_checker.h"
24 #include "proof/proof_node.h"
25 #include "theory/rewriter.h"
30 PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager
* pnm
,
36 d_ctx(c
? c
: &d_context
),
38 d_helperProofs(pnm
, d_ctx
),
39 d_inputPf(pnm
, c
, "InputProof"),
46 void PreprocessProofGenerator::notifyInput(Node n
)
48 notifyNewAssert(n
, &d_inputPf
);
51 void PreprocessProofGenerator::notifyNewAssert(Node n
, ProofGenerator
* pg
)
53 if (n
.isConst() && n
.getConst
<bool>())
55 // ignore true assertions
58 Trace("smt-proof-pp-debug")
59 << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n
60 << " from " << (pg
== nullptr ? "null" : pg
->identify()) << std::endl
;
61 if (d_src
.find(n
) == d_src
.end())
63 // if no proof generator provided for (non-true) assertion
66 checkEagerPedantic(d_ra
);
68 d_src
[n
] = TrustNode::mkTrustLemma(n
, pg
);
72 Trace("smt-proof-pp-debug") << "...already proven" << std::endl
;
76 void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn
)
78 notifyNewAssert(tn
.getProven(), tn
.getGenerator());
81 void PreprocessProofGenerator::notifyPreprocessed(Node n
,
85 // only do anything if indeed it rewrote
90 // call the trusted version
91 notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n
, np
, pg
));
94 void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp
)
98 // no rewrite, nothing to do
101 Assert(tnp
.getKind() == TrustNodeKind::REWRITE
);
102 Node np
= tnp
.getNode();
103 Trace("smt-proof-pp-debug")
104 << "PreprocessProofGenerator::notifyPreprocessed: " << tnp
<< std::endl
;
105 if (d_src
.find(np
) == d_src
.end())
107 if (tnp
.getGenerator() == nullptr)
109 checkEagerPedantic(d_rpp
);
115 Trace("smt-proof-pp-debug") << "...already proven" << std::endl
;
119 std::shared_ptr
<ProofNode
> PreprocessProofGenerator::getProofFor(Node f
)
121 Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
122 << ") input " << f
<< std::endl
;
123 NodeTrustNodeMap::iterator it
= d_src
.find(f
);
124 if (it
== d_src
.end())
126 Trace("smt-pppg") << "...no proof for " << identify() << " " << f
128 // could be an assumption, return nullptr
131 // make CDProof to construct the proof below
135 std::vector
<Node
> transChildren
;
136 std::unordered_set
<Node
> processed
;
138 // we connect the proof of f to its source via the map d_src until we
139 // discover that its source is a preprocessing lemma (a lemma stored in d_src)
140 // or otherwise it is assumed to be an input assumption.
144 if (it
!= d_src
.end())
146 Assert((*it
).second
.getNode() == curr
);
147 // get the proven node
148 Node proven
= (*it
).second
.getProven();
149 Assert(!proven
.isNull());
150 Trace("smt-pppg") << "...process proven " << proven
<< std::endl
;
151 if (processed
.find(proven
) != processed
.end())
153 Unhandled() << "Cyclic steps in preprocess proof generator";
156 processed
.insert(proven
);
157 bool proofStepProcessed
= false;
159 // if a generator for the step was provided, it is stored in the proof
160 Trace("smt-pppg-debug")
161 << "...get provided proof " << (*it
).second
<< std::endl
;
162 std::shared_ptr
<ProofNode
> pfr
= (*it
).second
.toProofNode();
165 Trace("smt-pppg-debug") << "...add provided " << *pfr
<< std::endl
;
166 Assert(pfr
->getResult() == proven
);
168 proofStepProcessed
= true;
171 Trace("smt-pppg-debug") << "...update" << std::endl
;
172 TrustNodeKind tnk
= (*it
).second
.getKind();
173 if (tnk
== TrustNodeKind::REWRITE
)
175 Trace("smt-pppg-debug")
176 << "...rewritten from " << proven
[0] << std::endl
;
177 Assert(proven
.getKind() == kind::EQUAL
);
178 if (!proofStepProcessed
)
180 // maybe its just a simple rewrite?
181 if (proven
[1] == theory::Rewriter::rewrite(proven
[0]))
183 Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl
;
184 cdp
.addStep(proven
, PfRule::REWRITE
, {}, {proven
[0]});
185 proofStepProcessed
= true;
188 transChildren
.push_back(proven
);
189 // continue with source
192 // find the next node
193 Trace("smt-pppg") << "...continue " << curr
<< std::endl
;
194 it
= d_src
.find(curr
);
198 Trace("smt-pppg") << "...lemma" << std::endl
;
199 Assert(tnk
== TrustNodeKind::LEMMA
);
202 if (!proofStepProcessed
)
204 Trace("smt-pppg-debug")
205 << "...justify missing step with "
206 << (tnk
== TrustNodeKind::LEMMA
? d_ra
: d_rpp
) << std::endl
;
207 // add trusted step, the rule depends on the kind of trust node
209 proven
, tnk
== TrustNodeKind::LEMMA
? d_ra
: d_rpp
, {}, {proven
});
214 // prove ( curr == f ), which is not necessary if they are the same
216 if (!CDProof::isSame(f
, curr
))
218 Node fullRewrite
= curr
.eqNode(f
);
219 if (transChildren
.size() >= 2)
221 Trace("smt-pppg") << "...apply trans to get " << fullRewrite
<< std::endl
;
222 std::reverse(transChildren
.begin(), transChildren
.end());
223 cdp
.addStep(fullRewrite
, PfRule::TRANS
, transChildren
, {});
225 Trace("smt-pppg") << "...eq_resolve to prove" << std::endl
;
227 cdp
.addStep(f
, PfRule::EQ_RESOLVE
, {curr
, fullRewrite
}, {});
228 Trace("smt-pppg") << "...finished" << std::endl
;
231 // overall, proof is:
232 // --------- from proof generator ---------- from proof generator
233 // F_1 = F_2 ... F_{n-1} = F_n
234 // ---? -------------------------------------------------- TRANS
236 // ---------------- EQ_RESOLVE
238 // Note F_1 may have been given a proof if it was not an input assumption.
240 return cdp
.getProofFor(f
);
243 ProofNodeManager
* PreprocessProofGenerator::getManager() { return d_pnm
; }
245 LazyCDProof
* PreprocessProofGenerator::allocateHelperProof()
247 return d_helperProofs
.allocateProof(nullptr, d_ctx
);
250 std::string
PreprocessProofGenerator::identify() const { return d_name
; }
252 void PreprocessProofGenerator::checkEagerPedantic(PfRule r
)
254 if (options::proofEagerChecking())
256 // catch a pedantic failure now, which otherwise would not be
257 // triggered since we are doing lazy proof generation
258 ProofChecker
* pc
= d_pnm
->getChecker();
259 std::stringstream serr
;
260 if (pc
->isPedanticFailure(r
, serr
))
262 Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "