Previous  Up  Next

Module Trace_tstp

module Trace_tstp: sig .. end

Trace of a TSTP prover


type id = Ast_tptp.name 
type term = Libzipperposition.STerm.t 
type form = Libzipperposition.STerm.t 
type clause = term Libzipperposition.SLiteral.t list 
type t =
| Axiom of string * string
| Theory of string
| InferForm of form * step lazy_t
| InferClause of clause * step lazy_t 
type step = {
   id : id;
   rule : string;
   parents : t array;
   esa : bool; (*
Equisatisfiable step?
*)
} 
val equal : t -> t -> bool
val compare : t -> t -> int
val mk_f_axiom : id:id ->
       form -> file:string -> name:string -> t
val mk_c_axiom : id:id ->
       clause -> file:string -> name:string -> t
val mk_f_step : ?esa:bool ->
       id:id ->
       form -> rule:string -> t list -> t
val mk_c_step : ?esa:bool ->
       id:id ->
       clause -> rule:string -> t list -> t
val is_axiom : t -> bool
val is_theory : t -> bool
val is_step : t -> bool
val is_proof_of_false : t -> bool
val get_id : t -> id
Obtain the ID of the proof step.
Raises Invalid_argument if the step is Axiom or Theory
val force : t -> unit
Force the lazy proof step, if any

Proof traversal


module StepTbl: Hashtbl.S  with type key = t
type proof_set = unit StepTbl.t 
val is_dag : t -> bool
Is the proof a proper DAG?
val 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.
val to_seq : t -> t Sequence.t
Traversal of parent proofs
val depth : t -> int
Max depth of the proof
val size : t -> int
Number of nodes in the proof

IO


type 'a or_error = [ `Error of string | `Ok of 'a ] 
val of_decls : form Ast_tptp.t Sequence.t -> t or_error
Try to extract a proof from a list of TSTP statements.
val parse : ?recursive:bool -> string -> t or_error
Try to parse a proof from a file.
include Interfaces.PRINT

Debug printing, non recursive
val pp1 : t CCFormat.printer
Print proof step, and its parents
val pp_tstp : t CCFormat.printer
print the whole proofs