package libzipperposition

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

Module Libzipperposition.SClauseSource

Simple Clause

Sourcetype flag
Sourcetype 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

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

Flags

Sourceval flag_lemma : flag

clause is a lemma

Sourceval flag_persistent : flag

clause cannot be redundant

Sourceval flag_redundant : flag

clause has been shown to be redundant

Sourceval flag_backward_simplified : flag

clause has been backward simplified

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

set boolean flag

Sourceval get_flag : flag -> t -> bool

get value of boolean flag

Sourceval new_flag : unit -> flag

new flag that can be used on clauses

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

IO

Sourceval pp_tstp_full : t CCFormat.printer

Print in a toplevel TPTP statement

Sourceval pp_trail_tstp : Trail.t CCFormat.printer

Proofs

Sourceval mk_proof_res : t -> Logtk.Proof.Result.t