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"
37 using namespace __gnu_cxx
;
42 * Helper debugging functions
45 void printDebug(::Minisat::Lit l
);
46 void printDebug(::Minisat::Clause
& c
);
53 ResStep(::Minisat::Lit l
, ClauseId i
, bool s
) :
60 typedef std::vector
< ResStep
> ResSteps
;
61 typedef std::set
< ::Minisat::Lit
> LitSet
;
67 LitSet
* d_redundantLits
;
69 ResChain(ClauseId start
);
70 void addStep(::Minisat::Lit
, ClauseId
, bool);
71 bool redundantRemoved() { return (d_redundantLits
== NULL
|| d_redundantLits
->empty()); }
72 void addRedundantLit(::Minisat::Lit lit
);
75 ClauseId
getStart() { return d_start
; }
76 ResSteps
& getSteps() { return d_steps
; }
77 LitSet
* getRedundant() { return d_redundantLits
; }
81 typedef std::hash_map
< ClauseId
, ::Minisat::CRef
> IdClauseMap
;
82 typedef std::hash_map
< ::Minisat::CRef
, ClauseId
> ClauseIdMap
;
83 typedef std::hash_map
< ClauseId
, ::Minisat::Lit
> IdUnitMap
;
84 typedef std::hash_map
< int, ClauseId
> UnitIdMap
; //FIXME
85 typedef std::hash_map
< ClauseId
, ResChain
*> IdResMap
;
86 typedef std::hash_set
< ClauseId
> IdHashSet
;
87 typedef std::vector
< ResChain
* > ResStack
;
89 typedef std::hash_set
< int > VarSet
;
90 typedef std::set
< ClauseId
> IdSet
;
91 typedef std::vector
< ::Minisat::Lit
> LitVector
;
94 class ProofProxy
: public ProofProxyAbstract
{
98 ProofProxy(SatProof
* pf
);
99 void updateCRef(::Minisat::CRef oldref
, ::Minisat::CRef newref
);
104 ::Minisat::Solver
* d_solver
;
106 IdClauseMap d_idClause
;
107 ClauseIdMap d_clauseId
;
111 IdHashSet d_inputClauses
;
114 IdResMap d_resChains
;
118 static ClauseId d_idCounter
;
119 const ClauseId d_emptyClauseId
;
120 const ClauseId d_nullId
;
121 // proxy class to break circular dependencies
124 // temporary map for updating CRefs
125 ClauseIdMap d_temp_clauseId
;
126 IdClauseMap d_temp_idClause
;
128 SatProof(::Minisat::Solver
* solver
, bool checkRes
= false);
130 void print(ClauseId id
);
131 void printRes(ClauseId id
);
132 void printRes(ResChain
* res
);
134 bool isInputClause(ClauseId id
);
135 bool isUnit(ClauseId id
);
136 bool isUnit(::Minisat::Lit lit
);
137 bool hasResolution(ClauseId id
);
138 void createLitSet(ClauseId id
, LitSet
& set
);
139 void registerResolution(ClauseId id
, ResChain
* res
);
141 ClauseId
getClauseId(::Minisat::CRef clause
);
142 ClauseId
getClauseId(::Minisat::Lit lit
);
143 ::Minisat::CRef
getClauseRef(ClauseId id
);
144 ::Minisat::Lit
getUnit(ClauseId id
);
145 ClauseId
getUnitId(::Minisat::Lit lit
);
146 ::Minisat::Clause
& getClause(ClauseId id
);
147 virtual void printProof();
149 bool checkResolution(ClauseId id
);
151 * Constructs a resolution tree that proves lit
152 * and returns the ClauseId for the unit clause lit
153 * @param lit the literal we are proving
157 ClauseId
resolveUnit(::Minisat::Lit lit
);
159 * Does a depth first search on removed literals and adds the literals
160 * to be removed in the proper order to the stack.
162 * @param lit the literal we are recusing on
163 * @param removedSet the previously computed set of redundantant literals
164 * @param removeStack the stack of literals in reverse order of resolution
166 void removedDfs(::Minisat::Lit lit
, LitSet
* removedSet
, LitVector
& removeStack
, LitSet
& inClause
, LitSet
& seen
);
167 void removeRedundantFromRes(ResChain
* res
, ClauseId id
);
169 void startResChain(::Minisat::CRef start
);
170 void addResolutionStep(::Minisat::Lit lit
, ::Minisat::CRef clause
, bool sign
);
172 * Pops the current resolution of the stack and stores it
173 * in the resolution map. Also registers the @param clause.
174 * @param clause the clause the resolution is proving
176 void endResChain(::Minisat::CRef clause
);
177 void endResChain(::Minisat::Lit lit
);
179 * Stores in the current derivation the redundant literals that were
180 * eliminated from the conflict clause during conflict clause minimization.
181 * @param lit the eliminated literal
183 void storeLitRedundant(::Minisat::Lit lit
);
185 /// update the CRef Id maps when Minisat does memory reallocation x
186 void updateCRef(::Minisat::CRef old_ref
, ::Minisat::CRef new_ref
);
187 void finishUpdateCRef();
190 * Constructs the empty clause resolution from the final conflict
194 void finalizeProof(::Minisat::CRef conflict
);
196 /// clause registration methods
197 ClauseId
registerClause(const ::Minisat::CRef clause
, bool isInput
= false);
198 ClauseId
registerUnitClause(const ::Minisat::Lit lit
, bool isInput
= false);
200 * Marks the deleted clauses as deleted. Note we may still use them in the final
204 void markDeleted(::Minisat::CRef clause
);
206 * Constructs the resolution of ~q and resolves it with the current
207 * resolution thus eliminating q from the current clause
208 * @param q the literal to be resolved out
210 void resolveOutUnit(::Minisat::Lit q
);
212 * Constructs the resolution of the literal lit. Called when a clause
213 * containing lit becomes satisfied and is removed.
216 void storeUnitResolution(::Minisat::Lit lit
);
218 ProofProxy
* getProxy() {return d_proxy
; }
221 class LFSCSatProof
: public SatProof
{
224 std::ostringstream d_varSS
;
225 std::ostringstream d_lemmaSS
;
226 std::ostringstream d_clauseSS
;
227 std::ostringstream d_paren
;
229 IdHashSet d_seenInput
;
231 inline std::string
varName(::Minisat::Lit lit
);
232 inline std::string
clauseName(ClauseId id
);
234 void collectLemmas(ClauseId id
);
235 void printResolution(ClauseId id
);
236 void printInputClause(ClauseId id
);
238 void printVariables();
243 LFSCSatProof(::Minisat::Solver
* solver
, bool checkRes
= false):
244 SatProof(solver
, checkRes
),