package alt-ergo-lib

  1. Overview
  2. Docs

Parameters

Signature

type sat_env = SAT.t
type used_context
type res = [
  1. | `Sat of sat_env
  2. | `Unknown of sat_env
  3. | `Unsat
]
type status =
  1. | Unsat of Commands.sat_tdecl * Explanation.t
  2. | Inconsistent of Commands.sat_tdecl
  3. | Sat of Commands.sat_tdecl * sat_env
  4. | Unknown of Commands.sat_tdecl * sat_env
  5. | Timeout of Commands.sat_tdecl option
  6. | Preprocess
val process_decl : (status -> int -> unit) -> used_context -> (res * Explanation.t) Stdlib.Stack.t -> (sat_env * res * Explanation.t) -> Commands.sat_tdecl -> sat_env * res * Explanation.t
val print_status : status -> int -> unit
val init_all_used_context : unit -> used_context
val choose_used_context : used_context -> goal_name:string -> used_context
OCaml

Innovation. Community. Security.