问题

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;
}

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;
}

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

答案1

得分: 1

有一些问题存在，但根本问题在于你的公理化并不足以约束mod/quot的值，以产生你认为应该得到的结果。特别地，有无限种方式满足你的假设，z3只是选择其中一种。我详细说明一下。

我会省略Java代码部分，因为它并没有增加任何有价值的信息。但是直接用SMTLib代码编写你在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 &gt; 0, mod(X,k) &lt; k)
(assert (=> (> k 0.0) (< (mod X k) k)))

; Implies(k &lt; 0, mod(X,k) &lt; -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)))

在最终的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

<details>
<summary>英文:</summary>

There&#39;s a few issues here, but the fundamental problem is that your axiomatization does not sufficiently constrain the value of `mod`/`quot` values to produce what you think it should be. In particular, there is an infinite number of ways to satisfy your assumptions and z3 just picks one. Let me elaborate.

I&#39;m going to elide Java coding here, as it doesn&#39;t add anything of value. But directly code what you wrote in SMTLib. While the coding is in SMTLib, the conclusion applies to your program as well.

In SMTLib notation, this is what you are stating. (Cleaned-up from your output, after adding the fact that `remainder` is the same as `modxk` and simplified for readability):

(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, kquot(X,k) + mod(X,k) == X))
(assert (=> (distinct k 0.0) (= X (+ (mod X k) ( k (quot X k))))))

This is the code you'll be morally generating from your Java program, once you get all the glitches sorted out and perhaps give names to `X` and `k` for readability.
Let's see what output `z3` produces for this program. Add the following lines at the end:

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

Running z3 on this final SMTLib program produces:

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

In more familiar notation, this is saying `mod` is `5.5` and `quot` is `0.1`.
You will protest this of course, as you wanted `mod` to be `0.1`! Indeed, if you go through all the assertions you put in, you'll see that these values do satisfy all of them. Let's go over them one-by-one:
* `Implies(k != 0, 0 <= mod(X,k))` Yes, we have `k=6`, and `0 <= 5.5` holds.
* `Implies(k > 0, mod(X,k) < k)` Yes, we have `k=6` and `5.5 < 6` holds
* `Implies(k < 0, mod(X,k) < -k)` Since we have `k=6` this implication is trivially true.
* `Implies(k != 0, k*quot(X,k) + mod(X,k) == X)`. We have `k=6`, and the consequent says `6 * 0.1 + 5.5` must be `6.1`, and that is indeed corrrect.
So, z3 did find you values that do satisfy your constraints, and that's what an SMT solver is designed to do.
To drive home the point, add the following constraint to the program and run it again:

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

Now z3 says:

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

What we did was to tell z3 that we want `mod X k` to be something other than `5.5`. And it said, OK, I'll make it `5`, and set `quot X k` to be `11/60` and all your axioms are going to be satisfied again. We can keep playing this game forever, as a moment of thought reveals there's an infinite number of values that satisfy your constraints.
The important point here is to note that there is no claim that these are the *only* values that satisfy your constraints. Indeed, you were expecting z3 to pick `0.1` for `quot` and `1` for `mod`, satisfying the equation `6 * 1 + 0.1 = 6.1`. But there's nothing in your axiomatization that requires these values to be picked. At this point, what you need to do is to ask yourself how (if possible!) you can put in more axioms about `mod` and `quot` for real numbers such that the solution would be unique. I'd recommend use paper and pencil to write down what your axioms must be such that the values would be uniquely determined. (I'm not saying this is doable by the way. I'm not sure if `quot`/`mod` really makes much sense for reals.)
If you can indeed come up with such a unique axiomatization, then try it with z3 to solve this problem for you. Unless you have a unique axiomatization in mind, z3 will always pick *some* assignment to variables that satisfy whatever you throw at it, which will be quite unlikely to match your expectations.
A detour via integers
=====================
One solution I can think of is to restrict the value of `quot` to be an integer. That is, make it a function with the following signature:

(declare-fun quot (Real Real) Int)

If you try this axiomatization instead, you'll find that z3 now produces:

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

which is probably what you had in mind. Note that when you mix integers and reals like this you can create constraints that are too hard for the SMT-solver to deal with. (In this particular case it works because all you have are constants.) But we can discuss the ramifications of that if you run into issues.
</details>