src/prop/cryptominisat.h

   1 /*********************                                                        */
   2 /*! \file cryptominisat.h
   3  ** \verbatim
   4  ** Original author: lianah
   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 cryptominisat sat solver for cvc4 (bitvectors).
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #pragma once
  22
  23 #include "prop/sat_solver.h"
  24
  25 #ifdef CVC4_USE_CRYPTOMINISAT
  26 #include <cryptominisat4/cryptominisat.h>
  27 namespace CVC4 {
  28 namespace prop {
  29
  30 class CryptoMinisatSolver : public SatSolver {
  31
  32 private:
  33   CMSat::SATSolver* d_solver;
  34   unsigned d_numVariables;
  35   bool d_okay;
  36   SatVariable d_true;
  37   SatVariable d_false;
  38 public:
  39   CryptoMinisatSolver(StatisticsRegistry* registry,
  40                       const std::string& name = "");
  41   virtual ~CryptoMinisatSolver();
  42
  43   ClauseId addClause(SatClause& clause, bool removable);
  44   ClauseId addXorClause(SatClause& clause, bool rhs, bool removable);
  45
  46   bool nativeXor() { return true; }
  47
  48   SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
  49
  50   SatVariable trueVar();
  51   SatVariable falseVar();
  52
  53   void markUnremovable(SatLiteral lit);
  54
  55   void interrupt();
  56
  57   SatValue solve();
  58   SatValue solve(long unsigned int&);
  59   bool ok() const;
  60   SatValue value(SatLiteral l);
  61   SatValue modelValue(SatLiteral l);
  62
  63   unsigned getAssertionLevel() const;
  64
  65
  66   // helper methods for converting from the internal Minisat representation
  67
  68   static SatVariable toSatVariable(CMSat::Var var);
  69   static CMSat::Lit toInternalLit(SatLiteral lit);
  70   static SatLiteral toSatLiteral(CMSat::Lit lit);
  71   static SatValue toSatLiteralValue(bool res);
  72   static SatValue toSatLiteralValue(CMSat::lbool res);
  73
  74   static void  toInternalClause(SatClause& clause, std::vector<CMSat::Lit>& internal_clause);
  75   static void  toSatClause (std::vector<CMSat::Lit>& clause, SatClause& sat_clause);
  76
  77   class Statistics {
  78   public:
  79     StatisticsRegistry* d_registry;
  80     IntStat d_statCallsToSolve;
  81     IntStat d_xorClausesAdded;
  82     IntStat d_clausesAdded;
  83     TimerStat d_solveTime;
  84     bool d_registerStats;
  85     Statistics(StatisticsRegistry* registry,
  86                const std::string& prefix);
  87     ~Statistics();
  88   };
  89
  90   Statistics d_statistics;
  91 };
  92 } // CVC4::prop
  93 } // CVC4
  94
  95 #else // CVC4_USE_CRYPTOMINISAT
  96
  97 namespace CVC4 {
  98 namespace prop {
  99
 100 class CryptoMinisatSolver : public SatSolver {
 101
 102 public:
 103   CryptoMinisatSolver(StatisticsRegistry* registry,
 104                       const std::string& name = "") { Unreachable(); }
 105   /** Assert a clause in the solver. */
 106   ClauseId addClause(SatClause& clause, bool removable) {
 107     Unreachable();
 108   }
 109
 110   /** Return true if the solver supports native xor resoning */
 111   bool nativeXor() { Unreachable(); }
 112
 113   /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
 114   ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
 115     Unreachable();
 116   }
 117
 118   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); }
 119   SatVariable trueVar() { Unreachable(); }
 120   SatVariable falseVar() { Unreachable(); }
 121   SatValue solve() { Unreachable(); }
 122   SatValue solve(long unsigned int&) { Unreachable(); }
 123   void interrupt() { Unreachable(); }
 124   SatValue value(SatLiteral l) { Unreachable(); }
 125   SatValue modelValue(SatLiteral l) { Unreachable(); }
 126   unsigned getAssertionLevel() const { Unreachable(); }
 127   bool ok() const { return false;};
 128
 129
 130 };/* class CryptoMinisatSolver */
 131 } // CVC4::prop
 132 } // CVC4
 133
 134 #endif // CVC4_USE_CRYPTOMINISAT