cool / src / lib / minisat_stub.c @ de84f40d
History  View  Annotate  Download (3.33 KB)
1 
#define __STDC_LIMIT_MACROS


2 
#define __STDC_FORMAT_MACROS

3  
4 
extern "C" { 
5 
#include <caml/mlvalues.h> 
6 
#include <caml/alloc.h> 
7 
#include <caml/memory.h> 
8 
#include <caml/custom.h> 
9 
} 
10  
11 
//#include "minisat2/Solver.h"

12 
#include <minisat/core/Solver.h> 
13  
14 
//

15 
using namespace Minisat; 
16  
17 
extern "C" { 
18 
CAMLprim value mkLit_stub(value var, value sign); 
19 
CAMLprim value var_stub(value lit); 
20 
CAMLprim value sign_stub(value lit); 
21 
CAMLprim value neg_lit_stub(value lit); 
22  
23 
CAMLprim value new_solver_stub(value v); 
24 
CAMLprim value newVar_stub(value solver); 
25 
CAMLprim value addClause_stub(value solver, value lits); 
26 
CAMLprim value solve_stub(value solver, value assumps); 
27 
CAMLprim value modelValue_stub(value solver, value lit); 
28 
CAMLprim value get_conflict_stub(value solver); 
29  
30 
void finalize_solver(value solver);

31  
32 
char identifier[] = "minisat_stub"; 
33  
34 
struct custom_operations solver_ops =

35 
{ identifier, &finalize_solver, custom_compare_default, 
36 
custom_hash_default, custom_serialize_default, custom_deserialize_default }; 
37 
} 
38  
39 
CAMLprim value mkLit_stub(value var, value sign) { 
40 
Var v = Int_val(var); 
41 
bool s = Bool_val(sign);

42 
//int l = toInt(Lit(v, s));

43 
int l = toInt(mkLit(v, s));

44 
return Val_int(l);

45 
} 
46  
47 
CAMLprim value var_stub(value lit) { 
48 
Lit l = toLit(Int_val(lit)); 
49 
Var v = var(l); 
50 
return Val_int(v);

51 
} 
52  
53 
CAMLprim value sign_stub(value lit) { 
54 
Lit l = toLit(Int_val(lit)); 
55 
bool s = sign(l);

56 
return Val_bool(s);

57 
} 
58  
59 
CAMLprim value neg_lit_stub(value lit) { 
60 
Lit l = toLit(Int_val(lit)); 
61 
int nl = toInt(~l);

62 
return Val_int(nl);

63 
} 
64  
65 
CAMLprim value new_solver_stub(value v) { 
66 
CAMLparam1(v); 
67 
CAMLlocal1(result); 
68 
result = caml_alloc_custom(&solver_ops, sizeof(Solver *), 0, 1); 
69 
Solver *solv = new Solver(); 
70 
Solver **temp = (Solver **)Data_custom_val(result); 
71 
*temp = solv; 
72 
CAMLreturn (result); 
73 
} 
74  
75 
CAMLprim value newVar_stub(value solver) { 
76 
Solver *solv = *((Solver **)Data_custom_val(solver)); 
77 
Var var = solv>newVar(); 
78 
return Val_int(var);

79 
} 
80  
81 
CAMLprim value addClause_stub(value solver, value lits) { 
82 
Solver *solv = *((Solver **)Data_custom_val(solver)); 
83 
vec<Lit> ps; 
84 
value block = lits; 
85 
while (Is_block(block)) {

86 
Lit lit = toLit(Int_val(Field(block, 0)));

87 
ps.push(lit); 
88 
block = Field(block, 1);

89 
} 
90 
bool okay = solv>addClause(ps);

91 
return Val_bool(okay);

92 
} 
93  
94 
CAMLprim value solve_stub(value solver, value assumps) { 
95 
Solver *solv = *((Solver **)Data_custom_val(solver)); 
96 
vec<Lit> ass; 
97 
value block = assumps; 
98 
while (Is_block(block)) {

99 
Lit lit = toLit(Int_val(Field(block, 0)));

100 
ass.push(lit); 
101 
block = Field(block, 1);

102 
} 
103 
bool isSat = solv>solve(ass);

104 
return Val_bool(isSat);

105 
} 
106  
107 
CAMLprim value modelValue_stub(value solver, value lit) { 
108 
Solver *solv = *((Solver **)Data_custom_val(solver)); 
109 
Lit l = toLit(Int_val(lit)); 
110 
lbool status = solv>modelValue(l); 
111 
return Val_int(toInt(status));

112 
} 
113  
114 
CAMLprim value get_conflict_stub(value solver) { 
115 
CAMLparam1(solver); 
116 
CAMLlocal2(res, r); 
117 
Solver *solv = *((Solver **)Data_custom_val(solver)); 
118 
res = Val_int(0);

119 
for (int i = 0; i < solv>conflict.size(); ++i) { 
120 
int lit = toInt(solv>conflict[i]);

121 
r = caml_alloc_small(2, 0); 
122 
Field(r, 0) = Val_int(lit);

123 
Field(r, 1) = res;

124 
res = r; 
125 
} 
126 
CAMLreturn(res); 
127 
} 
128  
129 
void finalize_solver(value solver) {

130 
Solver *solv = *((Solver **)Data_custom_val(solver)); 
131 
delete solv; 
132 
return;

133 
} 