Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Abdalrhman Mohamed, Haniel Barbosa
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * ****************************************************************************
12 : : *
13 : : * The proof manager of the SMT engine.
14 : : */
15 : :
16 : : #include "smt/proof_manager.h"
17 : :
18 : : #include "options/base_options.h"
19 : : #include "options/main_options.h"
20 : : #include "options/smt_options.h"
21 : : #include "proof/alethe/alethe_node_converter.h"
22 : : #include "proof/alethe/alethe_post_processor.h"
23 : : #include "proof/alethe/alethe_printer.h"
24 : : #include "proof/alf/alf_printer.h"
25 : : #include "proof/dot/dot_printer.h"
26 : : #include "proof/lfsc/lfsc_post_processor.h"
27 : : #include "proof/lfsc/lfsc_printer.h"
28 : : #include "proof/proof_checker.h"
29 : : #include "proof/proof_node_algorithm.h"
30 : : #include "proof/proof_node_manager.h"
31 : : #include "rewriter/rewrite_db.h"
32 : : #include "smt/assertions.h"
33 : : #include "smt/difficulty_post_processor.h"
34 : : #include "smt/env.h"
35 : : #include "smt/preprocess_proof_generator.h"
36 : : #include "smt/proof_post_processor.h"
37 : : #include "smt/smt_solver.h"
38 : :
39 : : using namespace cvc5::internal::rewriter;
40 : : namespace cvc5::internal {
41 : : namespace smt {
42 : :
43 : 18616 : PfManager::PfManager(Env& env)
44 : : : EnvObj(env),
45 : : d_rewriteDb(nullptr),
46 : : d_pchecker(nullptr),
47 : : d_pnm(nullptr),
48 : 18616 : d_pfpp(nullptr)
49 : : {
50 : : // construct the rewrite db only if DSL rewrites are enabled
51 : 18616 : if (options().proof.proofGranularityMode
52 : : == options::ProofGranularityMode::DSL_REWRITE
53 [ + + ][ - + ]: 18616 : || options().proof.proofGranularityMode
[ + + ]
54 : : == options::ProofGranularityMode::DSL_REWRITE_STRICT)
55 : : {
56 : 3185 : d_rewriteDb.reset(new RewriteDb);
57 [ - + ]: 3185 : if (isOutputOn(OutputTag::RARE_DB))
58 : : {
59 [ - - ]: 0 : if (options().proof.proofFormatMode != options::ProofFormatMode::CPC)
60 : : {
61 [ - - ]: 0 : Warning()
62 : : << "WARNING: Assuming --proof-format=cpc when printing the RARE "
63 : 0 : "database with -o rare-db"
64 : 0 : << std::endl;
65 : : }
66 : 0 : proof::AlfNodeConverter atp(nodeManager());
67 : 0 : proof::AlfPrinter alfp(d_env, atp, d_rewriteDb.get());
68 : : const std::map<ProofRewriteRule, RewriteProofRule>& rules =
69 : 0 : d_rewriteDb->getAllRules();
70 : 0 : std::stringstream ss;
71 [ - - ]: 0 : for (const std::pair<const ProofRewriteRule, RewriteProofRule>& r : rules)
72 : : {
73 : 0 : alfp.printDslRule(ss, r.first);
74 : : }
75 : 0 : output(OutputTag::RARE_DB) << ss.str();
76 : : }
77 : : }
78 : : // enable the proof checker and the proof node manager
79 : 18616 : d_pchecker.reset(
80 : 18616 : new ProofChecker(statisticsRegistry(),
81 : 18616 : options().proof.proofCheck,
82 : 18616 : static_cast<uint32_t>(options().proof.proofPedantic),
83 : 18616 : d_rewriteDb.get()));
84 : 18616 : d_pnm.reset(new ProofNodeManager(
85 : 18616 : env.getOptions(), env.getRewriter(), d_pchecker.get()));
86 : : // Now, initialize the proof postprocessor with the environment.
87 : : // By default the post-processor will update all assumptions, which
88 : : // can lead to SCOPE subproofs of the form
89 : : // A
90 : : // ...
91 : : // B1 B2
92 : : // ... ...
93 : : // ------------
94 : : // C
95 : : // ------------- SCOPE [B1, B2]
96 : : // B1 ^ B2 => C
97 : : //
98 : : // where A is an available assumption from outside the scope (note
99 : : // that B1 was an assumption of this SCOPE subproof but since it could
100 : : // be inferred from A, it was updated). This shape is problematic for
101 : : // the Alethe reconstruction, so we disable the update of scoped
102 : : // assumptions (which would disable the update of B1 in this case).
103 : 18616 : d_pfpp = std::make_unique<ProofPostprocess>(
104 : : env,
105 : 18616 : d_rewriteDb.get(),
106 : 37232 : options().proof.proofFormatMode != options::ProofFormatMode::ALETHE);
107 : :
108 : : // add rules to eliminate here
109 : 18616 : if (options().proof.proofGranularityMode
110 [ + + ]: 18616 : != options::ProofGranularityMode::MACRO)
111 : : {
112 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_EQ_INTRO);
113 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_PRED_INTRO);
114 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_PRED_ELIM);
115 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_SR_PRED_TRANSFORM);
116 : : // Alethe does not require macro resolution to be expanded
117 [ + + ]: 10371 : if (options().proof.proofFormatMode != options::ProofFormatMode::ALETHE)
118 : : {
119 : 8895 : d_pfpp->setEliminateRule(ProofRule::MACRO_RESOLUTION_TRUST);
120 : 8895 : d_pfpp->setEliminateRule(ProofRule::MACRO_RESOLUTION);
121 : : }
122 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_ARITH_SCALE_SUM_UB);
123 : 10371 : if (options().proof.proofGranularityMode
124 [ + - ]: 10371 : != options::ProofGranularityMode::REWRITE)
125 : : {
126 : 10371 : d_pfpp->setEliminateRule(ProofRule::SUBS);
127 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_REWRITE);
128 : : // if in a DSL rewrite mode
129 : 10371 : if (options().proof.proofGranularityMode
130 [ + + ]: 10371 : != options::ProofGranularityMode::THEORY_REWRITE)
131 : : {
132 : : // this eliminates theory rewriting steps with finer-grained DSL rules
133 : 3185 : d_pfpp->setEliminateAllTrustedRules();
134 : : }
135 : : }
136 : : // theory-specific lazy proof reconstruction
137 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_STRING_INFERENCE);
138 : 10371 : d_pfpp->setEliminateRule(ProofRule::MACRO_BV_BITBLAST);
139 : : // we only try to eliminate TRUST if not macro level
140 : 10371 : d_pfpp->setEliminateRule(ProofRule::TRUST);
141 : : }
142 : 18616 : d_false = nodeManager()->mkConst(false);
143 : 18616 : }
144 : :
145 : 37203 : PfManager::~PfManager() {}
146 : :
147 : : // TODO: Remove in favor of `std::erase_if` with C++ 20+ (see cvc5-wishues#137).
148 : : template <class T, class Alloc, class Pred>
149 : 10178 : constexpr typename std::vector<T, Alloc>::size_type erase_if(
150 : : std::vector<T, Alloc>& c, Pred pred)
151 : : {
152 : : typename std::vector<T, Alloc>::iterator it =
153 : 10178 : std::remove_if(c.begin(), c.end(), pred);
154 : 10178 : typename std::vector<T, Alloc>::size_type r = std::distance(it, c.end());
155 : 10178 : c.erase(it, c.end());
156 : 10178 : return r;
157 : : }
158 : :
159 : 13852 : std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
160 : : std::shared_ptr<ProofNode> pfn, SmtSolver& smt, ProofScopeMode scopeMode)
161 : : {
162 : 13852 : Assertions& as = smt.getAssertions();
163 : : PreprocessProofGenerator* pppg =
164 : 13852 : smt.getPreprocessor()->getPreprocessProofGenerator();
165 : : // Note this assumes that connectProofToAssertions is only called once per
166 : : // unsat response. This method would need to cache its result otherwise.
167 [ + - ]: 27704 : Trace("smt-proof")
168 : 13852 : << "SolverEngine::connectProofToAssertions(): get proof body...\n";
169 : :
170 [ - + ]: 13852 : if (TraceIsOn("smt-proof-debug"))
171 : : {
172 [ - - ]: 0 : Trace("smt-proof-debug")
173 : 0 : << "SolverEngine::connectProofToAssertions(): Proof node for false:\n";
174 [ - - ]: 0 : Trace("smt-proof-debug") << *pfn.get() << std::endl;
175 [ - - ]: 0 : Trace("smt-proof-debug") << "=====" << std::endl;
176 : : }
177 : 27704 : std::vector<Node> assertions;
178 : 13852 : getAssertions(as, assertions);
179 : :
180 [ - + ]: 13852 : if (TraceIsOn("smt-proof"))
181 : : {
182 [ - - ]: 0 : Trace("smt-proof")
183 : 0 : << "SolverEngine::connectProofToAssertions(): get free assumptions..."
184 : 0 : << std::endl;
185 : 0 : std::vector<Node> fassumps;
186 : 0 : expr::getFreeAssumptions(pfn.get(), fassumps);
187 [ - - ]: 0 : Trace("smt-proof") << "SolverEngine::connectProofToAssertions(): initial "
188 : 0 : "free assumptions are:\n";
189 [ - - ]: 0 : for (const Node& a : fassumps)
190 : : {
191 [ - - ]: 0 : Trace("smt-proof") << "- " << a << std::endl;
192 : : }
193 : :
194 [ - - ]: 0 : Trace("smt-proof")
195 : 0 : << "SolverEngine::connectProofToAssertions(): assertions are:\n";
196 [ - - ]: 0 : for (const Node& n : assertions)
197 : : {
198 [ - - ]: 0 : Trace("smt-proof") << "- " << n << std::endl;
199 : : }
200 [ - - ]: 0 : Trace("smt-proof") << "=====" << std::endl;
201 : : }
202 : :
203 [ + - ]: 27704 : Trace("smt-proof")
204 : 13852 : << "SolverEngine::connectProofToAssertions(): postprocess...\n";
205 [ - + ][ - + ]: 13852 : Assert(d_pfpp != nullptr);
[ - - ]
206 : : // Note that in incremental mode, we cannot set assertions here, as it
207 : : // permits the postprocessor to merge subproofs at a higher user context
208 : : // level into proofs that are used in a lower user context level.
209 [ + + ]: 13852 : if (!options().base.incrementalSolving)
210 : : {
211 : 10178 : d_pfpp->setAssertions(assertions, false);
212 : : }
213 [ + - ]: 13852 : d_pfpp->process(pfn, pppg);
214 : :
215 [ + + ][ + - ]: 13852 : switch (scopeMode)
216 : : {
217 : 48 : case ProofScopeMode::NONE:
218 : : {
219 : 48 : return pfn;
220 : : }
221 : : // Now make the final scope(s), which ensure(s) that the only open leaves
222 : : // of the proof are the assertions (and definitions). If we are pruning
223 : : // the input, we will try to minimize the used assertions (and definitions).
224 : 8715 : case ProofScopeMode::UNIFIED:
225 : : {
226 [ + - ]: 17430 : Trace("smt-proof") << "SolverEngine::connectProofToAssertions(): make "
227 : 8715 : "unified scope...\n";
228 : : return d_pnm->mkScope(
229 : 8715 : pfn, assertions, true, options().proof.proofPruneInput);
230 : : }
231 : 5089 : case ProofScopeMode::DEFINITIONS_AND_ASSERTIONS:
232 : : {
233 [ + - ]: 10178 : Trace("smt-proof")
234 : 5089 : << "SolverEngine::connectProofToAssertions(): make split scope...\n";
235 : : // To support proof pruning for nested scopes, we need to:
236 : : // 1. Minimize assertions of closed unified scope.
237 : 10178 : std::vector<Node> unifiedAssertions;
238 : 5089 : getAssertions(as, unifiedAssertions);
239 : : Pf pf = d_pnm->mkScope(
240 : 15267 : pfn, unifiedAssertions, true, options().proof.proofPruneInput);
241 : : // if this is violated, there is unsoundness since we have shown
242 : : // false that does not depend on the input.
243 [ - + ][ - + ]: 5089 : AlwaysAssert(pf->getRule() == ProofRule::SCOPE);
[ - - ]
244 : : // 2. Extract minimum unified assertions from the scope node.
245 : 10178 : std::unordered_set<Node> minUnifiedAssertions;
246 : 5089 : minUnifiedAssertions.insert(pf->getArguments().cbegin(),
247 : 5089 : pf->getArguments().cend());
248 : : // 3. Split those assertions into minimized definitions and assertions.
249 : 10178 : std::vector<Node> minDefinitions;
250 : 10178 : std::vector<Node> minAssertions;
251 : 5089 : getDefinitionsAndAssertions(as, minDefinitions, minAssertions);
252 : 100332 : std::function<bool(Node)> predicate = [&minUnifiedAssertions](Node n) {
253 : 50166 : return minUnifiedAssertions.find(n) == minUnifiedAssertions.cend();
254 : 5089 : };
255 : 5089 : erase_if(minDefinitions, predicate);
256 : 5089 : erase_if(minAssertions, predicate);
257 : : // 4. Extract proof from unified scope and encapsulate it with split
258 : : // scopes introducing minimized definitions and assertions.
259 : : return d_pnm->mkNode(
260 : : ProofRule::SCOPE,
261 : : {d_pnm->mkNode(ProofRule::SCOPE, pf->getChildren(), minAssertions)},
262 : 10178 : minDefinitions);
263 : : }
264 : 0 : default: Unreachable();
265 : : }
266 : : }
267 : :
268 : 5057 : void PfManager::printProof(std::ostream& out,
269 : : std::shared_ptr<ProofNode> fp,
270 : : options::ProofFormatMode mode,
271 : : const std::map<Node, std::string>& assertionNames)
272 : : {
273 [ + - ]: 5057 : Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
274 : : // We don't want to invalidate the proof nodes in fp, since these may be
275 : : // reused in further check-sat calls, or they may be used again if the
276 : : // user asks for the proof again (in non-incremental mode). We don't need to
277 : : // clone if the printing below does not modify the proof, which is the case
278 : : // for proof formats ALF and NONE.
279 [ + + ]: 5057 : if (mode != options::ProofFormatMode::CPC
280 [ + + ]: 3444 : && mode != options::ProofFormatMode::NONE)
281 : : {
282 : 3205 : fp = fp->clone();
283 : : }
284 : :
285 : : // according to the proof format, post process and print the proof node
286 [ - + ]: 5057 : if (mode == options::ProofFormatMode::DOT)
287 : : {
288 : 0 : proof::DotPrinter dotPrinter(d_env);
289 : 0 : dotPrinter.print(out, fp.get());
290 : : }
291 [ + + ]: 5057 : else if (mode == options::ProofFormatMode::CPC)
292 : : {
293 [ - + ][ - + ]: 1613 : Assert(fp->getRule() == ProofRule::SCOPE);
[ - - ]
294 : 3226 : proof::AlfNodeConverter atp(nodeManager());
295 : 1613 : proof::AlfPrinter alfp(d_env, atp, d_rewriteDb.get());
296 : 1613 : alfp.print(out, fp);
297 : : }
298 [ + + ]: 3444 : else if (mode == options::ProofFormatMode::ALETHE)
299 : : {
300 : 1793 : options::ProofCheckMode oldMode = options().proof.proofCheck;
301 : 1793 : d_pnm->getChecker()->setProofCheckMode(options::ProofCheckMode::NONE);
302 : : proof::AletheNodeConverter anc(nodeManager(),
303 : 3586 : options().proof.proofAletheDefineSkolems);
304 : 3586 : proof::AletheProofPostprocess vpfpp(d_env, anc);
305 [ + + ]: 1793 : if (vpfpp.process(fp))
306 : : {
307 : 1200 : proof::AletheProofPrinter vpp(d_env, anc);
308 : 1200 : vpp.print(out, fp, assertionNames);
309 : : }
310 : : else
311 : : {
312 : 593 : out << "(error " << vpfpp.getError() << ")";
313 : : }
314 : 1793 : d_pnm->getChecker()->setProofCheckMode(oldMode);
315 : : }
316 [ + + ]: 1651 : else if (mode == options::ProofFormatMode::LFSC)
317 : : {
318 [ - + ][ - + ]: 1412 : Assert(fp->getRule() == ProofRule::SCOPE);
[ - - ]
319 : 2824 : proof::LfscNodeConverter ltp(nodeManager());
320 : 2824 : proof::LfscProofPostprocess lpp(d_env, ltp);
321 : 1412 : lpp.process(fp);
322 : 2824 : proof::LfscPrinter lp(d_env, ltp, d_rewriteDb.get());
323 : 1412 : lp.print(out, fp.get());
324 : : }
325 : : else
326 : : {
327 : : // otherwise, print using default printer
328 : : // we call the printing method explicitly because we may want to print the
329 : : // final proof node with conclusions
330 : 239 : fp->printDebug(out, options().proof.proofPrintConclusion);
331 : : }
332 : 5057 : }
333 : :
334 : 395 : void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
335 : : SmtSolver& smt)
336 : : {
337 [ + - ]: 395 : Trace("difficulty-proc") << "Translate difficulty start" << std::endl;
338 [ + - ]: 395 : Trace("difficulty") << "PfManager::translateDifficultyMap" << std::endl;
339 [ + + ]: 395 : if (dmap.empty())
340 : : {
341 : 194 : return;
342 : : }
343 : 203 : std::map<Node, Node> dmapp = dmap;
344 : 203 : dmap.clear();
345 [ + - ]: 203 : Trace("difficulty-proc") << "Get ppAsserts" << std::endl;
346 : 203 : std::vector<Node> ppAsserts;
347 [ + + ]: 618 : for (const std::pair<const Node, Node>& ppa : dmapp)
348 : : {
349 [ + - ]: 830 : Trace("difficulty") << " preprocess difficulty: " << ppa.second << " for "
350 : 415 : << ppa.first << std::endl;
351 : : // The difficulty manager should only report difficulty for preprocessed
352 : : // assertions, or we will get an open proof below. This is ensured
353 : : // internally by the difficuly manager.
354 : 415 : ppAsserts.push_back(ppa.first);
355 : : }
356 [ + - ]: 203 : Trace("difficulty-proc") << "Make SAT refutation" << std::endl;
357 : : // assume a SAT refutation from all input assertions that were marked
358 : : // as having a difficulty
359 : 406 : CDProof cdp(d_env);
360 : 203 : Node fnode = nodeManager()->mkConst(false);
361 : 203 : cdp.addStep(fnode, ProofRule::SAT_REFUTATION, ppAsserts, {});
362 : 203 : std::shared_ptr<ProofNode> pf = cdp.getProofFor(fnode);
363 [ + - ]: 203 : Trace("difficulty-proc") << "Get final proof" << std::endl;
364 : 203 : std::shared_ptr<ProofNode> fpf = connectProofToAssertions(pf, smt);
365 [ + - ]: 203 : Trace("difficulty-debug") << "Final proof is " << *fpf.get() << std::endl;
366 : : // We are typically a SCOPE here, although if we are not, then the proofs
367 : : // have no free assumptions. If this is the case, then the only difficulty
368 : : // was incremented on auxiliary lemmas added during preprocessing. Since
369 : : // there are no dependencies, then the difficulty map is empty.
370 [ + + ]: 203 : if (fpf->getRule() != ProofRule::SCOPE)
371 : : {
372 : 2 : return;
373 : : }
374 : 201 : fpf = fpf->getChildren()[0];
375 : : // analyze proof
376 [ - + ][ - + ]: 201 : Assert(fpf->getRule() == ProofRule::SAT_REFUTATION);
[ - - ]
377 : 201 : const std::vector<std::shared_ptr<ProofNode>>& children = fpf->getChildren();
378 : 402 : DifficultyPostprocessCallback dpc;
379 : 201 : ProofNodeUpdater dpnu(d_env, dpc);
380 [ + - ]: 201 : Trace("difficulty-proc") << "Compute accumulated difficulty" << std::endl;
381 : : // For each child of SAT_REFUTATION, we increment the difficulty on all
382 : : // "source" free assumptions (see DifficultyPostprocessCallback) by the
383 : : // difficulty of the preprocessed assertion.
384 [ + + ]: 614 : for (const std::shared_ptr<ProofNode>& c : children)
385 : : {
386 : 413 : Node res = c->getResult();
387 [ - + ][ - + ]: 413 : Assert(dmapp.find(res) != dmapp.end());
[ - - ]
388 [ + - ]: 413 : Trace("difficulty-debug") << " process: " << res << std::endl;
389 [ + - ]: 413 : Trace("difficulty-debug") << " .dvalue: " << dmapp[res] << std::endl;
390 [ + - ]: 413 : Trace("difficulty-debug") << " ..proof: " << *c.get() << std::endl;
391 [ - + ]: 413 : if (!dpc.setCurrentDifficulty(dmapp[res]))
392 : : {
393 : 0 : continue;
394 : : }
395 : 413 : dpnu.process(c);
396 : : }
397 : : // get the accumulated difficulty map from the callback
398 : 201 : dpc.getDifficultyMap(dmap);
399 [ + - ]: 201 : Trace("difficulty-proc") << "Translate difficulty end" << std::endl;
400 : : }
401 : :
402 : 0 : ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
403 : :
404 : 18630 : ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
405 : :
406 : 0 : rewriter::RewriteDb* PfManager::getRewriteDatabase() const
407 : : {
408 : 0 : return d_rewriteDb.get();
409 : : }
410 : :
411 : 18941 : void PfManager::getAssertions(Assertions& as, std::vector<Node>& assertions)
412 : : {
413 : : // note that the assertion list is always available
414 : 18941 : const context::CDList<Node>& al = as.getAssertionList();
415 [ + + ]: 185812 : for (const Node& a : al)
416 : : {
417 : 166871 : assertions.push_back(a);
418 : : }
419 : 18941 : }
420 : :
421 : 5089 : void PfManager::getDefinitionsAndAssertions(Assertions& as,
422 : : std::vector<Node>& definitions,
423 : : std::vector<Node>& assertions)
424 : : {
425 : 5089 : const context::CDList<Node>& defs = as.getAssertionListDefinitions();
426 [ + + ]: 6508 : for (const Node& d : defs)
427 : : {
428 : : // Keep treating (mutually) recursive functions as declarations +
429 : : // assertions.
430 [ + + ]: 1419 : if (d.getKind() == Kind::EQUAL)
431 : : {
432 : 1377 : definitions.push_back(d);
433 : : }
434 : : }
435 : 5089 : const context::CDList<Node>& asserts = as.getAssertionList();
436 [ + + ]: 55269 : for (const Node& a : asserts)
437 : : {
438 : 50180 : if (std::find(definitions.cbegin(), definitions.cend(), a)
439 [ + + ]: 100360 : == definitions.cend())
440 : : {
441 : 48789 : assertions.push_back(a);
442 : : }
443 : : }
444 : 5089 : }
445 : :
446 : : } // namespace smt
447 : : } // namespace cvc5::internal
|
