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 #include "util/proof.h"
  36
  37 namespace std {
  38 using namespace __gnu_cxx;
  39 }
  40
  41 namespace CVC4 {
  42 /**
  43  * Helper debugging functions
  44  *
  45  */
  46 void printDebug(::Minisat::Lit l);
  47 void printDebug(::Minisat::Clause& c);
  48
  49 typedef int ClauseId;
  50 struct ResStep {
  51   ::Minisat::Lit lit;
  52   ClauseId id;
  53   bool sign;
  54   ResStep(::Minisat::Lit l, ClauseId i, bool s) :
  55     lit(l),
  56     id(i),
  57     sign(s)
  58   {}
  59 };
  60
  61 typedef std::vector< ResStep > ResSteps;
  62 typedef std::set < ::Minisat::Lit> LitSet;
  63
  64 class ResChain {
  65 private:
  66   ClauseId       d_start;
  67   ResSteps       d_steps;
  68   LitSet*        d_redundantLits;
  69 public:
  70   ResChain(ClauseId start);
  71   void addStep(::Minisat::Lit, ClauseId, bool);
  72   bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); }
  73   void addRedundantLit(::Minisat::Lit lit);
  74   ~ResChain();
  75   // accessor methods
  76   ClauseId  getStart()     { return d_start; }
  77   ResSteps& getSteps()     { return d_steps; }
  78   LitSet*   getRedundant() { return d_redundantLits; }
  79 };
  80
  81
  82 typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap;
  83 typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
  84 typedef std::hash_map < ClauseId, ::Minisat::Lit>   IdUnitMap;
  85 typedef std::hash_map < int, ClauseId>            UnitIdMap; //FIXME
  86 typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
  87 typedef std::hash_set < ClauseId >                IdHashSet;
  88 typedef std::vector   < ResChain* >               ResStack;
  89
  90 typedef std::hash_set < int >                     VarSet;
  91 typedef std::set < ClauseId >                     IdSet;
  92 typedef std::vector < ::Minisat::Lit >              LitVector;
  93 class SatProof;
  94
  95 class ProofProxy : public ProofProxyAbstract {
  96 private:
  97   SatProof* d_proof;
  98 public:
  99   ProofProxy(SatProof* pf);
 100   void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
 101 };
 102
 103 class SatProof : public Proof {
 104 protected:
 105   ::Minisat::Solver*    d_solver;
 106   // clauses
 107   IdClauseMap         d_idClause;
 108   ClauseIdMap         d_clauseId;
 109   IdUnitMap           d_idUnit;
 110   UnitIdMap           d_unitId;
 111   IdHashSet           d_deleted;
 112   IdHashSet           d_inputClauses;
 113
 114   // resolutions
 115   IdResMap            d_resChains;
 116   ResStack            d_resStack;
 117   bool                d_checkRes;
 118
 119   static ClauseId     d_idCounter;
 120   const ClauseId      d_emptyClauseId;
 121   const ClauseId      d_nullId;
 122   // proxy class to break circular dependencies
 123   ProofProxy*         d_proxy;
 124
 125   // temporary map for updating CRefs
 126   ClauseIdMap         d_temp_clauseId;
 127   IdClauseMap         d_temp_idClause;
 128 public:
 129   SatProof(::Minisat::Solver* solver, bool checkRes = false);
 130 protected:
 131   void print(ClauseId id);
 132   void printRes(ClauseId id);
 133   void printRes(ResChain* res);
 134
 135   bool isInputClause(ClauseId id);
 136   bool isUnit(ClauseId id);
 137   bool isUnit(::Minisat::Lit lit);
 138   bool hasResolution(ClauseId id);
 139   void createLitSet(ClauseId id, LitSet& set);
 140   void registerResolution(ClauseId id, ResChain* res);
 141
 142   ClauseId      getClauseId(::Minisat::CRef clause);
 143   ClauseId      getClauseId(::Minisat::Lit lit);
 144   ::Minisat::CRef getClauseRef(ClauseId id);
 145   ::Minisat::Lit  getUnit(ClauseId id);
 146   ClauseId      getUnitId(::Minisat::Lit lit);
 147   ::Minisat::Clause& getClause(ClauseId id);
 148   virtual void toStream(std::ostream& out);
 149
 150   bool checkResolution(ClauseId id);
 151   /**
 152    * Constructs a resolution tree that proves lit
 153    * and returns the ClauseId for the unit clause lit
 154    * @param lit the literal we are proving
 155    *
 156    * @return
 157    */
 158   ClauseId resolveUnit(::Minisat::Lit lit);
 159   /**
 160    * Does a depth first search on removed literals and adds the literals
 161    * to be removed in the proper order to the stack.
 162    *
 163    * @param lit the literal we are recusing on
 164    * @param removedSet the previously computed set of redundantant literals
 165    * @param removeStack the stack of literals in reverse order of resolution
 166    */
 167   void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
 168   void removeRedundantFromRes(ResChain* res, ClauseId id);
 169 public:
 170   void startResChain(::Minisat::CRef start);
 171   void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign);
 172   /**
 173    * Pops the current resolution of the stack and stores it
 174    * in the resolution map. Also registers the 'clause' parameter
 175    * @param clause the clause the resolution is proving
 176    */
 177   void endResChain(::Minisat::CRef clause);
 178   void endResChain(::Minisat::Lit lit);
 179   /**
 180    * Stores in the current derivation the redundant literals that were
 181    * eliminated from the conflict clause during conflict clause minimization.
 182    * @param lit the eliminated literal
 183    */
 184   void storeLitRedundant(::Minisat::Lit lit);
 185
 186   /// update the CRef Id maps when Minisat does memory reallocation x
 187   void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref);
 188   void finishUpdateCRef();
 189
 190   /**
 191    * Constructs the empty clause resolution from the final conflict
 192    *
 193    * @param conflict
 194    */
 195   void finalizeProof(::Minisat::CRef conflict);
 196
 197   /// clause registration methods
 198   ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);
 199   ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false);
 200   /**
 201    * Marks the deleted clauses as deleted. Note we may still use them in the final
 202    * resolution.
 203    * @param clause
 204    */
 205   void markDeleted(::Minisat::CRef clause);
 206   /**
 207    * Constructs the resolution of ~q and resolves it with the current
 208    * resolution thus eliminating q from the current clause
 209    * @param q the literal to be resolved out
 210    */
 211   void     resolveOutUnit(::Minisat::Lit q);
 212   /**
 213    * Constructs the resolution of the literal lit. Called when a clause
 214    * containing lit becomes satisfied and is removed.
 215    * @param lit
 216    */
 217   void     storeUnitResolution(::Minisat::Lit lit);
 218
 219   ProofProxy* getProxy() {return d_proxy; }
 220 };
 221
 222 class LFSCSatProof: public SatProof {
 223 private:
 224   VarSet             d_seenVars;
 225   std::ostringstream d_varSS;
 226   std::ostringstream d_lemmaSS;
 227   std::ostringstream d_clauseSS;
 228   std::ostringstream d_paren;
 229   IdSet              d_seenLemmas;
 230   IdHashSet          d_seenInput;
 231
 232   inline std::string varName(::Minisat::Lit lit);
 233   inline std::string clauseName(ClauseId id);
 234
 235   void collectLemmas(ClauseId id);
 236   void printResolution(ClauseId id);
 237   void printInputClause(ClauseId id);
 238
 239   void printVariables();
 240   void printClauses();
 241   void flush(std::ostream& out);
 242
 243 public:
 244   LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
 245     SatProof(solver, checkRes),
 246     d_seenVars(),
 247     d_varSS(),
 248     d_lemmaSS(),
 249     d_paren(),
 250     d_seenLemmas(),
 251     d_seenInput()
 252   {}
 253   virtual void toStream(std::ostream& out);
 254 };
 255
 256 }
 257
 258 #endif