I'm a z3 beginner, so please bear with me when I ask the following:
I've tried to implement the modulo operation for the type RealExpr in Java with the help of: https://github.com/Z3Prover/z3/issues/557.
What I want to solve is a simple modulo calculation, for example: 6.1 mod 6 = 0.1. But when I print the result I get the value 1/2 instead.
Here is the code:
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;
}
I've also tried to remove the seperate function mkRealMod and to put the corresponding code for the modulo operation into the main function but that does not seem to change.
I don't see why the constraints could be wrong.
What did I miss here? How can the result be 1/2?
I used the solver.toString() method before solver.check() and this is what came out:
(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)))
There'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'm going to elide Java coding here, as it doesn'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, k*quot(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 holdsImplies(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.
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.