Method arrayExample3

examples/java/JavaExample.java:452–487

(Context ctx)

    // / <remarks>This example also shows how to use the <code>distinct</code>
    // construct.</remarks>
    public void arrayExample3(Context ctx) throws TestFailedException
    {
        System.out.println("ArrayExample3");
        Log.append("ArrayExample2");

        for (int n = 2; n <= 5; n++)
        {
            System.out.println("n = " + Integer.toString(n));

            Sort bool_type = ctx.mkBoolSort();
            Sort array_type = ctx.mkArraySort(bool_type, bool_type);
            Expr[] a = new Expr[n];

            /* create arrays */
            for (int i = 0; i < n; i++)
            {
                a[i] = ctx.mkConst("array_" + Integer.toString(i), array_type);
            }

            /* assert distinct(a[0], ..., a[n]) */
            BoolExpr d = ctx.mkDistinct(a);
            System.out.println(d);

            /* context is satisfiable if n < 5 */
            Model model = check(ctx, d, n < 5 ? Status.SATISFIABLE
                    : Status.UNSATISFIABLE);
            if (n < 5)
            {
                for (int i = 0; i < n; i++)
                {
                    System.out.println(a[i].toString() + " = "
                            + model.evaluate(a[i], false));
                }
            }
        }
    }

    // / Sudoku solving example.