Source file `AC_intf.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

open Logtk

type spec = {
  sym : ID.t;
  ty : Type.t;
}

module type S = sig
  module Env : Env.S
  module C : module type of Env.C

  val on_add : spec Signal.t

  val add : proof:Proof.parent -> ID.t -> Type.t -> unit
  (** Declare that the given symbol is AC, and update the Env subsequently
      by adding clauses, etc. *)

  val is_ac : ID.t -> bool

  val find_proof : ID.t -> Proof.parent
  (** Recover the proof for the AC-property of this symbol.
      @raise Not_found if the symbol is not AC *)

  val symbols : unit -> ID.Set.t
  (** set of AC symbols *)

  val symbols_of_terms : Term.t Iter.t -> 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 : Statement.clause_t -> unit
  (** Check whether the statement contains an "AC" attribute, do the proper
      declaration in this case *)

  (** {2 Rules} *)

  val is_trivial_lit : 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 *)
end