diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ab13bb943..8dcf3dda6 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1553,7 +1553,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') @@ -1564,7 +1564,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') diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 051a54696..dda8807c9 100644 --- a/src/api/ml/z3.ml +++ b/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 @@ -1435,6 +1479,12 @@ struct let (r, v) = Z3native.get_numeral_int (Expr.gnc x) (Expr.gno x) in 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) @@ -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)))) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index c554d7564..4122f40f2 100644 --- a/src/api/ml/z3.mli +++ b/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 @@ -1201,10 +1204,13 @@ sig val mk_sort : context -> Sort.sort (** The numerator of a rational numeral. *) - val get_numerator : Expr.expr-> Expr.expr + val get_numerator : Expr.expr -> Expr.expr (** The denominator of a rational numeral. *) - val get_denominator : Expr.expr-> Expr.expr + 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.*) @@ -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