1 /********************* */
4 ** Top contributors (to current version):
5 ** Tim King, Liana Hadarean, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Resolution proof
17 #include "cvc4_private.h"
19 #ifndef __CVC4__SAT__PROOF_H
20 #define __CVC4__SAT__PROOF_H
27 #include <unordered_map>
30 #include "context/cdhashmap.h"
31 #include "context/cdmaybe.h"
32 #include "expr/expr.h"
33 #include "proof/clause_id.h"
34 #include "proof/proof_manager.h"
35 #include "util/proof.h"
36 #include "util/statistics_registry.h"
38 // Forward declarations.
41 template <class Solver
>
43 } /* namespace CVC4 */
47 * Helper debugging functions
49 template <class Solver
>
50 void printDebug(typename
Solver::TLit l
);
51 template <class Solver
>
52 void printDebug(typename
Solver::TClause
& c
);
56 THEORY_LEMMA
, // we need to distinguish because we must reprove deleted
59 }; /* enum ClauseKind */
61 template <class Solver
>
63 typename
Solver::TLit lit
;
66 ResStep(typename
Solver::TLit l
, ClauseId i
, bool s
)
67 : lit(l
), id(i
), sign(s
) {}
68 }; /* struct ResStep */
70 template <class Solver
>
73 typedef std::vector
<ResStep
<Solver
> > ResSteps
;
74 typedef std::set
<typename
Solver::TLit
> LitSet
;
76 ResChain(ClauseId start
);
79 void addStep(typename
Solver::TLit
, ClauseId
, bool);
80 bool redundantRemoved() {
81 return (d_redundantLits
== NULL
|| d_redundantLits
->empty());
83 void addRedundantLit(typename
Solver::TLit lit
);
86 ClauseId
getStart() const { return d_start
; }
87 const ResSteps
& getSteps() const { return d_steps
; }
88 LitSet
* getRedundant() const { return d_redundantLits
; }
93 LitSet
* d_redundantLits
;
94 }; /* class ResChain */
96 template <class Solver
>
99 typedef ResChain
<Solver
> ResolutionChain
;
101 typedef std::set
<typename
Solver::TLit
> LitSet
;
102 typedef std::set
<typename
Solver::TVar
> VarSet
;
103 typedef std::unordered_map
<ClauseId
, typename
Solver::TCRef
> IdCRefMap
;
104 typedef std::unordered_map
<typename
Solver::TCRef
, ClauseId
> ClauseIdMap
;
105 typedef context::CDHashMap
<ClauseId
, typename
Solver::TLit
> IdUnitMap
;
106 typedef context::CDHashMap
<int, ClauseId
> UnitIdMap
;
107 typedef context::CDHashMap
<ClauseId
, ResolutionChain
*> IdResMap
;
108 typedef std::unordered_map
<ClauseId
, uint64_t> IdProofRuleMap
;
109 typedef std::vector
<ResolutionChain
*> ResStack
;
110 typedef std::set
<ClauseId
> IdSet
;
111 typedef std::vector
<typename
Solver::TLit
> LitVector
;
112 typedef std::unordered_map
<ClauseId
, typename
Solver::TClause
&>
114 typedef std::unordered_map
<ClauseId
, LitVector
*> IdToConflicts
;
117 TSatProof(Solver
* solver
, context::Context
* context
,
118 const std::string
& name
, bool checkRes
= false);
119 virtual ~TSatProof();
120 void setCnfProof(CnfProof
* cnf_proof
);
122 void startResChain(typename
Solver::TLit start
);
123 void startResChain(typename
Solver::TCRef start
);
124 void addResolutionStep(typename
Solver::TLit lit
,
125 typename
Solver::TCRef clause
, bool sign
);
127 * Pops the current resolution of the stack and stores it
128 * in the resolution map. Also registers the 'clause' parameter
129 * @param clause the clause the resolution is proving
131 // void endResChain(typename Solver::TCRef clause);
132 void endResChain(typename
Solver::TLit lit
);
133 void endResChain(ClauseId id
);
136 * Pops the current resolution of the stack *without* storing it.
138 void cancelResChain();
141 * Stores in the current derivation the redundant literals that were
142 * eliminated from the conflict clause during conflict clause minimization.
143 * @param lit the eliminated literal
145 void storeLitRedundant(typename
Solver::TLit lit
);
147 /// update the CRef Id maps when Minisat does memory reallocation x
148 void updateCRef(typename
Solver::TCRef old_ref
,
149 typename
Solver::TCRef new_ref
);
150 void finishUpdateCRef();
153 * Constructs the empty clause resolution from the final conflict
157 void finalizeProof(typename
Solver::TCRef conflict
);
159 /// clause registration methods
161 ClauseId
registerClause(const typename
Solver::TCRef clause
, ClauseKind kind
);
162 ClauseId
registerUnitClause(const typename
Solver::TLit lit
, ClauseKind kind
);
163 void registerTrueLit(const typename
Solver::TLit lit
);
164 void registerFalseLit(const typename
Solver::TLit lit
);
166 ClauseId
getTrueUnit() const;
167 ClauseId
getFalseUnit() const;
169 void registerAssumption(const typename
Solver::TVar var
);
170 ClauseId
registerAssumptionConflict(const typename
Solver::TLitVec
& confl
);
172 ClauseId
storeUnitConflict(typename
Solver::TLit lit
, ClauseKind kind
);
175 * Marks the deleted clauses as deleted. Note we may still use them in the
180 void markDeleted(typename
Solver::TCRef clause
);
181 bool isDeleted(ClauseId id
) { return d_deleted
.find(id
) != d_deleted
.end(); }
183 * Constructs the resolution of ~q and resolves it with the current
184 * resolution thus eliminating q from the current clause
185 * @param q the literal to be resolved out
187 void resolveOutUnit(typename
Solver::TLit q
);
189 * Constructs the resolution of the literal lit. Called when a clause
190 * containing lit becomes satisfied and is removed.
193 void storeUnitResolution(typename
Solver::TLit lit
);
195 ProofProxy
<Solver
>* getProxy() { return d_proxy
; }
197 * Constructs the SAT proof for the given clause,
198 * by collecting the needed clauses in the d_seen
199 * data-structures, also notifying the proofmanager.
201 void constructProof(ClauseId id
);
202 void constructProof() { constructProof(d_emptyClauseId
); }
203 void refreshProof(ClauseId id
);
204 void refreshProof() { refreshProof(d_emptyClauseId
); }
205 bool proofConstructed() const;
206 void collectClauses(ClauseId id
);
207 bool derivedEmptyClause() const;
208 prop::SatClause
* buildClause(ClauseId id
);
210 virtual void printResolution(ClauseId id
, std::ostream
& out
,
211 std::ostream
& paren
) = 0;
212 virtual void printResolutions(std::ostream
& out
, std::ostream
& paren
) = 0;
213 virtual void printResolutionEmptyClause(std::ostream
& out
,
214 std::ostream
& paren
) = 0;
215 virtual void printAssumptionsResolution(ClauseId id
, std::ostream
& out
,
216 std::ostream
& paren
) = 0;
218 void collectClausesUsed(IdToSatClause
& inputs
, IdToSatClause
& lemmas
);
220 void storeClauseGlue(ClauseId clause
, int glue
);
223 void print(ClauseId id
) const;
224 void printRes(ClauseId id
) const;
225 void printRes(const ResolutionChain
& res
) const;
227 bool isInputClause(ClauseId id
) const;
228 bool isLemmaClause(ClauseId id
) const;
229 bool isAssumptionConflict(ClauseId id
) const;
231 bool isUnit(ClauseId id
) const;
232 typename
Solver::TLit
getUnit(ClauseId id
) const;
234 bool isUnit(typename
Solver::TLit lit
) const;
235 ClauseId
getUnitId(typename
Solver::TLit lit
) const;
239 bool hasResolutionChain(ClauseId id
) const;
241 /** Returns the resolution chain associated with id. Assert fails if
242 * hasResolution(id) does not hold. */
243 const ResolutionChain
& getResolutionChain(ClauseId id
) const;
245 /** Returns a mutable pointer to the resolution chain associated with id.
246 * Assert fails if hasResolution(id) does not hold. */
247 ResolutionChain
* getMutableResolutionChain(ClauseId id
);
249 void createLitSet(ClauseId id
, LitSet
& set
);
252 * Registers a ClauseId with a resolution chain res.
253 * Takes ownership of the memory associated with res.
255 void registerResolution(ClauseId id
, ResolutionChain
* res
);
258 bool hasClauseIdForCRef(typename
Solver::TCRef clause
) const;
259 ClauseId
getClauseIdForCRef(typename
Solver::TCRef clause
) const;
261 bool hasClauseIdForLiteral(typename
Solver::TLit lit
) const;
262 ClauseId
getClauseIdForLiteral(typename
Solver::TLit lit
) const;
264 bool hasClauseRef(ClauseId id
) const;
265 typename
Solver::TCRef
getClauseRef(ClauseId id
) const;
268 const typename
Solver::TClause
& getClause(typename
Solver::TCRef ref
) const;
269 typename
Solver::TClause
* getMutableClause(typename
Solver::TCRef ref
);
271 void getLitVec(ClauseId id
, LitVector
& vec
);
272 virtual void toStream(std::ostream
& out
);
274 bool checkResolution(ClauseId id
);
277 * Constructs a resolution tree that proves lit
278 * and returns the ClauseId for the unit clause lit
279 * @param lit the literal we are proving
283 ClauseId
resolveUnit(typename
Solver::TLit lit
);
286 * Does a depth first search on removed literals and adds the literals
287 * to be removed in the proper order to the stack.
289 * @param lit the literal we are recursing on
290 * @param removedSet the previously computed set of redundant literals
291 * @param removeStack the stack of literals in reverse order of resolution
293 void removedDfs(typename
Solver::TLit lit
, LitSet
* removedSet
,
294 LitVector
& removeStack
, LitSet
& inClause
, LitSet
& seen
);
295 void removeRedundantFromRes(ResChain
<Solver
>* res
, ClauseId id
);
297 std::string
varName(typename
Solver::TLit lit
);
298 std::string
clauseName(ClauseId id
);
300 void addToProofManager(ClauseId id
, ClauseKind kind
);
301 void addToCnfProof(ClauseId id
);
305 context::Context
* d_context
;
306 CnfProof
* d_cnfProof
;
309 IdCRefMap d_idClause
;
310 ClauseIdMap d_clauseId
;
314 IdToSatClause d_deletedTheoryLemmas
;
316 IdHashSet d_inputClauses
;
317 IdHashSet d_lemmaClauses
;
318 VarSet d_assumptions
; // assumption literals for bv solver
319 IdHashSet d_assumptionConflicts
; // assumption conflicts not actually added
321 IdToConflicts d_assumptionConflictsDebug
;
326 * Map from ClauseId to resolution chain corresponding proving the
327 * clause corresponding to the ClauseId. d_resolutionChains owns the
328 * memory of the ResChain* it contains.
330 IdResMap d_resolutionChains
;
333 * Stack containting current ResChain* we are working on. d_resStack
334 * owns the memory for the ResChain* it contains. Invariant: no
335 * ResChain* pointer can be both in d_resStack and
336 * d_resolutionChains. Memory ownership is transfered from
337 * d_resStack to d_resolutionChains via registerResolution.
342 const ClauseId d_emptyClauseId
;
343 const ClauseId d_nullId
;
344 // proxy class to break circular dependencies
345 ProofProxy
<Solver
>* d_proxy
;
347 // temporary map for updating CRefs
348 ClauseIdMap d_temp_clauseId
;
349 IdCRefMap d_temp_idClause
;
352 context::CDMaybe
<ClauseId
> d_unitConflictId
;
360 IdToSatClause d_seenInputs
;
361 IdToSatClause d_seenLemmas
;
364 std::unordered_map
<ClauseId
, int> d_glueMap
;
366 IntStat d_numLearnedClauses
;
367 IntStat d_numLearnedInProof
;
368 IntStat d_numLemmasInProof
;
369 AverageStat d_avgChainLength
;
370 HistogramStat
<uint64_t> d_resChainLengths
;
371 HistogramStat
<uint64_t> d_usedResChainLengths
;
372 HistogramStat
<uint64_t> d_clauseGlue
;
373 HistogramStat
<uint64_t> d_usedClauseGlue
;
374 Statistics(const std::string
& name
);
378 bool d_satProofConstructed
;
379 Statistics d_statistics
;
380 }; /* class TSatProof */
385 TSatProof
<S
>* d_proof
;
388 ProofProxy(TSatProof
<S
>* pf
);
389 void updateCRef(typename
S::TCRef oldref
, typename
S::TCRef newref
);
390 }; /* class ProofProxy */
392 template <class SatSolver
>
393 class LFSCSatProof
: public TSatProof
<SatSolver
> {
396 LFSCSatProof(SatSolver
* solver
, context::Context
* context
,
397 const std::string
& name
, bool checkRes
= false)
398 : TSatProof
<SatSolver
>(solver
, context
, name
, checkRes
) {}
399 void printResolution(ClauseId id
,
401 std::ostream
& paren
) override
;
402 void printResolutions(std::ostream
& out
, std::ostream
& paren
) override
;
403 void printResolutionEmptyClause(std::ostream
& out
,
404 std::ostream
& paren
) override
;
405 void printAssumptionsResolution(ClauseId id
,
407 std::ostream
& paren
) override
;
408 }; /* class LFSCSatProof */
410 template <class Solver
>
411 prop::SatLiteral
toSatLiteral(typename
Solver::TLit lit
);
414 * Convert from minisat clause to SatClause
419 template <class Solver
>
420 void toSatClause(const typename
Solver::TClause
& minisat_cl
,
421 prop::SatClause
& sat_cl
);
423 } /* CVC4 namespace */
425 #endif /* __CVC4__SAT__PROOF_H */