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 <op1> 2) <op2> 3) <op3> 4) <op4> 5) <op5> 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?

score 4 · Accepted Answer · answered Jul 11 '17 at 16:08

4

Unfortunately I don't have access to C# to try this out, but I'm curious why you need a call to mkExist at all? Since you already have the variables b1..b6 created via calls to MkConst, you should simply be using them to both assert your constraint and then refute the models as you do the "all-sat" loop, without any calls to mkExist and also without calling new inside your loop to create new ones.

answered Jul 11 '17 at 16:08

alias

28,120
2
23
40

Well, that doesn't answer my question, but that solves my task in a more efficient way. Thanks a lot! – ForNeVeR Jul 13 '17 at 15:17
1

There's in general no means of accessing variables bound in a quantifier in SMTLib. Of course you're using the C# interface and there might be a Z3 specific way to do so, but only top-level variables are typically visible in calls to get-model etc. See this answer: https://stackoverflow.com/questions/7179777/z3-extracting-existential-model-values/7181987#7181987 which is quite relevant to your question. – alias Jul 13 '17 at 17:44

Accessing variable of `exists` scope in Z3

1 Answers1