Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / minisat.ml @ 1d36cd07

History | View | Annotate | Download (1.22 KB)

1
type var = int
2
type lit = int
3
type solver
4
type litstatus = LTRUE | LFALSE | LUNDEF
5

    
6
(* "noalloc" is deprecated in OCaml 4.03 and should be replaced by [@@noalloc]
7
   once 4.03 becomes the minimum required version
8
*)
9
external var_to_lit : var -> bool -> lit = "mkLit_stub" "noalloc"
10
external lit_to_var : lit -> var = "var_stub" "noalloc"
11
external sign : lit -> bool = "sign_stub" "noalloc"
12
external neg_lit : lit -> lit = "neg_lit_stub" "noalloc"
13

    
14
external new_solver : unit -> solver = "new_solver_stub"
15
external new_variable : solver -> var = "newVar_stub" "noalloc"
16
external add_clause : solver -> lit list -> bool = "addClause_stub" "noalloc"
17
external invoke_solver : solver -> lit list -> bool = "solve_stub" "noalloc"
18
external modelValue : solver -> lit -> int = "modelValue_stub" "noalloc"
19
external get_conflict_stub : solver -> lit list = "get_conflict_stub"
20
let get_conflict solver =
21
  (*
22
    get_conflict_stub solver
23
   *)
24
  List.map (fun l -> neg_lit l) (get_conflict_stub solver)
25

    
26
let literal_status solver lit =
27
  match modelValue solver lit with
28
(*
29
  | -1 -> LFALSE
30
  | 0 -> LUNDEF
31
  | 1 -> LTRUE
32
*)
33
  | 0 -> LTRUE
34
  | 1 -> LFALSE
35
  | 2 -> LUNDEF
36
  | _ -> failwith "Unknown status (file minisat.ml)"
37

    
38
(* vim: set et sw=2 sts=2 ts=8 : *)