sig
  type context
  and typ
  and expr
  and var_decl
  and model
  and assertion_id = int
  and lbool = False | Undef | True
  and var_decl_iterator
  and unsat_core = Yices.assertion_id array
  external version : unit -> string = "camlidl_yices_yices_version"
  external set_verbosity : int -> unit = "camlidl_yices_yices_set_verbosity"
  external enable_type_checker : bool -> unit
    = "camlidl_yices_yices_enable_type_checker"
  external enable_log_file : string -> unit
    = "camlidl_yices_yices_enable_log_file"
  external set_arith_only : bool -> unit
    = "camlidl_yices_yices_set_arith_only"
  external set_max_num_conflicts_in_maxsat_iteration : int -> unit
    = "camlidl_yices_yices_set_max_num_conflicts_in_maxsat_iteration"
  external set_max_num_iterations_in_maxsat : int -> unit
    = "camlidl_yices_yices_set_max_num_iterations_in_maxsat"
  external set_maxsat_initial_cost : int64 -> unit
    = "camlidl_yices_yices_set_maxsat_initial_cost"
  external mk_context : unit -> Yices.context
    = "camlidl_yices_yices_mk_context"
  external del_context : Yices.context -> unit
    = "camlidl_yices_yices_del_context"
  external reset : Yices.context -> unit = "camlidl_yices_yices_reset"
  external dump_context : Yices.context -> unit
    = "camlidl_yices_yices_dump_context"
  external push : Yices.context -> unit = "camlidl_yices_yices_push"
  external pop : Yices.context -> unit = "camlidl_yices_yices_pop"
  external assert_simple : Yices.context -> Yices.expr -> unit
    = "camlidl_yices_yices_assert"
  external assert_weighted :
    Yices.context -> Yices.expr -> int64 -> Yices.assertion_id
    = "camlidl_yices_yices_assert_weighted"
  external assert_retractable :
    Yices.context -> Yices.expr -> Yices.assertion_id
    = "camlidl_yices_yices_assert_retractable"
  external retract : Yices.context -> Yices.assertion_id -> unit
    = "camlidl_yices_yices_retract"
  external inconsistent : Yices.context -> int
    = "camlidl_yices_yices_inconsistent"
  external check : Yices.context -> Yices.lbool = "camlidl_yices_yices_check"
  external max_sat : Yices.context -> Yices.lbool
    = "camlidl_yices_yices_max_sat"
  external max_sat_cost_leq : Yices.context -> int64 -> Yices.lbool
    = "camlidl_yices_yices_max_sat_cost_leq"
  external find_weighted_model : Yices.context -> bool -> Yices.lbool
    = "camlidl_yices_yices_find_weighted_model"
  external get_unsat_core : Yices.context -> Yices.unsat_core
    = "camlidl_yices_get_unsat_core"
  external get_model : Yices.context -> Yices.model
    = "camlidl_yices_yices_get_model"
  external get_value : Yices.model -> Yices.var_decl -> Yices.lbool
    = "camlidl_yices_yices_get_value"
  external get_int_value : Yices.model -> Yices.var_decl -> int32
    = "camlidl_yices_yices_get_int_value"
  external get_arith_value : Yices.model -> Yices.var_decl -> int32 * int32
    = "camlidl_yices_yices_get_arith_value"
  external get_double_value : Yices.model -> Yices.var_decl -> float
    = "camlidl_yices_yices_get_double_value"
  external get_arith_value_as_string :
    Yices.model -> Yices.var_decl -> string
    = "camlidl_yices_yices_get_arith_value_as_string"
  val get_ratio_value : Yices.model -> Yices.var_decl -> Ratio.ratio
  val get_big_int_value : Yices.model -> Yices.var_decl -> Big_int.big_int
  external get_bitvector_value :
    Yices.model -> Yices.var_decl -> int -> bool array
    = "camlidl_yices_yices_get_bitvector_value"
  val get_bv_value : Yices.model -> Yices.var_decl -> int -> bool array
  external get_scalar_value : Yices.model -> Yices.var_decl -> int
    = "camlidl_yices_yices_get_scalar_value"
  external get_scalar_value_name : Yices.model -> Yices.var_decl -> string
    = "camlidl_yices_yices_get_scalar_value_name"
  external get_assertion_value : Yices.model -> Yices.assertion_id -> bool
    = "camlidl_yices_yices_get_assertion_value"
  external evaluate_in_model : Yices.model -> Yices.expr -> Yices.lbool
    = "camlidl_yices_yices_evaluate_in_model"
  external display_model : Yices.model -> unit
    = "camlidl_yices_yices_display_model"
  external get_cost : Yices.model -> int64 = "camlidl_yices_yices_get_cost"
  external get_cost_as_double : Yices.model -> float
    = "camlidl_yices_yices_get_cost_as_double"
  val iter_bool_var_decl : (Yices.var_decl -> unit) -> Yices.context -> unit
  external parse_expression : Yices.context -> string -> Yices.expr
    = "camlidl_yices_yices_parse_expression"
  external parse_type : Yices.context -> string -> Yices.typ
    = "camlidl_yices_yices_parse_type"
  external parse_command : Yices.context -> string -> unit
    = "camlidl_yices_yices_parse_command"
  external mk_type : Yices.context -> string -> Yices.typ
    = "camlidl_yices_yices_mk_type"
  val number_type_name : string
  val real_type_name : string
  val int_type_name : string
  val nat_type_name : string
  val bool_type_name : string
  val any_type_name : string
  external mk_bitvector_type : Yices.context -> int -> Yices.typ
    = "camlidl_yices_yices_mk_bitvector_type"
  val mk_bv_type : Yices.context -> int -> Yices.typ
  external mk_function_type :
    Yices.context -> Yices.typ array -> Yices.typ -> Yices.typ
    = "camlidl_yices_yices_mk_function_type"
  external mk_tuple_type : Yices.context -> Yices.typ array -> Yices.typ
    = "camlidl_yices_yices_mk_tuple_type"
  external mk_bool_var_decl : Yices.context -> string -> Yices.var_decl
    = "camlidl_yices_yices_mk_bool_var_decl"
  external mk_var_decl :
    Yices.context -> string -> Yices.typ -> Yices.var_decl
    = "camlidl_yices_yices_mk_var_decl"
  external get_var_decl_from_name : Yices.context -> string -> Yices.var_decl
    = "camlidl_yices_yices_get_var_decl_from_name"
  external get_var_decl : Yices.expr -> Yices.var_decl
    = "camlidl_yices_yices_get_var_decl"
  external get_var_decl_name : Yices.var_decl -> string
    = "camlidl_yices_yices_get_var_decl_name"
  external mk_var_from_decl : Yices.context -> Yices.var_decl -> Yices.expr
    = "camlidl_yices_yices_mk_var_from_decl"
  external mk_bool_var_from_decl :
    Yices.context -> Yices.var_decl -> Yices.expr
    = "camlidl_yices_yices_mk_bool_var_from_decl"
  external mk_bool_var : Yices.context -> string -> Yices.expr
    = "camlidl_yices_yices_mk_bool_var"
  external mk_fresh_bool_var : Yices.context -> Yices.expr
    = "camlidl_yices_yices_mk_fresh_bool_var"
  external mk_true : Yices.context -> Yices.expr
    = "camlidl_yices_yices_mk_true"
  external mk_false : Yices.context -> Yices.expr
    = "camlidl_yices_yices_mk_false"
  external mk_or : Yices.context -> Yices.expr array -> Yices.expr
    = "camlidl_yices_yices_mk_or"
  external mk_and : Yices.context -> Yices.expr array -> Yices.expr
    = "camlidl_yices_yices_mk_and"
  external mk_not : Yices.context -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_not"
  external mk_eq : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_eq"
  external mk_diseq : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_diseq"
  external mk_ite :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_ite"
  external mk_app :
    Yices.context -> Yices.expr -> Yices.expr array -> Yices.expr
    = "camlidl_yices_yices_mk_app"
  external mk_function_update :
    Yices.context ->
    Yices.expr -> Yices.expr array -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_function_update"
  external mk_tuple_literal : Yices.context -> Yices.expr array -> Yices.expr
    = "camlidl_yices_yices_mk_tuple_literal"
  external mk_num : Yices.context -> int -> Yices.expr
    = "camlidl_yices_yices_mk_num"
  external mk_num_from_string : Yices.context -> string -> Yices.expr
    = "camlidl_yices_yices_mk_num_from_string"
  external mk_sum : Yices.context -> Yices.expr array -> Yices.expr
    = "camlidl_yices_yices_mk_sum"
  external mk_sub : Yices.context -> Yices.expr array -> Yices.expr
    = "camlidl_yices_yices_mk_sub"
  external mk_mul : Yices.context -> Yices.expr array -> Yices.expr
    = "camlidl_yices_yices_mk_mul"
  external mk_lt : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_lt"
  external mk_le : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_le"
  external mk_gt : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_gt"
  external mk_ge : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_ge"
  external mk_bv_constant : Yices.context -> int -> int32 -> Yices.expr
    = "camlidl_yices_yices_mk_bv_constant"
  external mk_bv_constant_from_array :
    Yices.context -> bool array -> Yices.expr
    = "camlidl_yices_yices_mk_bv_constant_from_array"
  external mk_bv_add :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_add"
  external mk_bv_sub :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_sub"
  external mk_bv_mul :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_mul"
  external mk_bv_minus : Yices.context -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_minus"
  external mk_bv_concat :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_concat"
  external mk_bv_and :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_and"
  external mk_bv_or : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_or"
  external mk_bv_xor :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_xor"
  external mk_bv_not : Yices.context -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_not"
  external mk_bv_extract :
    Yices.context -> int -> int -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_extract"
  external mk_bv_sign_extend :
    Yices.context -> Yices.expr -> int -> Yices.expr
    = "camlidl_yices_yices_mk_bv_sign_extend"
  external mk_bv_shift_left0 :
    Yices.context -> Yices.expr -> int -> Yices.expr
    = "camlidl_yices_yices_mk_bv_shift_left0"
  external mk_bv_shift_left1 :
    Yices.context -> Yices.expr -> int -> Yices.expr
    = "camlidl_yices_yices_mk_bv_shift_left1"
  external mk_bv_shift_right0 :
    Yices.context -> Yices.expr -> int -> Yices.expr
    = "camlidl_yices_yices_mk_bv_shift_right0"
  external mk_bv_shift_right1 :
    Yices.context -> Yices.expr -> int -> Yices.expr
    = "camlidl_yices_yices_mk_bv_shift_right1"
  external mk_bv_lt : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_lt"
  external mk_bv_le : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_le"
  external mk_bv_gt : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_gt"
  external mk_bv_ge : Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_ge"
  external mk_bv_slt :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_slt"
  external mk_bv_sle :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_sle"
  external mk_bv_sgt :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_sgt"
  external mk_bv_sge :
    Yices.context -> Yices.expr -> Yices.expr -> Yices.expr
    = "camlidl_yices_yices_mk_bv_sge"
  external pp_expr : Yices.expr -> unit = "camlidl_yices_yices_pp_expr"
  module Future :
    sig
      external interrupt : Yices.context -> unit
        = "camlidl_yices_yices_interrupt"
      external get_lite_context : Yices.context -> Yicesl.context
        = "camlidl_yices_yices_get_lite_context"
    end
end