module Formula: sig .. end
McSat formulas
type
The type of atomic formulas over terms.
val equal : t -> t -> bool
Equality over formulas.
val hash : t -> int
Hashing function for formulas. Should be such that two formulas equal according
to Expr_intf.S.equal have the same hash.
val print : Format.formatter -> t -> unit
Printing function used among other thing for debugging.
val dummy : t
Constant formula. A valid formula should never be physically equal to dummy
val neg : t -> t
Formula negation
val norm : t -> t * Expr_intf.negated
Returns a 'normalized' form of the formula, possibly negated
(in which case return Negated).
norm must be so that a and neg a normalise to the same formula,
but one returns Negated and the other Same_sign.