Module `AC.Make`

Parameters

Env : Env.S

Signature

module Env = Env

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