Method finiteDomainExample

examples/java/JavaExample.java:2116–2134

(Context ctx)

    }

    public void finiteDomainExample(Context ctx)
    {
        System.out.println("FiniteDomainExample");
        Log.append("FiniteDomainExample");

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