Library for Zipperposition


module Env : Env.S


module Env = Env
module C : sig ... end
val add : proof:Logtk.Proof.parent -> Logtk.ID.t -> Logtk.Type.t -> unit

Declare that the given symbol is AC, and update the Env subsequently by adding clauses, etc.

val is_ac : Logtk.ID.t -> bool
val find_proof : Logtk.ID.t -> Logtk.Proof.parent

Recover the proof for the AC-property of this symbol.

  • raises Not_found

    if the symbol is not AC

val symbols : unit -> Logtk.ID.Set.t

set of AC symbols

val symbols_of_terms : Logtk.Term.t Iter.t -> Logtk.ID.Set.t

set of AC symbols occurring in the given term

val exists_ac : unit -> bool

Is there any AC symbol?

val scan_statement : Logtk.Statement.clause_t -> unit

Check whether the statement contains an "AC" attribute, do the proper declaration in this case


val is_trivial_lit : Logtk.Literal.t -> bool

Is the literal AC-trivial?

val is_trivial : C.t -> bool

Check whether the clause is AC-trivial

val simplify : Env.simplify_rule

Simplify the clause modulo AC

val setup : unit -> unit

Register on Env