Module Certificate

module Certificate: sig .. end
Certificates for Kind 2. This contains the base type as well as some combinators for certificates.
Author(s): Alain Mebsout

type t = int * Term.t 
The type of certificates
type symbols = {
   phi : string; (*
Name of function symbol for k-inductive invariant
*)
   init : string; (*
Name of function symbol for init
*)
   prop : string; (*
Name of function symbol for property
*)
   trans : string; (*
Name of function symbol for transition relation
*)
}
type out = {
   k : int; (*
k of certificate
*)
   names : symbols; (*
names for I, T, P and PHI
*)
   dirname : string; (*
Directory where certificates and proofs are produced
*)
   proofname : string; (*
Name for the final LFSC proof
*)
   base : string; (*
File name for base case check
*)
   induction : string; (*
File name for inductive case check
*)
   implication : string; (*
File name for implication of property check
*)
   dummy_trace : string; (*
File name for dummy file to trace function definitions in LFSC
*)
}
The type of certificates outputs, these are file names for the intermediate SMT-LIB 2 certificates
type system = {
   names : symbols;
   smt2_file : string;
   smt2_lfsc_trace_file : string;
}
type invariant = {
   k : int;
   name : string;
   dirname : string;
   phi_file : string;
   phi_lfsc_trace_file : string;
   base : string; (*
File name for base case check
*)
   induction : string; (*
File name for inductive case check
*)
   implication : string; (*
File name for implication of property check
*)
   for_system : system;
   kind2_system : system;
   jkind_system : system;
   obs_system : system;
}
val merge : t list -> t
Merge certificates into one. The resulting certificate is a certificate for the conjunction of the original invariants.
val split : t -> t list
Split a certificate following the boolean strucutre of its inductive invariant
val split_certs : t list -> t list
Split a list of certificates
val size : t -> int
Gives a measure to compare the size of the inductive invariants contained in a certificate.