Module `Logtk_parsers.Trace_tstp`Source

Trace of a TSTP prover

Sourcetype id = Ast_tptp.name

Sourcetype term = Logtk.STerm.t

Sourcetype form = Logtk.STerm.t

Sourcetype clause = term Logtk.SLiteral.t list

Sourcetype t =

| Axiom of string * string
| Theory of string
| InferForm of form * step lazy_t
| InferClause of clause * step lazy_t

Sourceand step = {

id : id;
rule : string;
parents : t array;
esa : bool;
(*
Equisatisfiable step?
*)

}

Sourceval equal : t -> t -> bool

Sourceval compare : t -> t -> int

Sourceval mk_f_axiom : id:id -> form -> file:string -> name:string -> t

Sourceval mk_c_axiom : id:id -> clause -> file:string -> name:string -> t

Sourceval mk_f_step : ?esa:bool -> id:id -> form -> rule:string -> t list -> t

Sourceval mk_c_step : ?esa:bool -> id:id -> clause -> rule:string -> t list -> t

Sourceval is_axiom : t -> bool

Sourceval is_theory : t -> bool

Sourceval is_step : t -> bool

Sourceval is_proof_of_false : t -> bool

Sourceval get_id : t -> id

Obtain the ID of the proof step.

raises Invalid_argument
if the step is Axiom or Theory

Sourceval force : t -> unit

Force the lazy proof step, if any

Proof traversal

Sourcemodule StepTbl : Hashtbl.S with type key = t

Sourcetype proof_set = unit StepTbl.t

Sourceval is_dag : t -> bool

Is the proof a proper DAG?

Sourceval traverse : ?traversed:proof_set -> t -> (t -> unit) -> unit

Traverse the proof. Each proof node is traversed only once, using the set to recognize already traversed proofs.

Sourceval to_seq : t -> t Iter.t

Traversal of parent proofs

Sourceval depth : t -> int

Max depth of the proof

Sourceval size : t -> int

Number of nodes in the proof

IO

Sourcetype 'a or_error = ('a, string) CCResult.t

Sourceval of_decls : form Ast_tptp.t Iter.t -> t or_error

Try to extract a proof from a list of TSTP statements.

Sourceval parse : ?recursive:bool -> string -> t or_error

Try to parse a proof from a file.

Debug printing, non recursive

include Logtk.Interfaces.PRINT with type t := t

Sourceval pp : t CCFormat.printer

Sourceval to_string : t -> string

Sourceval pp1 : t CCFormat.printer

Print proof step, and its parents

Sourceval pp_tstp : t CCFormat.printer

print the whole proofs

Install

Dune Dependency

Authors

Maintainers

Sources

doc/logtk.parsers/Logtk_parsers/Trace_tstp/index.html

Module `Logtk_parsers.Trace_tstp`Source

Trace of a TSTP prover

Proof traversal

IO

package logtk

Install

Dune Dependency

Authors

Maintainers

Sources

doc/logtk.parsers/Logtk_parsers/Trace_tstp/index.html

Module Logtk_parsers.Trace_tstpSource

Trace of a TSTP prover

Proof traversal

IO

Module `Logtk_parsers.Trace_tstp`Source