Previous  Up  Next

Module Smt_sig.S.Formula

module Formula: sig .. end
type comparator =
| Eq (*

equality (=)

*)
| Neq (*

disequality (<>)

*)
| Le (*

inequality (<=)

*)
| Lt (*

strict inequality (<)

*)

The type of comparators:

type combinator =
| And (*

conjunction

*)
| Or (*

disjunction

*)
| Imp (*

implication

*)
| Not (*

negation

*)

The type of operators

type literal

The type of literals

type t

The type of ground formulas

val f_true : t

The formula which represents true

val f_false : t

The formula which represents false

val make_lit : comparator -> Smt_sig.S.Term.t list -> t

make_lit cmp [t1; t2] creates the literal (t1 <cmp> t2).

val make : combinator ->
       t list -> t

make cmb [f_1; ...; f_n] creates the formula (f_1 <cmb> ... <cmb> f_n).

val make_cnf : t -> literal list list

make_cnf f returns a conjunctive normal form of f under the form: a list (which is a conjunction) of lists (which are disjunctions) of literals.

val print : Format.formatter -> t -> unit

print fmt f prints the formula on the formatter fmt.