From eea13a087f0caec61ec1ef3235944921a07b97e3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 21 Feb 2013 14:17:35 +0000 Subject: [PATCH] ML API savegame Signed-off-by: Christoph M. Wintersteiger --- examples/ml/ml_example.ml | 124 +++++++++++++++++++------------------- src/api/ml/z3.ml | 18 +++--- src/api/ml/z3.mli | 23 ++++--- src/api/ml/z3_rich.ml | 43 +++++++------ src/api/ml/z3_rich.mli | 13 ++-- 5 files changed, 107 insertions(+), 114 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index 823a08fe2..f7a4cbc00 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -162,70 +162,68 @@ let basic_tests ( ctx : context ) = else Printf.printf "Test passed.\n" ) ; - model_converter_test ctx -(* - // Real num/den test. - RatNum rn = ctx.MkReal(42, 43); - Expr inum = rn.Numerator; - Expr iden = rn.Denominator; - Console.WriteLine("Numerator: " + inum + " Denominator: " + iden); - if (inum.ToString() != "42" || iden.ToString() != "43") - throw new TestFailedException(); - - if (rn.ToDecimalString(3) != "0.976?") - throw new TestFailedException(); - - BigIntCheck(ctx, ctx.MkReal("-1231231232/234234333")); - BigIntCheck(ctx, ctx.MkReal("-123123234234234234231232/234234333")); - BigIntCheck(ctx, ctx.MkReal("-234234333")); - BigIntCheck(ctx, ctx.MkReal("234234333/2")); - - - string bn = "1234567890987654321"; - - if (ctx.MkInt(bn).BigInteger.ToString() != bn) - throw new TestFailedException(); - - if (ctx.MkBV(bn, 128).BigInteger.ToString() != bn) - throw new TestFailedException(); - - if (ctx.MkBV(bn, 32).BigInteger.ToString() == bn) - throw new TestFailedException(); - - // Error handling test. - try - { - IntExpr i = ctx.MkInt("1/2"); - throw new TestFailedException(); // unreachable - } - catch (Z3Exception) - { - } - } -*) + model_converter_test ctx ; + (* Real num/den test. *) + let rn = Real.mk_numeral_nd ctx 42 43 in + let inum = (get_numerator rn) in + let iden = get_denominator rn in + Printf.printf "Numerator: %s Denominator: %s\n" (Real.to_string inum) (Real.to_string iden) ; + if ((Real.to_string inum) <> "42" or (Real.to_string iden) <> "43") then + raise (TestFailedException "") + else + Printf.printf "Test passed.\n" + ; + if ((to_decimal_string rn 3) <> "0.976?") then + raise (TestFailedException "") + else + Printf.printf "Test passed.\n" + ; + if (to_decimal_string (Real.mk_numeral_s ctx "-1231231232/234234333") 5 <> "-5.25640?") then + raise (TestFailedException "") + else if (to_decimal_string (Real.mk_numeral_s ctx "-123123234234234234231232/234234333") 5 <> "-525641278361333.28170?") then + raise (TestFailedException "") + else if (to_decimal_string (Real.mk_numeral_s ctx "-234234333") 5 <> "-234234333") then + raise (TestFailedException "") + else if (to_decimal_string (Real.mk_numeral_s ctx "234234333/2") 5 <> "117117166.5") then + raise (TestFailedException "") + ; + (* Error handling test. *) + try ( + let i = Integer.mk_numeral_s ctx "1/2" in + raise (TestFailedException "") (* unreachable *) + ) + with Z3native.Exception(_) -> ( + Printf.printf "Exception caught, OK.\n" + ) let _ = - if not (Log.open_ "z3.log") then - raise (TestFailedException "Log couldn't be opened.") - else - ( - Printf.printf "Running Z3 version %s\n" Version.to_string ; - let cfg = [("model", "true"); ("proof", "false")] in - let ctx = (mk_context cfg) in - let is = (Symbol.mk_int ctx 42) in - let ss = (Symbol.mk_string ctx "mySymbol") in - let bs = (Boolean.mk_sort ctx) in - let ints = (Integer.mk_sort ctx) in - let rs = (Real.mk_sort ctx) in - Printf.printf "int symbol: %s\n" (Symbol.to_string is); - Printf.printf "string symbol: %s\n" (Symbol.to_string ss); - Printf.printf "bool sort: %s\n" (Sort.to_string bs); - Printf.printf "int sort: %s\n" (Sort.to_string ints); - Printf.printf "real sort: %s\n" (Sort.to_string rs); - basic_tests ctx ; - Printf.printf "Disposing...\n"; - Gc.full_major () - ); - Printf.printf "Exiting.\n"; + try ( + if not (Log.open_ "z3.log") then + raise (TestFailedException "Log couldn't be opened.") + else + ( + Printf.printf "Running Z3 version %s\n" Version.to_string ; + let cfg = [("model", "true"); ("proof", "false")] in + let ctx = (mk_context cfg) in + let is = (Symbol.mk_int ctx 42) in + let ss = (Symbol.mk_string ctx "mySymbol") in + let bs = (Boolean.mk_sort ctx) in + let ints = (Integer.mk_sort ctx) in + let rs = (Real.mk_sort ctx) in + Printf.printf "int symbol: %s\n" (Symbol.to_string is); + Printf.printf "string symbol: %s\n" (Symbol.to_string ss); + Printf.printf "bool sort: %s\n" (Sort.to_string bs); + Printf.printf "int sort: %s\n" (Sort.to_string ints); + Printf.printf "real sort: %s\n" (Sort.to_string rs); + basic_tests ctx ; + Printf.printf "Disposing...\n"; + Gc.full_major () + ); + Printf.printf "Exiting.\n" ; + exit 0 + ) with Z3native.Exception(msg) -> ( + Printf.printf "Z3 EXCEPTION: %s\n" msg ; + exit 1 + ) ;; diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 0676f1a39..e62732924 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -11,7 +11,6 @@ open Z3enums let null = Z3native.mk_null() let is_null o = (Z3native.is_null o) - (* Internal types *) type z3_native_context = { m_n_ctx : Z3native.z3_context; m_n_obj_cnt: int; } type context = z3_native_context @@ -21,7 +20,6 @@ type z3_native_object = { mutable m_n_obj : Z3native.ptr ; inc_ref : Z3native.z3_context -> Z3native.ptr -> unit; dec_ref : Z3native.z3_context -> Z3native.ptr -> unit } - (** Internal stuff *) module Internal = @@ -1455,11 +1453,11 @@ struct let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) - let mk_int_const ( ctx : context ) ( name : Symbol.symbol ) = + let mk_const ( ctx : context ) ( name : Symbol.symbol ) = Expr.mk_const ctx name (mk_sort ctx) - let mk_int_const_s ( ctx : context ) ( name : string ) = - mk_int_const ctx (Symbol.mk_string ctx name) + let mk_const_s ( ctx : context ) ( name : string ) = + mk_const ctx (Symbol.mk_string ctx name) let mk_mod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) @@ -1467,10 +1465,10 @@ struct let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_int_numeral_s ( ctx : context ) ( v : string ) = + let mk_numeral_s ( ctx : context ) ( v : string ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx))) - let mk_int_numeral_i ( ctx : context ) ( v : int ) = + let mk_numeral_i ( ctx : context ) ( v : int ) = expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx))) let mk_int2real ( ctx : context ) ( t : expr ) = @@ -1496,11 +1494,11 @@ struct let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) - let mk_real_const ( ctx : context ) ( name : Symbol.symbol ) = + let mk_const ( ctx : context ) ( name : Symbol.symbol ) = Expr.mk_const ctx name (mk_sort ctx) - let mk_real_const_s ( ctx : context ) ( name : string ) = - mk_real_const ctx (Symbol.mk_string ctx name) + let mk_const_s ( ctx : context ) ( name : string ) = + mk_const ctx (Symbol.mk_string ctx name) let mk_numeral_nd ( ctx : context ) ( num : int ) ( den : int) = if (den == 0) then diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 908b3023d..d7e179cd4 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -30,7 +30,6 @@ type context (** Create a context object *) val mk_context : (string * string) list -> context - (** Interaction logging for Z3 Note that this is a global, static log and if multiple Context objects are created, it logs the interaction with all of them. *) @@ -1117,10 +1116,10 @@ sig end (** Functions to manipulate arithmetic expressions *) -module rec Arithmetic : +module Arithmetic : sig (** Integer Arithmetic *) - module rec Integer : + module Integer : sig (** Create a new integer sort. *) val mk_sort : context -> Sort.sort @@ -1132,10 +1131,10 @@ sig val to_string : Expr.expr -> string (** Creates an integer constant. *) - val mk_int_const : context -> Symbol.symbol -> Expr.expr + val mk_const : context -> Symbol.symbol -> Expr.expr (** Creates an integer constant. *) - val mk_int_const_s : context -> string -> Expr.expr + val mk_const_s : context -> string -> Expr.expr (** Create an expression representing t1 mod t2. The arguments must have int type. *) @@ -1146,11 +1145,11 @@ sig val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create an integer numeral. *) - val mk_int_numeral_s : context -> string -> Expr.expr + val mk_numeral_s : context -> string -> Expr.expr (** Create an integer numeral. @return A Term with the given value and sort Integer *) - val mk_int_numeral_i : context -> int -> Expr.expr + val mk_numeral_i : context -> int -> Expr.expr (** Coerce an integer to a real. @@ -1174,7 +1173,7 @@ sig end (** Real Arithmetic *) - and Real : + module Real : sig (** Create a real sort. *) val mk_sort : context -> Sort.sort @@ -1193,10 +1192,10 @@ sig val to_string : Expr.expr-> string (** Creates a real constant. *) - val mk_real_const : context -> Symbol.symbol -> Expr.expr + val mk_const : context -> Symbol.symbol -> Expr.expr (** Creates a real constant. *) - val mk_real_const_s : context -> string -> Expr.expr + val mk_const_s : context -> string -> Expr.expr (** Create a real numeral from a fraction. @return A Term with rational value and sort Real @@ -1222,7 +1221,7 @@ sig end (** Algebraic Numbers *) - and AlgebraicNumber : + module AlgebraicNumber : sig (** Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^precision. @@ -1339,7 +1338,7 @@ sig end (** Functions to manipulate bit-vector expressions *) -and BitVector : +module BitVector : sig (** Create a new bit-vector sort. *) val mk_sort : context -> int -> Sort.sort diff --git a/src/api/ml/z3_rich.ml b/src/api/ml/z3_rich.ml index 052ca5e22..0c2f95b6b 100644 --- a/src/api/ml/z3_rich.ml +++ b/src/api/ml/z3_rich.ml @@ -1,4 +1,4 @@ -(** +\(** The Z3 ML/Ocaml Interface. Copyright (C) 2012 Microsoft Corporation @@ -11,7 +11,6 @@ open Z3enums let null = Z3native.mk_null() let is_null o = (Z3native.is_null o) - (* Internal types *) type z3_native_context = { m_n_ctx : Z3native.z3_context; m_n_obj_cnt: int; } type context = z3_native_context @@ -1679,12 +1678,12 @@ sig val mk_sort : context -> int_sort val get_int : int_num -> int val to_string : int_num -> string - val mk_int_const : context -> Symbol.symbol -> int_expr - val mk_int_const_s : context -> string -> int_expr + val mk_const : context -> Symbol.symbol -> int_expr + val mk_const_s : context -> string -> int_expr val mk_mod : context -> int_expr -> int_expr -> int_expr val mk_rem : context -> int_expr -> int_expr -> int_expr - val mk_int_numeral_s : context -> string -> int_num - val mk_int_numeral_i : context -> int -> int_num + val mk_numeral_s : context -> string -> int_num + val mk_numeral_i : context -> int -> int_num val mk_int2real : context -> int_expr -> Real.real_expr val mk_int2bv : context -> int -> int_expr -> BitVector.bitvec_expr end @@ -1709,8 +1708,8 @@ sig val get_denominator : rat_num -> Integer.int_num val to_decimal_string : rat_num -> int -> string val to_string : rat_num -> string - val mk_real_const : context -> Symbol.symbol -> real_expr - val mk_real_const_s : context -> string -> real_expr + val mk_const : context -> Symbol.symbol -> real_expr + val mk_const_s : context -> string -> real_expr val mk_numeral_nd : context -> int -> int -> rat_num val mk_numeral_s : context -> string -> rat_num val mk_numeral_i : context -> int -> rat_num @@ -1816,12 +1815,12 @@ end = struct val mk_sort : context -> int_sort val get_int : int_num -> int val to_string : int_num -> string - val mk_int_const : context -> Symbol.symbol -> int_expr - val mk_int_const_s : context -> string -> int_expr + val mk_const : context -> Symbol.symbol -> int_expr + val mk_const_s : context -> string -> int_expr val mk_mod : context -> int_expr -> int_expr -> int_expr val mk_rem : context -> int_expr -> int_expr -> int_expr - val mk_int_numeral_s : context -> string -> int_num - val mk_int_numeral_i : context -> int -> int_num + val mk_numeral_s : context -> string -> int_num + val mk_numeral_i : context -> int -> int_num val mk_int2real : context -> int_expr -> Real.real_expr val mk_int2bv : context -> int -> int_expr -> BitVector.bitvec_expr end = struct @@ -1884,11 +1883,11 @@ end = struct let to_string ( x : int_num ) = Z3native.get_numeral_string (ngnc x) (ngno x) - let mk_int_const ( ctx : context ) ( name : Symbol.symbol ) = + let mk_const ( ctx : context ) ( name : Symbol.symbol ) = IntExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with IntSort(ArithSort(s)) -> s))) - let mk_int_const_s ( ctx : context ) ( name : string ) = - mk_int_const ctx (Symbol.mk_string ctx name) + let mk_const_s ( ctx : context ) ( name : string ) = + mk_const ctx (Symbol.mk_string ctx name) let mk_mod ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = int_expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (egno t1) (egno t2)) @@ -1896,10 +1895,10 @@ end = struct let mk_rem ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = int_expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (egno t1) (egno t2)) - let mk_int_numeral_s ( ctx : context ) ( v : string ) = + let mk_numeral_s ( ctx : context ) ( v : string ) = int_num_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx))) - let mk_int_numeral_i ( ctx : context ) ( v : int ) = + let mk_numeral_i ( ctx : context ) ( v : int ) = int_num_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (sgno (mk_sort ctx))) let mk_int2real ( ctx : context ) ( t : int_expr ) = @@ -1930,8 +1929,8 @@ end = struct val get_denominator : rat_num -> Integer.int_num val to_decimal_string : rat_num -> int -> string val to_string : rat_num -> string - val mk_real_const : context -> Symbol.symbol -> real_expr - val mk_real_const_s : context -> string -> real_expr + val mk_const : context -> Symbol.symbol -> real_expr + val mk_const_s : context -> string -> real_expr val mk_numeral_nd : context -> int -> int -> rat_num val mk_numeral_s : context -> string -> rat_num val mk_numeral_i : context -> int -> rat_num @@ -2002,11 +2001,11 @@ end = struct let to_string ( x : rat_num ) = Z3native.get_numeral_string (ngnc x) (ngno x) - let mk_real_const ( ctx : context ) ( name : Symbol.symbol ) = + let mk_const ( ctx : context ) ( name : Symbol.symbol ) = RealExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with RealSort(ArithSort(s)) -> s))) - let mk_real_const_s ( ctx : context ) ( name : string ) = - mk_real_const ctx (Symbol.mk_string ctx name) + let mk_const_s ( ctx : context ) ( name : string ) = + mk_const ctx (Symbol.mk_string ctx name) let mk_numeral_nd ( ctx : context ) ( num : int ) ( den : int) = if (den == 0) then diff --git a/src/api/ml/z3_rich.mli b/src/api/ml/z3_rich.mli index 8b6681e11..f2ecd326d 100644 --- a/src/api/ml/z3_rich.mli +++ b/src/api/ml/z3_rich.mli @@ -34,7 +34,6 @@ type context (** Create a context object *) val mk_context : (string * string) list -> context - (** Interaction logging for Z3 Note that this is a global, static log and if multiple Context objects are created, it logs the interaction with all of them. *) @@ -1219,10 +1218,10 @@ sig val to_string : int_num -> string (** Creates an integer constant. *) - val mk_int_const : context -> Symbol.symbol -> int_expr + val mk_const : context -> Symbol.symbol -> int_expr (** Creates an integer constant. *) - val mk_int_const_s : context -> string -> int_expr + val mk_const_s : context -> string -> int_expr (** Create an expression representing t1 mod t2. The arguments must have int type. *) @@ -1233,11 +1232,11 @@ sig val mk_rem : context -> int_expr -> int_expr -> int_expr (** Create an integer numeral. *) - val mk_int_numeral_s : context -> string -> int_num + val mk_numeral_s : context -> string -> int_num (** Create an integer numeral. @return A Term with the given value and sort Integer *) - val mk_int_numeral_i : context -> int -> int_num + val mk_numeral_i : context -> int -> int_num (** Coerce an integer to a real. @@ -1291,10 +1290,10 @@ sig val to_string : rat_num -> string (** Creates a real constant. *) - val mk_real_const : context -> Symbol.symbol -> real_expr + val mk_const : context -> Symbol.symbol -> real_expr (** Creates a real constant. *) - val mk_real_const_s : context -> string -> real_expr + val mk_const_s : context -> string -> real_expr (** Create a real numeral from a fraction. @return A Term with rational value and sort Real