Source file `minisat.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
(* This file is free software. See file "license" for more details. *)

type t
type 'a printer = Format.formatter -> 'a -> unit

module Lit = struct
  type t = int

  let[@inline] make n =
    assert (n > 0);
    n + n + 1

  let[@inline] neg n = n lxor 1
  let[@inline] abs n = n land (max_int - 1)
  let equal : t -> t -> bool = ( = )
  let compare : t -> t -> int = compare
  let[@inline] hash (x : t) : int = Hashtbl.hash x

  let[@inline] apply_sign sign t =
    if sign then
      t
    else
      neg t

  let[@inline] sign n =
    if n land 1 = 1 then
      true
    else
      false

  let[@inline] to_int n = n lsr 1

  let to_string x =
    (if sign x then
      ""
    else
      "-")
    ^ string_of_int (to_int x)

  let pp out x = Format.pp_print_string out (to_string x)
end

type assumptions = Lit.t array

module Raw = struct
  external create : unit -> t = "caml_minisat_new"
  external delete : t -> unit = "caml_minisat_delete"

  external ensure_var : t -> Lit.t -> unit = "caml_minisat_ensure_var"
    [@@noalloc]

  external add_clause_a : t -> Lit.t array -> bool = "caml_minisat_add_clause_a"
    [@@noalloc]

  external simplify : t -> bool = "caml_minisat_simplify" [@@noalloc]
  external solve : t -> Lit.t array -> bool = "caml_minisat_solve"
  external nvars : t -> int = "caml_minisat_nvars" [@@noalloc]
  external nclauses : t -> int = "caml_minisat_nclauses" [@@noalloc]
  external nconflicts : t -> int = "caml_minisat_nconflicts" [@@noalloc]
  external value : t -> Lit.t -> int = "caml_minisat_value" [@@noalloc]

  external value_level_0 : t -> Lit.t -> int = "caml_minisat_value_level_0"
    [@@noalloc]

  external set_verbose : t -> int -> unit = "caml_minisat_set_verbose"
  external okay : t -> bool = "caml_minisat_okay" [@@noalloc]
  external core : t -> Lit.t array = "caml_minisat_core"
  external to_dimacs : t -> string -> unit = "caml_minisat_to_dimacs"
  external interrupt : t -> unit = "caml_minisat_interrupt" [@@noalloc]

  external clear_interrupt : t -> unit = "caml_minisat_clear_interrupt"
    [@@noalloc]
end

let create () =
  let s = Raw.create () in
  Gc.finalise Raw.delete s;
  s

exception Unsat

let okay = Raw.okay
let check_ret_ b = if not b then raise Unsat
let ensure_lit_exists s l = Raw.ensure_var s l
let add_clause_a s a = Raw.add_clause_a s a |> check_ret_
let add_clause_l s lits = add_clause_a s (Array.of_list lits)

let pp_clause out l =
  Format.fprintf out "[@[<hv>";
  let first = ref true in
  List.iter
    (fun x ->
      if !first then
        first := false
      else
        Format.fprintf out ",@ ";
      Lit.pp out x)
    l;
  Format.fprintf out "@]]"

let simplify s = Raw.simplify s |> check_ret_
let solve ?(assumptions = [||]) s = Raw.solve s assumptions |> check_ret_
let unsat_core = Raw.core

type value =
  | V_undef
  | V_true
  | V_false

let string_of_value = function
  | V_undef -> "undef"
  | V_true -> "true"
  | V_false -> "false"

let pp_value out x = Format.pp_print_string out (string_of_value x)

let[@inline] conv_value_ = function
  | 1 -> V_true
  | 0 -> V_undef
  | -1 -> V_false
  | _ -> assert false

let[@inline] value s lit = conv_value_ (Raw.value s lit)
let[@inline] value_at_level_0 s lit = conv_value_ (Raw.value_level_0 s lit)
let set_verbose = Raw.set_verbose
let interrupt = Raw.interrupt
let clear_interrupt = Raw.clear_interrupt
let n_clauses = Raw.nclauses
let n_vars = Raw.nvars
let n_conflicts = Raw.nconflicts

module Debug = struct
  let to_dimacs_file = Raw.to_dimacs
end