Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / minisat.mli @ 7c4d2eb4

History | View | Annotate | Download (455 Bytes)

1 4fd28192 Thorsten WiƟmann
type var = private int
2
type lit = private int
3
type solver
4
type litstatus = LTRUE | LFALSE | LUNDEF
5
6
val var_to_lit : var -> bool -> lit
7
val lit_to_var : lit -> var
8
val sign : lit -> bool
9
val neg_lit : lit -> lit
10
11
val new_solver : unit -> solver
12
val new_variable : solver -> var
13
val add_clause : solver -> lit list -> bool
14
val invoke_solver : solver -> lit list -> bool
15
val literal_status : solver -> lit -> litstatus
16
val get_conflict : solver -> lit list