Merged bit-vector and uf proof branch.

1 files changed, 191 insertions, 100 deletions

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 52319431c..95a4c8907 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -20,63 +20,63 @@
 #define __CVC4__SAT__PROOF_H
 
 #include <stdint.h>
-
 #include <ext/hash_map>
 #include <ext/hash_set>
 #include <iosfwd>
 #include <set>
 #include <sstream>
 #include <vector>
-
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
+#include "util/proof.h"
+#include "util/statistics_registry.h"
+
 
 namespace CVC4 {
-namespace Minisat {
-  class Solver;
-  typedef uint32_t CRef;
-}/* Minisat namespace */
-}
 
-#include "prop/minisat/core/SolverTypes.h"
-#include "util/proof.h"
-#include "prop/sat_solver_types.h"
-namespace std {
-  using namespace __gnu_cxx;
-}/* std namespace */
 
-namespace CVC4 {
+class CnfProof;
 
 /**
  * Helper debugging functions
  */
-void printDebug(Minisat::Lit l);
-void printDebug(Minisat::Clause& c);
+template <class Solver> void printDebug(typename Solver::TLit l);
+template <class Solver> void printDebug(typename Solver::TClause& c);
+
+enum ClauseKind {
+  INPUT,
+  THEORY_LEMMA, // we need to distinguish because we must reprove deleted theory lemmas
+  LEARNT
+};/* enum ClauseKind */
+
 
+template <class Solver>
 struct ResStep {
-  Minisat::Lit lit;
+  typename Solver::TLit lit;
   ClauseId id;
   bool sign;
-  ResStep(Minisat::Lit l, ClauseId i, bool s) :
+  ResStep(typename Solver::TLit l, ClauseId i, bool s) :
     lit(l),
     id(i),
     sign(s)
   {}
 };/* struct ResStep */
 
-typedef std::vector< ResStep > ResSteps;
-typedef std::set < Minisat::Lit> LitSet;
-
+template <class Solver>
 class ResChain {
+public:
+  typedef std::vector< ResStep<Solver> > ResSteps;
+  typedef std::set < typename Solver::TLit> LitSet;
+
 private:
   ClauseId       d_start;
   ResSteps       d_steps;
   LitSet*        d_redundantLits;
 public:
   ResChain(ClauseId start);
-  void addStep(Minisat::Lit, ClauseId, bool);
+  void addStep(typename Solver::TLit, ClauseId, bool);
   bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); }
-  void addRedundantLit(Minisat::Lit lit);
+  void addRedundantLit(typename Solver::TLit lit);
   ~ResChain();
   // accessor methods
   ClauseId  getStart()     { return d_start; }
@@ -84,35 +84,31 @@ public:
   LitSet*   getRedundant() { return d_redundantLits; }
 };/* class ResChain */
 
-typedef std::hash_map < ClauseId, Minisat::CRef > IdCRefMap;
-typedef std::hash_map < Minisat::CRef, ClauseId > ClauseIdMap;
-typedef std::hash_map < ClauseId, Minisat::Lit>   IdUnitMap;
-typedef std::hash_map < int, ClauseId>            UnitIdMap; //FIXME
-typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
-typedef std::hash_set < ClauseId >                IdHashSet;
-typedef std::hash_map < ClauseId, uint64_t >      IdProofRuleMap;
-typedef std::vector   < ResChain* >               ResStack;
-typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;
-typedef std::set < ClauseId >                     IdSet;
-typedef std::vector < Minisat::Lit >              LitVector;
-typedef __gnu_cxx::hash_map<ClauseId, Minisat::Clause& > IdToMinisatClause;
-
-class SatProof;
-
-class ProofProxy : public ProofProxyAbstract {
-private:
-  SatProof* d_proof;
-public:
-  ProofProxy(SatProof* pf);
-  void updateCRef(Minisat::CRef oldref, Minisat::CRef newref);
-};/* class ProofProxy */
-
+template <class Solver> class ProofProxy;
 
 class CnfProof;
 
-class SatProof {
+template<class Solver>
+class TSatProof {
 protected:
-  Minisat::Solver*    d_solver;
+  typedef std::set < typename Solver::TLit> LitSet;
+  typedef std::set < typename Solver::TVar> VarSet;
+  typedef std::hash_map < ClauseId, typename Solver::TCRef > IdCRefMap;
+  typedef std::hash_map < typename Solver::TCRef, ClauseId > ClauseIdMap;
+  typedef std::hash_map < ClauseId, typename Solver::TLit>   IdUnitMap;
+  typedef std::hash_map < int, ClauseId>            UnitIdMap; 
+  typedef std::hash_map < ClauseId, ResChain<Solver>* >      IdResMap;
+  typedef std::hash_map < ClauseId, uint64_t >      IdProofRuleMap;
+  typedef std::vector   < ResChain<Solver>* >       ResStack;
+  //typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;
+  typedef std::set < ClauseId > IdSet;
+  typedef std::vector < typename Solver::TLit > LitVector;
+  typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause& > IdToMinisatClause;
+  typedef __gnu_cxx::hash_map<ClauseId, LitVector* > IdToConflicts;
+  
+  typename Solver::Solver*    d_solver;
+  CnfProof* d_cnfProof; 
+  
   // clauses
   IdCRefMap           d_idClause;
   ClauseIdMap         d_clauseId;
@@ -120,10 +116,14 @@ protected:
   UnitIdMap           d_unitId;
   IdHashSet           d_deleted;
   IdToSatClause       d_deletedTheoryLemmas;
-public:
-  IdProofRuleMap      d_inputClauses;
-  IdProofRuleMap      d_lemmaClauses;
+
 protected:
+  IdHashSet           d_inputClauses;
+  IdHashSet           d_lemmaClauses;
+  VarSet              d_assumptions; // assumption literals for bv solver
+  IdHashSet           d_assumptionConflicts; // assumption conflicts not actually added to SAT solver
+  IdToConflicts       d_assumptionConflictsDebug;
+  
   // resolutions
   IdResMap            d_resChains;
   ResStack            d_resStack;
@@ -132,38 +132,45 @@ protected:
   const ClauseId      d_emptyClauseId;
   const ClauseId      d_nullId;
   // proxy class to break circular dependencies
-  ProofProxy*         d_proxy;
+  ProofProxy<Solver>*         d_proxy;
 
   // temporary map for updating CRefs
   ClauseIdMap         d_temp_clauseId;
-  IdCRefMap         d_temp_idClause;
+  IdCRefMap           d_temp_idClause;
 
   // unit conflict
   ClauseId d_unitConflictId;
   bool d_storedUnitConflict;
+
+  ClauseId d_trueLit;
+  ClauseId d_falseLit;
+  
+  std::string d_name;
 public:
-  SatProof(Minisat::Solver* solver, bool checkRes = false);
-  virtual ~SatProof();
+  TSatProof(Solver* solver, const std::string& name, bool checkRes = false);
+  virtual ~TSatProof();
+  void setCnfProof(CnfProof* cnf_proof);
 protected:
   void print(ClauseId id);
   void printRes(ClauseId id);
-  void printRes(ResChain* res);
+  void printRes(ResChain<Solver>* res);
 
   bool isInputClause(ClauseId id);
-  bool isTheoryConflict(ClauseId id);
   bool isLemmaClause(ClauseId id);
+  bool isAssumptionConflict(ClauseId id);
   bool isUnit(ClauseId id);
-  bool isUnit(Minisat::Lit lit);
+  bool isUnit(typename Solver::TLit lit);
   bool hasResolution(ClauseId id);
   void createLitSet(ClauseId id, LitSet& set);
-  void registerResolution(ClauseId id, ResChain* res);
-
-  ClauseId      getClauseId(Minisat::CRef clause);
-  ClauseId      getClauseId(Minisat::Lit lit);
-  Minisat::CRef getClauseRef(ClauseId id);
-  Minisat::Lit  getUnit(ClauseId id);
-  ClauseId      getUnitId(Minisat::Lit lit);
-  Minisat::Clause& getClause(Minisat::CRef ref);
+  void registerResolution(ClauseId id, ResChain<Solver>* res);
+
+  ClauseId      getClauseId(typename Solver::TCRef clause);
+  ClauseId      getClauseId(typename Solver::TLit lit);
+  typename Solver::TCRef getClauseRef(ClauseId id);
+  typename Solver::TLit  getUnit(ClauseId id);
+  ClauseId      getUnitId(typename Solver::TLit lit);
+  typename Solver::TClause& getClause(typename Solver::TCRef ref);
+  void getLitVec(ClauseId id, LitVector& vec);
   virtual void toStream(std::ostream& out);
 
   bool checkResolution(ClauseId id);
@@ -174,7 +181,7 @@ protected:
    *
    * @return
    */
-  ClauseId resolveUnit(Minisat::Lit lit);
+  ClauseId resolveUnit(typename Solver::TLit lit);
   /**
    * Does a depth first search on removed literals and adds the literals
    * to be removed in the proper order to the stack.
@@ -183,27 +190,35 @@ protected:
    * @param removedSet the previously computed set of redundant literals
    * @param removeStack the stack of literals in reverse order of resolution
    */
-  void removedDfs(Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
-  void removeRedundantFromRes(ResChain* res, ClauseId id);
+  void removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
+  void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id);
 public:
-  void startResChain(Minisat::CRef start);
-  void addResolutionStep(Minisat::Lit lit, Minisat::CRef clause, bool sign);
+  void startResChain(typename Solver::TLit start);
+  void startResChain(typename Solver::TCRef start);
+  void addResolutionStep(typename Solver::TLit lit, typename Solver::TCRef clause, bool sign);
   /**
    * Pops the current resolution of the stack and stores it
    * in the resolution map. Also registers the 'clause' parameter
    * @param clause the clause the resolution is proving
    */
-  void endResChain(Minisat::CRef clause);
-  void endResChain(Minisat::Lit lit);
+  //void endResChain(typename Solver::TCRef clause);
+  void endResChain(typename Solver::TLit lit);
+  void endResChain(ClauseId id);
+  /** 
+   * Pops the current resolution of the stack *without* storing it. 
+   * 
+   */
+  void cancelResChain();
+
   /**
    * Stores in the current derivation the redundant literals that were
    * eliminated from the conflict clause during conflict clause minimization.
    * @param lit the eliminated literal
    */
-  void storeLitRedundant(Minisat::Lit lit);
+  void storeLitRedundant(typename Solver::TLit lit);
 
   /// update the CRef Id maps when Minisat does memory reallocation x
-  void updateCRef(Minisat::CRef old_ref, Minisat::CRef new_ref);
+  void updateCRef(typename Solver::TCRef old_ref, typename Solver::TCRef new_ref);
   void finishUpdateCRef();
 
   /**
@@ -211,66 +226,142 @@ public:
    *
    * @param conflict
    */
-  void finalizeProof(Minisat::CRef conflict);
+  void finalizeProof(typename Solver::TCRef conflict);
 
   /// clause registration methods
-  ClauseId registerClause(const Minisat::CRef clause, ClauseKind kind, uint64_t proof_id);
-  ClauseId registerUnitClause(const Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
-
-  void storeUnitConflict(Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
 
+  ClauseId registerClause(const typename Solver::TCRef clause,
+			  ClauseKind kind);
+  ClauseId registerUnitClause(const typename Solver::TLit lit,
+			      ClauseKind kind);
+  void registerTrueLit(const typename Solver::TLit lit);
+  void registerFalseLit(const typename Solver::TLit lit);
+
+  ClauseId getTrueUnit() const;
+  ClauseId getFalseUnit() const;
+
+  
+  void registerAssumption(const typename Solver::TVar var);
+  ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl);
+  
+  ClauseId storeUnitConflict(typename Solver::TLit lit,
+                             ClauseKind kind);
+ 
   /**
    * Marks the deleted clauses as deleted. Note we may still use them in the final
    * resolution.
    * @param clause
    */
-  void markDeleted(Minisat::CRef clause);
+  void markDeleted(typename Solver::TCRef clause);
   bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
   /**
    * Constructs the resolution of ~q and resolves it with the current
    * resolution thus eliminating q from the current clause
    * @param q the literal to be resolved out
    */
-  void     resolveOutUnit(Minisat::Lit q);
+  void resolveOutUnit(typename Solver::TLit q);
   /**
    * Constructs the resolution of the literal lit. Called when a clause
    * containing lit becomes satisfied and is removed.
    * @param lit
    */
-  void     storeUnitResolution(Minisat::Lit lit);
-
-  ProofProxy* getProxy() {return d_proxy; }
+  void storeUnitResolution(typename Solver::TLit lit);
 
+  ProofProxy<Solver>* getProxy() {return d_proxy; }
   /**
-     Constructs the SAT proof identifying the needed lemmas
+   * Constructs the SAT proof for the given clause,
+   * by collecting the needed clauses in the d_seen
+   * data-structures, also notifying the proofmanager.
    */
-  void constructProof();
-
+  void constructProof(ClauseId id);
+  void constructProof() {
+    constructProof(d_emptyClauseId);
+  }
+  void collectClauses(ClauseId id);
+  prop::SatClause* buildClause(ClauseId id);
 protected:
-  IdSet              d_seenLearnt;
-  IdHashSet          d_seenInput;
-  IdHashSet          d_seenTheoryConflicts;
-  IdHashSet          d_seenLemmas;
+  IdSet               d_seenLearnt;
+  IdToSatClause          d_seenInputs;
+  IdToSatClause          d_seenLemmas;
+
+  std::string varName(typename Solver::TLit lit);
+  std::string clauseName(ClauseId id);
 
-  inline std::string varName(Minisat::Lit lit);
-  inline std::string clauseName(ClauseId id);
 
-  void collectClauses(ClauseId id);
   void addToProofManager(ClauseId id, ClauseKind kind);
+  void addToCnfProof(ClauseId id);
 public:
+  virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0;
   virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
-};/* class SatProof */
+  virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren) = 0;
+  virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0;
+
 
-class LFSCSatProof : public SatProof {
+  void collectClausesUsed(IdToSatClause& inputs,
+                          IdToSatClause& lemmas);
+
+  void storeClauseGlue(ClauseId clause, int glue);
+
+private:
+  __gnu_cxx::hash_map<ClauseId, int> d_glueMap; 
+  struct Statistics {
+    IntStat d_numLearnedClauses;
+    IntStat d_numLearnedInProof;
+    IntStat d_numLemmasInProof;
+    AverageStat d_avgChainLength;
+    HistogramStat<uint64_t> d_resChainLengths;
+    HistogramStat<uint64_t> d_usedResChainLengths;
+    HistogramStat<uint64_t> d_clauseGlue;
+    HistogramStat<uint64_t> d_usedClauseGlue;
+    Statistics(const std::string& name);
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
+};/* class TSatProof */
+
+
+template <class S>
+class ProofProxy {
 private:
-  void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
+  TSatProof<S>* d_proof;
 public:
-  LFSCSatProof(Minisat::Solver* solver, bool checkRes = false)
-    : SatProof(solver, checkRes)
+  ProofProxy(TSatProof<S>* pf);
+  void updateCRef(typename S::TCRef oldref, typename S::TCRef newref);
+};/* class ProofProxy */
+
+
+template <class SatSolver> 
+class LFSCSatProof : public TSatProof<SatSolver> {
+private:
+
+public:
+  LFSCSatProof(SatSolver* solver, const std::string& name, bool checkRes = false)
+    : TSatProof<SatSolver>(solver, name, checkRes)
   {}
+  virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
   virtual void printResolutions(std::ostream& out, std::ostream& paren);
+  virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren);
+  virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren);
 };/* class LFSCSatProof */
 
+
+
+template<class Solver>
+prop::SatLiteral toSatLiteral(typename Solver::TLit lit); 
+
+
+/** 
+* Convert from minisat clause to SatClause
+* 
+* @param minisat_cl 
+* @param sat_cl 
+*/
+template<class Solver>
+void toSatClause(const typename Solver::TClause& minisat_cl,
+                 prop::SatClause& sat_cl);
+
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__SAT__PROOF_H */