Accessing the scope variable `exists` in Z3

I am trying to solve the following problem with Z3:

Having a set of four operators ( +

, -

, *

, /

), decide which statements can be replaced by the following terms, to make it true:

(((((1 <op1> 2) <op2> 3) <op3> 4) <op4> 5) <op5> 6) = 35

      

        
        
        
      

    

I need to print all valid answers. Here's an example of a Z3 program:

(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 solutions. I understand that to print all the solutions I need to add solver constraints after each iteration as this answer recommends , but I cannot figure out how to do this 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 supposed to work, but it doesn't
    }

      

        
        
        
      

    

I'm having problems accessing variables from scope exists

: it seems to model.Eval(b1, true)

return some value, but not the value solver decided to use on the current iteration. And even asking for the values ​​of these constants further pollutes the solver area (for example, I can see these constants in full in the output file):

(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 correct values ​​and not pollute the area?