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:Proof.t list -> 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 -> Proof.t list
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.FOTerm.t Sequence.t -> Logtk.ID.Set.t
set of AC symbols occurring in the given term
val proofs : unit -> Proof.t list
All proofs for all AC axioms
val exists_ac : unit -> bool
Is there any AC symbol?
val axioms : Logtk.ID.t -> Logtk.Type.t -> C.t list
List of (persistent) axioms that are needed for simplifications to
be complete for the given symbol. The ctx is required for type inference
and building clauses .
val scan_statement : ('a, Logtk.FOTerm.t, Logtk.Type.t) Logtk.Statement.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