backends/minisat/minisat_wrap.cc

   1 #include "minisat_wrap.h"
   2
   3 /* variables are indexed from 0 in minisat, but we like 1-based indexing. */
   4
   5 #define LISPVAR2MINISAT(x) ((x-1))
   6 #define MINISATVAR2LISP(x) ((x+1))
   7
   8
   9 extern "C" {
  10 struct minisat_solver {
  11   SimpSolver *solver;
  12   vec<Lit> *incumbent_clause;
  13   vec<Lit> *assumptions;
  14 };
  15
  16 static void
  17 init_minisat_solver(struct minisat_solver *s)
  18 {
  19   return;
  20 };
  21
  22 struct minisat_solver *
  23 alloc_minisat_solver()
  24 {
  25   struct minisat_solver *res = (struct minisat_solver*) malloc(sizeof(struct minisat_solver));
  26   if(res) {
  27     res->solver=new SimpSolver();
  28     res->incumbent_clause=new vec<Lit>();
  29     res->assumptions=new vec<Lit>();
  30   };
  31   return res;
  32 }
  33
  34 void
  35 free_minisat_solver(struct minisat_solver *s)
  36 {
  37   if(s->solver)
  38     delete s->solver;
  39   if(s->incumbent_clause)
  40     delete s->incumbent_clause;
  41   if(s->assumptions)
  42     delete s->assumptions;
  43
  44   free(s);
  45 }
  46
  47 int
  48 minisat_set_option(struct minisat_solver *s, const char* optionname, int val)
  49 {
  50   return -1;
  51 }
  52
  53 enum minisat_result
  54 minisat_solve(struct minisat_solver *s)
  55 {
  56   int res;
  57
  58   /* solve */
  59   res=s->solver->solve(*(s->assumptions),true,true);
  60      /* res=s->solver->solve(s->assumptions); */
  61
  62   if(res)
  63     return MINISAT_SAT;
  64   else
  65     return MINISAT_UNSAT;
  66 }
  67
  68 int
  69 minisat_sol_val(struct minisat_solver *s, int varidx)
  70 {
  71   lbool val = s->solver->model[LISPVAR2MINISAT(varidx)];
  72
  73   if(val==l_True)
  74     return 1;
  75   else if(val==l_False)
  76     return 0;
  77   else
  78     return -1;
  79 }
  80
  81 void
  82 minisat_add_var_to_clause(struct minisat_solver *s, int varid)
  83 {
  84   if(varid==0) {
  85     s->solver->addClause(*(s->incumbent_clause));
  86     s->incumbent_clause->clear();
  87   } else {
  88     int var = abs(varid) - 1;
  89
  90     while(var >= s->solver->nVars())
  91       s->solver->newVar();
  92
  93 //     assert(var < s->solver->nVars());
  94
  95
  96     s->incumbent_clause->push(varid>0 ? Lit(var) : ~Lit(var));
  97   }
  98 }
  99
 100 void
 101 minisat_set_numvars(struct minisat_solver *s, int numvars)
 102 {
 103   return;
 104   // minisat_add_clause does automatic resizing
 105   while (numvars > s->solver->nVars())
 106     s->solver->newVar();
 107 }
 108
 109 void
 110 minisat_clear_assumptions(struct minisat_solver *s)
 111 {
 112   s->assumptions->clear();
 113 }
 114
 115   /* returns current number of assumptions after adding VARID */
 116 int
 117 minisat_add_assumption(struct minisat_solver *s, int varid)
 118 {
 119
 120   int var = abs(varid) - 1;
 121
 122   s->assumptions->push(varid>0 ? Lit(var) : ~Lit(var));
 123   return s->assumptions->size();
 124
 125 }
 126 } /* extern "C" */