ML API: Added get_bit_int and get_ratio

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

scripts/mk_util.py

@@ -1534,7 +1534,7 @@ class MLExampleComponent(ExampleComponent):
             out.write('\t%s ' % OCAMLC)
             if DEBUG_MODE:
                 out.write('-g ')
-            out.write('-custom -o ml_example.byte -I api/ml -cclib "-L. -lz3" z3.cma')
+            out.write('-custom -o ml_example.byte -I api/ml -cclib "-L. -lz3" nums.cma z3.cma')
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s/%s' % (self.to_ex_dir, mlfile))
             out.write('\n')
@@ -1545,7 +1545,7 @@ class MLExampleComponent(ExampleComponent):
             out.write('\t%s ' % OCAMLOPT)
             if DEBUG_MODE:
                 out.write('-g ')
-            out.write('-o ml_example$(EXE_EXT) -I api/ml -cclib "-L. -lz3" z3.cmxa')
+            out.write('-o ml_example$(EXE_EXT) -I api/ml -cclib "-L. -lz3" nums.cmxa z3.cmxa')
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s/%s' % (self.to_ex_dir, mlfile))
             out.write('\n')

src/api/ml/META

@@ -0,0 +1,7 @@
+# META file for the "z3" package:
+version = "VERSION"
+description = "Z3 Theorem Prover (OCaml API)"
+requires = "num"
+archive(byte) = "z3.cma"
+archive(native) = "z3.cmxa"
+linkopts = "-cclib -lz3"

src/api/ml/z3.ml

@@ -1425,6 +1425,50 @@ end
 
 module Arithmetic =
 struct
+  let is_int ( x : expr ) =
+    (Z3native.is_numeral_ast (Expr.gnc x) (Expr.gno x)) &&
+      ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == INT_SORT)
+      
+  let is_arithmetic_numeral ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM)
+
+  let is_le ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE)
+
+  let is_ge ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE)
+
+  let is_lt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LT)
+
+  let is_gt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GT)
+
+  let is_add ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ADD)
+
+  let is_sub ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SUB)
+
+  let is_uminus ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UMINUS)
+
+  let is_mul ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MUL)
+
+  let is_div ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_DIV)
+
+  let is_idiv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IDIV)
+
+  let is_remainder ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REM)
+
+  let is_modulus ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD)
+
+  let is_inttoreal ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL)
+
+  let is_real_to_int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT)
+
+  let is_real_is_int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT)
+
+  let is_real ( x : expr ) =
+    ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == REAL_SORT)
+      
+  let is_int_numeral ( x : expr ) = (Expr.is_numeral x) && (is_int x)
+
+  let is_rat_numeral ( x : expr ) = (Expr.is_numeral x) && (is_real x)
+    
+  let is_algebraic_number ( x : expr ) = Z3native.is_algebraic_number (Expr.gnc x) (Expr.gno x)
 
   module Integer =
   struct     
@@ -1436,6 +1480,12 @@ struct
       if r then v
       else raise (Z3native.Exception "Conversion failed.")
 
+    let get_big_int ( x : expr ) = 
+      if (is_int_numeral x) then 
+	let s = to_string(x) in
+	(Big_int.big_int_of_string s)
+      else raise (Z3native.Exception "Conversion failed.")
+	
     let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
 
     let mk_const ( ctx : context ) ( name : Symbol.symbol ) =
@@ -1474,6 +1524,12 @@ struct
     let get_denominator ( x : expr ) =
       expr_of_ptr (Expr.gc x) (Z3native.get_denominator (Expr.gnc x) (Expr.gno x))
 	
+    let get_ratio ( x : expr ) = 
+      if (is_rat_numeral x)  then
+	let s = to_string(x) in
+	(Ratio.ratio_of_string s)
+      else raise (Z3native.Exception "Conversion failed.")
+
     let to_decimal_string ( x : expr ) ( precision : int ) = 
       Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision
 	
@@ -1518,51 +1574,6 @@ struct
     end
   end
 
-  let is_int ( x : expr ) =
-    (Z3native.is_numeral_ast (Expr.gnc x) (Expr.gno x)) &&
-      ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == INT_SORT)
-      
-  let is_arithmetic_numeral ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM)
-
-  let is_le ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE)
-
-  let is_ge ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE)
-
-  let is_lt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LT)
-
-  let is_gt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GT)
-
-  let is_add ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ADD)
-
-  let is_sub ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SUB)
-
-  let is_uminus ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UMINUS)
-
-  let is_mul ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MUL)
-
-  let is_div ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_DIV)
-
-  let is_idiv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IDIV)
-
-  let is_remainder ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REM)
-
-  let is_modulus ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD)
-
-  let is_inttoreal ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL)
-
-  let is_real_to_int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT)
-
-  let is_real_is_int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT)
-
-  let is_real ( x : expr ) =
-    ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == REAL_SORT)
-      
-  let is_int_numeral ( x : expr ) = (Expr.is_numeral x) && (is_int x)
-
-  let is_rat_num ( x : expr ) = (Expr.is_numeral x) && (is_real x)
-    
-  let is_algebraic_number ( x : expr ) = Z3native.is_algebraic_number (Expr.gnc x) (Expr.gno x)
-
   let mk_add ( ctx : context ) ( t : expr list ) =
     let f x = (Expr.gno x) in
     (expr_of_ptr ctx (Z3native.mk_add (context_gno ctx) (List.length t) (Array.of_list (List.map f t))))

src/api/ml/z3.mli

@@ -1149,6 +1149,9 @@ sig
     (** Retrieve the int value. *)
     val get_int : Expr.expr -> int
 
+    (** Get a big_int from an integer numeral *)
+    val get_big_int : Expr.expr -> Big_int.big_int
+
     (** Returns a string representation of the numeral. *)
     val to_string : Expr.expr -> string
 
@@ -1206,6 +1209,9 @@ sig
     (** The denominator of a rational numeral. *)
     val get_denominator : Expr.expr -> Expr.expr
 
+    (** Get a ratio from a real numeral *)
+    val get_ratio : Expr.expr -> Ratio.ratio
+
     (** Returns a string representation in decimal notation. 
 	The result has at most as many decimal places as indicated by the int argument.*)
     val to_decimal_string : Expr.expr-> int -> string
@@ -1323,7 +1329,7 @@ sig
   val is_int_numeral : Expr.expr -> bool
 
   (** Indicates whether the term is a real numeral. *)
-  val is_rat_num : Expr.expr -> bool
+  val is_rat_numeral : Expr.expr -> bool
 
   (** Indicates whether the term is an algebraic number *)
   val is_algebraic_number : Expr.expr -> bool