S (alt-ergo-lib.AltErgoLib.Frontend.S)

type sat_env

type used_context

type status =

| Unsat of Commands.sat_tdecl * Explanation.t

| Inconsistent of Commands.sat_tdecl

| Sat of Commands.sat_tdecl * sat_env

| Unknown of Commands.sat_tdecl * sat_env

| Timeout of Commands.sat_tdecl option

| Preprocess

val process_decl : 
  ( status -> int64 -> unit ) ->
  used_context ->
  (sat_env * bool * Explanation.t) ->
  Commands.sat_tdecl ->
  sat_env * bool * Explanation.t

val print_status : status -> int64 -> unit

val init_all_used_context : unit -> used_context

val choose_used_context : used_context -> goal_name:string -> used_context