minisat.ml

type var = int
type lit = int
type solver
type litstatus = LTRUE | LFALSE | LUNDEF

external var_to_lit : var -> bool -> lit = "mkLit_stub" "noalloc"
external lit_to_var : lit -> var = "var_stub" "noalloc"
external sign : lit -> bool = "sign_stub" "noalloc"
external neg_lit : lit -> lit = "neg_lit_stub" "noalloc"

external new_solver : unit -> solver = "new_solver_stub"
external new_variable : solver -> var = "newVar_stub" "noalloc"
external add_clause : solver -> lit list -> bool = "addClause_stub" "noalloc"
external invoke_solver : solver -> lit list -> bool = "solve_stub" "noalloc"
external modelValue : solver -> lit -> int = "modelValue_stub" "noalloc"
external get_conflict_stub : solver -> lit list = "get_conflict_stub"
let get_conflict solver =
  (*
    get_conflict_stub solver
   *)
  List.map (fun l -> neg_lit l) (get_conflict_stub solver)

let literal_status solver lit =
  match modelValue solver lit with
(*
  | -1 -> LFALSE
  | 0 -> LUNDEF
  | 1 -> LTRUE
*)
  | 0 -> LTRUE
  | 1 -> LFALSE
  | 2 -> LUNDEF
  | _ -> failwith "Unknown status (file minisat.ml)"