module Make:
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