package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

(* 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

  (** {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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct