From 0d4b4b30b1622cc732bdcfff5c1ead64928bbdbd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 02:58:06 -0700 Subject: [PATCH] change storage layout of .Net binding Z3_bool to byte to deal with uninitialized memory reads on larger allocation sizes. Bug introduced when switching from defining Z3_bool as int to the bool type from stdbool Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/api/api_arith.cpp | 6 ++---- src/api/dotnet/AST.cs | 2 +- src/api/dotnet/ASTMap.cs | 2 +- src/api/dotnet/BitVecNum.cs | 8 ++++---- src/api/dotnet/Context.cs | 20 +++++++++++--------- src/api/dotnet/Expr.cs | 21 ++++++++++----------- src/api/dotnet/FPNum.cs | 24 ++++++++++++------------ src/api/dotnet/FiniteDomainNum.cs | 8 ++++---- src/api/dotnet/FuncDecl.cs | 2 +- src/api/dotnet/Global.cs | 4 ++-- src/api/dotnet/Goal.cs | 8 ++++---- src/api/dotnet/IntNum.cs | 8 ++++---- src/api/dotnet/Model.cs | 4 ++-- src/api/dotnet/Params.cs | 4 ++-- src/api/dotnet/Quantifier.cs | 12 ++++++------ src/api/dotnet/Sort.cs | 2 +- src/api/dotnet/Statistics.cs | 4 ++-- src/api/java/Expr.java | 4 ++-- src/api/python/z3/z3.py | 2 +- src/api/z3_api.h | 4 ++-- 21 files changed, 75 insertions(+), 76 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 4452ae613..b082c96e1 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -73,7 +73,7 @@ Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctype # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', - FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'bool', SYMBOL : 'IntPtr', + FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr', PRINT_MODE : 'uint', ERROR_CODE : 'uint' } # Mapping to Java types diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 524d9393d..f245dfd18 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -119,11 +119,9 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { + Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { LOG_Z3_is_algebraic_number(c, a); - int r = mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? 1 : 0; - //IF_VERBOSE(10, verbose_stream() << r << "\n"); - return r; + return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? Z3_TRUE : Z3_FALSE; } Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) { diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index 64ec88d09..2460c50f0 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -43,7 +43,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject)); + 0 != Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 9dcb3ef82..f7c1c5914 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -37,7 +37,7 @@ namespace Microsoft.Z3 { Contract.Requires(k != null); - return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); + return 0 != Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); } /// diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs index c6055db14..66054761a 100644 --- a/src/api/dotnet/BitVecNum.cs +++ b/src/api/dotnet/BitVecNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ba76ae7eb..325758263 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -1963,7 +1963,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(t); - return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed))); + return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0))); } /// @@ -1980,7 +1980,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); + return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0))); } /// @@ -2031,7 +2031,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); + return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0))); } /// @@ -2080,7 +2080,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); + return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0))); } /// @@ -3135,7 +3135,9 @@ namespace Microsoft.Z3 public BitVecNum MkBV(bool[] bits) { Contract.Ensures(Contract.Result() != null); - return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, bits)); + byte[] _bits = new byte[bits.Length]; + for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0); + return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits)); } @@ -4184,7 +4186,7 @@ namespace Microsoft.Z3 public FPNum MkFPInf(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative)); + return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); } /// @@ -4195,7 +4197,7 @@ namespace Microsoft.Z3 public FPNum MkFPZero(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative)); + return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); } /// @@ -4241,7 +4243,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } /// @@ -4254,7 +4256,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } /// diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 942baffab..849d1af79 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -179,7 +179,7 @@ namespace Microsoft.Z3 /// public bool IsNumeral { - get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) ; } + get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; } } /// @@ -188,7 +188,7 @@ namespace Microsoft.Z3 /// True if the term is well-sorted, false otherwise. public bool IsWellSorted { - get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) ; } + get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; } } /// @@ -256,7 +256,7 @@ namespace Microsoft.Z3 return (IsExpr && Native.Z3_is_eq_sort(Context.nCtx, Native.Z3_mk_bool_sort(Context.nCtx), - Native.Z3_get_sort(Context.nCtx, NativeObject)) ); + Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0); } } @@ -423,7 +423,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) && + return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_ARRAY_SORT); } @@ -789,7 +789,7 @@ namespace Microsoft.Z3 /// Check whether expression is a string constant. /// /// a Boolean - public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject); } } + public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject) != 0; } } /// /// Retrieve string corresponding to string constant. @@ -1336,7 +1336,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) && + return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_RELATION_SORT); } @@ -1458,7 +1458,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) && + return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); } } @@ -1789,7 +1789,7 @@ namespace Microsoft.Z3 [Pure] internal override void CheckNativeObject(IntPtr obj) { - if (Native.Z3_is_app(Context.nCtx, obj) == false && + if (Native.Z3_is_app(Context.nCtx, obj) == 0 && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST) throw new Z3Exception("Underlying object is not a term"); @@ -1822,11 +1822,10 @@ namespace Microsoft.Z3 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); - if ( // Z3_sort_kind.Z3_REAL_SORT == sk && - 0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? + if (0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); - if (Native.Z3_is_numeral_ast(ctx.nCtx, obj)) + if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0) { switch (sk) diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index 4a2575fe4..b6d349149 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -52,7 +52,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Sign is not a Boolean value"); return res != 0; } @@ -86,7 +86,7 @@ namespace Microsoft.Z3 get { UInt64 result = 0; - if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == false) + if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return result; } @@ -111,7 +111,7 @@ namespace Microsoft.Z3 /// public string Exponent(bool biased = true) { - return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased); + return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0)); } /// @@ -120,7 +120,7 @@ namespace Microsoft.Z3 public Int64 ExponentInt64(bool biased = true) { Int64 result = 0; - if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased) == false) + if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, (byte)(biased? 1 : 0)) == 0) throw new Z3Exception("Exponent is not a 64 bit integer"); return result; } @@ -133,43 +133,43 @@ namespace Microsoft.Z3 /// public BitVecExpr ExponentBV(bool biased = true) { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased)); + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0))); } /// /// Indicates whether the numeral is a NaN. /// - public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) ; } } + public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is a +oo or -oo. /// - public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) ; } } + public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is +zero or -zero. /// - public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) ; } } + public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is normal. /// - public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) ; } } + public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is subnormal. /// - public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) ; } } + public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is positive. /// - public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) ; } } + public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is negative. /// - public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) ; } } + public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } } #region Internal internal FPNum(Context ctx, IntPtr obj) diff --git a/src/api/dotnet/FiniteDomainNum.cs b/src/api/dotnet/FiniteDomainNum.cs index fb51e1014..52c0af8bd 100644 --- a/src/api/dotnet/FiniteDomainNum.cs +++ b/src/api/dotnet/FiniteDomainNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 39ddfad83..0587a2276 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -38,7 +38,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject)); + Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); } /// diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs index f242003a8..17963b33d 100644 --- a/src/api/dotnet/Global.cs +++ b/src/api/dotnet/Global.cs @@ -65,7 +65,7 @@ namespace Microsoft.Z3 public static string GetParameter(string id) { IntPtr t; - if (Native.Z3_global_param_get(id, out t) == false) + if (Native.Z3_global_param_get(id, out t) == 0) return null; else return Marshal.PtrToStringAnsi(t); @@ -91,7 +91,7 @@ namespace Microsoft.Z3 /// all contexts globally. public static void ToggleWarningMessages(bool enabled) { - Native.Z3_toggle_warning_messages(enabled); + Native.Z3_toggle_warning_messages((byte)(enabled ? 1 : 0)); } /// diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index a5e35fcd5..ef2e9a5da 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -103,7 +103,7 @@ namespace Microsoft.Z3 /// public bool Inconsistent { - get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) ; } + get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; } } /// @@ -163,7 +163,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedSat { - get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) ; } + get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; } } /// @@ -171,7 +171,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedUnsat { - get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) ; } + get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } } /// @@ -251,7 +251,7 @@ namespace Microsoft.Z3 internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } internal Goal(Context ctx, bool models, bool unsatCores, bool proofs) - : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models), (unsatCores), (proofs))) + : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0))) { Contract.Requires(ctx != null); } diff --git a/src/api/dotnet/IntNum.cs b/src/api/dotnet/IntNum.cs index 78fee44f4..64fd78ad2 100644 --- a/src/api/dotnet/IntNum.cs +++ b/src/api/dotnet/IntNum.cs @@ -49,7 +49,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -63,7 +63,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int"); return res; } @@ -77,7 +77,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -91,7 +91,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index 2c6d12dc0..96f62c9fb 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -86,7 +86,7 @@ namespace Microsoft.Z3 return null; else { - if (Native.Z3_is_as_array(Context.nCtx, n) == false) + if (Native.Z3_is_as_array(Context.nCtx, n) == 0) throw new Z3Exception("Argument was not an array constant"); IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n); return FuncInterp(new FuncDecl(Context, fd)); @@ -227,7 +227,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); IntPtr v = IntPtr.Zero; - if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion), ref v) == false) + if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0) throw new ModelEvaluationFailedException(); else return Expr.Create(Context, v); diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index eeda55755..f0f28d8d3 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -35,7 +35,7 @@ namespace Microsoft.Z3 { Contract.Requires(name != null); - Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value)); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (byte)(value ? 1 : 0)); return this; } @@ -90,7 +90,7 @@ namespace Microsoft.Z3 /// public Params Add(string name, bool value) { - Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value)); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (byte)(value ? 1 : 0)); return this; } diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index d729f7424..d13ca4003 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// public bool IsUniversal { - get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } + get { return 0 != Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } } /// @@ -41,7 +41,7 @@ namespace Microsoft.Z3 /// public bool IsExistential { - get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } + get { return 0 != Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } } /// @@ -193,7 +193,7 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) , weight, + NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight, AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(sorts), AST.ArrayToNative(sorts), Symbol.ArrayToNative(names), @@ -201,7 +201,7 @@ namespace Microsoft.Z3 } else { - NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall), weight, + NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (byte)(isForall ? 1 : 0), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), @@ -229,14 +229,14 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) , weight, + NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight, AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), body.NativeObject); } else { - NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall), weight, + NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (byte)(isForall ? 1 : 0), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index 66acc5c0f..e32fd1eb3 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -41,7 +41,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context == b.Context && - Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject)); + 0 != Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index 6708035bc..c94af625c 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -134,9 +134,9 @@ namespace Microsoft.Z3 { Entry e; string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i); - if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) ) + if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0) e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i)); - else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) ) + else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0) e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i)); else throw new Z3Exception("Unknown data entry value"); diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 75ec9aa75..db5c33e79 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -275,7 +275,7 @@ public class Expr extends AST **/ public boolean isAlgebraicNumber() { - return 0 != Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); + return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); } /** @@ -2108,7 +2108,7 @@ public class Expr extends AST Z3_sort_kind sk = Z3_sort_kind .fromInt(Native.getSortKind(ctx.nCtx(), s)); - if (Native.isAlgebraicNumber(ctx.nCtx(), obj) != 0) // is this a numeral ast? + if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); if (Native.isNumeralAst(ctx.nCtx(), obj)) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f6a5b1950..10198fcc5 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2455,7 +2455,7 @@ def _is_numeral(ctx, a): return Z3_is_numeral_ast(ctx.ref(), a) def _is_algebraic(ctx, a): - return 0 != Z3_is_algebraic_number(ctx.ref(), a) + return Z3_is_algebraic_number(ctx.ref(), a) def is_int_value(a): """Return `True` if `a` is an integer value of sort Int. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 74f0fd254..7e12f2fa7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4397,9 +4397,9 @@ extern "C" { /** \brief Return true if the given AST is a real algebraic number. - def_API('Z3_is_algebraic_number', INT, (_in(CONTEXT), _in(AST))) + def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST))) */ - int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); + Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); /** \brief Convert an \c ast into an \c APP_AST. This is just type casting.