package libzipperposition

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

Simple Clause

type flag
type t = private {
  1. id : int;
    (*

    unique ID of the clause

    *)
  2. lits : Logtk.Literal.t array;
    (*

    the literals

    *)
  3. trail : Trail.t;
    (*

    boolean trail

    *)
  4. mutable flags : flag;
    (*

    boolean flags for the clause

    *)
}

Basics

val make : trail:Trail.t -> Logtk.Literal.t array -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val id : t -> int
val lits : t -> Logtk.Literal.t array
val trail : t -> Trail.t
val is_empty : t -> bool
val length : t -> int
val update_trail : (Trail.t -> Trail.t) -> t -> t
val to_s_form : ?allow_free_db:bool -> ?ctx:Logtk.Term.Conv.ctx -> t -> Logtk.TypedSTerm.Form.t

Flags

val flag_initial : flag

clause comes from the input

val flag_lemma : flag

clause is a lemma

val flag_persistent : flag

clause cannot be redundant

val flag_redundant : flag

clause has been shown to be redundant

val flag_backward_simplified : flag

clause has been backward simplified

val flag_poly_arg_cong_res : flag

clause is the result of polymorphic ArgCong

val set_flag : flag -> t -> bool -> unit

set boolean flag

val get_flag : flag -> t -> bool

get value of boolean flag

val new_flag : unit -> flag

new flag that can be used on clauses

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

IO

val pp_vars : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp_tstp : t CCFormat.printer
val pp_tstp_full : t CCFormat.printer

Print in a toplevel TPTP statement

val pp_trail : Trail.t CCFormat.printer
val pp_trail_tstp : Trail.t CCFormat.printer

Proofs

val proof_tc : t -> t Logtk.Proof.Result.tc
val mk_proof_res : t -> Logtk.Proof.Result.t
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