src/prop/bvminisat/bvminisat.h

   1 /*********************                                                        */
   2 /*! \file bvminisat.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors:
   6  ** Minor contributors (to current version):
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2014  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 SAT Solver.
  15  **
  16  ** Implementation of the minisat for cvc4 (bitvectors).
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #pragma once
  22
  23 #include "prop/sat_solver.h"
  24 #include "prop/sat_solver_registry.h"
  25 #include "prop/bvminisat/simp/SimpSolver.h"
  26 #include "context/cdo.h"
  27
  28 namespace CVC4 {
  29 namespace prop {
  30
  31 class BVMinisatSatSolver : public BVSatSolverInterface, public context::ContextNotifyObj {
  32
  33 private:
  34
  35   class MinisatNotify : public BVMinisat::Notify {
  36     BVSatSolverInterface::Notify* d_notify;
  37   public:
  38     MinisatNotify(BVSatSolverInterface::Notify* notify)
  39     : d_notify(notify)
  40     {}
  41     bool notify(BVMinisat::Lit lit) {
  42       return d_notify->notify(toSatLiteral(lit));
  43     }
  44     void notify(BVMinisat::vec<BVMinisat::Lit>& clause) {
  45       SatClause satClause;
  46       toSatClause(clause, satClause);
  47       d_notify->notify(satClause);
  48     }
  49
  50     void safePoint() {
  51       d_notify->safePoint();
  52     }
  53   };
  54
  55   BVMinisat::SimpSolver* d_minisat;
  56   MinisatNotify* d_minisatNotify;
  57
  58   unsigned d_assertionsCount;
  59   context::CDO<unsigned> d_assertionsRealCount;
  60   context::CDO<unsigned> d_lastPropagation;
  61
  62 protected:
  63
  64   void contextNotifyPop();
  65
  66 public:
  67
  68   BVMinisatSatSolver() :
  69     ContextNotifyObj(NULL, false),
  70     d_assertionsRealCount(NULL, (unsigned)0),
  71     d_lastPropagation(NULL, (unsigned)0),
  72     d_statistics("")
  73   { Unreachable(); }
  74   BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name = "");
  75   ~BVMinisatSatSolver() throw(AssertionException);
  76
  77   void setNotify(Notify* notify);
  78
  79   void addClause(SatClause& clause, bool removable, uint64_t proof_id);
  80
  81   SatValue propagate();
  82
  83   SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
  84
  85   SatVariable trueVar() { return d_minisat->trueVar(); }
  86   SatVariable falseVar() { return d_minisat->falseVar(); }
  87
  88   void markUnremovable(SatLiteral lit);
  89
  90   bool spendResource();
  91
  92   void interrupt();
  93
  94   SatValue solve();
  95   SatValue solve(long unsigned int&);
  96   void getUnsatCore(SatClause& unsatCore);
  97
  98   SatValue value(SatLiteral l);
  99   SatValue modelValue(SatLiteral l);
 100
 101   void unregisterVar(SatLiteral lit);
 102   void renewVar(SatLiteral lit, int level = -1);
 103   unsigned getAssertionLevel() const;
 104
 105
 106   // helper methods for converting from the internal Minisat representation
 107
 108   static SatVariable     toSatVariable(BVMinisat::Var var);
 109   static BVMinisat::Lit    toMinisatLit(SatLiteral lit);
 110   static SatLiteral      toSatLiteral(BVMinisat::Lit lit);
 111   static SatValue toSatLiteralValue(bool res);
 112   static SatValue toSatLiteralValue(BVMinisat::lbool res);
 113
 114   static void  toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
 115   static void  toSatClause    (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause);
 116   void addMarkerLiteral(SatLiteral lit);
 117
 118   void explain(SatLiteral lit, std::vector<SatLiteral>& explanation);
 119
 120   SatValue assertAssumption(SatLiteral lit, bool propagate);
 121
 122   void popAssumption();
 123
 124   class Statistics {
 125   public:
 126     ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
 127     ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
 128     ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
 129     ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
 130     ReferenceStat<uint64_t> d_statTotLiterals;
 131     ReferenceStat<int> d_statEliminatedVars;
 132     IntStat d_statCallsToSolve;
 133     BackedStat<double> d_statSolveTime;
 134     bool d_registerStats;
 135     Statistics(const std::string& prefix);
 136     ~Statistics();
 137     void init(BVMinisat::SimpSolver* minisat);
 138   };
 139
 140   Statistics d_statistics;
 141 };
 142
 143 }
 144 }
 145
 146
 147
 148