Source file superposition_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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93

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

open Logtk
open Libzipperposition

module type S = sig
  module Env : Env.S
  module C : module type of Env.C with type t = Env.C.t
  module PS : module type of Env.ProofState with type C.t = Env.C.t
  module Stm : Stream.S with module C = Env.C
  module StmQ : StreamQueue.S with module Stm = Stm

  (** {5 Term Indices} *)

  val idx_sup_into : unit -> PS.TermIndex.t
  (** index for superposition into the set *)

  val idx_sup_from : unit -> PS.TermIndex.t
  (** index for superposition from the set *)

  val idx_fv : unit -> PS.SubsumptionIndex.t
  (** index for subsumption *)

  (** {5 Inference Rules} *)

  val infer_active: Env.binary_inf_rule
  (** superposition where given clause is active *)

  val infer_passive: Env.binary_inf_rule
  (** superposition where given clause is passive *)

  val infer_equality_resolution: Env.unary_inf_rule

  val infer_equality_factoring: Env.unary_inf_rule

  (** {5 Extraction of clauses from the queue (HO feature)} *)

  val extract_from_stream_queue: Env.generate_rule
  (** Extracts at most as many clauses from the stream queue as there are
      streams in the queue. If called with [~full=true] extracts only one clause
      but may loop forever. *)

  val extract_from_stream_queue_fix_stm: Env.generate_rule
  (** Same as [extract_from_stream_queue] with a different extraction heuristic
      If possible, all clauses are taken from the first stream *)

  (** {5 Simplifications rules} *)

  val is_tautology : C.t -> bool
  (** Check whether the clause is a (syntactic) tautology, ie whether
      it contains true or "A" and "not A" *)

  val is_semantic_tautology : C.t -> bool
  (** semantic tautology deletion, using a congruence closure algorithm
      to see if negative literals imply some positive Literal.t *)

  val handle_distinct_constants : Env.lit_rewrite_rule
  (** Decide on "quoted" "symbols" (which are all distinct) *)

  val basic_simplify : Env.simplify_rule
  (** basic simplifications (remove duplicate literals, trivial literals,
      destructive equality resolution...) *)

  val subsumes : Literal.t array -> Literal.t array -> bool
  (** subsumes c1 c2 iff c1 subsumes c2 *)

  val subsumes_with :
    Literals.t Scoped.t ->
    Literals.t Scoped.t ->
    (Subst.FO.t * Proof.tag list) option
  (** returns subsuming subst if the first clause subsumes the second one *)

  val eq_subsumes : Literal.t array -> Literal.t array -> bool
  (** equality subsumption *)

  val subsumed_by_active_set : C.t -> bool
  (** check whether the clause is subsumed by any clause in the set *)

  val subsumed_in_active_set : Env.backward_redundant_rule
  (** list of clauses in the active set that are subsumed by the clause *)

  val contextual_literal_cutting : Env.simplify_rule
  (** contextual Literal.t cutting of the given clause by the active set  *)

  val condensation : Env.simplify_rule
  (** condensation *)

  (** {5 Registration} *)

  val register : unit -> unit
  (** Register rules in the environment *)
end