From 76ca64b93be26bfe56eca5b89737916c92e4576d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 9 Aug 2015 18:56:42 +0200
Subject: [PATCH] add consistency per request from Gabriel R

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/ml/z3.ml  |  7 ++++---
 src/api/ml/z3.mli | 34 +++++++++++++++++-----------------
 2 files changed, 21 insertions(+), 20 deletions(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index f6b793e5a..34caf2be8 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -2766,7 +2766,7 @@ struct
   let get_help ( x : fixedpoint ) =
     Z3native.fixedpoint_get_help (z3obj_gnc x) (z3obj_gno x)
       
-  let set_params ( x : fixedpoint ) ( p : Params.params )=
+  let set_parameters ( x : fixedpoint ) ( p : Params.params )=
     Z3native.fixedpoint_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p)
       
   let get_param_descrs ( x : fixedpoint ) =
@@ -2868,7 +2868,8 @@ end
 
 module Optimize =  
 struct 
-  type opt = z3_native_object 
+  type optimize = z3_native_object 
+  type opt = optimize
   type handle = { opt : opt; h : int } 
  
  
@@ -2888,7 +2889,7 @@ struct
     Z3native.optimize_get_help (z3obj_gnc x) (z3obj_gno x) 
  
  
-  let set_params ( x : opt ) ( p : Params.params )= 
+  let set_parameters ( x : opt ) ( p : Params.params )= 
     Z3native.optimize_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) 
         
   let get_param_descrs ( x : opt ) = 
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 938a9c194..9905fa209 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -3136,7 +3136,7 @@ sig
   val get_help : fixedpoint -> string
 
   (** Sets the fixedpoint solver parameters. *)
-  val set_params : fixedpoint -> Params.params -> unit
+  val set_parameters : fixedpoint -> Params.params -> unit
 
   (** Retrieves parameter descriptions for Fixedpoint solver. *)
   val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs
@@ -3230,52 +3230,52 @@ end
 (** Optimization *) 
 module Optimize : 
 sig 
-  type opt  
+  type optimize  
   type handle 
  
  
   (** Create a Optimize context. *) 
-  val mk_opt : context -> opt 
+  val mk_opt : context -> optimize 
       
   (** A string that describes all available optimize solver parameters. *) 
-  val get_help : opt -> string 
+  val get_help : optimize -> string 
  
  
   (** Sets the optimize solver parameters. *) 
-  val set_params : opt -> Params.params -> unit 
+  val set_parameters : optimize -> Params.params -> unit 
  
  
   (** Retrieves parameter descriptions for Optimize solver. *) 
-  val get_param_descrs : opt -> Params.ParamDescrs.param_descrs 
+  val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs 
  
  
   (** Assert a constraints into the optimize solver. *)         
-  val add : opt -> Expr.expr list -> unit 
+  val add : optimize -> 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 
+  val add_soft : optimize -> Expr.expr -> int -> string -> handle 
  
  
   (** Add maximization objective. 
    *)  
-  val maximize : opt -> Expr.expr -> handle 
+  val maximize : optimize -> Expr.expr -> handle 
  
  
   (** Add minimization objective. 
    *)  
-  val minimize : opt -> Expr.expr -> handle 
+  val minimize : optimize -> Expr.expr -> handle 
     
   (** Checks whether the assertions in the context are satisfiable and solves objectives. 
    *)         
-  val check : opt -> Solver.status 
+  val check : optimize -> Solver.status 
  
  
   (** Retrieve model from satisfiable context *) 
-  val get_model : opt -> Model.model 
+  val get_model : optimize -> Model.model 
  
  
   (** Retrieve lower bound in current model for handle *) 
@@ -3292,25 +3292,25 @@ sig
  
   (** Creates a backtracking point. 
       {!pop} *) 
-  val push : opt -> unit 
+  val push : optimize -> unit 
 
 
   (** Backtrack one backtracking point. 
       Note that an exception is thrown if Pop is called without a corresponding [Push] 
       {!push} *) 
-  val pop : opt -> unit 
+  val pop : optimize -> unit 
 
  
   (** Retrieve explanation why optimize engine returned status Unknown. *)                 
-  val get_reason_unknown : opt -> string 
+  val get_reason_unknown : optimize -> string 
 
  
   (** Retrieve SMT-LIB string representation of optimize object. *) 
-  val to_string : opt -> string 
+  val to_string : optimize -> string 
  
  
   (** Retrieve statistics information from the last call to check *) 
-  val get_statistics : opt -> Statistics.statistics 
+  val get_statistics : optimize -> Statistics.statistics 
 end