src/proof/sat_proof.h

   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-2020 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;
  64   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);
  78   bool redundantRemoved() {
  79     return (d_redundantLits == NULL || d_redundantLits->empty());
  80   }
  81   void addRedundantLit(typename Solver::TLit lit);
  82
  83   // accessor methods
  84   ClauseId getStart() const { return d_start; }
  85   const ResSteps& getSteps() const { return d_steps; }
  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);
 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);
 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);
 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
 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
 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 */