mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

workaround non-deterministic behavior of is_irrational_numeral test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-29 18:16:32 -07:00
parent 481b177d47
commit f1d27cd487
20 changed files with 77 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/update_api.py
View file

@ -73,7 +73,7 @@ Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctype
# Mapping to .NET types # Mapping to .NET types
Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr', FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'bool', SYMBOL : 'IntPtr',
PRINT_MODE : 'uint', ERROR_CODE : 'uint' } PRINT_MODE : 'uint', ERROR_CODE : 'uint' }
# Mapping to Java types # Mapping to Java types

6
src/api/api_arith.cpp
View file

@ -120,12 +120,8 @@ extern "C" {
} }
Z3_bool 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) {
Z3_TRY;
LOG_Z3_is_algebraic_number(c, a); LOG_Z3_is_algebraic_number(c, a);
RESET_ERROR_CODE(); return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a));
expr * e = to_expr(a);
return mk_c(c)->autil().is_irrational_algebraic_numeral(e);
Z3_CATCH_RETURN(Z3_FALSE);
} }
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) { Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) {

2
src/api/dotnet/AST.cs
View file

@ -43,7 +43,7 @@ namespace Microsoft.Z3
(!Object.ReferenceEquals(a, null) && (!Object.ReferenceEquals(a, null) &&
!Object.ReferenceEquals(b, null) && !Object.ReferenceEquals(b, null) &&
a.Context.nCtx == b.Context.nCtx && 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));
} }
/// <summary> /// <summary>

2
src/api/dotnet/ASTMap.cs
View file

@ -37,7 +37,7 @@ namespace Microsoft.Z3
{ {
Contract.Requires(k != null); Contract.Requires(k != null);
return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0; return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject);
} }
/// <summary> /// <summary>

8
src/api/dotnet/BitVecNum.cs
View file

@ -39,7 +39,7 @@ namespace Microsoft.Z3
get get
{ {
UInt64 res = 0; UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not a 64 bit unsigned"); throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res; return res;
} }
@ -53,7 +53,7 @@ namespace Microsoft.Z3
get get
{ {
int res = 0; int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not an int"); throw new Z3Exception("Numeral is not an int");
return res; return res;
} }
@ -67,7 +67,7 @@ namespace Microsoft.Z3
get get
{ {
Int64 res = 0; Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not an int64"); throw new Z3Exception("Numeral is not an int64");
return res; return res;
} }
@ -81,7 +81,7 @@ namespace Microsoft.Z3
get get
{ {
uint res = 0; uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not a uint"); throw new Z3Exception("Numeral is not a uint");
return res; return res;
} }

20
src/api/dotnet/Context.cs
View file

@ -1963,7 +1963,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<IntExpr>() != null); Contract.Ensures(Contract.Result<IntExpr>() != null);
CheckContextMatch(t); CheckContextMatch(t);
return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0)); return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed)));
} }
/// <summary> /// <summary>
@ -1980,7 +1980,7 @@ namespace Microsoft.Z3
CheckContextMatch(t1); CheckContextMatch(t1);
CheckContextMatch(t2); CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
} }
/// <summary> /// <summary>
@ -2031,7 +2031,7 @@ namespace Microsoft.Z3
CheckContextMatch(t1); CheckContextMatch(t1);
CheckContextMatch(t2); CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
} }
/// <summary> /// <summary>
@ -2080,7 +2080,7 @@ namespace Microsoft.Z3
CheckContextMatch(t1); CheckContextMatch(t1);
CheckContextMatch(t2); CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
} }
/// <summary> /// <summary>
@ -3135,9 +3135,7 @@ namespace Microsoft.Z3
public BitVecNum MkBV(bool[] bits) public BitVecNum MkBV(bool[] bits)
{ {
Contract.Ensures(Contract.Result<BitVecNum>() != null); Contract.Ensures(Contract.Result<BitVecNum>() != null);
int[] _bits = new int[bits.Length]; return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, bits));
for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0;
return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
} }
@ -4186,7 +4184,7 @@ namespace Microsoft.Z3
public FPNum MkFPInf(FPSort s, bool negative) public FPNum MkFPInf(FPSort s, bool negative)
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0)); return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative));
} }
/// <summary> /// <summary>
@ -4197,7 +4195,7 @@ namespace Microsoft.Z3
public FPNum MkFPZero(FPSort s, bool negative) public FPNum MkFPZero(FPSort s, bool negative)
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0)); return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative));
} }
/// <summary> /// <summary>
@ -4243,7 +4241,7 @@ namespace Microsoft.Z3
public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn, exp, sig, s.NativeObject));
} }
/// <summary> /// <summary>
@ -4256,7 +4254,7 @@ namespace Microsoft.Z3
public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn, exp, sig, s.NativeObject));
} }
/// <summary> /// <summary>

22
src/api/dotnet/Expr.cs
View file

@ -179,7 +179,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool IsNumeral public bool IsNumeral
{ {
get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) ; }
} }
/// <summary> /// <summary>
@ -188,7 +188,7 @@ namespace Microsoft.Z3
/// <returns>True if the term is well-sorted, false otherwise.</returns> /// <returns>True if the term is well-sorted, false otherwise.</returns>
public bool IsWellSorted public bool IsWellSorted
{ {
get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) ; }
} }
/// <summary> /// <summary>
@ -239,7 +239,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool IsAlgebraicNumber public bool IsAlgebraicNumber
{ {
get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); }
} }
#endregion #endregion
@ -256,7 +256,7 @@ namespace Microsoft.Z3
return (IsExpr && return (IsExpr &&
Native.Z3_is_eq_sort(Context.nCtx, Native.Z3_is_eq_sort(Context.nCtx,
Native.Z3_mk_bool_sort(Context.nCtx), Native.Z3_mk_bool_sort(Context.nCtx),
Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0); Native.Z3_get_sort(Context.nCtx, NativeObject)) );
} }
} }
@ -423,7 +423,7 @@ namespace Microsoft.Z3
{ {
get get
{ {
return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && return (Native.Z3_is_app(Context.nCtx, NativeObject) &&
(Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
== Z3_sort_kind.Z3_ARRAY_SORT); == Z3_sort_kind.Z3_ARRAY_SORT);
} }
@ -789,7 +789,7 @@ namespace Microsoft.Z3
/// Check whether expression is a string constant. /// Check whether expression is a string constant.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <returns>a Boolean</returns>
public bool IsString { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } } public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject); } }
/// <summary> /// <summary>
/// Retrieve string corresponding to string constant. /// Retrieve string corresponding to string constant.
@ -1336,7 +1336,7 @@ namespace Microsoft.Z3
{ {
get get
{ {
return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && return (Native.Z3_is_app(Context.nCtx, NativeObject) &&
Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
== (uint)Z3_sort_kind.Z3_RELATION_SORT); == (uint)Z3_sort_kind.Z3_RELATION_SORT);
} }
@ -1458,7 +1458,7 @@ namespace Microsoft.Z3
{ {
get get
{ {
return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && return (Native.Z3_is_app(Context.nCtx, NativeObject) &&
Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
} }
} }
@ -1822,11 +1822,13 @@ namespace Microsoft.Z3
IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj); IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast? if (Z3_sort_kind.Z3_REAL_SORT == sk &&
Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast?
return new AlgebraicNum(ctx, obj); return new AlgebraicNum(ctx, obj);
if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0) if (Native.Z3_is_numeral_ast(ctx.nCtx, obj))
{ {
switch (sk) switch (sk)
{ {
case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj); case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);

24
src/api/dotnet/FPNum.cs
View file

@ -52,7 +52,7 @@ namespace Microsoft.Z3
get get
{ {
int res = 0; int res = 0;
if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Sign is not a Boolean value"); throw new Z3Exception("Sign is not a Boolean value");
return res != 0; return res != 0;
} }
@ -86,7 +86,7 @@ namespace Microsoft.Z3
get get
{ {
UInt64 result = 0; UInt64 result = 0;
if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == false)
throw new Z3Exception("Significand is not a 64 bit unsigned integer"); throw new Z3Exception("Significand is not a 64 bit unsigned integer");
return result; return result;
} }
@ -111,7 +111,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public string Exponent(bool biased = true) public string Exponent(bool biased = true)
{ {
return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0); return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased);
} }
/// <summary> /// <summary>
@ -120,7 +120,7 @@ namespace Microsoft.Z3
public Int64 ExponentInt64(bool biased = true) public Int64 ExponentInt64(bool biased = true)
{ {
Int64 result = 0; Int64 result = 0;
if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0) if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased) == false)
throw new Z3Exception("Exponent is not a 64 bit integer"); throw new Z3Exception("Exponent is not a 64 bit integer");
return result; return result;
} }
@ -133,43 +133,43 @@ namespace Microsoft.Z3
/// </remarks> /// </remarks>
public BitVecExpr ExponentBV(bool biased = true) public BitVecExpr ExponentBV(bool biased = true)
{ {
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0)); return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased));
} }
/// <summary> /// <summary>
/// Indicates whether the numeral is a NaN. /// Indicates whether the numeral is a NaN.
/// </summary> /// </summary>
public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) ; } }
/// <summary> /// <summary>
/// Indicates whether the numeral is a +oo or -oo. /// Indicates whether the numeral is a +oo or -oo.
/// </summary> /// </summary>
public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) ; } }
/// <summary> /// <summary>
/// Indicates whether the numeral is +zero or -zero. /// Indicates whether the numeral is +zero or -zero.
/// </summary> /// </summary>
public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } } public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) ; } }
/// <summary> /// <summary>
/// Indicates whether the numeral is normal. /// Indicates whether the numeral is normal.
/// </summary> /// </summary>
public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) ; } }
/// <summary> /// <summary>
/// Indicates whether the numeral is subnormal. /// Indicates whether the numeral is subnormal.
/// </summary> /// </summary>
public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } } public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) ; } }
/// <summary> /// <summary>
/// Indicates whether the numeral is positive. /// Indicates whether the numeral is positive.
/// </summary> /// </summary>
public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) ; } }
/// <summary> /// <summary>
/// Indicates whether the numeral is negative. /// Indicates whether the numeral is negative.
/// </summary> /// </summary>
public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } } public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) ; } }
#region Internal #region Internal
internal FPNum(Context ctx, IntPtr obj) internal FPNum(Context ctx, IntPtr obj)

8
src/api/dotnet/FiniteDomainNum.cs
View file

@ -39,7 +39,7 @@ namespace Microsoft.Z3
get get
{ {
UInt64 res = 0; UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not a 64 bit unsigned"); throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res; return res;
} }
@ -53,7 +53,7 @@ namespace Microsoft.Z3
get get
{ {
int res = 0; int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not an int"); throw new Z3Exception("Numeral is not an int");
return res; return res;
} }
@ -67,7 +67,7 @@ namespace Microsoft.Z3
get get
{ {
Int64 res = 0; Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not an int64"); throw new Z3Exception("Numeral is not an int64");
return res; return res;
} }
@ -81,7 +81,7 @@ namespace Microsoft.Z3
get get
{ {
uint res = 0; uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not a uint"); throw new Z3Exception("Numeral is not a uint");
return res; return res;
} }

2
src/api/dotnet/FuncDecl.cs
View file

@ -38,7 +38,7 @@ namespace Microsoft.Z3
(!Object.ReferenceEquals(a, null) && (!Object.ReferenceEquals(a, null) &&
!Object.ReferenceEquals(b, null) && !Object.ReferenceEquals(b, null) &&
a.Context.nCtx == b.Context.nCtx && a.Context.nCtx == b.Context.nCtx &&
Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject));
} }
/// <summary> /// <summary>

4
src/api/dotnet/Global.cs
View file

@ -65,7 +65,7 @@ namespace Microsoft.Z3
public static string GetParameter(string id) public static string GetParameter(string id)
{ {
IntPtr t; IntPtr t;
if (Native.Z3_global_param_get(id, out t) == 0) if (Native.Z3_global_param_get(id, out t) == false)
return null; return null;
else else
return Marshal.PtrToStringAnsi(t); return Marshal.PtrToStringAnsi(t);
@ -91,7 +91,7 @@ namespace Microsoft.Z3
/// all contexts globally.</remarks> /// all contexts globally.</remarks>
public static void ToggleWarningMessages(bool enabled) public static void ToggleWarningMessages(bool enabled)
{ {
Native.Z3_toggle_warning_messages((enabled) ? 1 : 0); Native.Z3_toggle_warning_messages(enabled);
} }
/// <summary> /// <summary>

8
src/api/dotnet/Goal.cs
View file

@ -103,7 +103,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool Inconsistent public bool Inconsistent
{ {
get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) ; }
} }
/// <summary> /// <summary>
@ -163,7 +163,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool IsDecidedSat public bool IsDecidedSat
{ {
get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) ; }
} }
/// <summary> /// <summary>
@ -171,7 +171,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool IsDecidedUnsat public bool IsDecidedUnsat
{ {
get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) ; }
} }
/// <summary> /// <summary>
@ -251,7 +251,7 @@ namespace Microsoft.Z3
internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
internal Goal(Context ctx, bool models, bool unsatCores, bool proofs) internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
: base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0)) : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models), (unsatCores), (proofs)))
{ {
Contract.Requires(ctx != null); Contract.Requires(ctx != null);
} }

8
src/api/dotnet/IntNum.cs
View file

@ -49,7 +49,7 @@ namespace Microsoft.Z3
get get
{ {
UInt64 res = 0; UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not a 64 bit unsigned"); throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res; return res;
} }
@ -63,7 +63,7 @@ namespace Microsoft.Z3
get get
{ {
int res = 0; int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not an int"); throw new Z3Exception("Numeral is not an int");
return res; return res;
} }
@ -77,7 +77,7 @@ namespace Microsoft.Z3
get get
{ {
Int64 res = 0; Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not an int64"); throw new Z3Exception("Numeral is not an int64");
return res; return res;
} }
@ -91,7 +91,7 @@ namespace Microsoft.Z3
get get
{ {
uint res = 0; uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
throw new Z3Exception("Numeral is not a uint"); throw new Z3Exception("Numeral is not a uint");
return res; return res;
} }

4
src/api/dotnet/Model.cs
View file

@ -86,7 +86,7 @@ namespace Microsoft.Z3
return null; return null;
else else
{ {
if (Native.Z3_is_as_array(Context.nCtx, n) == 0) if (Native.Z3_is_as_array(Context.nCtx, n) == false)
throw new Z3Exception("Argument was not an array constant"); throw new Z3Exception("Argument was not an array constant");
IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n); IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
return FuncInterp(new FuncDecl(Context, fd)); return FuncInterp(new FuncDecl(Context, fd));
@ -227,7 +227,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
IntPtr v = IntPtr.Zero; IntPtr v = IntPtr.Zero;
if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0) if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion), ref v) == false)
throw new ModelEvaluationFailedException(); throw new ModelEvaluationFailedException();
else else
return Expr.Create(Context, v); return Expr.Create(Context, v);

4
src/api/dotnet/Params.cs
View file

@ -35,7 +35,7 @@ namespace Microsoft.Z3
{ {
Contract.Requires(name != null); Contract.Requires(name != null);
Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0); Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value));
return this; return this;
} }
@ -90,7 +90,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public Params Add(string name, bool value) public Params Add(string name, bool value)
{ {
Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0); Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value));
return this; return this;
} }

12
src/api/dotnet/Quantifier.cs
View file

@ -33,7 +33,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool IsUniversal public bool IsUniversal
{ {
get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); }
} }
/// <summary> /// <summary>
@ -41,7 +41,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool IsExistential public bool IsExistential
{ {
get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject) != 0; } get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); }
} }
/// <summary> /// <summary>
@ -193,7 +193,7 @@ namespace Microsoft.Z3
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight, NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) , weight,
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(sorts), AST.ArrayToNative(sorts), AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
Symbol.ArrayToNative(names), Symbol.ArrayToNative(names),
@ -201,7 +201,7 @@ namespace Microsoft.Z3
} }
else else
{ {
NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight, NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall), weight,
AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
@ -229,14 +229,14 @@ namespace Microsoft.Z3
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight, NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) , weight,
AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(bound), AST.ArrayToNative(bound),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
body.NativeObject); body.NativeObject);
} }
else else
{ {
NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight, NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall), weight,
AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(bound), AST.ArrayToNative(bound),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),

2
src/api/dotnet/Sort.cs
View file

@ -41,7 +41,7 @@ namespace Microsoft.Z3
(!Object.ReferenceEquals(a, null) && (!Object.ReferenceEquals(a, null) &&
!Object.ReferenceEquals(b, null) && !Object.ReferenceEquals(b, null) &&
a.Context == b.Context && 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));
} }
/// <summary> /// <summary>

4
src/api/dotnet/Statistics.cs
View file

@ -134,9 +134,9 @@ namespace Microsoft.Z3
{ {
Entry e; Entry e;
string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i); string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0) if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) )
e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i)); 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) != 0) else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) )
e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i)); e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i));
else else
throw new Z3Exception("Unknown data entry value"); throw new Z3Exception("Unknown data entry value");

7
src/ast/arith_decl_plugin.cpp
View file

@ -638,6 +638,11 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
return true; return true;
} }
bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const {
return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM);
}
#define IS_INT_EXPR_DEPTH_LIMIT 100 #define IS_INT_EXPR_DEPTH_LIMIT 100
bool arith_recognizers::is_int_expr(expr const *e) const { bool arith_recognizers::is_int_expr(expr const *e) const {
if (is_int(e)) return true; if (is_int(e)) return true;
@ -678,7 +683,7 @@ void arith_util::init_plugin() {
m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid)); m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
} }
bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) { bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) {
if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM)) if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM))
return false; return false;
am().set(val, to_irrational_algebraic_numeral(n)); am().set(val, to_irrational_algebraic_numeral(n));

5
src/ast/arith_decl_plugin.h
View file

@ -229,7 +229,7 @@ public:
family_id get_family_id() const { return m_afid; } family_id get_family_id() const { return m_afid; }
bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; } bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; }
bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); } bool is_irrational_algebraic_numeral(expr const * n) const;
bool is_numeral(expr const * n, rational & val, bool & is_int) const; bool is_numeral(expr const * n, rational & val, bool & is_int) const;
bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); } bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); } bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); }
@ -338,8 +338,7 @@ public:
return plugin().am(); return plugin().am();
} }
bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); } bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val);
bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n); algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); } sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }