Added finite domain expressions and numerals to the .NET, Java, and Python APIs.

Relates to #318

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));

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(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));

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);

src/api/dotnet/FiniteDomainExpr.cs

@@ -0,0 +1,38 @@
+/*++
+Copyright (<c>) 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
+{
+    /// <summary>
+    /// Finite-domain expressions
+    /// </summary>
+    public class FiniteDomainExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for DatatypeExpr </summary>
+        internal FiniteDomainExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/FiniteDomainNum.cs

@@ -0,0 +1,115 @@
+/*++
+Copyright (<c>) 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
+{
+    /// <summary>
+    /// Finite-domain numerals
+    /// </summary>
+    [ContractVerification(true)]
+    public class FiniteDomainNum : FiniteDomainExpr
+    {
+        /// <summary>
+        /// Retrieve the 64-bit unsigned integer value.
+        /// </summary>
+        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;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the int value.
+        /// </summary>
+        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;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the 64-bit int value.
+        /// </summary>
+        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;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the int value.
+        /// </summary>
+        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
+        /// <summary>
+        /// Retrieve the BigInteger value.
+        /// </summary>
+        public BigInteger BigInteger
+        {
+            get
+            {
+                return BigInteger.Parse(this.ToString());
+            }
+        }
+#endif
+
+        /// <summary>
+        /// Returns a string representation of the numeral.
+        /// </summary>
+        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
+    }
+}

src/api/dotnet/Microsoft.Z3.csproj

@@ -342,6 +342,8 @@
     <Compile Include="ConstructorList.cs" />
     <Compile Include="DatatypeExpr.cs" />
     <Compile Include="DatatypeSort.cs" />
+    <Compile Include="FiniteDomainExpr.cs" />
+    <Compile Include="FiniteDomainNum.cs" />
     <Compile Include="FPExpr.cs" />
     <Compile Include="FPNum.cs" />
     <Compile Include="FPRMExpr.cs" />

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: ;
         }
 

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);
+    }
+}

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();
+        }
+    }
+}

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