src/proof/sat_proof.h

   1 /*********************                                                        */
   2 /*! \file sat_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Liana Hadarean, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 template <class Solver>
  42 class ProofProxy;
  43 } /* namespace CVC4 */
  44
  45 namespace CVC4 {
  46 /**
  47  * Helper debugging functions
  48  */
  49 template <class Solver>
  50 void printDebug(typename Solver::TLit l);
  51 template <class Solver>
  52 void printDebug(typename Solver::TClause& c);
  53
  54 enum ClauseKind {
  55   INPUT,
  56   THEORY_LEMMA,  // we need to distinguish because we must reprove deleted
  57                  // theory lemmas
  58   LEARNT
  59 }; /* enum ClauseKind */
  60
  61 template <class Solver>
  62 struct ResStep {
  63   typename Solver::TLit lit;
  64   ClauseId id;
  65   bool sign;
  66   ResStep(typename Solver::TLit l, ClauseId i, bool s)
  67       : lit(l), id(i), sign(s) {}
  68 }; /* struct ResStep */
  69
  70 template <class Solver>
  71 class ResChain {
  72  public:
  73   typedef std::vector<ResStep<Solver> > ResSteps;
  74   typedef std::set<typename Solver::TLit> LitSet;
  75
  76   ResChain(ClauseId start);
  77   ~ResChain();
  78
  79   void addStep(typename Solver::TLit, ClauseId, bool);
  80   bool redundantRemoved() {
  81     return (d_redundantLits == NULL || d_redundantLits->empty());
  82   }
  83   void addRedundantLit(typename Solver::TLit lit);
  84
  85   // accessor methods
  86   ClauseId getStart() const { return d_start; }
  87   const ResSteps& getSteps() const { return d_steps; }
  88   LitSet* getRedundant() const { return d_redundantLits; }
  89
  90  private:
  91   ClauseId d_start;
  92   ResSteps d_steps;
  93   LitSet* d_redundantLits;
  94 }; /* class ResChain */
  95
  96 template <class Solver>
  97 class TSatProof {
  98  protected:
  99   typedef ResChain<Solver> ResolutionChain;
 100
 101   typedef std::set<typename Solver::TLit> LitSet;
 102   typedef std::set<typename Solver::TVar> VarSet;
 103   typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap;
 104   typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
 105   typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
 106   typedef context::CDHashMap<int, ClauseId> UnitIdMap;
 107   typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
 108   typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap;
 109   typedef std::vector<ResolutionChain*> ResStack;
 110   typedef std::set<ClauseId> IdSet;
 111   typedef std::vector<typename Solver::TLit> LitVector;
 112   typedef std::unordered_map<ClauseId, typename Solver::TClause&>
 113       IdToMinisatClause;
 114   typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts;
 115
 116  public:
 117   TSatProof(Solver* solver, context::Context* context,
 118             const std::string& name, bool checkRes = false);
 119   virtual ~TSatProof();
 120   void setCnfProof(CnfProof* cnf_proof);
 121
 122   void startResChain(typename Solver::TLit start);
 123   void startResChain(typename Solver::TCRef start);
 124   void addResolutionStep(typename Solver::TLit lit,
 125                          typename Solver::TCRef clause, bool sign);
 126   /**
 127    * Pops the current resolution of the stack and stores it
 128    * in the resolution map. Also registers the 'clause' parameter
 129    * @param clause the clause the resolution is proving
 130    */
 131   // void endResChain(typename Solver::TCRef clause);
 132   void endResChain(typename Solver::TLit lit);
 133   void endResChain(ClauseId id);
 134
 135   /**
 136    * Pops the current resolution of the stack *without* storing it.
 137    */
 138   void cancelResChain();
 139
 140   /**
 141    * Stores in the current derivation the redundant literals that were
 142    * eliminated from the conflict clause during conflict clause minimization.
 143    * @param lit the eliminated literal
 144    */
 145   void storeLitRedundant(typename Solver::TLit lit);
 146
 147   /// update the CRef Id maps when Minisat does memory reallocation x
 148   void updateCRef(typename Solver::TCRef old_ref,
 149                   typename Solver::TCRef new_ref);
 150   void finishUpdateCRef();
 151
 152   /**
 153    * Constructs the empty clause resolution from the final conflict
 154    *
 155    * @param conflict
 156    */
 157   void finalizeProof(typename Solver::TCRef conflict);
 158
 159   /// clause registration methods
 160
 161   ClauseId registerClause(const typename Solver::TCRef clause, ClauseKind kind);
 162   ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind);
 163   void registerTrueLit(const typename Solver::TLit lit);
 164   void registerFalseLit(const typename Solver::TLit lit);
 165
 166   ClauseId getTrueUnit() const;
 167   ClauseId getFalseUnit() const;
 168
 169   void registerAssumption(const typename Solver::TVar var);
 170   ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl);
 171
 172   ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind);
 173
 174   /**
 175    * Marks the deleted clauses as deleted. Note we may still use them in the
 176    * final
 177    * resolution.
 178    * @param clause
 179    */
 180   void markDeleted(typename Solver::TCRef clause);
 181   bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
 182   /**
 183    * Constructs the resolution of ~q and resolves it with the current
 184    * resolution thus eliminating q from the current clause
 185    * @param q the literal to be resolved out
 186    */
 187   void resolveOutUnit(typename Solver::TLit q);
 188   /**
 189    * Constructs the resolution of the literal lit. Called when a clause
 190    * containing lit becomes satisfied and is removed.
 191    * @param lit
 192    */
 193   void storeUnitResolution(typename Solver::TLit lit);
 194
 195   ProofProxy<Solver>* getProxy() { return d_proxy; }
 196   /**
 197    * Constructs the SAT proof for the given clause,
 198    * by collecting the needed clauses in the d_seen
 199    * data-structures, also notifying the proofmanager.
 200    */
 201   void constructProof(ClauseId id);
 202   void constructProof() { constructProof(d_emptyClauseId); }
 203   void refreshProof(ClauseId id);
 204   void refreshProof() { refreshProof(d_emptyClauseId); }
 205   bool proofConstructed() const;
 206   void collectClauses(ClauseId id);
 207   bool derivedEmptyClause() const;
 208   prop::SatClause* buildClause(ClauseId id);
 209
 210   virtual void printResolution(ClauseId id, std::ostream& out,
 211                                std::ostream& paren) = 0;
 212   virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
 213   virtual void printResolutionEmptyClause(std::ostream& out,
 214                                           std::ostream& paren) = 0;
 215   virtual void printAssumptionsResolution(ClauseId id, std::ostream& out,
 216                                           std::ostream& paren) = 0;
 217
 218   void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas);
 219
 220   void storeClauseGlue(ClauseId clause, int glue);
 221
 222  protected:
 223   void print(ClauseId id) const;
 224   void printRes(ClauseId id) const;
 225   void printRes(const ResolutionChain& res) const;
 226
 227   bool isInputClause(ClauseId id) const;
 228   bool isLemmaClause(ClauseId id) const;
 229   bool isAssumptionConflict(ClauseId id) const;
 230
 231   bool isUnit(ClauseId id) const;
 232   typename Solver::TLit getUnit(ClauseId id) const;
 233
 234   bool isUnit(typename Solver::TLit lit) const;
 235   ClauseId getUnitId(typename Solver::TLit lit) const;
 236
 237
 238
 239   bool hasResolutionChain(ClauseId id) const;
 240
 241   /** Returns the resolution chain associated with id. Assert fails if
 242    * hasResolution(id) does not hold. */
 243   const ResolutionChain& getResolutionChain(ClauseId id) const;
 244
 245   /** Returns a mutable pointer to the resolution chain associated with id.
 246    * Assert fails if hasResolution(id) does not hold. */
 247   ResolutionChain* getMutableResolutionChain(ClauseId id);
 248
 249   void createLitSet(ClauseId id, LitSet& set);
 250
 251   /**
 252    * Registers a ClauseId with a resolution chain res.
 253    * Takes ownership of the memory associated with res.
 254    */
 255   void registerResolution(ClauseId id, ResolutionChain* res);
 256
 257
 258   bool hasClauseIdForCRef(typename Solver::TCRef clause) const;
 259   ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const;
 260
 261   bool hasClauseIdForLiteral(typename Solver::TLit lit) const;
 262   ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const;
 263
 264   bool hasClauseRef(ClauseId id) const;
 265   typename Solver::TCRef getClauseRef(ClauseId id) const;
 266
 267
 268   const typename Solver::TClause& getClause(typename Solver::TCRef ref) const;
 269   typename Solver::TClause* getMutableClause(typename Solver::TCRef ref);
 270
 271   void getLitVec(ClauseId id, LitVector& vec);
 272   virtual void toStream(std::ostream& out);
 273
 274   bool checkResolution(ClauseId id);
 275
 276   /**
 277    * Constructs a resolution tree that proves lit
 278    * and returns the ClauseId for the unit clause lit
 279    * @param lit the literal we are proving
 280    *
 281    * @return
 282    */
 283   ClauseId resolveUnit(typename Solver::TLit lit);
 284
 285   /**
 286    * Does a depth first search on removed literals and adds the literals
 287    * to be removed in the proper order to the stack.
 288    *
 289    * @param lit the literal we are recursing on
 290    * @param removedSet the previously computed set of redundant literals
 291    * @param removeStack the stack of literals in reverse order of resolution
 292    */
 293   void removedDfs(typename Solver::TLit lit, LitSet* removedSet,
 294                   LitVector& removeStack, LitSet& inClause, LitSet& seen);
 295   void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id);
 296
 297   std::string varName(typename Solver::TLit lit);
 298   std::string clauseName(ClauseId id);
 299
 300   void addToProofManager(ClauseId id, ClauseKind kind);
 301   void addToCnfProof(ClauseId id);
 302
 303   // Internal data.
 304   Solver* d_solver;
 305   context::Context* d_context;
 306   CnfProof* d_cnfProof;
 307
 308   // clauses
 309   IdCRefMap d_idClause;
 310   ClauseIdMap d_clauseId;
 311   IdUnitMap d_idUnit;
 312   UnitIdMap d_unitId;
 313   IdHashSet d_deleted;
 314   IdToSatClause d_deletedTheoryLemmas;
 315
 316   IdHashSet d_inputClauses;
 317   IdHashSet d_lemmaClauses;
 318   VarSet d_assumptions;             // assumption literals for bv solver
 319   IdHashSet d_assumptionConflicts;  // assumption conflicts not actually added
 320                                     // to SAT solver
 321   IdToConflicts d_assumptionConflictsDebug;
 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_emptyClauseId;
 343   const ClauseId d_nullId;
 344   // proxy class to break circular dependencies
 345   ProofProxy<Solver>* d_proxy;
 346
 347   // temporary map for updating CRefs
 348   ClauseIdMap d_temp_clauseId;
 349   IdCRefMap d_temp_idClause;
 350
 351   // unit conflict
 352   context::CDMaybe<ClauseId> d_unitConflictId;
 353
 354   ClauseId d_trueLit;
 355   ClauseId d_falseLit;
 356
 357   std::string d_name;
 358
 359   IdSet d_seenLearnt;
 360   IdToSatClause d_seenInputs;
 361   IdToSatClause d_seenLemmas;
 362
 363    private:
 364   std::unordered_map<ClauseId, int> d_glueMap;
 365   struct Statistics {
 366     IntStat d_numLearnedClauses;
 367     IntStat d_numLearnedInProof;
 368     IntStat d_numLemmasInProof;
 369     AverageStat d_avgChainLength;
 370     HistogramStat<uint64_t> d_resChainLengths;
 371     HistogramStat<uint64_t> d_usedResChainLengths;
 372     HistogramStat<uint64_t> d_clauseGlue;
 373     HistogramStat<uint64_t> d_usedClauseGlue;
 374     Statistics(const std::string& name);
 375     ~Statistics();
 376   };
 377
 378   bool d_satProofConstructed;
 379   Statistics d_statistics;
 380 }; /* class TSatProof */
 381
 382 template <class S>
 383 class ProofProxy {
 384  private:
 385   TSatProof<S>* d_proof;
 386
 387  public:
 388   ProofProxy(TSatProof<S>* pf);
 389   void updateCRef(typename S::TCRef oldref, typename S::TCRef newref);
 390 }; /* class ProofProxy */
 391
 392 template <class SatSolver>
 393 class LFSCSatProof : public TSatProof<SatSolver> {
 394  private:
 395  public:
 396   LFSCSatProof(SatSolver* solver, context::Context* context,
 397                const std::string& name, bool checkRes = false)
 398     : TSatProof<SatSolver>(solver, context, name, checkRes) {}
 399   void printResolution(ClauseId id,
 400                        std::ostream& out,
 401                        std::ostream& paren) override;
 402   void printResolutions(std::ostream& out, std::ostream& paren) override;
 403   void printResolutionEmptyClause(std::ostream& out,
 404                                   std::ostream& paren) override;
 405   void printAssumptionsResolution(ClauseId id,
 406                                   std::ostream& out,
 407                                   std::ostream& paren) override;
 408 }; /* class LFSCSatProof */
 409
 410 template <class Solver>
 411 prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
 412
 413 /**
 414  * Convert from minisat clause to SatClause
 415  *
 416  * @param minisat_cl
 417  * @param sat_cl
 418  */
 419 template <class Solver>
 420 void toSatClause(const typename Solver::TClause& minisat_cl,
 421                  prop::SatClause& sat_cl);
 422
 423 } /* CVC4 namespace */
 424
 425 #endif /* __CVC4__SAT__PROOF_H */