Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / minisat.ml @ 40a714df

History | View | Annotate | Download (1.06 KB)

1 4fd28192 Thorsten WiƟmann
type var = int
2
type lit = int
3
type solver
4
type litstatus = LTRUE | LFALSE | LUNDEF
5
6
external var_to_lit : var -> bool -> lit = "mkLit_stub" "noalloc"
7
external lit_to_var : lit -> var = "var_stub" "noalloc"
8
external sign : lit -> bool = "sign_stub" "noalloc"
9
external neg_lit : lit -> lit = "neg_lit_stub" "noalloc"
10
11
external new_solver : unit -> solver = "new_solver_stub"
12
external new_variable : solver -> var = "newVar_stub" "noalloc"
13
external add_clause : solver -> lit list -> bool = "addClause_stub" "noalloc"
14
external invoke_solver : solver -> lit list -> bool = "solve_stub" "noalloc"
15
external modelValue : solver -> lit -> int = "modelValue_stub" "noalloc"
16
external get_conflict_stub : solver -> lit list = "get_conflict_stub"
17
let get_conflict solver =
18
  (*
19
    get_conflict_stub solver
20
   *)
21
  List.map (fun l -> neg_lit l) (get_conflict_stub solver)
22
23
let literal_status solver lit =
24
  match modelValue solver lit with
25
(*
26
  | -1 -> LFALSE
27
  | 0 -> LUNDEF
28
  | 1 -> LTRUE
29
*)
30
  | 0 -> LTRUE
31
  | 1 -> LFALSE
32
  | 2 -> LUNDEF
33
  | _ -> failwith "Unknown status (file minisat.ml)"