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
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
|
/********************* */
/*! \file sat_proof.h
** \verbatim
** Original author: lianah
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Resolution proof
**
** Resolution proof
**/
#ifndef __CVC4__SAT__PROOF_H
#define __CVC4__SAT__PROOF_H
#include <iostream>
#include <stdint.h>
#include <vector>
#include <set>
#include <ext/hash_map>
#include <ext/hash_set>
#include <sstream>
namespace Minisat {
class Solver;
typedef uint32_t CRef;
}
#include "prop/minisat/core/SolverTypes.h"
namespace std {
using namespace __gnu_cxx;
}
namespace CVC4 {
/**
* Helper debugging functions
*
*/
void printDebug(::Minisat::Lit l);
void printDebug(::Minisat::Clause& c);
typedef int ClauseId;
struct ResStep {
::Minisat::Lit lit;
ClauseId id;
bool sign;
ResStep(::Minisat::Lit l, ClauseId i, bool s) :
lit(l),
id(i),
sign(s)
{}
};
typedef std::vector< ResStep > ResSteps;
typedef std::set < ::Minisat::Lit> LitSet;
class ResChain {
private:
ClauseId d_start;
ResSteps d_steps;
LitSet* d_redundantLits;
public:
ResChain(ClauseId start);
void addStep(::Minisat::Lit, ClauseId, bool);
bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); }
void addRedundantLit(::Minisat::Lit lit);
~ResChain();
// accessor methods
ClauseId getStart() { return d_start; }
ResSteps& getSteps() { return d_steps; }
LitSet* getRedundant() { return d_redundantLits; }
};
typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap;
typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
typedef std::hash_map < ClauseId, ::Minisat::Lit> IdUnitMap;
typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME
typedef std::hash_map < ClauseId, ResChain*> IdResMap;
typedef std::hash_set < ClauseId > IdHashSet;
typedef std::vector < ResChain* > ResStack;
typedef std::hash_set < int > VarSet;
typedef std::set < ClauseId > IdSet;
typedef std::vector < ::Minisat::Lit > LitVector;
class SatProof;
class ProofProxy : public ProofProxyAbstract {
private:
SatProof* d_proof;
public:
ProofProxy(SatProof* pf);
void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
};
class SatProof {
protected:
::Minisat::Solver* d_solver;
// clauses
IdClauseMap d_idClause;
ClauseIdMap d_clauseId;
IdUnitMap d_idUnit;
UnitIdMap d_unitId;
IdHashSet d_deleted;
IdHashSet d_inputClauses;
// resolutions
IdResMap d_resChains;
ResStack d_resStack;
bool d_checkRes;
static ClauseId d_idCounter;
const ClauseId d_emptyClauseId;
const ClauseId d_nullId;
// proxy class to break circular dependencies
ProofProxy* d_proxy;
// temporary map for updating CRefs
ClauseIdMap d_temp_clauseId;
IdClauseMap d_temp_idClause;
public:
SatProof(::Minisat::Solver* solver, bool checkRes = false);
protected:
void print(ClauseId id);
void printRes(ClauseId id);
void printRes(ResChain* res);
bool isInputClause(ClauseId id);
bool isUnit(ClauseId id);
bool isUnit(::Minisat::Lit lit);
bool hasResolution(ClauseId id);
void createLitSet(ClauseId id, LitSet& set);
void registerResolution(ClauseId id, ResChain* res);
ClauseId getClauseId(::Minisat::CRef clause);
ClauseId getClauseId(::Minisat::Lit lit);
::Minisat::CRef getClauseRef(ClauseId id);
::Minisat::Lit getUnit(ClauseId id);
ClauseId getUnitId(::Minisat::Lit lit);
::Minisat::Clause& getClause(ClauseId id);
virtual void printProof();
bool checkResolution(ClauseId id);
/**
* Constructs a resolution tree that proves lit
* and returns the ClauseId for the unit clause lit
* @param lit the literal we are proving
*
* @return
*/
ClauseId resolveUnit(::Minisat::Lit lit);
/**
* Does a depth first search on removed literals and adds the literals
* to be removed in the proper order to the stack.
*
* @param lit the literal we are recusing on
* @param removedSet the previously computed set of redundantant literals
* @param removeStack the stack of literals in reverse order of resolution
*/
void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
void removeRedundantFromRes(ResChain* res, ClauseId id);
public:
void startResChain(::Minisat::CRef start);
void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign);
/**
* Pops the current resolution of the stack and stores it
* in the resolution map. Also registers the @param clause.
* @param clause the clause the resolution is proving
*/
void endResChain(::Minisat::CRef clause);
void endResChain(::Minisat::Lit lit);
/**
* Stores in the current derivation the redundant literals that were
* eliminated from the conflict clause during conflict clause minimization.
* @param lit the eliminated literal
*/
void storeLitRedundant(::Minisat::Lit lit);
/// update the CRef Id maps when Minisat does memory reallocation x
void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref);
void finishUpdateCRef();
/**
* Constructs the empty clause resolution from the final conflict
*
* @param conflict
*/void finalizeProof(::Minisat::CRef conflict);
/// clause registration methods
ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);
ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false);
/**
* Marks the deleted clauses as deleted. Note we may still use them in the final
* resolution.
* @param clause
*/
void markDeleted(::Minisat::CRef clause);
/**
* Constructs the resolution of ~q and resolves it with the current
* resolution thus eliminating q from the current clause
* @param q the literal to be resolved out
*/
void resolveOutUnit(::Minisat::Lit q);
/**
* Constructs the resolution of the literal lit. Called when a clause
* containing lit becomes satisfied and is removed.
* @param lit
*/
void storeUnitResolution(::Minisat::Lit lit);
ProofProxy* getProxy() {return d_proxy; }
};
class LFSCSatProof: public SatProof {
private:
VarSet d_seenVars;
std::ostringstream d_varSS;
std::ostringstream d_lemmaSS;
std::ostringstream d_clauseSS;
std::ostringstream d_paren;
IdSet d_seenLemmas;
IdHashSet d_seenInput;
inline std::string varName(::Minisat::Lit lit);
inline std::string clauseName(ClauseId id);
void collectLemmas(ClauseId id);
void printResolution(ClauseId id);
void printInputClause(ClauseId id);
void printVariables();
void printClauses();
void flush();
public:
LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
SatProof(solver, checkRes),
d_seenVars(),
d_varSS(),
d_lemmaSS(),
d_paren(),
d_seenLemmas(),
d_seenInput()
{}
void printProof();
};
}
#endif
|