ML API: added interpolation, bugfixes.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

scripts/update_api.py

@@ -334,6 +334,8 @@ def param2ml(p):
             return "ptr"
     elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
         return "%s array" % type2ml(param_type(p))
+    elif k == OUT_MANAGED_ARRAY:
+        return "%s array" % type2ml(param_type(p));
     else:
         return type2ml(param_type(p))
 
@@ -1067,7 +1069,7 @@ def ml_method_name(name):
     return name[3:] # Remove Z3_
 
 def is_out_param(p):
-     if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
+     if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY:
          return True
      else:
          return False
@@ -1411,6 +1413,8 @@ def mk_ml():
                         type2str(param_type(param)),
                         type2str(param_type(param)),
                         param_array_capacity_pos(param)))
+            elif k == OUT_MANAGED_ARRAY:
+                ml_wrapper.write('  %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
             elif k == IN_ARRAY or k == INOUT_ARRAY:
                 t = param_type(param)
                 ts = type2str(t)
@@ -1449,7 +1453,7 @@ def mk_ml():
             else:
                 ml_wrapper.write(', ')
             k = param_kind(param)
-            if k == OUT or k == INOUT:
+            if k == OUT or k == INOUT or k == OUT_MANAGED_ARRAY:
                 ml_wrapper.write('&_a%s' %  i)
             else:
                 ml_wrapper.write('_a%i' % i)
@@ -1465,6 +1469,8 @@ def mk_ml():
                 if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
                     ml_wrapper.write('  _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p)))
                     ml_wrapper.write('  for (_i = 0; _i < _a%s; _i++) { value t; %s Store_field(_a%s_val, _i, t); }\n' % (param_array_capacity_pos(p), ml_set_wrap(param_type(p), 't', '_a' + str(i) + '[_i]'), i))
+                elif param_kind(p) == OUT_MANAGED_ARRAY:
+                    ml_wrapper.write('  %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a"  + str(i) ))
                 elif is_out_param(p):
                     ml_wrapper.write('  %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a"  + str(i) ))
                 i = i + 1

src/api/ml/z3.ml

@@ -629,7 +629,6 @@ sig
   val to_string : params -> string
 
   val update_param_value : context -> string -> string -> unit
-  val get_param_value : context -> string -> string option
   val set_print_mode : context -> Z3enums.ast_print_mode -> unit
 end = struct
   type params = z3_native_object
@@ -688,13 +687,6 @@ end = struct
   let update_param_value ( ctx : context ) ( id : string) ( value : string )=
     Z3native.update_param_value (context_gno ctx) id value
 
-  let get_param_value ( ctx : context ) ( id : string ) =
-    let (r, v) = (Z3native.get_param_value (context_gno ctx) id) in
-    if not r then
-      None
-    else 
-      Some v
-
   let set_print_mode ( ctx : context ) ( value : ast_print_mode ) =
     Z3native.set_ast_print_mode (context_gno ctx) (int_of_ast_print_mode value)
 end
@@ -2683,6 +2675,65 @@ struct
 			  (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls)))))
 end
 
+module Interpolation = 
+struct
+  let mk_interpolant ( ctx : context ) ( a : expr ) =
+    (expr_of_ptr ctx (Z3native.mk_interpolant (context_gno ctx) (Expr.gno a)))
+    
+  let mk_interpolation_context ( settings : ( string * string ) list ) =
+    let cfg = Z3native.mk_config () in
+    let f e = (Z3native.set_param_value cfg (fst e) (snd e)) in
+    (List.iter f settings) ;
+    let v = Z3native.mk_interpolation_context cfg in
+    Z3native.del_config(cfg) ;
+    Z3native.set_ast_print_mode v (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ;
+    Z3native.set_internal_error_handler v ;
+    let res = { m_n_ctx = v; m_n_obj_cnt = 0 } in
+    let f = fun o -> dispose_context o in
+    Gc.finalise f res;
+    res
+
+  let get_interpolant ( ctx : context ) ( pf : expr ) ( pat: expr ) ( p : Params.params ) =
+    (ASTVector.create ctx (Z3native.get_interpolant (context_gno ctx) (Expr.gno pf) (Expr.gno pat) (z3obj_gno p)))
+      
+  let compute_interpolant ( ctx : context ) ( pat : expr ) ( p : Params.params ) =
+    let (r, interp, model) = (Z3native.compute_interpolant (context_gno ctx) (Expr.gno pat) (z3obj_gno p)) in
+    match (lbool_of_int r) with
+      | L_TRUE -> ((ASTVector.create ctx interp), (Model.create ctx model))
+      | _ -> raise (Z3native.Exception "Error computing interpolant.")
+      
+  let get_interpolation_profile ( ctx : context ) =
+    (Z3native.interpolation_profile (context_gno ctx))
+      
+  let read_interpolation_problem ( ctx : context ) ( filename : string ) =
+    let (r, num, cnsts, parents, error, num_theory, theory) = (Z3native.read_interpolation_problem (context_gno ctx) filename) in
+    match r with 
+      | 0 -> raise (Z3native.Exception "Interpolation problem could not be read.")
+      | _ ->
+	let f1 i = (expr_of_ptr ctx (Array.get cnsts i)) in
+	let f2 i = (Array.get parents i) in
+	let f3 i = (expr_of_ptr ctx (Array.get theory i)) in 
+	((mk_list f1 num),
+	 (mk_list f2 num),
+	 (mk_list f3 num_theory))
+          
+  let check_interpolant ( ctx : context ) ( num : int ) ( cnsts : Expr.expr list ) ( parents : int list ) ( interps : Expr.expr list ) ( num_theory : int ) ( theory : Expr.expr list ) =
+    let (r, str) = (Z3native.check_interpolant (context_gno ctx) 
+		      num
+		      (let f x = Expr.gno x in (Array.of_list (List.map f cnsts)))
+		      (Array.of_list parents)
+		      (let f x = Expr.gno x in (Array.of_list (List.map f interps)))
+		      num_theory
+		      (let f x = Expr.gno x in (Array.of_list (List.map f theory)))) in
+    match (lbool_of_int r) with
+      | L_UNDEF -> raise (Z3native.Exception "Interpolant could not be verified.")
+      | L_FALSE -> raise (Z3native.Exception "Interpolant could not be verified.")
+      | _ -> ()
+
+  let write_interpolation_problem ( ctx : context ) ( num : int ) ( cnsts : Expr.expr list ) ( parents : int list ) ( filename : string ) ( num_theory : int ) ( theory : Expr.expr list ) =
+    (Z3native.write_interpolation_problem (context_gno ctx) num (expr_lton cnsts) (Array.of_list parents) filename num_theory (expr_lton theory)) ;
+    ()
+end
 
 let set_global_param ( id : string ) ( value : string ) =
   (Z3native.global_param_set id value)

src/api/ml/z3.mli

@@ -445,16 +445,9 @@ sig
       The list of all configuration parameters can be obtained using the Z3 executable:
       [z3.exe -p]
       Only a few configuration parameters are mutable once the context is created.
-     An exception is thrown when trying to modify an immutable parameter.
+      An exception is thrown when trying to modify an immutable parameter. *)
-     {!get_param_value} *)
   val update_param_value : context -> string -> string -> unit
     
-  (** Get a configuration parameter.
-     
-     Returns None if the parameter value does not exist.
-     {!update_param_value} *)
-  val get_param_value : context -> string -> string option
-
   (** Selects the format used for pretty-printing expressions.
       
       The default mode for pretty printing expressions is to produce
@@ -1621,7 +1614,6 @@ sig
 
   (** Unsigned division.
       
-     
       It is defined as the floor of [t1/t2] if \c t2 is
       different from zero. If [t2] is zero, then the result
       is undefined.
@@ -2922,6 +2914,52 @@ sig
   val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
 end
 
+(** Interpolation *)
+module Interpolation :
+sig
+
+  (** Create an AST node marking a formula position for interpolation.
+      The expression must have Boolean sort. *)
+  val mk_interpolant : context -> Expr.expr -> Expr.expr
+    
+  (** The interpolation context is suitable for generation of interpolants.
+      For more information on interpolation please refer
+      too the C/C++ API, which is well documented. *)
+  val mk_interpolation_context : (string * string) list -> context
+
+  (** Gets an interpolant.
+      For more information on interpolation please refer
+      too the C/C++ API, which is well documented. *)
+  val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> AST.ASTVector.ast_vector
+
+  (** Computes an interpolant.
+      For more information on interpolation please refer
+      too the C/C++ API, which is well documented. *)
+  val compute_interpolant : context -> Expr.expr -> Params.params -> (AST.ASTVector.ast_vector * Model.model)
+
+  (** Retrieves an interpolation profile.
+      For more information on interpolation please refer
+      too the C/C++ API, which is well documented. *)
+  val get_interpolation_profile : context -> string
+    
+  (** Read an interpolation problem from file.
+      For more information on interpolation please refer
+      too the C/C++ API, which is well documented. *)
+  val read_interpolation_problem : context -> string -> (Expr.expr list * int list * Expr.expr list)
+    
+  (** Check the correctness of an interpolant.
+      For more information on interpolation please refer
+      too the C/C++ API, which is well documented. *)
+  val check_interpolant : context -> int -> Expr.expr list -> int list -> Expr.expr list -> int -> Expr.expr list -> unit
+
+  (** Write an interpolation problem to file suitable for reading with
+      Z3_read_interpolation_problem.
+      For more information on interpolation please refer
+      too the C/C++ API, which is well documented. *)
+  val write_interpolation_problem : context -> int -> Expr.expr list -> int list -> string -> int -> Expr.expr list -> unit
+
+end
+
 (** Set a global (or module) parameter, which is shared by all Z3 contexts.
     
     When a Z3 module is initialized it will use the value of these parameters
@@ -2941,7 +2979,7 @@ val set_global_param : string -> string -> unit
 (** Get a global (or module) parameter.
     
     Returns None if the parameter does not exist.
-    The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
+    The caller must invoke #Z3_global_param_del_value to delete the value returned at param_value.
     This function cannot be invoked simultaneously from different threads without synchronization.
     The result string stored in param_value is stored in a shared location.
 *)