1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Gereon Kremer, Haniel Barbosa
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* The proof manager of SmtEngine.
*/
#include "cvc5_private.h"
#ifndef CVC5__SMT__PROOF_MANAGER_H
#define CVC5__SMT__PROOF_MANAGER_H
#include "context/cdhashmap.h"
#include "expr/node.h"
namespace cvc5 {
class Env;
class ProofChecker;
class ProofNode;
class ProofNodeManager;
class SmtEngine;
namespace smt {
class Assertions;
class PreprocessProofGenerator;
class ProofPostproccess;
/**
* This class is responsible for managing the proof output of SmtEngine, as
* well as setting up the global proof checker and proof node manager.
*
* The proof production of an SmtEngine is directly impacted by whether, and
* how, we are producing unsat cores:
*
* - If we are producing unsat cores using the old proof infrastructure, then
* SmtEngine will not have proofs in the sense of this proof manager.
*
* - If we are producing unsat cores using this proof infrastructure, then the
* SmtEngine will have proofs using this proof manager, according to the unsat
* core mode:
*
* - assumption mode: proofs only for preprocessing, not in sat solver or
* theory engine, and level of granularity set to off (unless otherwise
* specified by the user)
*
* - sat-proof mode: proofs for preprocessing + sat solver, not in theory
* engine and level of granularity set to off (unless otherwise specified by
* the user)
*
* - full-proof mode: proofs for the whole solver as normal
*
* Note that if --produce-proofs is set then full-proof mode of unsat cores is
* forced.
*
* - If we are not producing unsat cores then the SmtEngine will have proofs as
* long as --produce-proofs is on.
*
* - If SmtEngine has been configured in a way that is incompatible with proofs
* then unsat core production will be disabled.
*/
class PfManager
{
public:
PfManager(Env& env, SmtEngine* smte);
~PfManager();
/**
* Print the proof on the given output stream.
*
* The argument pfn is the proof for false in the current context.
*
* Throws an assertion failure if pg cannot provide a closed proof with
* respect to assertions in as. Note this includes equalities of the form
* (= f (lambda (...) t)) which originate from define-fun commands for f.
* These are considered assertions in the final proof.
*/
void printProof(std::ostream& out,
std::shared_ptr<ProofNode> pfn,
Assertions& as);
/**
* Check proof, same as above, without printing.
*/
void checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
/**
* Get final proof.
*
* The argument pfn is the proof for false in the current context.
*/
std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn,
Assertions& as);
//--------------------------- access to utilities
/** Get a pointer to the ProofChecker owned by this. */
ProofChecker* getProofChecker() const;
/** Get a pointer to the ProofNodeManager owned by this. */
ProofNodeManager* getProofNodeManager() const;
/** Get the proof generator for proofs of preprocessing. */
smt::PreprocessProofGenerator* getPreprocessProofGenerator() const;
//--------------------------- end access to utilities
private:
/**
* Set final proof, which initializes d_finalProof to the given proof node of
* false, postprocesses it, and stores it in d_finalProof.
*/
void setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
/**
* Get assertions from the assertions
*/
void getAssertions(Assertions& as,
std::vector<Node>& assertions);
/** Reference to the env of SmtEngine */
Env& d_env;
/** The false node */
Node d_false;
/** For the new proofs module */
std::unique_ptr<ProofChecker> d_pchecker;
/** A proof node manager based on the above checker */
std::unique_ptr<ProofNodeManager> d_pnm;
/** The preprocess proof generator. */
std::unique_ptr<smt::PreprocessProofGenerator> d_pppg;
/** The proof post-processor */
std::unique_ptr<smt::ProofPostproccess> d_pfpp;
/**
* The final proof produced by the SMT engine.
* Combines the proofs of preprocessing, prop engine and theory engine, to be
* connected by setFinalProof().
*/
std::shared_ptr<ProofNode> d_finalProof;
}; /* class SmtEngine */
} // namespace smt
} // namespace cvc5
#endif /* CVC5__SMT__PROOF_MANAGER_H */
|
