From 81fce55d784e173b1eb31f384f1a5ed8750dccdc Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 4 Nov 2016 21:22:01 +0000
Subject: [PATCH] Updated optimization ML API. Addresses #776.

---
 src/api/ml/z3.ml  |  8 ++++++--
 src/api/ml/z3.mli | 40 ++++++++++++++++++++++++++++------------
 2 files changed, 34 insertions(+), 14 deletions(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index b7016c4c8..245fd460b 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -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
 
 
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 1c91b28aa..594472030 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -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