Z3 求解器 Java API：为 RealExpr 实现模运算

Question

我是 z3 初学者，所以当我问以下问题时请耐心等待：

我尝试在 Java 中实现类型 RealExpr 的模运算，并借助于：https://github.com/Z3Prover/z3/issues/557.

我想解决的是一个简单的模计算，例如：6.1 mod 6 = 0.1。但是当我打印结果时，我得到的是 1/2 的值。

代码如下：

public static void main(String[] args) {
        HashMap<String, String> cfg = new HashMap<String, String>();
        cfg.put("model", "true");
        Context ctx = new Context(cfg);
        Solver solver = ctx.mkSolver();
        Model model = null;

        // Initialize Constants
        // 6.1
        RealExpr x = (RealExpr) ctx.mkAdd(ctx.mkReal(6), ctx.mkReal(1, 10));
        // 6
        RealExpr k = ctx.mkReal(6);

        RealExpr result = mkRealMod(x, k, ctx, solver);
        solver.add(ctx.mkAnd(ctx.mkGt(result, ctx.mkReal(0)), ctx.mkLt(result, k)));

        if (solver.check() == Status.SATISFIABLE) {
            System.out.println("Satisfiable");
            model = solver.getModel();
            Expr result_value = model.evaluate(result, false);
            System.out.println("result: " + result_value);
        }
        else {
            System.out.println("Status " + solver.check());
            System.out.println("Unsatisfiable");
        }

    ctx.close();
    }

    public static RealExpr mkRealMod(RealExpr x, RealExpr k, Context ctx, Solver solver) {
        RealExpr remainder;

        Sort[] domain = { ctx.getRealSort(), ctx.getRealSort() };
        FuncDecl mod = ctx.mkFuncDecl("mod", domain, ctx.getRealSort());
        FuncDecl quot = ctx.mkFuncDecl("quot", domain, ctx.getRealSort());

        RealExpr zero = ctx.mkReal(0);
        RealExpr minusK = (RealExpr) ctx.mkSub(zero, k);

        RealExpr[] xk = {x,k};
        RealExpr modxk = (RealExpr) ctx.mkApp(mod, xk);
        RealExpr quotxk = (RealExpr) ctx.mkApp(quot, xk);

        RealExpr calc = (RealExpr) ctx.mkAdd(ctx.mkMul(k, quotxk), modxk);

        // Implies(k != 0, 0 <= mod(X,k)),
        solver.add(ctx.mkImplies(ctx.mkNot(ctx.mkEq(k, zero)), ctx.mkLe(zero, modxk)));
        // Implies(k > 0, mod(X,k) < k),
        solver.add(ctx.mkImplies(ctx.mkGt(k,zero), ctx.mkLt(modxk, k)));
        // Implies(k < 0, mod(X,k) < -k),
        solver.add(ctx.mkImplies(ctx.mkLt(k,zero), ctx.mkLt(modxk, minusK)));
        // Implies(k != 0, k*quot(X,k) + mod(X,k) == X))
        solver.add(ctx.mkImplies(ctx.mkNot(ctx.mkEq(k, zero)), ctx.mkEq(calc, x)));
        remainder = modxk;

        return remainder;
    }

我也尝试删除单独的函数 mkRealMod 并将模运算的相应代码放入主函数中，但这似乎没有改变。

我不明白为什么约束会出错。

我错过了什么？结果怎么会是1/2？

我在 solver.check() 之前使用了 solver.toString() 方法，结果是这样的：

(declare-fun mod (Real Real) Real)
(declare-fun quot (Real Real) Real)
(declare-fun remainder () Real)
(assert (=> (not (= 6.0 0.0)) (<= 0.0 (mod (+ 6.0 (/ 1.0 10.0)) 6.0))))
(assert (=> (> 6.0 0.0) (< (mod (+ 6.0 (/ 1.0 10.0)) 6.0) 6.0)))
(assert (=> (< 6.0 0.0) (< (mod (+ 6.0 (/ 1.0 10.0)) 6.0) (- 0.0 6.0))))
(assert (let ((a!1 (+ (* 6.0 (quot (+ 6.0 (/ 1.0 10.0)) 6.0))
              (mod (+ 6.0 (/ 1.0 10.0)) 6.0))))
  (=> (not (= 6.0 0.0)) (= a!1 (+ 6.0 (/ 1.0 10.0))))))
(assert (and (> remainder 0.0) (< remainder 6.0)))

Answer 1

这里有一些问题，但根本问题是您的公理化没有充分约束 mod/quot 值的值以产生您认为应该的值。特别是，有无数种方法可以满足您的假设，而 z3 只会选择一种。让我详细说明。

我将省略 Java 此处的编码，因为它不会增加任何有价值的东西。但直接编码你在 SMTLib 中编写的内容。虽然代码在 SMTLib 中，但结论也适用于您的程序。

在 SMTLib 表示法中，这就是您所说的内容。（在添加 remainder 与 modxk 相同的事实并为便于阅读而简化后，从输出中清理）：

(declare-fun mod  (Real Real) Real)
(declare-fun quot (Real Real) Real)

(define-fun X () Real (+ 6.0 (/ 1.0 10.0)))
(define-fun k () Real 6.0)

; Implies(k != 0, 0 <= mod(X,k))
(assert (=> (distinct k 0.0) (<= 0 (mod X k))))

; Implies(k > 0, mod(X,k) < k)
(assert (=> (> k 0.0) (< (mod X k) k)))

; Implies(k < 0, mod(X,k) < -k)
(assert (=> (< k 0.0) (< (mod X k) (- 0 k))))

; Implies(k != 0, k*quot(X,k) + mod(X,k) == X))
(assert (=> (distinct k 0.0) (= X (+ (mod X k) (* k (quot X k))))))

这是您将从道德上从您的 Java 程序中生成的代码，一旦您解决了所有故障并可能为 X 和 k 命名以提高可读性.

让我们看看 z3 为这个程序产生了什么输出。在末尾添加以下行：

(check-sat)
(get-value ((mod X k)))
(get-value ((quot X k)))

运行 z3 在这个最终的 SMTLib 程序上产生：

sat
(((mod X k) (/ 11.0 2.0)))
(((quot X k) (/ 1.0 10.0)))

用更熟悉的表示法，这就是说 mod 是 5.5 而 quot 是 0.1。

你当然会抗议，因为你希望 mod 成为 0.1！实际上，如果仔细检查您输入的所有断言，您会发现这些值确实满足所有断言。让我们一一回顾：

Implies(k != 0, 0 <= mod(X,k)) 是的，我们有 k=6，0 <= 5.5 成立。
Implies(k > 0, mod(X,k) < k) 是的，我们有 k=6 和 5.5 < 6 持有
Implies(k < 0, mod(X,k) < -k) 因为我们有 k=6 这个推论是微不足道的。
Implies(k != 0, k*quot(X,k) + mod(X,k) == X)。我们有 k=6，结果说 6 * 0.1 + 5.5 必须是 6.1，这确实是正确的。

因此，z3 确实找到了满足您的约束的值，这就是 SMT 求解器的设计目的。

要明确这一点，请将以下约束添加到程序中并再次运行：

(assert (distinct (mod X k) 5.5))

现在 z3 说：

sat
(((mod X k) 5.0))
(((quot X k) (/ 11.0 60.0)))

我们所做的是告诉 z3 我们希望 mod X k 不是 5.5。它说，好吧，我将它设为 5，并将 quot X k 设置为 11/60，您所有的公理都将再次得到满足。我们可以永远玩这个游戏，因为一念之间就会发现有无数个值可以满足您的限制。

这里的重点是要注意，没有人声称这些是仅满足您的约束的值。实际上，您期望 z3 为 quot 选择 0.1，为 mod 选择 1，满足等式 6 * 1 + 0.1 = 6.1。但是在您的公理化中没有任何东西需要选择这些值。此时，您需要做的是问问自己如何（如果可能的话！）您可以为实数输入更多关于 mod 和 quot 的公理，以使解唯一。我建议使用纸和铅笔写下您的公理必须是什么，以便可以唯一确定值。（顺便说一句，我并不是说这是可行的。我不确定 quot/mod 是否真的对实数有意义。）

如果你真的能想出这样一个独特的公理化，那就用z3试试吧，帮你解决这个问题。除非你有一个独特的公理化，否则 z3 总是会选择一些赋值给满足你的任何要求的变量，这不太可能符合你的期望。

绕过整数

我能想到的一种解决方案是将quot的值限制为整数。也就是说，使其成为具有以下签名的函数：

(declare-fun quot (Real Real) Int)

如果您改为尝试这种公理化，您会发现 z3 现在产生：

sat
(((mod X k) (/ 1.0 10.0)))
(((quot X k) 1))

这可能就是您的想法。请注意，当您像这样混合整数和实数时，您可能会创建 SMT 求解器难以处理的约束。（在这种特殊情况下它有效，因为你拥有的只是常量。）但是如果你运行遇到问题，我们可以讨论它的后果。

Z3 求解器 Java API：为 RealExpr 实现模运算

Z3 Solver Java API: Implementing Modulo Operation for RealExpr

java

z3

modulo

绕过整数