title: Accessing variable of `exists` scope in Z3
body: <p>I am trying to solve the following problem with Z3:</p>
  
  <p>Having set of four operators (<code>+</code>, <code>-</code>, <code>*</code>, <code>/</code>), decide which operators could be substituted in the following expression to make it true:</p>
  
  <pre><code>(((((1 &lt;op1&gt; 2) &lt;op2&gt; 3) &lt;op3&gt; 4) &lt;op4&gt; 5) &lt;op5&gt; 6) = 35
  </code></pre>
  
  <p>I need to print all of the valid answers. Here's a sample program in Z3 language:</p>
  
  <pre><code>(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)
  </code></pre>
  
  <p>(<a href="http://rise4fun.com/Z3/8usN" rel="nofollow noreferrer">http://rise4fun.com/Z3/8usN</a>)</p>
  
  <p>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 <a href="https://stackoverflow.com/a/13398853/2684760">like that answer recommends</a>, but I can't get how to do it with C#.</p>
  
  <p>Here's my current code (C# 7):</p>
  
  <pre><code>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) =&gt;
          (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 =&gt; 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 =&gt; context.MkNot(context.MkEq(o, model.Eval(o, true)))))); // That's supposed to work, but it doesn't
      }
  </code></pre>
  
  <p>I have problems accessing variables from the <code>exists</code> scope: it seems that <code>model.Eval(b1, true)</code> returns some value, but <em>not</em> 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):</p>
  
  <pre><code>(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
  </code></pre>
  
  <p>How do I fix my program to add constraints on the proper values and don't pollute the scope?</p>