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
|
module type S = sig
type reason
end
module type SOLVER = sig
type state
type reason
type var = int
type lit
val lit_of_var : var -> bool -> lit
val initialize_problem :
?print_var:(Format.formatter -> int -> unit) -> int -> state
val propagate : state -> unit
val protect : state -> unit
val reset : state -> unit
type value = True | False | Unknown
val assignment : state -> value array
val add_rule : state -> lit array -> reason list -> unit
val associate_vars : state -> lit -> var list -> unit
val solve : state -> var -> bool
val solve_lst : state -> var list -> bool
val collect_reasons : state -> var -> reason list
val collect_reasons_lst : state -> var list -> reason list
end
module F (X : S) : SOLVER with type reason = X.reason
|
