From eb5af100bda2a799669993dbd32c36dcc3d12260 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Aug 2015 17:49:20 +0200 Subject: [PATCH] adding optimize bindings for ML, adding get_reason_unknown to optimize, mentioned in pull request issue #188, second edition Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 8 ++++ src/api/dotnet/Optimize.cs | 9 ++++ src/api/java/Fixedpoint.java | 1 - src/api/java/Optimize.java | 9 ++++ src/api/ml/z3.ml | 86 +++++++++++++++++++++++++++++++++++ src/api/ml/z3.mli | 87 ++++++++++++++++++++++++++++++++++++ src/api/python/z3.py | 4 ++ src/api/z3_api.h | 9 ++++ src/opt/opt_context.cpp | 7 +++ src/opt/opt_context.h | 2 +- 10 files changed, 220 insertions(+), 2 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index d9369092a..0f322c6e9 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -142,6 +142,14 @@ extern "C" { Z3_CATCH_RETURN(Z3_L_UNDEF); } + Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize o) { + Z3_TRY; + LOG_Z3_optimize_to_string(c, o); + RESET_ERROR_CODE(); + return mk_c(c)->mk_external_string(to_optimize_ptr(o)->reason_unknown()); + Z3_CATCH_RETURN(""); + } + Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o) { Z3_TRY; LOG_Z3_optimize_get_model(c, o); diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index dc94db78a..501603668 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -232,6 +232,15 @@ namespace Microsoft.Z3 return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index)); } + /// + /// Return a string the describes why the last to check returned unknown + /// + public String getReasonUnknown() + { + Contract.Ensures(Contract.Result() != null); + return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject); + } + /// /// Print the context to a string (SMT-LIB parseable benchmark). diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index e1fccdf4f..0bdbfb571 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -213,7 +213,6 @@ public class Fixedpoint extends Z3Object **/ public String getReasonUnknown() { - return Native.fixedpointGetReasonUnknown(getContext().nCtx(), getNativeObject()); } diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index d80aa124d..f12bb7e06 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -224,6 +224,15 @@ public class Optimize extends Z3Object { return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index)); } + + /** + * Return a string the describes why the last to check returned unknown + **/ + public String getReasonUnknown() + { + return Native.optimizeGetReasonUnknown(getContext().nCtx(), + getNativeObject()); + } /** diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 51eb35e29..f6b793e5a 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -2866,6 +2866,92 @@ struct end +module Optimize = +struct + type opt = z3_native_object + type handle = { opt : opt; h : int } + + + let mk_handle (x : opt) h = { opt = x; h = h } + + + let mk_opt (ctx : context) = + let res : opt = { m_ctx = ctx; + m_n_obj = null ; + inc_ref = Z3native.optimzie_inc_ref ; + dec_ref = Z3native.optimzie_dec_ref } in + (z3obj_sno res ctx (Z3native.mk_optimize (context_gno ctx))) ; + (z3obj_create res) ; + res + + let get_help ( x : opt ) = + Z3native.optimize_get_help (z3obj_gnc x) (z3obj_gno x) + + + let set_params ( x : opt ) ( p : Params.params )= + Z3native.optimize_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) + + let get_param_descrs ( x : opt ) = + Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.optimize_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) + + let add ( x : opt ) ( constraints : expr list ) = + let f e = (Z3native.optimize_add (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) in + List.iter f constraints + + + let add_soft ( x : opt) ( e : Expr.expr) ( w : int) ( s : string ) = + mk_handle x (Z3native.optimize_add_soft (z3obj_gnc x) (z3obj_gno x) (Expr.gno e) w s) + + + let maximize ( x : opt) ( e : Expr.expr ) = + mk_handle x (Z3native.optimize_maximize (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) + + + let minimize ( x : opt) ( e : Expr.expr ) = + mk_handle x (Z3native.optimize_minimize (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) + + let check ( x : opt ) = + let r = lbool_of_int (Z3native.optimize_check_sat (z3obj_gnc x) (z3obj_gno x) in + match r with + | L_TRUE -> SATISFIABLE + | L_FALSE -> UNSATISFIABLE + | _ -> UNKNOWN + + + let get_model ( x : opt ) = + let q = Z3native.optimize_get_model (z3obj_gnc x) (z3obj_gno x) in + if (Z3native.is_null q) then + None + else + Some (Model.create (z3obj_gc x) q) + + let get_lower ( x : handle ) = + expr_of_ptr (z3obj_gnc x.opt) (Z3native.optimize_get_lower (z3obj_gnc x) (z3obj_gno x) h.h) + + let get_upper ( x : handle ) = + expr_of_ptr (z3obj_gnc x.opt) (Z3native.optimize_get_upper (z3obj_gnc x) (z3obj_gno x) h.h) + + + let get_value ( x : handle ) = + expr_of_ptr (z3obj_gnc x.opt) (Z3native.optimize_get_value (z3obj_gnc x) (z3obj_gno x) h.h) + + let push ( x : opt ) = Z3native.optimize_push (z3obj_gnc x) (z3obj_gno x) n + + let pop ( x : opt ) = Z3native.optimize_pop (z3obj_gnc x) (z3obj_gno x) + + let get_reason_unknown ( x : opt ) = + Z3native.optimize_get_reason_unknown (z3obj_gnc x) (z3obj_gno x) + + let to_string ( x : opt ) = Z3native.optimize_to_string (z3obj_gnc x) (z3obj_gno x) + + + let get_statistics ( x : opt ) = + let s = Z3native.optimize_get_statistics (z3obj_gnc x) (z3obj_gno x) in + (Statistics.create (z3obj_gc x) s) + + +end + module SMT = struct let benchmark_to_smtstring ( ctx : context ) ( name : string ) ( logic : string ) ( status : string ) ( attributes : string ) ( assumptions : expr list ) ( formula : expr ) = diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index e0f89565d..938a9c194 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3227,6 +3227,93 @@ sig val parse_file : fixedpoint -> string -> Expr.expr list end +(** Optimization *) +module Optimize : +sig + type opt + type handle + + + (** Create a Optimize context. *) + val mk_opt : context -> opt + + (** A string that describes all available optimize solver parameters. *) + val get_help : opt -> string + + + (** Sets the optimize solver parameters. *) + val set_params : opt -> Params.params -> unit + + + (** Retrieves parameter descriptions for Optimize solver. *) + val get_param_descrs : opt -> Params.ParamDescrs.param_descrs + + + (** Assert a constraints into the optimize solver. *) + val add : opt -> Expr.expr list -> unit + + + (** Asssert a soft constraint. + Supply integer weight and string that identifies a group + of soft constraints. + *) + val add_soft : opt -> Expr.expr -> int -> string -> handle + + + (** Add maximization objective. + *) + val maximize : opt -> Expr.expr -> handle + + + (** Add minimization objective. + *) + val minimize : opt -> Expr.expr -> handle + + (** Checks whether the assertions in the context are satisfiable and solves objectives. + *) + val check : opt -> Solver.status + + + (** Retrieve model from satisfiable context *) + val get_model : opt -> Model.model + + + (** Retrieve lower bound in current model for handle *) + val get_lower : handle -> Expr.expr + + + (** Retrieve upper bound in current model for handle *) + val get_upper : handle -> Expr.expr + + + (** Retrieve value in current model for handle *) + val get_value : handle -> Expr.expr + + + (** Creates a backtracking point. + {!pop} *) + val push : opt -> unit + + + (** Backtrack one backtracking point. + Note that an exception is thrown if Pop is called without a corresponding [Push] + {!push} *) + val pop : opt -> unit + + + (** Retrieve explanation why optimize engine returned status Unknown. *) + val get_reason_unknown : opt -> string + + + (** Retrieve SMT-LIB string representation of optimize object. *) + val to_string : opt -> string + + + (** Retrieve statistics information from the last call to check *) + val get_statistics : opt -> Statistics.statistics +end + + (** Functions for handling SMT and SMT2 expressions and files *) module SMT : sig diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 56d2cda89..e4394e9b2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6494,6 +6494,10 @@ class Optimize(Z3PPObject): """Check satisfiability while optimizing objective functions.""" return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize)) + def reason_unknown(self): + """Return a string that describes why the last `check()` returned `unknown`.""" + return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize) + def model(self): """Return a model for the last check().""" try: diff --git a/src/api/z3_api.h b/src/api/z3_api.h index a646f93ca..212fa12fd 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6240,6 +6240,15 @@ END_MLAPI_EXCLUDE Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o); + /** + \brief Retrieve a string that describes the last status returned by #Z3_optimize_check. + + Use this method when #Z3_optimize_check returns Z3_L_UNDEF. + + def_API('Z3_optimize_get_reason_unknown', STRING, (_in(CONTEXT), _in(OPTIMIZE) )) + */ + Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c,Z3_optimize d); + /** \brief Retrieve the model for the last #Z3_optimize_check diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8edebd460..857e0ae7e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -457,6 +457,13 @@ namespace opt { return is_sat; } + std::string context::reason_unknown() const { + if (m_solver.get()) { + return m_solver->reason_unknown(); + } + return std::string("unknown"); + } + void context::display_bounds(std::ostream& out, bounds_t const& b) const { for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 50847134d..4b14a0115 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -187,7 +187,7 @@ namespace opt { virtual proof* get_proof() { return 0; } virtual void get_labels(svector & r) {} virtual void get_unsat_core(ptr_vector & r) {} - virtual std::string reason_unknown() const { return std::string("unknown"); } + virtual std::string reason_unknown() const; virtual void display_assignment(std::ostream& out); virtual bool is_pareto() { return m_pareto.get() != 0; }