src/prop/minisat/minisat.h

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