src/proof/sat_proof.h

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