mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Updated optimization ML API. Addresses #776.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-04 21:22:01 +00:00
parent e7f7090a01
commit 81fce55d78
2 changed files with 34 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1906,13 +1906,17 @@ struct
let q = Z3native.optimize_get_model (gc x) x in
if Z3native.is_null_model q then None else Some q
let get_lower (x:handle) (idx:int) = Z3native.optimize_get_lower (gc x.opt) x.opt idx
let get_upper (x:handle) (idx:int) = Z3native.optimize_get_upper (gc x.opt) x.opt idx
let get_lower (x:handle) = Z3native.optimize_get_lower (gc x.opt) x.opt x.h
let get_upper (x:handle) = Z3native.optimize_get_upper (gc x.opt) x.opt x.h
let push (x:optimize) = Z3native.optimize_push (gc x) x
let pop (x:optimize) = Z3native.optimize_pop (gc x) x
let get_reason_unknown (x:optimize) = Z3native.optimize_get_reason_unknown (gc x) x
let to_string (x:optimize) = Z3native.optimize_to_string (gc x) x
let get_statistics (x:optimize) = Z3native.optimize_get_statistics (gc x) x
let from_file (x:optimize) (s:string) = Z3native.optimize_from_file (gc x) x s
let from_string (x:optimize) (s:string) = Z3native.optimize_from_string (gc x) x s
let get_assertions (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_assertions (gc x) x)
let get_objectives (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_statistics (gc x) x)
end

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

@ -3236,33 +3236,28 @@ sig
(** Asssert a soft constraint.
Supply integer weight and string that identifies a group
of soft constraints.
*)
of soft constraints. *)
val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle
(** Add maximization objective.
*)
(** Add maximization objective. *)
val maximize : optimize -> Expr.expr -> handle
(** Add minimization objective.
*)
(** Add minimization objective. *)
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 : optimize -> Solver.status
(** Retrieve model from satisfiable context *)
val get_model : optimize -> Model.model option
(** Retrieve lower bound in current model for handle *)
val get_lower : handle -> int -> Expr.expr
val get_lower : handle -> Expr.expr
(** Retrieve upper bound in current model for handle *)
val get_upper : handle -> int -> Expr.expr
val get_upper : handle -> Expr.expr
(** Creates a backtracking point.
{!pop} *)
(** Creates a backtracking point. {!pop} *)
val push : optimize -> unit
(** Backtrack one backtracking point.
@ -3278,6 +3273,27 @@ sig
(** Retrieve statistics information from the last call to check *)
val get_statistics : optimize -> Statistics.statistics
(** Parse an SMT-LIB2 file with assertions, soft constraints and optimization
objectives. Add the parsed constraints and objectives to the optimization
context. *)
val from_file : optimize -> string -> unit
(** Parse an SMT-LIB2 string with assertions, soft constraints and optimization
objectives. Add the parsed constraints and objectives to the optimization
context. *)
val from_string : optimize -> string -> unit
(** Return the set of asserted formulas on the optimization context. *)
val get_assertions : optimize -> Expr.expr list
(** Return objectives on the optimization context. If the objective function
is a max-sat objective it is returned as a Pseudo-Boolean (minimization)
sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...). If the objective
function is entered as a maximization objective, then return the
corresponding minimization objective. In this way the resulting
objective function is always returned as a minimization objective. *)
val get_objectives : optimize -> Expr.expr list
end