Method finiteDomainExample

examples/java/JavaGenericExample.java:1922–1940

(Context ctx)

    }

    public <S, T> void finiteDomainExample(Context ctx)
    {
        System.out.println("FiniteDomainExample");
        Log.append("FiniteDomainExample");

        FiniteDomainSort<S> s = ctx.mkFiniteDomainSort("S", 10);
        FiniteDomainSort<T> t = ctx.mkFiniteDomainSort("T", 10);
        FiniteDomainNum<S> s1 = (FiniteDomainNum<S>) ctx.mkNumeral(1, s);
        FiniteDomainNum<T> t1 = (FiniteDomainNum<T>) ctx.mkNumeral(1, t);
        System.out.println(s);
        System.out.println(t);
        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));
    }

    public void floatingPointExample1(Context ctx) throws TestFailedException
    {