P (dolmen_loop.Dolmen_loop.Export.Smtlib2.P)

val add_named : Env.t -> Env.term_cst -> Env.term -> Env.t

val set_split_dec : 
  Env.t ->
  (string -> ([ `Neg | `Pos ] * string * string) option) ->
  Env.t

val match_prop_literal : 
  Env.term ->
  [ `Cst of Env.term_cst | `Neg of Env.term_cst | `Not_a_prop_literal ]

val ty : Env.t -> Stdlib.Format.formatter -> Env.ty -> unit

val term : Env.t -> Stdlib.Format.formatter -> Env.term -> unit

val echo : Env.t -> Stdlib.Format.formatter -> string -> unit

val set_logic : Env.t -> Stdlib.Format.formatter -> string -> unit

val set_info : Env.t -> Stdlib.Format.formatter -> Sexpr.t -> unit

val set_option : Env.t -> Stdlib.Format.formatter -> Sexpr.t -> unit

val get_info : Env.t -> Stdlib.Format.formatter -> Sexpr.t -> unit

val get_option : Env.t -> Stdlib.Format.formatter -> Sexpr.t -> unit

val get_value : Env.t -> Stdlib.Format.formatter -> Env.term list -> unit

val pop : Env.t -> Stdlib.Format.formatter -> int -> unit

val push : Env.t -> Stdlib.Format.formatter -> int -> unit

val declare_sort : Env.t -> Stdlib.Format.formatter -> Env.ty_cst -> unit

val declare_datatype : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.ty_cst
   * Env.ty_var list
   * (Env.term_cst * (Env.ty * Env.term_cst) list) list) ->
  unit

val declare_datatypes : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.ty_cst
   * Env.ty_var list
   * (Env.term_cst * (Env.ty * Env.term_cst) list) list)
    list ->
  unit

val declare_fun : Env.t -> Stdlib.Format.formatter -> Env.term_cst -> unit

val define_sort : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.ty_cst * Env.ty_var list * Env.ty) ->
  unit

val define_fun : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.term_cst * Env.ty_var list * Env.term_var list * Env.term) ->
  unit

val define_fun_rec : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.term_cst * Env.ty_var list * Env.term_var list * Env.term) ->
  unit

val define_funs_rec : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.term_cst * Env.ty_var list * Env.term_var list * Env.term) list ->
  unit

val assert_ : Env.t -> Stdlib.Format.formatter -> Env.term -> unit

val check_sat : Env.t -> Stdlib.Format.formatter -> unit -> unit

val check_sat_assuming : 
  Env.t ->
  Stdlib.Format.formatter ->
  Env.term list ->
  unit

val reset : Env.t -> Stdlib.Format.formatter -> unit -> unit

val reset_assertions : Env.t -> Stdlib.Format.formatter -> unit -> unit

val get_unsat_core : Env.t -> Stdlib.Format.formatter -> unit -> unit

val get_unsat_assumptions : Env.t -> Stdlib.Format.formatter -> unit -> unit

val get_proof : Env.t -> Stdlib.Format.formatter -> unit -> unit

val get_model : Env.t -> Stdlib.Format.formatter -> unit -> unit

val get_assertions : Env.t -> Stdlib.Format.formatter -> unit -> unit

val get_assignment : Env.t -> Stdlib.Format.formatter -> unit -> unit

val exit : Env.t -> Stdlib.Format.formatter -> unit -> unit