src/prop/minisat/minisat.h

   1 /*********************                                                        */
   2 /*! \file minisat.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, 2010, 2011  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.
  17  **/
  18
  19 #pragma once
  20
  21 #include "prop/sat_solver.h"
  22 #include "prop/sat_solver_registry.h"
  23 #include "prop/minisat/simp/SimpSolver.h"
  24
  25 namespace CVC4 {
  26 namespace prop {
  27
  28 class MinisatSatSolver : public DPLLSatSolverInterface {
  29
  30   /** The SatSolver used */
  31   Minisat::SimpSolver* d_minisat;
  32
  33   /** The SatSolver uses this to communicate with the theories */
  34   TheoryProxy* d_theoryProxy;
  35
  36   /** Context we will be using to synchronize the sat solver */
  37   context::Context* d_context;
  38
  39 public:
  40
  41   MinisatSatSolver();
  42   ~MinisatSatSolver();
  43
  44   static SatVariable     toSatVariable(Minisat::Var var);
  45   static Minisat::Lit    toMinisatLit(SatLiteral lit);
  46   static SatLiteral      toSatLiteral(Minisat::Lit lit);
  47   static SatValue        toSatLiteralValue(bool res);
  48   static SatValue        toSatLiteralValue(Minisat::lbool res);
  49   static Minisat::lbool  toMinisatlbool(SatValue val);
  50   //(Commented because not in use) static bool            tobool(SatValue val);
  51
  52   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
  53   static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
  54   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
  55   void initialize(context::Context* context, TheoryProxy* theoryProxy);
  56
  57   void addClause(SatClause& clause, bool removable);
  58
  59   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
  60   SatVariable trueVar() { return d_minisat->trueVar(); }
  61   SatVariable falseVar() { return d_minisat->falseVar(); }
  62
  63   SatValue solve();
  64   SatValue solve(long unsigned int&);
  65
  66   void interrupt();
  67
  68   SatValue value(SatLiteral l);
  69
  70   SatValue modelValue(SatLiteral l);
  71
  72   bool properExplanation(SatLiteral lit, SatLiteral expl) const;
  73
  74   /** Incremental interface */
  75
  76   unsigned getAssertionLevel() const;
  77
  78   void push();
  79
  80   void pop();
  81
  82   void requirePhase(SatLiteral lit);
  83
  84   bool flipDecision();
  85
  86   bool isDecision(SatVariable decn) const;
  87
  88   class Statistics {
  89   private:
  90     ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
  91     ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
  92     ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
  93     ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
  94     ReferenceStat<uint64_t> d_statTotLiterals;
  95   public:
  96     Statistics();
  97     ~Statistics();
  98     void init(Minisat::SimpSolver* d_minisat);
  99   };
 100   Statistics d_statistics;
 101
 102 };
 103
 104 } // prop namespace
 105 } // cvc4 namespace
 106