From 9ad065a538815a6c13b6d890920f44d9418df8d3 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sat, 15 Aug 2015 23:51:43 +0100
Subject: [PATCH] Bugfixes for the optimization module in the ML API

---
 src/api/ml/z3.ml  | 38 +++++++++++++++++---------------------
 src/api/ml/z3.mli | 12 ++++--------
 2 files changed, 21 insertions(+), 29 deletions(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 34caf2be8..91f0756b7 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -2879,8 +2879,8 @@ struct
   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 
+                        inc_ref = Z3native.optimize_inc_ref ; 
+                        dec_ref = Z3native.optimize_dec_ref } in 
       (z3obj_sno res ctx (Z3native.mk_optimize (context_gno ctx))) ; 
       (z3obj_create res) ; 
       res 
@@ -2896,27 +2896,27 @@ struct
     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 
+    let f e = (Z3native.optimize_assert (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 add_soft ( x : opt ) ( e : Expr.expr) ( w : string ) ( s : Symbol.symbol ) = 
+    mk_handle x (Z3native.optimize_assert_soft (z3obj_gnc x) (z3obj_gno x) (Expr.gno e) w (Symbol.gno s)) 
  
  
-  let maximize ( x : opt) ( e :  Expr.expr ) =  
+  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 ) =  
+  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  
+     let r = lbool_of_int (Z3native.optimize_check (z3obj_gnc x) (z3obj_gno x)) in  
      match r with 
-       | L_TRUE -> SATISFIABLE 
-       | L_FALSE -> UNSATISFIABLE 
-       | _ -> UNKNOWN 
+       | L_TRUE -> Solver.SATISFIABLE 
+       | L_FALSE -> Solver.UNSATISFIABLE 
+       | _ -> Solver.UNKNOWN 
  
  
   let get_model ( x : opt ) =  
@@ -2926,17 +2926,13 @@ struct
      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_lower ( x : handle ) ( idx : int )  = 
+      expr_of_ptr (z3obj_gc x.opt) (Z3native.optimize_get_lower (z3obj_gnc x.opt) (z3obj_gno x.opt) idx) 
  
-  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 get_upper ( x : handle ) ( idx : int ) =  
+      expr_of_ptr (z3obj_gc x.opt) (Z3native.optimize_get_upper (z3obj_gnc x.opt) (z3obj_gno x.opt) idx)  
+  
+  let push ( x : opt ) = Z3native.optimize_push (z3obj_gnc x) (z3obj_gno x)
  
   let pop ( x : opt ) = Z3native.optimize_pop (z3obj_gnc x) (z3obj_gno x) 
  
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 9905fa209..ffc95fb2f 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -3257,7 +3257,7 @@ sig
      Supply integer weight and string that identifies a group 
       of soft constraints.  
    *) 
-  val add_soft : optimize -> Expr.expr -> int -> string -> handle 
+  val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle 
  
  
   (** Add maximization objective. 
@@ -3275,19 +3275,15 @@ sig
  
  
   (** Retrieve model from satisfiable context *) 
-  val get_model : optimize -> Model.model 
+  val get_model : optimize -> Model.model option
  
  
   (** Retrieve lower bound in current model for handle *) 
-  val get_lower : handle -> Expr.expr 
+  val get_lower : handle -> int -> 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 
+  val get_upper : handle -> int -> Expr.expr 
 
  
   (** Creates a backtracking point.