Accessing variable of `exists` scope in Z3

Question

I am trying to solve the following problem with Z3:

Having set of four operators (+, -, *, /), decide which operators could be substituted in the following expression to make it true:

(((((1  2)  3)  4)  5)  6) = 35

I need to print all of the valid answers. Here's a sample program in Z3 language:

(declare-datatypes () ((operator (Plus) (Minus) (Mult) (Divid))))
(define-fun myf ((x Int) (z operator) (y Int)) Int
      (ite (= z Plus) (+ x y)
         (ite (= z Minus) (- x y)
           (ite (= z Mult) (* x y)
               (div x y)))))
(assert
  (exists ((b1 operator) (b2 operator) (b3 operator) (b4 operator) (b5 operator))
    (= (myf(myf(myf(myf(myf 1 b1 2) b2 3) b3 4) b4 5) b5 6) 35)
  )
)

(check-sat)
(get-model)
(exit)

(http://rise4fun.com/Z3/8usN)

It doesn't print all of the solutions. I understand that to print all the solutions I need to add constraints to the solver after every iteration like that answer recommends, but I can't get how to do it with C#.

Here's my current code (C# 7):

using (var context = new Context())
{
    var @operator = context.MkEnumSort("operator", "Plus", "Minus", "Mult", "Div");
    var plus = @operator.Consts[0];
    var minus = @operator.Consts[1];
    var mult = @operator.Consts[2];

    IntExpr myf(IntExpr x, Expr z, IntExpr y) =>
        (IntExpr)context.MkITE(context.MkEq(z, plus), context.MkAdd(x, y),
            context.MkITE(context.MkEq(z, minus), context.MkSub(x, y),
                context.MkITE(context.MkEq(z, mult), context.MkMul(x, y),
                    context.MkDiv(x, y))));

    var solver = context.MkSolver();

    var b1 = context.MkConst("b1", @operator);
    var b2 = context.MkConst("b2", @operator);
    var b3 = context.MkConst("b3", @operator);
    var b4 = context.MkConst("b4", @operator);
    var b5 = context.MkConst("b5", @operator);

    solver.Assert(
        context.MkExists(
            new[] { b1, b2, b3, b4, b5 },
            context.MkEq(
                myf(
                    myf(
                        myf(
                            myf(
                                myf(
                                    context.MkInt(1),
                                    b1,
                                    context.MkInt(2)),
                                b2,
                                context.MkInt(3)),
                            b3,
                            context.MkInt(4)),
                        b4,
                        context.MkInt(5)),
                    b5,
                    context.MkInt(6)),
                context.MkInt(35))));

    while (Status.SATISFIABLE == solver.Check())
    {
        var operators = new[] { b1, b2, b3, b4, b5 };
        var model = solver.Model;
        var values = operators.Select(o => model.Eval(o, true)); // That doesn't return the right values

        Console.WriteLine(model);
        Console.WriteLine(string.Join(" ", values));

        solver.Add(context.MkOr(
            operators.Select(o => context.MkNot(context.MkEq(o, model.Eval(o, true)))))); // That's supposed to work, but it doesn't
    }

I have problems accessing variables from the exists scope: it seems that model.Eval(b1, true) returns some value, but not the value solver have decided to use on the current iteration. And even asking the values of these constants further pollutes the solver scope (e.g. I can see these constants in the model output all the way):

(define-fun b3!2 () operator
  Mult)
(define-fun b2!3 () operator
  Mult)
(define-fun b5!0 () operator
  Minus)
(define-fun b1!4 () operator
  Plus)
(define-fun b4!1 () operator
  Plus)
# ^ ^ ^ ^ these seems like the proper values
(define-fun b1 () operator
  Minus)
(define-fun b2 () operator
  Minus)
(define-fun b3 () operator
  Minus)
(define-fun b4 () operator
  Minus)
(define-fun b5 () operator
  Minus)
# ^ ^ ^ ^ and I don't know why it prints these

How do I fix my program to add constraints on the proper values and don't pollute the scope?

Accessing variable of `exists` scope in Z3

1 Answers