module Formula_intf:sig..end
SMT formulas
This module defines the required implementation of formulas for an SMT solver.
type
| |
Negated |
(* | changed sign | *) |
| |
Same_sign |
(* | kept sign | *) |
This type is used during the normalisation of formulas.
See Expr_intf.S.norm for more details.
module type S =sig..end