Previous  Up  Next

Module ProofStep

module ProofStep: sig .. end

Manipulate proofs


module Loc: Libzipperposition.ParseLocation
type form = Libzipperposition.TypedSTerm.t 
type bool_lit = BBox.Lit.t 
type 'a sequence = ('a -> unit) -> unit 
val section : Libzipperposition.Util.Section.t
type rule_info =
| I_subst of Libzipperposition.Substs.t
| I_pos of Libzipperposition.Position.t
| I_comment of string 
type rule = {
   rule_name : string;
   rule_info : rule_info list;
} 
val mk_rule : ?subst:Libzipperposition.Substs.t list ->
       ?pos:Libzipperposition.Position.t list ->
       ?comment:string list -> string -> rule
type kind =
| Inference of rule
| Simplification of rule
| Esa of rule
| Assert of Libzipperposition.StatementSrc.t
| Goal of Libzipperposition.StatementSrc.t
| Data of Libzipperposition.StatementSrc.t
* Libzipperposition.Type.t Libzipperposition.Statement.data
| Trivial (*
trivial, or trivial within theories
*)
Classification of proof steps
type result =
| Form of form
| Clause of SClause.t
| BoolClause of bool_lit list 
type t = private {
   id : int;
   kind : kind;
   dist_to_goal : int option;
   parents : of_ list;
}
A proof step, without the conclusion
type of_ = {
   step : t;
   result : result;
}
Proof Step with its conclusion
type proof = of_ 
val result : of_ -> result
val step : of_ -> t
val kind : t -> kind
val parents : t -> of_ list
val compare : t -> t -> int
val hash : t -> int
val equal : t -> t -> bool
val compare_proof : of_ -> of_ -> int
val equal_proof : of_ -> of_ -> bool
val hash_proof : of_ -> int
module PTbl: CCHashtbl.S  with type key = of_

Constructors and utils

In all the following constructors, theories defaults to the empty list. Axiom constructors have default role "axiom"
val mk_trivial : t
val mk_data : Libzipperposition.StatementSrc.t ->
       Libzipperposition.Type.t Libzipperposition.Statement.data -> t
val mk_assert : Libzipperposition.StatementSrc.t -> t
val mk_goal : Libzipperposition.StatementSrc.t -> t
val mk_assert' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
val mk_goal' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
val mk_inference : rule:rule -> of_ list -> t
val mk_simp : rule:rule -> of_ list -> t
val mk_esa : rule:rule -> of_ list -> t
val mk_f_trivial : form -> of_
val mk_f_inference : rule:rule -> form -> of_ list -> of_
val mk_f_simp : rule:rule -> form -> of_ list -> of_
val mk_f_esa : rule:rule -> form -> of_ list -> of_
val mk_c : t -> SClause.t -> of_
val mk_bc : t -> bool_lit list -> of_
val adapt_f : of_ -> form -> of_
val adapt_c : of_ -> SClause.t -> of_
val is_trivial : t -> bool
val is_assert : t -> bool
Proof: the statement was asserted in some file
val is_goal : t -> bool
The statement comes from the negation of a goal in some file
val rule : t -> rule option
Rule name for Esa/Simplification/Inference steps
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val compare_by_result : of_ -> of_ -> int
Compare proofs by their result

Proof traversal


val distance_to_goal : t -> int option
distance_to_conjecture p returns None if p has no ancestor that is a conjecture (including p itself). It returns Some d if d is the distance, in the proof graph, to the closest conjecture ancestor of p

IO


val pp_rule : info:bool -> rule CCFormat.printer
val pp_src : Libzipperposition.StatementSrc.t CCFormat.printer
val pp_src_tstp : Libzipperposition.StatementSrc.t CCFormat.printer
val pp_kind : kind CCFormat.printer
val pp_kind_tstp : kind CCFormat.printer