mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

add consistency per request from Gabriel R

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-09 18:56:42 +02:00
parent eb5af100bd
commit 76ca64b93b
2 changed files with 21 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/ml/z3.ml
View file

@ -2766,7 +2766,7 @@ struct
let get_help ( x : fixedpoint ) = let get_help ( x : fixedpoint ) =
Z3native.fixedpoint_get_help (z3obj_gnc x) (z3obj_gno x) Z3native.fixedpoint_get_help (z3obj_gnc x) (z3obj_gno x)
let set_params ( x : fixedpoint ) ( p : Params.params )= let set_parameters ( x : fixedpoint ) ( p : Params.params )=
Z3native.fixedpoint_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) Z3native.fixedpoint_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p)
let get_param_descrs ( x : fixedpoint ) = let get_param_descrs ( x : fixedpoint ) =
@ -2868,7 +2868,8 @@ end
module Optimize = module Optimize =
struct struct
type opt = z3_native_object type optimize = z3_native_object
type opt = optimize
type handle = { opt : opt; h : int } type handle = { opt : opt; h : int }
@ -2888,7 +2889,7 @@ struct
Z3native.optimize_get_help (z3obj_gnc x) (z3obj_gno x) Z3native.optimize_get_help (z3obj_gnc x) (z3obj_gno x)
let set_params ( x : opt ) ( p : Params.params )= let set_parameters ( x : opt ) ( p : Params.params )=
Z3native.optimize_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) Z3native.optimize_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p)
let get_param_descrs ( x : opt ) = let get_param_descrs ( x : opt ) =

34
src/api/ml/z3.mli
View file

@ -3136,7 +3136,7 @@ sig
val get_help : fixedpoint -> string val get_help : fixedpoint -> string
(** Sets the fixedpoint solver parameters. *) (** Sets the fixedpoint solver parameters. *)
val set_params : fixedpoint -> Params.params -> unit val set_parameters : fixedpoint -> Params.params -> unit
(** Retrieves parameter descriptions for Fixedpoint solver. *) (** Retrieves parameter descriptions for Fixedpoint solver. *)
val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs
@ -3230,52 +3230,52 @@ end
(** Optimization *) (** Optimization *)
module Optimize : module Optimize :
sig sig
type opt type optimize
type handle type handle
(** Create a Optimize context. *) (** Create a Optimize context. *)
val mk_opt : context -> opt val mk_opt : context -> optimize
(** A string that describes all available optimize solver parameters. *) (** A string that describes all available optimize solver parameters. *)
val get_help : opt -> string val get_help : optimize -> string
(** Sets the optimize solver parameters. *) (** Sets the optimize solver parameters. *)
val set_params : opt -> Params.params -> unit val set_parameters : optimize -> Params.params -> unit
(** Retrieves parameter descriptions for Optimize solver. *) (** Retrieves parameter descriptions for Optimize solver. *)
val get_param_descrs : opt -> Params.ParamDescrs.param_descrs val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs
(** Assert a constraints into the optimize solver. *) (** Assert a constraints into the optimize solver. *)
val add : opt -> Expr.expr list -> unit val add : optimize -> Expr.expr list -> unit
(** Asssert a soft constraint. (** Asssert a soft constraint.
Supply integer weight and string that identifies a group Supply integer weight and string that identifies a group
of soft constraints. of soft constraints.
*) *)
val add_soft : opt -> Expr.expr -> int -> string -> handle val add_soft : optimize -> Expr.expr -> int -> string -> handle
(** Add maximization objective. (** Add maximization objective.
*) *)
val maximize : opt -> Expr.expr -> handle val maximize : optimize -> Expr.expr -> handle
(** Add minimization objective. (** Add minimization objective.
*) *)
val minimize : opt -> Expr.expr -> handle val minimize : optimize -> Expr.expr -> handle
(** Checks whether the assertions in the context are satisfiable and solves objectives. (** Checks whether the assertions in the context are satisfiable and solves objectives.
*) *)
val check : opt -> Solver.status val check : optimize -> Solver.status
(** Retrieve model from satisfiable context *) (** Retrieve model from satisfiable context *)
val get_model : opt -> Model.model val get_model : optimize -> Model.model
(** Retrieve lower bound in current model for handle *) (** Retrieve lower bound in current model for handle *)
@ -3292,25 +3292,25 @@ sig
(** Creates a backtracking point. (** Creates a backtracking point.
{!pop} *) {!pop} *)
val push : opt -> unit val push : optimize -> unit
(** Backtrack one backtracking point. (** Backtrack one backtracking point.
Note that an exception is thrown if Pop is called without a corresponding [Push] Note that an exception is thrown if Pop is called without a corresponding [Push]
{!push} *) {!push} *)
val pop : opt -> unit val pop : optimize -> unit
(** Retrieve explanation why optimize engine returned status Unknown. *) (** Retrieve explanation why optimize engine returned status Unknown. *)
val get_reason_unknown : opt -> string val get_reason_unknown : optimize -> string
(** Retrieve SMT-LIB string representation of optimize object. *) (** Retrieve SMT-LIB string representation of optimize object. *)
val to_string : opt -> string val to_string : optimize -> string
(** Retrieve statistics information from the last call to check *) (** Retrieve statistics information from the last call to check *)
val get_statistics : opt -> Statistics.statistics val get_statistics : optimize -> Statistics.statistics
end end