module type S = sig .. end
module Env: Env.S
module C: module type of Env.C
val on_add : AC_intf.spec Logtk.Signal.t
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 Sequence.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
Rules
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