package yices2_bindings

  1. Overview
  2. Docs
val assert_blocking_clause : Yices2_low.Types.context_t Ctypes.ptr -> unit
type assertions = Term.t list list
type options
type t = {
  1. config : Config.t option;
  2. context : Yices2_low.Types.context_t Ctypes.ptr;
  3. assertions : assertions ref;
  4. options : options;
  5. log : Action.t list ref;
}
val to_sexp : t -> Sexplib.Type.t list
val malloc : ?config:Config.t -> unit -> t
val free : t -> unit
val status : t -> Types.smt_status
val reset : t -> unit
val push : t -> unit
val pop : t -> unit
val enable_option : t -> option:string -> unit
val disable_option : t -> option:string -> unit
val assert_formula : t -> Term.t -> unit
val assert_formulas : t -> Term.t list -> unit
val check_with_assumptions : ?param:Yices2_low.Types.param_t Ctypes.ptr -> t -> Term.t list -> Types.smt_status
val stop : t -> unit
val get_model : t -> keep_subst:bool -> Model.t
val get_unsat_core : t -> Term.t list
val declare_type : t -> string -> unit
val declare_fun : t -> string -> Type.t -> unit