1 /*********************                                                        */
2 /*! \file sat_proof.h
3  ** \verbatim
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
11  **
12  ** \brief Resolution proof
13  **
14  ** Resolution proof
15  **/
16 
17 #include "cvc4_private.h"
18 
19 #ifndef __CVC4__SAT__PROOF_H
20 #define __CVC4__SAT__PROOF_H
21 
22 #include <stdint.h>
23 
24 #include <iosfwd>
25 #include <set>
26 #include <sstream>
27 #include <unordered_map>
28 #include <vector>
29 
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"
37 
38 // Forward declarations.
39 namespace CVC4 {
40 class CnfProof;
41 } /* namespace CVC4 */
42 
43 namespace CVC4 {
44 /**
45  * Helper debugging functions
46  */
47 template <class Solver>
48 void printDebug(typename Solver::TLit l);
49 template <class Solver>
50 void printDebug(typename Solver::TClause& c);
51 
52 enum ClauseKind {
53   INPUT,
54   THEORY_LEMMA,  // we need to distinguish because we must reprove deleted
55                  // theory lemmas
56   LEARNT
57 }; /* enum ClauseKind */
58 
59 template <class Solver>
60 struct ResStep {
61   typename Solver::TLit lit;
62   ClauseId id;
63   bool sign;
ResStepResStep64   ResStep(typename Solver::TLit l, ClauseId i, bool s)
65       : lit(l), id(i), sign(s) {}
66 }; /* struct ResStep */
67 
68 template <class Solver>
69 class ResChain {
70  public:
71   typedef std::vector<ResStep<Solver> > ResSteps;
72   typedef std::set<typename Solver::TLit> LitSet;
73 
74   ResChain(ClauseId start);
75   ~ResChain();
76 
77   void addStep(typename Solver::TLit, ClauseId, bool);
redundantRemoved()78   bool redundantRemoved() {
79     return (d_redundantLits == NULL || d_redundantLits->empty());
80   }
81   void addRedundantLit(typename Solver::TLit lit);
82 
83   // accessor methods
getStart()84   ClauseId getStart() const { return d_start; }
getSteps()85   const ResSteps& getSteps() const { return d_steps; }
getRedundant()86   LitSet* getRedundant() const { return d_redundantLits; }
87 
88  private:
89   ClauseId d_start;
90   ResSteps d_steps;
91   LitSet* d_redundantLits;
92 }; /* class ResChain */
93 
94 template <class Solver>
95 class TSatProof {
96  protected:
97   typedef ResChain<Solver> ResolutionChain;
98 
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&>
111       IdToMinisatClause;
112   typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts;
113 
114  public:
115   TSatProof(Solver* solver, context::Context* context,
116             const std::string& name, bool checkRes = false);
117   ~TSatProof();
118 
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);
123   /**
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
127    */
128   // void endResChain(typename Solver::TCRef clause);
129   void endResChain(typename Solver::TLit lit);
130   void endResChain(ClauseId id);
131 
132   /**
133    * Pops the current resolution of the stack *without* storing it.
134    */
135   void cancelResChain();
136 
137   /**
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
141    */
142   void storeLitRedundant(typename Solver::TLit lit);
143 
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();
148 
149   /**
150    * Constructs the empty clause resolution from the final conflict
151    *
152    * @param conflict
153    */
154   void finalizeProof(typename Solver::TCRef conflict);
155 
156   /// clause registration methods
157 
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);
162 
163   ClauseId getTrueUnit() const;
164   ClauseId getFalseUnit() const;
165 
166   void registerAssumption(const typename Solver::TVar var);
167   ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl);
168 
169   ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind);
170 
171   /**
172    * Marks the deleted clauses as deleted. Note we may still use them in the
173    * final
174    * resolution.
175    * @param clause
176    */
177   void markDeleted(typename Solver::TCRef clause);
isDeleted(ClauseId id)178   bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
179   /**
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
183    */
184   void resolveOutUnit(typename Solver::TLit q);
185   /**
186    * Constructs the resolution of the literal lit. Called when a clause
187    * containing lit becomes satisfied and is removed.
188    * @param lit
189    */
190   void storeUnitResolution(typename Solver::TLit lit);
191 
192   /**
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.
196    */
197   void constructProof(ClauseId id);
constructProof()198   void constructProof() { constructProof(d_emptyClauseId); }
199   void refreshProof(ClauseId id);
refreshProof()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);
205 
206   void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas);
207 
208   void storeClauseGlue(ClauseId clause, int glue);
209 
210   bool isInputClause(ClauseId id) const;
211   bool isLemmaClause(ClauseId id) const;
212   bool isAssumptionConflict(ClauseId id) const;
213 
214   bool hasResolutionChain(ClauseId id) const;
215 
216   /** Returns the resolution chain associated with id. Assert fails if
217    * hasResolution(id) does not hold. */
218   const ResolutionChain& getResolutionChain(ClauseId id) const;
219 
getName()220   const std::string& getName() const { return d_name; }
getEmptyClauseId()221   const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; }
getSeenLearnt()222   const IdSet& getSeenLearnt() const { return d_seenLearnt; }
getAssumptionConflicts()223   const IdToConflicts& getAssumptionConflicts() const
224   {
225     return d_assumptionConflictsDebug;
226   }
227 
228  private:
229   bool isUnit(ClauseId id) const;
230   typename Solver::TLit getUnit(ClauseId id) const;
231 
232   bool isUnit(typename Solver::TLit lit) const;
233   ClauseId getUnitId(typename Solver::TLit lit) const;
234 
235   void createLitSet(ClauseId id, LitSet& set);
236 
237   /**
238    * Registers a ClauseId with a resolution chain res.
239    * Takes ownership of the memory associated with res.
240    */
241   void registerResolution(ClauseId id, ResolutionChain* res);
242 
243 
244   bool hasClauseIdForCRef(typename Solver::TCRef clause) const;
245   ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const;
246 
247   bool hasClauseIdForLiteral(typename Solver::TLit lit) const;
248   ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const;
249 
250   bool hasClauseRef(ClauseId id) const;
251   typename Solver::TCRef getClauseRef(ClauseId id) const;
252 
253 
254   const typename Solver::TClause& getClause(typename Solver::TCRef ref) const;
255 
256   void getLitVec(ClauseId id, LitVector& vec);
257 
258   bool checkResolution(ClauseId id);
259 
260   /**
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
264    *
265    * @return
266    */
267   ClauseId resolveUnit(typename Solver::TLit lit);
268 
269   /**
270    * Does a depth first search on removed literals and adds the literals
271    * to be removed in the proper order to the stack.
272    *
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
276    */
277   void removedDfs(typename Solver::TLit lit, LitSet* removedSet,
278                   LitVector& removeStack, LitSet& inClause, LitSet& seen);
279   void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id);
280 
281   void print(ClauseId id) const;
282   void printRes(ClauseId id) const;
283   void printRes(const ResolutionChain& res) const;
284 
285   std::unordered_map<ClauseId, int> d_glueMap;
286   struct Statistics {
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);
296     ~Statistics();
297   };
298 
299   std::string d_name;
300 
301   const ClauseId d_emptyClauseId;
302   IdSet d_seenLearnt;
303   IdToConflicts d_assumptionConflictsDebug;
304 
305   // Internal data.
306   Solver* d_solver;
307   context::Context* d_context;
308 
309   // clauses
310   IdCRefMap d_idClause;
311   ClauseIdMap d_clauseId;
312   IdUnitMap d_idUnit;
313   UnitIdMap d_unitId;
314   IdHashSet d_deleted;
315   IdToSatClause d_deletedTheoryLemmas;
316 
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
321                                     // to SAT solver
322 
323   // Resolutions.
324 
325   /**
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.
329    */
330   IdResMap d_resolutionChains;
331 
332    /*
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.
338    */
339   ResStack d_resStack;
340   bool d_checkRes;
341 
342   const ClauseId d_nullId;
343 
344   // temporary map for updating CRefs
345   ClauseIdMap d_temp_clauseId;
346   IdCRefMap d_temp_idClause;
347 
348   // unit conflict
349   context::CDMaybe<ClauseId> d_unitConflictId;
350 
351   ClauseId d_trueLit;
352   ClauseId d_falseLit;
353 
354   IdToSatClause d_seenInputs;
355   IdToSatClause d_seenLemmas;
356 
357   bool d_satProofConstructed;
358   Statistics d_statistics;
359 }; /* class TSatProof */
360 
361 template <class Solver>
362 prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
363 
364 /**
365  * Convert from minisat clause to SatClause
366  *
367  * @param minisat_cl
368  * @param sat_cl
369  */
370 template <class Solver>
371 void toSatClause(const typename Solver::TClause& minisat_cl,
372                  prop::SatClause& sat_cl);
373 
374 } /* CVC4 namespace */
375 
376 #endif /* __CVC4__SAT__PROOF_H */
377