src/theory/bv/bv_solver_types.h

   1 //*********************                                                        */
   2 /*! \file bv_solver_types.h
   3  ** \verbatim
   4  ** Original author: lianah
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   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 Definitions of the SatSolver literal and clause types
  15  **
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef __CVC4__BV__SOLVER__TYPES_H
  21 #define __CVC4__BV__SOLVER__TYPES_H
  22
  23 #define BV_MINISAT
  24 //#define BV_PICOSAT
  25
  26 #ifdef BV_MINISAT  /* BV_MINISAT if we are using the minisat solver for the theory of bitvectors*/
  27 #include "theory/bv/bvminisat/core/Solver.h"
  28 #include "theory/bv/bvminisat/core/SolverTypes.h"
  29 #include "theory/bv/bvminisat/simp/SimpSolver.h"
  30 #endif   /* BV_MINISAT */
  31
  32 #ifdef BV_PICOSAT  /* BV_PICOSAT */
  33 #include "picosat/picosat.h"
  34 #endif  /* BV_PICOSAT */
  35
  36 #include "expr/node.h"
  37 #include <vector>
  38 #include <list>
  39 #include <iostream>
  40 #include <math.h>
  41 #include <ext/hash_map>
  42 #include "context/cdlist.h"
  43 #include "util/stats.h"
  44
  45
  46 namespace CVC4 {
  47 namespace theory {
  48 namespace bv {
  49
  50 #endif /* BV_MINISAT */
  51
  52
  53
  54 // #ifdef BV_PICOSAT /* BV_PICOSAT */
  55 // /**
  56 //  * PICOSAT type-definitions
  57 //  *
  58 //  *
  59 //  */
  60
  61 // typedef int SatVar;
  62 // typedef int SatLit;
  63
  64 // std::string toStringLit(SatLit lit);
  65
  66
  67 // SatLit neg(const SatLit& lit);
  68
  69 // struct SatLitHash {
  70 //   static size_t hash (const SatLit& lit) {
  71 //     return (size_t) lit;
  72 //   }
  73
  74 // };
  75
  76 // struct SatLitHashFunction {
  77 //   size_t operator()(SatLit lit) const {
  78 //     return (size_t) lit;
  79 //   }
  80 // };
  81
  82 // struct SatLitLess{
  83 //   static bool compare(const SatLit& x, const SatLit& y)
  84 //   {
  85 //     return x < y;
  86 //   }
  87 // };
  88
  89 // #endif /* BV_PICOSAT */
  90
  91 // #ifdef BV_PICOSAT  /* BV_PICOSAT */
  92
  93 // /**
  94 //  * Some helper functions that should be defined for each SAT solver supported
  95 //  *
  96 //  *
  97 //  * @return
  98 //  */
  99
 100 // SatLit mkLit(SatVar var);
 101 // SatVar mkVar(SatLit lit);
 102 // bool   polarity(SatLit lit);
 103
 104
 105 // /**
 106 //  * Wrapper to create the impression of a SatSolver class for Picosat
 107 //  * which is written in C
 108 //  */
 109
 110 // class SatSolver: public SatSolverInterface {
 111 //   int d_varCount;
 112 //   bool d_started;
 113 // public:
 114 //   SatSolver() :
 115 //     d_varCount(0),
 116 //     d_started(false)
 117 //   {
 118 //     picosat_init(); /// call constructor
 119 //     picosat_enable_trace_generation(); // required for unsat cores
 120 //   }
 121
 122 //   ~SatSolver() {
 123 //     picosat_reset();
 124 //   }
 125
 126 //   void   addClause(const SatClause* cl) {
 127 //     Assert (cl);
 128 //     const SatClause& clause = *cl;
 129 //     for (unsigned i = 0; i < clause.size(); ++i ) {
 130 //       picosat_add(clause[i]);
 131 //     }
 132 //     picosat_add(0); // ends clause
 133 //   }
 134
 135 //   bool   solve () {
 136 //     if(d_started) {
 137 //       picosat_remove_learned(100);
 138 //     }
 139 //     int res = picosat_sat(-1); // no decision limit
 140 //     // 0 UNKNOWN, 10 SATISFIABLE and 20 UNSATISFIABLE
 141 //     d_started = true;
 142 //     Assert (res == 10 || res == 20);
 143 //     return res == 10;
 144 //   }
 145
 146 //   bool   solve(const context::CDList<SatLit> & assumps) {
 147 //     context::CDList<SatLit>::const_iterator it = assumps.begin();
 148 //     for (; it!= assumps.end(); ++it) {
 149 //       picosat_assume(*it);
 150 //     }
 151 //     return solve ();
 152 //   }
 153
 154 //   SatVar newVar() { return ++d_varCount; }
 155
 156 //   void   setUnremovable(SatLit lit) {};
 157
 158 //   SatClause* getUnsatCore() {
 159 //     const int* failedAssumption = picosat_failed_assumptions();
 160 //     Assert(failedAssumption);
 161
 162 //     SatClause* unsatCore = new SatClause();
 163 //     while (*failedAssumption != 0) {
 164 //       SatLit lit = *failedAssumption;
 165 //       unsatCore->addLiteral(neg(lit));
 166 //       ++failedAssumption;
 167 //     }
 168 //     unsatCore->sort();
 169 //     return unsatCore;
 170 //   }
 171 // };
 172
 173
 174 // #endif  /* BV_PICOSAT */
 175
 176
 177
 178
 179 } /* bv namespace */
 180
 181 } /* theory namespace */
 182
 183 } /* CVC4 namespace */
 184
 185 #endif /* __CVC4__BV__SOLVER__TYPES_H */