Driver (sidekick-base.Sidekick

module Asolver = Sidekick_abstract_solver.Asolver

val th_bool_dyn : Sidekick_base.Solver.theory

val th_bool_static : Sidekick_base.Solver.theory

val th_bool : Sidekick_base.Config.t -> Sidekick_base.Solver.theory

val th_data : Sidekick_base.Solver.theory

val th_lra : Sidekick_base.Solver.theory

val th_ty_unin : Sidekick_base.Solver.theory

type 'a or_error = ('a, string) CCResult.t

type t

The SMTLIB driver

val create : 
  ?pp_cnf:bool ->
  ?proof_file:string ->
  ?pp_model:bool ->
  ?check:bool ->
  ?time:float ->
  ?memory:float ->
  ?progress:bool ->
  Asolver.t ->
  t

val process_stmt : t -> Sidekick_base.Statement.t -> unit or_error