package yices2_bindings

  1. Overview
  2. Docs
type t = Yices2_low.Types.context_t Ctypes.ptr
val malloc : ?config:Config.t -> unit -> t eh
val free : t -> unit
val reset : t -> unit
val push : t -> unit eh
val pop : t -> unit eh
val enable_option : t -> option:string -> unit eh
val disable_option : t -> option:string -> unit eh
val assert_formula : t -> Yices2_low.Types.term_t -> unit eh
val assert_formulas : t -> Yices2_low.Types.term_t list -> unit eh
val assert_blocking_clause : t -> unit eh
val check : ?param:Yices2_low.Types.param_t Ctypes.ptr -> t -> Yices2_low.Types.smt_status
val check_with_assumptions : ?param:Yices2_low.Types.param_t Ctypes.ptr -> t -> Yices2_low.Types.term_t list -> Yices2_low.Types.smt_status
val stop : t -> unit
val get_model : t -> keep_subst:bool -> Model.t eh
val get_unsat_core : t -> Yices2_low.Types.term_t list eh
OCaml

Innovation. Community. Security.