java - Z3 Solver Java API:为RealExpr实现模运算

Question

我是z3的初学者，所以当我提出以下要求时，请多多包涵：

我试图借助https://github.com/Z3Prover/z3/issues/557在Java中为类型RealExpr实现模运算。

我要解决的是一个简单的模运算，例如：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.toString()之前使用了 solver.check()方法，结果如下：

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

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

让我们看看该程序产生的输出 z3。在末尾添加以下行：

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

在此最终的SMTLib程序上运行z3会产生：

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为 0.1选择 quot，为 1选择 mod，满足等式 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求解器来说难以处理的约束。 （在这种特殊情况下，它起作用是因为您所拥有的都是常量。）但是，如果遇到问题，我们可以讨论其后果。