1 #include "minisat_wrap.h"
3 /* variables are indexed from 0 in minisat, but we like 1-based indexing. */
5 #define LISPVAR2MINISAT(x) ((x-1))
6 #define MINISATVAR2LISP(x) ((x+1))
10 struct minisat_solver
{
12 vec
<Lit
> *incumbent_clause
;
13 vec
<Lit
> *assumptions
;
17 init_minisat_solver(struct minisat_solver
*s
)
22 struct minisat_solver
*
23 alloc_minisat_solver()
25 struct minisat_solver
*res
= (struct minisat_solver
*) malloc(sizeof(struct minisat_solver
));
27 res
->solver
=new SimpSolver();
28 res
->incumbent_clause
=new vec
<Lit
>();
29 res
->assumptions
=new vec
<Lit
>();
35 free_minisat_solver(struct minisat_solver
*s
)
39 if(s
->incumbent_clause
)
40 delete s
->incumbent_clause
;
42 delete s
->assumptions
;
48 minisat_set_option(struct minisat_solver
*s
, const char* optionname
, int val
)
54 minisat_solve(struct minisat_solver
*s
)
59 res
=s
->solver
->solve(*(s
->assumptions
));
60 /* res=s->solver->solve(s->assumptions); */
69 minisat_sol_val(struct minisat_solver
*s
, int varidx
)
71 lbool val
= s
->solver
->model
[LISPVAR2MINISAT(varidx
)];
82 minisat_add_var_to_clause(struct minisat_solver
*s
, int varid
)
85 s
->solver
->addClause(*(s
->incumbent_clause
));
86 s
->incumbent_clause
->clear();
88 int var
= abs(varid
) - 1;
90 while(var
>= s
->solver
->nVars())
93 // assert(var < s->solver->nVars());
96 s
->incumbent_clause
->push(varid
>0 ? Lit(var
) : ~Lit(var
));
101 minisat_set_numvars(struct minisat_solver
*s
, int numvars
)
104 // minisat_add_clause does automatic resizing
105 while (numvars
> s
->solver
->nVars())
110 minisat_clear_assumptions(struct minisat_solver
*s
)
112 s
->assumptions
->clear();
115 /* returns current number of assumptions after adding VARID */
117 minisat_add_assumption(struct minisat_solver
*s
, int varid
)
120 int var
= abs(varid
) - 1;
122 s
->assumptions
->push(varid
>0 ? Lit(var
) : ~Lit(var
));
123 return s
->assumptions
->size();