Method arrayExample3

examples/java/JavaGenericExample.java:432–462

(Context ctx)

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

        for (int n = 2; n <= 5; n++)
        {
            System.out.printf("n = %d%n", n);

            BoolSort bool_type = ctx.mkBoolSort();
            ArraySort<BoolSort, BoolSort> array_type = ctx.mkArraySort(bool_type, bool_type);
            List<Expr<ArraySort<BoolSort, BoolSort>>> a = IntStream.range(0, n).mapToObj(i -> ctx.mkConst(String.format("array_%d", i), array_type)).collect(Collectors.toList());

            /* create arrays */

            /* assert distinct(a[0], ..., a[n]) */
            BoolExpr d = ctx.mkDistinct(a.toArray(new Expr[0]));
            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.printf("%s = %s%n", a.get(i), model.evaluate(a.get(i), false));
                }
            }
        }
    }

    // / Sudoku solving example.