package encoding

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Fresh : sig ... end

include Mappings_intf.S with type optimize = Z3.Optimize.optimize

type model

type solver

type status

type optimize = Z3.Optimize.optimize

type handle

exception Error of string

val update_param_value : 'a Params.param -> 'a -> unit

val mk_solver : unit -> solver

val interrupt : unit -> unit

val translate : solver -> solver

val push : solver -> unit

val pop : solver -> int -> unit

val reset : solver -> unit

val add_solver : solver -> Expr.t list -> unit

val check : solver -> Expr.t list -> status

val satisfiability : status -> Mappings_intf.satisfiability

val solver_model : solver -> model option

val value : model -> Expr.t -> Value.t

val values_of_model : ?symbols:Symbol.t list -> model -> Model.t

val expr_to_smtstring : Expr.t list -> bool -> string

val mk_optimize : unit -> optimize

val add_optimize : optimize -> Expr.t list -> unit

val maximize : optimize -> Expr.t -> handle

val minimize : optimize -> Expr.t -> handle

val optimize_model : optimize -> model option