backends/precosat/precosat_wrap.c

   1 /* C wrapper code for precosat */
   2
   3 #include "precosat_wrap.h"
   4 #include "precosat.hh"
   5
   6 extern "C" {
   7
   8 struct precosat_solver {
   9   PrecoSat::Solver * solver;
  10 };
  11
  12 static void
  13 init_precosat_solver(struct precosat_solver *s)
  14 {
  15   /* default initialization, similar to what precosatmain.cc does */
  16 /*   s->solver->set("verbose", 2); */
  17 /*   s->solver->set("print", 1); */
  18   return;
  19 };
  20
  21 struct precosat_solver *
  22 alloc_precosat_solver(int numvars)
  23 {
  24   struct precosat_solver *res = (struct precosat_solver*) malloc(sizeof(struct precosat_solver));
  25   if(res) {
  26     res->solver=new PrecoSat::Solver();
  27     res->solver->init(numvars);
  28     init_precosat_solver(res);
  29   };
  30   return res;
  31 }
  32
  33 void
  34 free_precosat_solver(struct precosat_solver *s)
  35 {
  36   s->solver->reset(); /* de-allocation not done in destructor...*/
  37   delete s->solver;
  38
  39   free(s);
  40 }
  41
  42 int
  43 precosat_set_option(struct precosat_solver *s, const char* optionname, int val)
  44 {
  45   return s->solver->set(optionname,val);
  46 }
  47
  48 enum precosat_result
  49 precosat_solve(struct precosat_solver *s)
  50 {
  51   int res;
  52   s->solver->fxopts();
  53
  54   res=s->solver->solve(INT_MAX);
  55
  56   if(res>0 && s->solver->satisfied())
  57     return PRECOSAT_SAT;
  58   else if (res<0)
  59     return PRECOSAT_UNSAT;
  60   else
  61     return PRECOSAT_ERROR;
  62 }
  63
  64 int
  65 precosat_sol_val(struct precosat_solver *s, int varidx)
  66 {
  67   return s->solver->val(varidx);
  68 }
  69
  70 void
  71 precosat_add_var_to_clause(struct precosat_solver *s, int varid)
  72 {
  73   s->solver->add(varid);
  74 }
  75
  76 void
  77 precosat_set_numvars(struct precosat_solver *s, int numvars)
  78 {
  79   while (numvars > s->solver->getMaxVar())
  80     s->solver->next();
  81 }
  82
  83 } /* extern "C" */
  84