adding optimize bindings for ML, adding get_reason_unknown to optimize, mentioned in pull request issue #188, second edition

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

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));
         }
 
+	/// <summary>
+	/// Return a string the describes why the last to check returned unknown
+	/// </summary>	
+    	public String getReasonUnknown()
+    	{
+            Contract.Ensures(Contract.Result<string>() != null);
+            return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
+    	}
+
 
         /// <summary>
         /// Print the context to a string (SMT-LIB parseable benchmark).

src/api/java/Fixedpoint.java

@@ -213,7 +213,6 @@ public class Fixedpoint extends Z3Object
      **/
     public String getReasonUnknown()
     {
-
         return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
                 getNativeObject());
     }

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());	
+    }
     
     
     /**

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 ) =

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

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:

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
 

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];

src/opt/opt_context.h

@@ -187,7 +187,7 @@ namespace opt {
         virtual proof* get_proof() { return 0; }
         virtual void get_labels(svector<symbol> & r) {}
         virtual void get_unsat_core(ptr_vector<expr> & 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; }