1 /********************* */
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Tim King, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 } /* namespace CVC4 */
45 * Helper debugging functions
47 template <class Solver
>
48 void printDebug(typename
Solver::TLit l
);
49 template <class Solver
>
50 void printDebug(typename
Solver::TClause
& c
);
54 THEORY_LEMMA
, // we need to distinguish because we must reprove deleted
57 }; /* enum ClauseKind */
59 template <class Solver
>
61 typename
Solver::TLit lit
;
64 ResStep(typename
Solver::TLit l
, ClauseId i
, bool s
)
65 : lit(l
), id(i
), sign(s
) {}
66 }; /* struct ResStep */
68 template <class Solver
>
71 typedef std::vector
<ResStep
<Solver
> > ResSteps
;
72 typedef std::set
<typename
Solver::TLit
> LitSet
;
74 ResChain(ClauseId start
);
77 void addStep(typename
Solver::TLit
, ClauseId
, bool);
78 bool redundantRemoved() {
79 return (d_redundantLits
== NULL
|| d_redundantLits
->empty());
81 void addRedundantLit(typename
Solver::TLit lit
);
84 ClauseId
getStart() const { return d_start
; }
85 const ResSteps
& getSteps() const { return d_steps
; }
86 LitSet
* getRedundant() const { return d_redundantLits
; }
91 LitSet
* d_redundantLits
;
92 }; /* class ResChain */
94 template <class Solver
>
97 typedef ResChain
<Solver
> ResolutionChain
;
99 typedef std::set
<typename
Solver::TLit
> LitSet
;
100 typedef std::set
<typename
Solver::TVar
> VarSet
;
101 typedef std::unordered_map
<ClauseId
, typename
Solver::TCRef
> IdCRefMap
;
102 typedef std::unordered_map
<typename
Solver::TCRef
, ClauseId
> ClauseIdMap
;
103 typedef context::CDHashMap
<ClauseId
, typename
Solver::TLit
> IdUnitMap
;
104 typedef context::CDHashMap
<int, ClauseId
> UnitIdMap
;
105 typedef context::CDHashMap
<ClauseId
, ResolutionChain
*> IdResMap
;
106 typedef std::unordered_map
<ClauseId
, uint64_t> IdProofRuleMap
;
107 typedef std::vector
<ResolutionChain
*> ResStack
;
108 typedef std::set
<ClauseId
> IdSet
;
109 typedef std::vector
<typename
Solver::TLit
> LitVector
;
110 typedef std::unordered_map
<ClauseId
, typename
Solver::TClause
&>
112 typedef std::unordered_map
<ClauseId
, LitVector
*> IdToConflicts
;
115 TSatProof(Solver
* solver
, context::Context
* context
,
116 const std::string
& name
, bool checkRes
= false);
119 void startResChain(typename
Solver::TLit start
);
120 void startResChain(typename
Solver::TCRef start
);
121 void addResolutionStep(typename
Solver::TLit lit
,
122 typename
Solver::TCRef clause
, bool sign
);
124 * Pops the current resolution of the stack and stores it
125 * in the resolution map. Also registers the 'clause' parameter
126 * @param clause the clause the resolution is proving
128 // void endResChain(typename Solver::TCRef clause);
129 void endResChain(typename
Solver::TLit lit
);
130 void endResChain(ClauseId id
);
133 * Pops the current resolution of the stack *without* storing it.
135 void cancelResChain();
138 * Stores in the current derivation the redundant literals that were
139 * eliminated from the conflict clause during conflict clause minimization.
140 * @param lit the eliminated literal
142 void storeLitRedundant(typename
Solver::TLit lit
);
144 /// update the CRef Id maps when Minisat does memory reallocation x
145 void updateCRef(typename
Solver::TCRef old_ref
,
146 typename
Solver::TCRef new_ref
);
147 void finishUpdateCRef();
150 * Constructs the empty clause resolution from the final conflict
154 void finalizeProof(typename
Solver::TCRef conflict
);
156 /// clause registration methods
158 ClauseId
registerClause(const typename
Solver::TCRef clause
, ClauseKind kind
);
159 ClauseId
registerUnitClause(const typename
Solver::TLit lit
, ClauseKind kind
);
160 void registerTrueLit(const typename
Solver::TLit lit
);
161 void registerFalseLit(const typename
Solver::TLit lit
);
163 ClauseId
getTrueUnit() const;
164 ClauseId
getFalseUnit() const;
166 void registerAssumption(const typename
Solver::TVar var
);
167 ClauseId
registerAssumptionConflict(const typename
Solver::TLitVec
& confl
);
169 ClauseId
storeUnitConflict(typename
Solver::TLit lit
, ClauseKind kind
);
172 * Marks the deleted clauses as deleted. Note we may still use them in the
177 void markDeleted(typename
Solver::TCRef clause
);
178 bool isDeleted(ClauseId id
) { return d_deleted
.find(id
) != d_deleted
.end(); }
180 * Constructs the resolution of ~q and resolves it with the current
181 * resolution thus eliminating q from the current clause
182 * @param q the literal to be resolved out
184 void resolveOutUnit(typename
Solver::TLit q
);
186 * Constructs the resolution of the literal lit. Called when a clause
187 * containing lit becomes satisfied and is removed.
190 void storeUnitResolution(typename
Solver::TLit lit
);
193 * Constructs the SAT proof for the given clause,
194 * by collecting the needed clauses in the d_seen
195 * data-structures, also notifying the proofmanager.
197 void constructProof(ClauseId id
);
198 void constructProof() { constructProof(d_emptyClauseId
); }
199 void refreshProof(ClauseId id
);
200 void refreshProof() { refreshProof(d_emptyClauseId
); }
201 bool proofConstructed() const;
202 void collectClauses(ClauseId id
);
203 bool derivedEmptyClause() const;
204 prop::SatClause
* buildClause(ClauseId id
);
206 void collectClausesUsed(IdToSatClause
& inputs
, IdToSatClause
& lemmas
);
208 void storeClauseGlue(ClauseId clause
, int glue
);
210 bool isInputClause(ClauseId id
) const;
211 bool isLemmaClause(ClauseId id
) const;
212 bool isAssumptionConflict(ClauseId id
) const;
214 bool hasResolutionChain(ClauseId id
) const;
216 /** Returns the resolution chain associated with id. Assert fails if
217 * hasResolution(id) does not hold. */
218 const ResolutionChain
& getResolutionChain(ClauseId id
) const;
220 const std::string
& getName() const { return d_name
; }
221 const ClauseId
& getEmptyClauseId() const { return d_emptyClauseId
; }
222 const IdSet
& getSeenLearnt() const { return d_seenLearnt
; }
223 const IdToConflicts
& getAssumptionConflicts() const
225 return d_assumptionConflictsDebug
;
229 bool isUnit(ClauseId id
) const;
230 typename
Solver::TLit
getUnit(ClauseId id
) const;
232 bool isUnit(typename
Solver::TLit lit
) const;
233 ClauseId
getUnitId(typename
Solver::TLit lit
) const;
235 void createLitSet(ClauseId id
, LitSet
& set
);
238 * Registers a ClauseId with a resolution chain res.
239 * Takes ownership of the memory associated with res.
241 void registerResolution(ClauseId id
, ResolutionChain
* res
);
244 bool hasClauseIdForCRef(typename
Solver::TCRef clause
) const;
245 ClauseId
getClauseIdForCRef(typename
Solver::TCRef clause
) const;
247 bool hasClauseIdForLiteral(typename
Solver::TLit lit
) const;
248 ClauseId
getClauseIdForLiteral(typename
Solver::TLit lit
) const;
250 bool hasClauseRef(ClauseId id
) const;
251 typename
Solver::TCRef
getClauseRef(ClauseId id
) const;
254 const typename
Solver::TClause
& getClause(typename
Solver::TCRef ref
) const;
256 void getLitVec(ClauseId id
, LitVector
& vec
);
258 bool checkResolution(ClauseId id
);
261 * Constructs a resolution tree that proves lit
262 * and returns the ClauseId for the unit clause lit
263 * @param lit the literal we are proving
267 ClauseId
resolveUnit(typename
Solver::TLit lit
);
270 * Does a depth first search on removed literals and adds the literals
271 * to be removed in the proper order to the stack.
273 * @param lit the literal we are recursing on
274 * @param removedSet the previously computed set of redundant literals
275 * @param removeStack the stack of literals in reverse order of resolution
277 void removedDfs(typename
Solver::TLit lit
, LitSet
* removedSet
,
278 LitVector
& removeStack
, LitSet
& inClause
, LitSet
& seen
);
279 void removeRedundantFromRes(ResChain
<Solver
>* res
, ClauseId id
);
281 void print(ClauseId id
) const;
282 void printRes(ClauseId id
) const;
283 void printRes(const ResolutionChain
& res
) const;
285 std::unordered_map
<ClauseId
, int> d_glueMap
;
287 IntStat d_numLearnedClauses
;
288 IntStat d_numLearnedInProof
;
289 IntStat d_numLemmasInProof
;
290 AverageStat d_avgChainLength
;
291 HistogramStat
<uint64_t> d_resChainLengths
;
292 HistogramStat
<uint64_t> d_usedResChainLengths
;
293 HistogramStat
<uint64_t> d_clauseGlue
;
294 HistogramStat
<uint64_t> d_usedClauseGlue
;
295 Statistics(const std::string
& name
);
301 const ClauseId d_emptyClauseId
;
303 IdToConflicts d_assumptionConflictsDebug
;
307 context::Context
* d_context
;
310 IdCRefMap d_idClause
;
311 ClauseIdMap d_clauseId
;
315 IdToSatClause d_deletedTheoryLemmas
;
317 IdHashSet d_inputClauses
;
318 IdHashSet d_lemmaClauses
;
319 VarSet d_assumptions
; // assumption literals for bv solver
320 IdHashSet d_assumptionConflicts
; // assumption conflicts not actually added
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_nullId
;
344 // temporary map for updating CRefs
345 ClauseIdMap d_temp_clauseId
;
346 IdCRefMap d_temp_idClause
;
349 context::CDMaybe
<ClauseId
> d_unitConflictId
;
354 IdToSatClause d_seenInputs
;
355 IdToSatClause d_seenLemmas
;
357 bool d_satProofConstructed
;
358 Statistics d_statistics
;
359 }; /* class TSatProof */
361 template <class Solver
>
362 prop::SatLiteral
toSatLiteral(typename
Solver::TLit lit
);
365 * Convert from minisat clause to SatClause
370 template <class Solver
>
371 void toSatClause(const typename
Solver::TClause
& minisat_cl
,
372 prop::SatClause
& sat_cl
);
374 } /* CVC4 namespace */
376 #endif /* CVC4__SAT__PROOF_H */