package why3find

  1. Overview
  2. Docs

Module Why3find.CrcSource

Sourcetype status = private
  1. | Stuck
  2. | Prover of Prover.desc * float
  3. | Tactic of {
    1. id : string;
    2. children : crc list;
    3. stuck : int;
    4. proved : int;
    5. depth : int;
    6. time : float;
    }
Sourceand crc = private {
  1. goal : Session.goal option;
  2. status : status;
}
Sourceval none : status
Sourceval stuck : ?goal:Session.goal -> unit -> crc
Sourceval prover : ?goal:Session.goal -> Prover.desc -> float -> crc
Sourceval tactic : ?goal:Session.goal -> Tactic.tactic -> crc list -> crc
Sourceval iter : (Session.goal -> status -> unit) -> crc -> unit

Iterates over all goals in the CRC. Tactic nodes are visite first, followed by their children.

Sourcetype verdict = [
  1. | `Valid of int
  2. | `Failed of int
  3. | `Partial of int * int
]
Sourceval verdict : crc -> verdict
Sourceval verdict_all : crc list -> verdict
Sourceval nverdict : stuck:int -> proved:int -> verdict
Sourceval get_stuck : crc -> int
Sourceval get_proved : crc -> int
Sourceval get_time : crc -> float
Sourceval get_depth : crc -> int
Sourceval size : crc -> int
Sourceval get_stuck_all : crc list -> int
Sourceval get_proved_all : crc list -> int
Sourceval get_time_all : crc list -> float
Sourceval get_depth_all : crc list -> int
Sourceval is_stuck : crc -> bool
Sourceval is_unknown : crc -> bool
Sourceval is_complete : crc -> bool
Sourceval pretty : Format.formatter -> crc -> unit
Sourceval pp_status : Format.formatter -> status -> unit
Sourceval pp_result : Format.formatter -> stuck:int -> proved:int -> unit
Sourceval dump : Format.formatter -> crc -> unit
Sourceval merge : crc -> crc -> crc
Sourceval of_json : Why3findUtils.Json.t -> crc
Sourceval to_json : crc -> Why3findUtils.Json.t