Module type Formula_intf.S

module type S = sig .. end

SMT formulas

type t

The type of atomic formulas.

type proof

An abstract type for proofs

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

Formula constant. A valid formula should never be physically equal to dummy

val neg : t -> t

Formula negation. Should be an involution, i.e. equal a (neg neg a) should always hold.

val norm : t -> t * Formula_intf.negated

Returns a 'normalized' form of the formula, possibly negated (in which case return Negated). This function is used to recognize the link between a formula a and its negation neg a, so the goal is that a and neg a normalise to the same formula, but one returns Same_sign and the other one returns Negated