Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / minisat_stub.c @ 1d36cd07

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
}