package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

Signature

module Env = E
module C : sig ... end
module PS : sig ... end

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_=a+1....c-1 (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 instance 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct