src/proof/sat_proof.h

   1 /*********************                                                        */
   2 /*! \file sat_proof.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief Resolution proof
  15  **
  16  ** Resolution proof
  17  **/
  18
  19 #ifndef __CVC4__SAT__PROOF_H
  20 #define __CVC4__SAT__PROOF_H
  21
  22 #include <iostream>
  23 #include <stdint.h>
  24 #include <vector>
  25 #include <set>
  26 #include <ext/hash_map>
  27 #include <ext/hash_set>
  28 #include <sstream>
  29 namespace Minisat {
  30 class Solver;
  31 typedef uint32_t CRef;
  32 }
  33
  34 #include "prop/minisat/core/SolverTypes.h"
  35
  36 namespace std {
  37 using namespace __gnu_cxx;
  38 }
  39
  40 namespace CVC4 {
  41 /**
  42  * Helper debugging functions
  43  *
  44  */
  45 void printDebug(::Minisat::Lit l);
  46 void printDebug(::Minisat::Clause& c);
  47
  48 typedef int ClauseId;
  49 struct ResStep {
  50   ::Minisat::Lit lit;
  51   ClauseId id;
  52   bool sign;
  53   ResStep(::Minisat::Lit l, ClauseId i, bool s) :
  54     lit(l),
  55     id(i),
  56     sign(s)
  57   {}
  58 };
  59
  60 typedef std::vector< ResStep > ResSteps;
  61 typedef std::set < ::Minisat::Lit> LitSet;
  62
  63 class ResChain {
  64 private:
  65   ClauseId       d_start;
  66   ResSteps       d_steps;
  67   LitSet*        d_redundantLits;
  68 public:
  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);
  73   ~ResChain();
  74   // accessor methods
  75   ClauseId  getStart()     { return d_start; }
  76   ResSteps& getSteps()     { return d_steps; }
  77   LitSet*   getRedundant() { return d_redundantLits; }
  78 };
  79
  80
  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;
  88
  89 typedef std::hash_set < int >                     VarSet;
  90 typedef std::set < ClauseId >                     IdSet;
  91 typedef std::vector < ::Minisat::Lit >              LitVector;
  92 class SatProof;
  93
  94 class ProofProxy : public ProofProxyAbstract {
  95 private:
  96   SatProof* d_proof;
  97 public:
  98   ProofProxy(SatProof* pf);
  99   void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
 100 };
 101
 102 class SatProof {
 103 protected:
 104   ::Minisat::Solver*    d_solver;
 105   // clauses
 106   IdClauseMap         d_idClause;
 107   ClauseIdMap         d_clauseId;
 108   IdUnitMap           d_idUnit;
 109   UnitIdMap           d_unitId;
 110   IdHashSet           d_deleted;
 111   IdHashSet           d_inputClauses;
 112
 113   // resolutions
 114   IdResMap            d_resChains;
 115   ResStack            d_resStack;
 116   bool                d_checkRes;
 117
 118   static ClauseId     d_idCounter;
 119   const ClauseId      d_emptyClauseId;
 120   const ClauseId      d_nullId;
 121   // proxy class to break circular dependencies
 122   ProofProxy*         d_proxy;
 123
 124   // temporary map for updating CRefs
 125   ClauseIdMap         d_temp_clauseId;
 126   IdClauseMap         d_temp_idClause;
 127 public:
 128   SatProof(::Minisat::Solver* solver, bool checkRes = false);
 129 protected:
 130   void print(ClauseId id);
 131   void printRes(ClauseId id);
 132   void printRes(ResChain* res);
 133
 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);
 140
 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();
 148
 149   bool checkResolution(ClauseId id);
 150   /**
 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
 154    *
 155    * @return
 156    */
 157   ClauseId resolveUnit(::Minisat::Lit lit);
 158   /**
 159    * Does a depth first search on removed literals and adds the literals
 160    * to be removed in the proper order to the stack.
 161    *
 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
 165    */
 166   void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
 167   void removeRedundantFromRes(ResChain* res, ClauseId id);
 168 public:
 169   void startResChain(::Minisat::CRef start);
 170   void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign);
 171   /**
 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
 175    */
 176   void endResChain(::Minisat::CRef clause);
 177   void endResChain(::Minisat::Lit lit);
 178   /**
 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
 182    */
 183   void storeLitRedundant(::Minisat::Lit lit);
 184
 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();
 188
 189   /**
 190    * Constructs the empty clause resolution from the final conflict
 191    *
 192    * @param conflict
 193    */
 194   void finalizeProof(::Minisat::CRef conflict);
 195
 196   /// clause registration methods
 197   ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);
 198   ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false);
 199   /**
 200    * Marks the deleted clauses as deleted. Note we may still use them in the final
 201    * resolution.
 202    * @param clause
 203    */
 204   void markDeleted(::Minisat::CRef clause);
 205   /**
 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
 209    */
 210   void     resolveOutUnit(::Minisat::Lit q);
 211   /**
 212    * Constructs the resolution of the literal lit. Called when a clause
 213    * containing lit becomes satisfied and is removed.
 214    * @param lit
 215    */
 216   void     storeUnitResolution(::Minisat::Lit lit);
 217
 218   ProofProxy* getProxy() {return d_proxy; }
 219 };
 220
 221 class LFSCSatProof: public SatProof {
 222 private:
 223   VarSet             d_seenVars;
 224   std::ostringstream d_varSS;
 225   std::ostringstream d_lemmaSS;
 226   std::ostringstream d_clauseSS;
 227   std::ostringstream d_paren;
 228   IdSet              d_seenLemmas;
 229   IdHashSet          d_seenInput;
 230
 231   inline std::string varName(::Minisat::Lit lit);
 232   inline std::string clauseName(ClauseId id);
 233
 234   void collectLemmas(ClauseId id);
 235   void printResolution(ClauseId id);
 236   void printInputClause(ClauseId id);
 237
 238   void printVariables();
 239   void printClauses();
 240   void flush();
 241
 242 public:
 243   LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
 244     SatProof(solver, checkRes),
 245     d_seenVars(),
 246     d_varSS(),
 247     d_lemmaSS(),
 248     d_paren(),
 249     d_seenLemmas(),
 250     d_seenInput()
 251   {}
 252   void printProof();
 253 };
 254
 255 }
 256
 257 #endif