package yices2_bindings

  1. Overview
  2. Docs
type t = Yices2_low.Types.context_t Ctypes.ptr
val malloc : ?config:Config.t -> unit -> t EH.t
val free : t -> unit
val reset : t -> unit
val push : t -> unit EH.t
val pop : t -> unit EH.t
val enable_option : t -> option:string -> unit EH.t
val disable_option : t -> option:string -> unit EH.t
val assert_formula : t -> Yices2_low.Types.term_t -> unit EH.t
val assert_formulas : t -> Yices2_low.Types.term_t list -> unit EH.t
val assert_blocking_clause : t -> unit EH.t
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.t
val get_unsat_core : t -> Yices2_low.Types.term_t list EH.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct