src/prop/bvminisat/bvminisat.h

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