Previous  Up  Next

Module Smt.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 t =
| Lit of Literal.LT.t
| Comb of combinator * t list
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.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.LT.t 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.