1 /********************* */
4 ** Original author: lianah
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Resolution proof
19 #ifndef __CVC4__SAT__PROOF_H
20 #define __CVC4__SAT__PROOF_H
26 #include <ext/hash_map>
27 #include <ext/hash_set>
31 typedef uint32_t CRef
;
34 #include "prop/minisat/core/SolverTypes.h"
35 #include "util/proof.h"
38 using namespace __gnu_cxx
;
43 * Helper debugging functions
46 void printDebug(::Minisat::Lit l
);
47 void printDebug(::Minisat::Clause
& c
);
54 ResStep(::Minisat::Lit l
, ClauseId i
, bool s
) :
61 typedef std::vector
< ResStep
> ResSteps
;
62 typedef std::set
< ::Minisat::Lit
> LitSet
;
68 LitSet
* d_redundantLits
;
70 ResChain(ClauseId start
);
71 void addStep(::Minisat::Lit
, ClauseId
, bool);
72 bool redundantRemoved() { return (d_redundantLits
== NULL
|| d_redundantLits
->empty()); }
73 void addRedundantLit(::Minisat::Lit lit
);
76 ClauseId
getStart() { return d_start
; }
77 ResSteps
& getSteps() { return d_steps
; }
78 LitSet
* getRedundant() { return d_redundantLits
; }
82 typedef std::hash_map
< ClauseId
, ::Minisat::CRef
> IdClauseMap
;
83 typedef std::hash_map
< ::Minisat::CRef
, ClauseId
> ClauseIdMap
;
84 typedef std::hash_map
< ClauseId
, ::Minisat::Lit
> IdUnitMap
;
85 typedef std::hash_map
< int, ClauseId
> UnitIdMap
; //FIXME
86 typedef std::hash_map
< ClauseId
, ResChain
*> IdResMap
;
87 typedef std::hash_set
< ClauseId
> IdHashSet
;
88 typedef std::vector
< ResChain
* > ResStack
;
90 typedef std::hash_set
< int > VarSet
;
91 typedef std::set
< ClauseId
> IdSet
;
92 typedef std::vector
< ::Minisat::Lit
> LitVector
;
95 class ProofProxy
: public ProofProxyAbstract
{
99 ProofProxy(SatProof
* pf
);
100 void updateCRef(::Minisat::CRef oldref
, ::Minisat::CRef newref
);
103 class SatProof
: public Proof
{
105 ::Minisat::Solver
* d_solver
;
107 IdClauseMap d_idClause
;
108 ClauseIdMap d_clauseId
;
112 IdHashSet d_inputClauses
;
115 IdResMap d_resChains
;
119 static ClauseId d_idCounter
;
120 const ClauseId d_emptyClauseId
;
121 const ClauseId d_nullId
;
122 // proxy class to break circular dependencies
125 // temporary map for updating CRefs
126 ClauseIdMap d_temp_clauseId
;
127 IdClauseMap d_temp_idClause
;
129 SatProof(::Minisat::Solver
* solver
, bool checkRes
= false);
131 void print(ClauseId id
);
132 void printRes(ClauseId id
);
133 void printRes(ResChain
* res
);
135 bool isInputClause(ClauseId id
);
136 bool isUnit(ClauseId id
);
137 bool isUnit(::Minisat::Lit lit
);
138 bool hasResolution(ClauseId id
);
139 void createLitSet(ClauseId id
, LitSet
& set
);
140 void registerResolution(ClauseId id
, ResChain
* res
);
142 ClauseId
getClauseId(::Minisat::CRef clause
);
143 ClauseId
getClauseId(::Minisat::Lit lit
);
144 ::Minisat::CRef
getClauseRef(ClauseId id
);
145 ::Minisat::Lit
getUnit(ClauseId id
);
146 ClauseId
getUnitId(::Minisat::Lit lit
);
147 ::Minisat::Clause
& getClause(ClauseId id
);
148 virtual void toStream(std::ostream
& out
);
150 bool checkResolution(ClauseId id
);
152 * Constructs a resolution tree that proves lit
153 * and returns the ClauseId for the unit clause lit
154 * @param lit the literal we are proving
158 ClauseId
resolveUnit(::Minisat::Lit lit
);
160 * Does a depth first search on removed literals and adds the literals
161 * to be removed in the proper order to the stack.
163 * @param lit the literal we are recusing on
164 * @param removedSet the previously computed set of redundantant literals
165 * @param removeStack the stack of literals in reverse order of resolution
167 void removedDfs(::Minisat::Lit lit
, LitSet
* removedSet
, LitVector
& removeStack
, LitSet
& inClause
, LitSet
& seen
);
168 void removeRedundantFromRes(ResChain
* res
, ClauseId id
);
170 void startResChain(::Minisat::CRef start
);
171 void addResolutionStep(::Minisat::Lit lit
, ::Minisat::CRef clause
, bool sign
);
173 * Pops the current resolution of the stack and stores it
174 * in the resolution map. Also registers the 'clause' parameter
175 * @param clause the clause the resolution is proving
177 void endResChain(::Minisat::CRef clause
);
178 void endResChain(::Minisat::Lit lit
);
180 * Stores in the current derivation the redundant literals that were
181 * eliminated from the conflict clause during conflict clause minimization.
182 * @param lit the eliminated literal
184 void storeLitRedundant(::Minisat::Lit lit
);
186 /// update the CRef Id maps when Minisat does memory reallocation x
187 void updateCRef(::Minisat::CRef old_ref
, ::Minisat::CRef new_ref
);
188 void finishUpdateCRef();
191 * Constructs the empty clause resolution from the final conflict
195 void finalizeProof(::Minisat::CRef conflict
);
197 /// clause registration methods
198 ClauseId
registerClause(const ::Minisat::CRef clause
, bool isInput
= false);
199 ClauseId
registerUnitClause(const ::Minisat::Lit lit
, bool isInput
= false);
201 * Marks the deleted clauses as deleted. Note we may still use them in the final
205 void markDeleted(::Minisat::CRef clause
);
207 * Constructs the resolution of ~q and resolves it with the current
208 * resolution thus eliminating q from the current clause
209 * @param q the literal to be resolved out
211 void resolveOutUnit(::Minisat::Lit q
);
213 * Constructs the resolution of the literal lit. Called when a clause
214 * containing lit becomes satisfied and is removed.
217 void storeUnitResolution(::Minisat::Lit lit
);
219 ProofProxy
* getProxy() {return d_proxy
; }
222 class LFSCSatProof
: public SatProof
{
225 std::ostringstream d_varSS
;
226 std::ostringstream d_lemmaSS
;
227 std::ostringstream d_clauseSS
;
228 std::ostringstream d_paren
;
230 IdHashSet d_seenInput
;
232 inline std::string
varName(::Minisat::Lit lit
);
233 inline std::string
clauseName(ClauseId id
);
235 void collectLemmas(ClauseId id
);
236 void printResolution(ClauseId id
);
237 void printInputClause(ClauseId id
);
239 void printVariables();
241 void flush(std::ostream
& out
);
244 LFSCSatProof(::Minisat::Solver
* solver
, bool checkRes
= false):
245 SatProof(solver
, checkRes
),
253 virtual void toStream(std::ostream
& out
);