Module Certificate

Certificates for Kind 2. This contains the base type as well as some combinators for certificates.

type t = int * Term.t

The type of certificates

type symbols = {
  1. vars : UfSymbol.t list;
    (*

    Names of state variables for the system

    *)
  2. phi : string;
    (*

    Name of function symbol for k-inductive invariant

    *)
  3. init : string;
    (*

    Name of function symbol for init

    *)
  4. prop : string;
    (*

    Name of function symbol for property

    *)
  5. trans : string;
    (*

    Name of function symbol for transition relation

    *)
}
type out = {
  1. k : int;
    (*

    k of certificate

    *)
  2. names : symbols;
    (*

    names for I, T, P and PHI

    *)
  3. dirname : string;
    (*

    Directory where certificates and proofs are produced

    *)
  4. proofname : string;
    (*

    Name for the final CPC proof

    *)
  5. base : string;
    (*

    File name for base case check

    *)
  6. induction : string;
    (*

    File name for inductive case check

    *)
  7. implication : string;
    (*

    File name for implication of property check

    *)
}

The type of certificates outputs, these are file names for the intermediate SMT-LIB 2 certificates

type system = {
  1. names : symbols;
  2. smt2_file : string;
}
type invariant = {
  1. k : int;
  2. name : string;
  3. dirname : string;
  4. phi_file : string;
  5. base : string;
    (*

    File name for base case check

    *)
  6. induction : string;
    (*

    File name for inductive case check

    *)
  7. implication : string;
    (*

    File name for implication of property check

    *)
  8. for_system : system;
  9. kind2_system : system;
  10. jkind_system : system;
  11. 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.