Module type Arith_int.S

module type S = sig .. end

module Env: Env.S

module C: module type of Env.C

module PS: module type of Env.ProofState

Equations and Inequations

val canc_sup_active : Env.binary_inf_rule

cancellative superposition where given clause is active

val canc_sup_passive : Env.binary_inf_rule

cancellative superposition where given clause is passive

val cancellation : Env.unary_inf_rule

cancellation (unifies some terms on both sides of a comparison operator)

val canc_equality_factoring : Env.unary_inf_rule

cancellative equality factoring

val canc_ineq_chaining : Env.binary_inf_rule

cancellative inequality chaining.

Also does case switch if conditions are present: C1 or a < b C2 or b < c ------------------------------------- C1 or C2 or or_ (b = i) if a and c are integer linear expressions whose difference is a constant. If a > c, then the range a...c is empty and the literal is just removed.

val canc_ineq_factoring : Env.unary_inf_rule

Factoring between two inequation literals

val canc_less_to_lesseq : Env.lit_rewrite_rule

Simplification: a < b ----> a+1 ≤ b

Divisibility

val canc_div_chaining : Env.binary_inf_rule

Chain together two divisibility literals, assuming they share the same prime

val canc_div_case_switch : Env.unary_inf_rule

Eliminate negative divisibility literals within a power-of-prime quotient of Z: not (d^i | m) ----->

val canc_div_prime_decomposition : Env.multi_simpl_rule

Eliminate divisibility literals with a non-power-of-prime quotient of Z (for instance 6 | a ---> { 2 | a, 3 | a })

val canc_divisibility : Env.unary_inf_rule

Infer divisibility constraints from integer equations, for instace C or 2a=b ----> C or 2 | b if a is maximal

Other

val is_tautology : C.t -> bool

is the clause a tautology w.r.t linear expressions?

val eliminate_unshielded : Env.multi_simpl_rule

Eliminate unshielded variables using an adaptation of Cooper's algorithm

Contributions to Env

val register : unit -> unit