package libzipperposition

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

Source file clause_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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
(* This file is free software, part of Zipperposition. See file "license" for more details. *)

open Logtk

type proof_step = Proof.Step.t
type proof = Proof.S.t

module type S = sig
  module Ctx : Ctx.S

  type t
  type clause = t

  (** {2 Flags} *)

  type flag = SClause.flag

  val set_flag : flag -> t -> bool -> unit (** set boolean flag *)

  val get_flag : flag -> t -> bool (** get value of boolean flag *)

  val mark_redundant : t -> unit
  val is_redundant : t -> bool
  val mark_backward_simplified : t -> unit
  val is_backward_simplified : t -> bool

  (** {2 Basics} *)

  include Interfaces.EQ with type t := t
  include Interfaces.HASH with type t := t
  val compare : t -> t -> int

  val id : t -> int
  val lits : t -> Literal.t array

  val is_ground : t -> bool
  val weight : t -> int

  module Tbl : CCHashtbl.S with type key = t

  val is_goal : t -> bool
  (** Looking at the clause's proof, return [true] iff the clause is an
      initial (negated) goal from the problem *)

  val distance_to_goal : t -> int option
  (** See {!Proof.distance_to_goal}, applied to the clause's proof *)

  val comes_from_goal : t -> bool
  (** [true] iff the clause is (indirectly) deduced from a goal or lemma *)

  (** {2 Boolean Abstraction} *)

  val pp_trail : Trail.t CCFormat.printer
  (** Printer for boolean trails, that uses {!Ctx} to display boxes *)

  val has_trail : t -> bool
  (** Has a non-empty trail? *)

  val trail : t -> Trail.t
  (** Get the clause's trail *)

  val trail_l : t list -> Trail.t
  (** Merge the trails of several clauses *)

  val update_trail : (Trail.t -> Trail.t) -> t -> t
  (** Change the trail. The resulting clause has same parents, proof
      and literals as the input one *)

  val trail_subsumes : t -> t -> bool
  (** [trail_subsumes c1 c2 = Trail.subsumes (get_trail c1) (get_trail c2)] *)

  val is_active : t -> v:Trail.valuation -> bool
  (** True if the clause's trail is active in this valuation *)

  val is_inj_axiom : t -> (ID.t * int) option
  (** Returns Some (sym,i) if clause is injectivity axiom for ith argument
      of symbol sym. *)

  (** {2 Constructors} *)

  val create :
    penalty:int ->
    trail:Trail.t ->
    Literal.t list ->
    proof_step ->
    t
  (** Build a new clause from the given literals.
      @param trail boolean trail
      @param penalty heuristic penalty due to history of the clause
        (the higher, the less likely the clause is to be picked soon)
      also takes a list of literals and a proof builder *)

  val create_a :
    penalty:int ->
    trail:Trail.t ->
    Literal.t array ->
    proof_step ->
    t
  (** Build a new clause from the given literals. *)

  val of_sclause :
    ?penalty:int ->
    SClause.t ->
    proof_step ->
    t

  val of_forms :
    ?penalty:int ->
    trail:Trail.t ->
    Term.t SLiteral.t list ->
    proof_step ->
    t
  (** Directly from list of formulas *)

  val of_forms_axiom :
    ?penalty:int ->
    file:string -> name:string ->
    Term.t SLiteral.t list -> t
  (** Construction from formulas as axiom (initial clause) *)

  val of_statement : ?convert_defs:bool -> Statement.clause_t -> t list
  (** Extract a clause from a statement, if any *)

  val proof_step : t -> proof_step
  (** Extract its proof from the clause *)

  val proof : t -> proof
  (** Obtain the pair [conclusion, step] *)

  val proof_parent : t -> Proof.Parent.t

  val proof_parent_subst : Subst.Renaming.t -> t Scoped.t -> Subst.t -> Proof.Parent.t

  val update_proof : t -> (proof_step -> proof_step) -> t
  (** [update_proof c f] creates a new clause that is
      similar to [c] in all aspects, but with
      the proof [f (proof_step c)] *)

  val proof_depth : t -> int

  val is_empty : t -> bool
  (** Is the clause an empty clause? *)

  val length : t -> int
  (** Number of literals *)

  val maxlits : t Scoped.t -> Subst.t -> CCBV.t
  (** List of maximal literals *)

  val is_maxlit : t Scoped.t -> Subst.t -> idx:int -> bool
  (** Is the i-th literal maximal in subst(clause)? Equivalent to
      Bitvector.get (maxlits ~ord c subst) i *)

  val eligible_res : t Scoped.t -> Subst.t -> CCBV.t
  (** Bitvector that indicates which of the literals of [subst(clause)]
      are eligible for resolution. THe literal has to be either maximal
      among selected literals of the same sign, if some literal is selected,
      or maximal if none is selected. *)

  val eligible_res_no_subst : t -> CCBV.t
  (** More efficient version of {!eligible_res} with [Subst.empty] *)

  val eligible_param : t Scoped.t -> Subst.t -> CCBV.t
  (** Bitvector that indicates which of the literals of [subst(clause)]
      are eligible for paramodulation. That means the literal
      is positive, no literal is selecteed, and the literal
      is maximal among literals of [subst(clause)]. *)

  val is_eligible_param : t Scoped.t -> Subst.t -> idx:int -> bool
  (** Check whether the [idx]-th literal is eligible for paramodulation *)

  val has_selected_lits : t -> bool
  (** does the clause have some selected literals? *)

  val is_selected : t -> int -> bool
  (** check whether a literal is selected *)

  val selected_lits : t -> (Literal.t * int) list
  (** get the list of selected literals *)

  val penalty : t -> int

  val is_unit_clause : t -> bool
  (** is the clause a unit clause? *)

  val is_oriented_rule : t -> bool
  (** Is the clause a positive oriented clause? *)

  val symbols : ?init:ID.Set.t -> ?include_types:bool -> t Iter.t -> ID.Set.t
  (** symbols that occur in the clause *)

  val to_sclause : t -> SClause.t

  val to_forms : t -> Term.t SLiteral.t list
  (** Easy iteration on an abstract view of literals *)

  val to_s_form : t -> TypedSTerm.Form.t

  val ground_clause : t -> t

  val eta_reduce : t -> t option

  (** {2 Iterators} *)

  module Seq : sig
    val lits : t -> Literal.t Iter.t
    val terms : t -> Term.t Iter.t
    val vars : t -> Type.t HVar.t Iter.t
  end

  val apply_subst : ?proof:Proof.Step.t option -> t Scoped.t -> Subst.FO.t -> t

  (** {2 Filter literals} *)

  module Eligible : sig
    type t = int -> Literal.t -> bool
    (** Eligibility criterion for a literal *)

    val res : clause -> t
    (** Only literals that are eligible for resolution *)

    val param : clause -> t
    (** Only literals that are eligible for paramodulation *)

    val eq : t
    (** Equations *)

    val arith : t

    val filter : (Literal.t -> bool) -> t

    val max : clause -> t
    (** Maximal literals of the clause *)

    val pos : t
    (** Only positive literals *)

    val pos_eq : t
    (** Only positive equational literals *)

    val neg : t
    (** Only negative literals *)

    val always : t
    (** All literals *)

    val combine : t list -> t
    (** Logical "and" of the given eligibility criteria. A literal is
        eligible only if all elements of the list say so. *)

    val ( ** ) : t -> t -> t
    (** Logical "and" *)

    val ( ++ ) : t -> t -> t
    (** Logical "or" *)

    val ( ~~ ) : t -> t
    (** Logical "not" *)
  end

  (** {2 Set of clauses} *)

  (** Simple set *)
  module ClauseSet : CCSet.S with type elt = t

  (** {2 Position} *)

  module Pos : sig
    val at : t -> Position.t -> Term.t
  end

  (** {2 Clauses with more data} *)

  (** Clause within which a subterm (and its position) are highlighted *)
  module WithPos : sig
    type t = {
      clause : clause;
      pos : Position.t;
      term : Term.t;
    }

    val compare : t -> t -> int
    val pp : t CCFormat.printer
  end

  (** {2 IO} *)

  val pp : t CCFormat.printer
  val pp_tstp : t CCFormat.printer
  val pp_tstp_full : t CCFormat.printer  (** Print in a cnf() statement *)

  val to_string : t -> string (** Debug printing to a  string *)

  val pp_set : ClauseSet.t CCFormat.printer
  val pp_set_tstp : ClauseSet.t CCFormat.printer

  (**/**)
  val check_types : t -> unit
  (**/**)
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