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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
/********************* */
/*! \file proof_manager.h
** \verbatim
** Original author: Liana Hadarean
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief A manager for Proofs
**
** A manager for Proofs.
**/
#include "cvc4_private.h"
#ifndef __CVC4__PROOF_MANAGER_H
#define __CVC4__PROOF_MANAGER_H
#include <iostream>
#include <map>
#include "proof/proof.h"
#include "util/proof.h"
#include "expr/node.h"
#include "theory/logic_info.h"
#include "theory/substitutions.h"
// forward declarations
namespace Minisat {
class Solver;
}/* Minisat namespace */
namespace CVC4 {
namespace prop {
class CnfStream;
}/* CVC4::prop namespace */
class SmtEngine;
typedef int ClauseId;
class Proof;
class SatProof;
class CnfProof;
class TheoryProof;
class LFSCSatProof;
class LFSCCnfProof;
class LFSCTheoryProof;
namespace prop {
typedef uint64_t SatVariable;
class SatLiteral;
typedef std::vector<SatLiteral> SatClause;
}/* CVC4::prop namespace */
// different proof modes
enum ProofFormat {
LFSC,
NATIVE
};/* enum ProofFormat */
std::string append(const std::string& str, uint64_t num);
typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause;
typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
typedef int ClauseId;
enum ClauseKind {
INPUT,
THEORY_LEMMA,
LEARNT
};/* enum ClauseKind */
enum ProofRule {
RULE_GIVEN, /* input assertion */
RULE_DERIVED, /* a "macro" rule */
RULE_RECONSTRUCT, /* prove equivalence using another method */
RULE_TRUST, /* trust without evidence (escape hatch until proofs are fully supported) */
RULE_INVALID, /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
RULE_CONFLICT, /* re-construct as a conflict */
RULE_ARRAYS_EXT, /* arrays, extensional */
RULE_ARRAYS_ROW, /* arrays, read-over-write */
};/* enum ProofRules */
class ProofManager {
SatProof* d_satProof;
CnfProof* d_cnfProof;
TheoryProof* d_theoryProof;
// information that will need to be shared across proofs
IdToClause d_inputClauses;
OrderedIdToClause d_theoryLemmas;
IdToClause d_theoryPropagations;
ExprSet d_inputFormulas;
ExprSet d_inputCoreFormulas;
ExprSet d_outputCoreFormulas;
//VarSet d_propVars;
int d_nextId;
Proof* d_fullProof;
ProofFormat d_format; // used for now only in debug builds
__gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction > d_deps;
// trace dependences back to unsat core
void traceDeps(TNode n);
protected:
LogicInfo d_logic;
public:
ProofManager(ProofFormat format = LFSC);
~ProofManager();
static ProofManager* currentPM();
// initialization
static void initSatProof(Minisat::Solver* solver);
static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
static void initTheoryProof();
static Proof* getProof(SmtEngine* smt);
static SatProof* getSatProof();
static CnfProof* getCnfProof();
static TheoryProof* getTheoryProof();
// iterators over data shared by proofs
typedef IdToClause::const_iterator clause_iterator;
typedef OrderedIdToClause::const_iterator ordered_clause_iterator;
typedef ExprSet::const_iterator assertions_iterator;
typedef VarSet::const_iterator var_iterator;
clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
size_t num_input_clauses() const { return d_inputClauses.size(); }
ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
size_t num_lemmas() const { return d_theoryLemmas.size(); }
assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
size_t num_assertions() const { return d_inputFormulas.size(); }
void printProof(std::ostream& os, TNode n);
void addAssertion(Expr formula, bool inUnsatCore);
void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
// note that n depends on dep (for cores)
void addDependence(TNode n, TNode dep);
assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
int nextId() { return d_nextId++; }
// variable prefixes
static std::string getInputClauseName(ClauseId id);
static std::string getLemmaName(ClauseId id);
static std::string getLemmaClauseName(ClauseId id);
static std::string getLearntClauseName(ClauseId id);
static std::string getVarName(prop::SatVariable var);
static std::string getAtomName(prop::SatVariable var);
static std::string getAtomName(TNode atom);
static std::string getLitName(prop::SatLiteral lit);
static std::string getLitName(TNode lit);
void setLogic(const LogicInfo& logic);
const std::string getLogic() const { return d_logic.getLogicString(); }
};/* class ProofManager */
class LFSCProof : public Proof {
LFSCSatProof* d_satProof;
LFSCCnfProof* d_cnfProof;
LFSCTheoryProof* d_theoryProof;
SmtEngine* d_smtEngine;
public:
LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory);
virtual void toStream(std::ostream& out);
virtual ~LFSCProof() {}
};/* class LFSCProof */
}/* CVC4 namespace */
#endif /* __CVC4__PROOF_MANAGER_H */
|
