在 Z3 中访问“exists”范围的变量

Question

我正在尝试用 Z3 解决以下问题：

拥有四个运算符（+、-、*、/）的集合，决定哪些运算符可以替换为以下表达式以使其为真：

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

我需要打印所有有效的答案。这是一个 Z3 语言的示例程序：

(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)

它不会打印所有的解决方案。我知道要打印所有解决方案，我需要在每次迭代后向求解器添加约束like that answer recommends，但我不知道如何使用 C#。

这是我当前的代码（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
    }

我在从exists 范围访问变量时遇到问题：似乎model.Eval(b1, true) 返回了一些值，但不是值求解器已决定在当前迭代中使用。甚至询问这些常量的值也会进一步污染求解器范围（例如，我可以在模型输出中看到这些常量）：

(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

如何修复我的程序以在正确的值上添加约束并且不污染范围？

Answer 1

很遗憾，我无法使用 C# 进行尝试，但我很好奇您为什么需要致电 mkExist？由于您已经通过调用MkConst 创建了变量b1..b6，因此您应该简单地使用它们来断言您的约束，然后在执行“全饱和”循环时反驳模型，没有对mkExist的任何调用，也没有在你的循环中调用new来创建新的。