Module Formula_intf

module Formula_intf: sig .. end

SMT formulas

This module defines the required implementation of formulas for an SMT solver.

type negated =

`\|`	`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