From cbda38ee80358203fb786dc3bd1972428f1f7815 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Dec 2015 17:01:52 +0000 Subject: [PATCH] Added finite domain expressions and numerals to the .NET, Java, and Python APIs. Relates to #318 --- examples/dotnet/Program.cs | 15 ++-- examples/java/JavaExample.java | 9 ++- src/api/dotnet/Expr.cs | 2 + src/api/dotnet/FiniteDomainExpr.cs | 38 ++++++++++ src/api/dotnet/FiniteDomainNum.cs | 115 +++++++++++++++++++++++++++++ src/api/dotnet/Microsoft.Z3.csproj | 2 + src/api/java/Expr.java | 4 + src/api/java/FiniteDomainExpr.java | 33 +++++++++ src/api/java/FiniteDomainNum.java | 76 +++++++++++++++++++ src/api/python/z3.py | 98 +++++++++++++++++++++++- 10 files changed, 380 insertions(+), 12 deletions(-) create mode 100644 src/api/dotnet/FiniteDomainExpr.cs create mode 100644 src/api/dotnet/FiniteDomainNum.cs create mode 100644 src/api/java/FiniteDomainExpr.java create mode 100644 src/api/java/FiniteDomainNum.java diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index afb3e8875..26c081ee2 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2055,15 +2055,16 @@ namespace test_mapi { Console.WriteLine("FiniteDomainExample"); - var s = ctx.MkFiniteDomainSort("S", 10); - var t = ctx.MkFiniteDomainSort("T", 10); - var s1 = ctx.MkNumeral(1, s); - var t1 = ctx.MkNumeral(1, t); - Console.WriteLine("{0}", s); - Console.WriteLine("{0}", t); + FiniteDomainSort s = ctx.MkFiniteDomainSort("S", 10); + FiniteDomainSort t = ctx.MkFiniteDomainSort("T", 10); + FiniteDomainNum s1 = (FiniteDomainNum)ctx.MkNumeral(1, s); + FiniteDomainNum t1 = (FiniteDomainNum)ctx.MkNumeral(1, t); + Console.WriteLine("{0} of size {1}", s, s.Size); + Console.WriteLine("{0} of size {1}", t, t.Size); Console.WriteLine("{0}", s1); - Console.WriteLine("{0}", ctx.MkNumeral(2, s)); Console.WriteLine("{0}", t1); + Console.WriteLine("{0}", s1.Int); + Console.WriteLine("{0}", t1.Int); // But you cannot mix numerals of different sorts // even if the size of their domains are the same: // Console.WriteLine("{0}", ctx.MkEq(s1, t1)); diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index e27bab3bf..74e94617d 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2163,13 +2163,14 @@ class JavaExample FiniteDomainSort s = ctx.mkFiniteDomainSort("S", 10); FiniteDomainSort t = ctx.mkFiniteDomainSort("T", 10); - Expr s1 = ctx.mkNumeral(1, s); - Expr t1 = ctx.mkNumeral(1, t); + FiniteDomainNum s1 = (FiniteDomainNum)ctx.mkNumeral(1, s); + FiniteDomainNum t1 = (FiniteDomainNum)ctx.mkNumeral(1, t); System.out.println(s); System.out.println(t); - System.out.println(s1); - System.out.println(ctx.mkNumeral(2, s)); + System.out.println(s1); System.out.println(t1); + System.out.println(s1.getInt()); + System.out.println(t1.getInt()); // But you cannot mix numerals of different sorts // even if the size of their domains are the same: // System.out.println(ctx.mkEq(s1, t1)); diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index a49b31f70..3b918d76d 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1815,6 +1815,7 @@ namespace Microsoft.Z3 case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj); case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj); case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj); + case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainNum(ctx, obj); } } @@ -1828,6 +1829,7 @@ namespace Microsoft.Z3 case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj); case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj); + case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj); } return new Expr(ctx, obj); diff --git a/src/api/dotnet/FiniteDomainExpr.cs b/src/api/dotnet/FiniteDomainExpr.cs new file mode 100644 index 000000000..59ccb9f32 --- /dev/null +++ b/src/api/dotnet/FiniteDomainExpr.cs @@ -0,0 +1,38 @@ +/*++ +Copyright () 2012 Microsoft Corporation + +Module Name: + + FiniteDomainExpr.cs + +Abstract: + + Z3 Managed API: Finite-domain Expressions + +Author: + + Christoph Wintersteiger (cwinter) 2015-12-02 + +Notes: + +--*/ +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// Finite-domain expressions + /// + public class FiniteDomainExpr : Expr + { + #region Internal + /// Constructor for DatatypeExpr + internal FiniteDomainExpr(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + #endregion + } +} diff --git a/src/api/dotnet/FiniteDomainNum.cs b/src/api/dotnet/FiniteDomainNum.cs new file mode 100644 index 000000000..52c0af8bd --- /dev/null +++ b/src/api/dotnet/FiniteDomainNum.cs @@ -0,0 +1,115 @@ +/*++ +Copyright () 2012 Microsoft Corporation + +Module Name: + + FiniteDomainNum.cs + +Abstract: + + Z3 Managed API: Finite-domain Numerals + +Author: + + Christoph Wintersteiger (cwinter) 2015-12-02 + +Notes: + +--*/ +using System; +using System.Diagnostics.Contracts; + +#if !FRAMEWORK_LT_4 +using System.Numerics; +#endif + +namespace Microsoft.Z3 +{ + /// + /// Finite-domain numerals + /// + [ContractVerification(true)] + public class FiniteDomainNum : FiniteDomainExpr + { + /// + /// Retrieve the 64-bit unsigned integer value. + /// + public UInt64 UInt64 + { + get + { + UInt64 res = 0; + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) + throw new Z3Exception("Numeral is not a 64 bit unsigned"); + return res; + } + } + + /// + /// Retrieve the int value. + /// + public int Int + { + get + { + int res = 0; + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) + throw new Z3Exception("Numeral is not an int"); + return res; + } + } + + /// + /// Retrieve the 64-bit int value. + /// + public Int64 Int64 + { + get + { + Int64 res = 0; + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) + throw new Z3Exception("Numeral is not an int64"); + return res; + } + } + + /// + /// Retrieve the int value. + /// + public uint UInt + { + get + { + uint res = 0; + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) + throw new Z3Exception("Numeral is not a uint"); + return res; + } + } + +#if !FRAMEWORK_LT_4 + /// + /// Retrieve the BigInteger value. + /// + public BigInteger BigInteger + { + get + { + return BigInteger.Parse(this.ToString()); + } + } +#endif + + /// + /// Returns a string representation of the numeral. + /// + public override string ToString() + { + return Native.Z3_get_numeral_string(Context.nCtx, NativeObject); + } + + #region Internal + internal FiniteDomainNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + #endregion + } +} diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 937edb69d..a753e0193 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -342,6 +342,8 @@ + + diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index a326da52c..9c75888e2 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2165,6 +2165,8 @@ public class Expr extends AST return new FPNum(ctx, obj); case Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj); + case Z3_FINITE_DOMAIN_SORT: + return new FiniteDomainNum(ctx, obj); default: ; } } @@ -2187,6 +2189,8 @@ public class Expr extends AST return new FPExpr(ctx, obj); case Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj); + case Z3_FINITE_DOMAIN_SORT: + return new FiniteDomainExpr(ctx, obj); default: ; } diff --git a/src/api/java/FiniteDomainExpr.java b/src/api/java/FiniteDomainExpr.java new file mode 100644 index 000000000..f7d930758 --- /dev/null +++ b/src/api/java/FiniteDomainExpr.java @@ -0,0 +1,33 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FiniteDomainExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2015-12-02 + +Notes: + +**/ + +package com.microsoft.z3; + +/** + * Finite-domain expressions + **/ +public class FiniteDomainExpr extends Expr +{ + /** + * Constructor for FiniteDomainExpr + * @throws Z3Exception on error + **/ + FiniteDomainExpr(Context ctx, long obj) + { + super(ctx, obj); + } +} diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java new file mode 100644 index 000000000..79845c700 --- /dev/null +++ b/src/api/java/FiniteDomainNum.java @@ -0,0 +1,76 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FiniteDomainNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2015-12-02 + +Notes: + +**/ + +package com.microsoft.z3; + +import java.math.BigInteger; + +/** + * Finite-domain Numerals + **/ +public class FiniteDomainNum extends FiniteDomainExpr +{ + + FiniteDomainNum(Context ctx, long obj) + { + super(ctx, obj); + } + + /** + * Retrieve the int value. + **/ + public int getInt() + { + Native.IntPtr res = new Native.IntPtr(); + if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not an int"); + return res.value; + } + + /** + * Retrieve the 64-bit int value. + **/ + public long getInt64() + { + Native.LongPtr res = new Native.LongPtr(); + if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not an int64"); + return res.value; + } + + /** + * Retrieve the BigInteger value. + **/ + public BigInteger getBigInteger() + { + return new BigInteger(this.toString()); + } + + /** + * Returns a string representation of the numeral. + **/ + public String toString() + { + try + { + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); + } catch (Z3Exception e) + { + return "Z3Exception: " + e.getMessage(); + } + } +} diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 444c025e6..47aff82f5 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -912,6 +912,11 @@ def _to_expr_ref(a, ctx): return FPNumRef(a, ctx) else: return FPRef(a, ctx) + if sk == Z3_FINITE_DOMAIN_SORT: + if k == Z3_NUMERAL_AST: + return FiniteDomainNumRef(a, ctx) + else: + return FiniteDomainRef(a, ctx) if sk == Z3_ROUNDING_MODE_SORT: return FPRMRef(a, ctx) return ExprRef(a, ctx) @@ -6395,7 +6400,7 @@ class Fixedpoint(Z3PPObject): ######################################### # -# Finite domain sorts +# Finite domains # ######################################### @@ -6415,6 +6420,97 @@ def FiniteDomainSort(name, sz, ctx=None): ctx = _get_ctx(ctx) return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx) +def is_finite_domain_sort(s): + """Return True if `s` is a Z3 finite-domain sort. + + >>> is_finite_domain_sort(FiniteDomainSort("S", 100)) + True + >>> is_finite_domain_sort(IntSort()) + False + """ + return isinstance(s, FiniteDomainSortRef) + + +class FiniteDomainRef(ExprRef): + """Finite-domain expressions.""" + + def sort(self): + """Return the sort of the finite-domain expression `self`.""" + return FiniteDomainSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) + + def as_string(self): + """Return a Z3 floating point expression as a Python string.""" + return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) + +def is_finite_domain(a): + """Return `True` if `a` is a Z3 finite-domain expression. + + >>> s = FiniteDomainSort("S", 100) + >>> b = Const('b', s) + >>> is_finite_domain(b) + True + >>> is_finite_domain(Int('x')) + False + """ + return isinstance(a, FiniteDomainRef) + + +class FiniteDomainNumRef(FiniteDomainRef): + """Integer values.""" + + def as_long(self): + """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. + + >>> s = FiniteDomainSort("S", 100) + >>> v = FiniteDomainVal(3, s) + >>> v + 3 + >>> v.as_long() + 1 + 4 + """ + return int(self.as_string()) + + def as_string(self): + """Return a Z3 finite-domain numeral as a Python string. + + >>> s = FiniteDomainSort("S", 100) + >>> v = FiniteDomainVal(42, s) + >>> v.as_string() + '42' + """ + return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) + + +def FiniteDomainVal(val, sort, ctx=None): + """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. + + >>> s = FiniteDomainSort("S", 256) + >>> FiniteDomainVal(255, s) + 255 + >>> FiniteDomainVal("100", s) + 100 + """ + if __debug__: + _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" ) + ctx = sort.ctx + return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx) + +def is_finite_domain_value(a): + """Return `True` if `a` is a Z3 finite-domain value. + + >>> s = FiniteDomainSort("S", 100) + >>> b = Const('b', s) + >>> is_finite_domain_value(b) + False + >>> b = FiniteDomainVal(10, s) + >>> b + 10 + >>> is_finite_domain_value(b) + True + """ + return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast()) + + ######################################### # # Optimize