package alt-ergo-lib

  1. Overview
  2. Docs

Module Frontend.Make

Parameters

Signature

type sat_env = SAT.t
type used_context
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 -> (bool * Explanation.t) Stack.t -> (sat_env * bool * Explanation.t) -> Commands.sat_tdecl -> sat_env * bool * 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