JKind prevents use of non-constant multiplication/division, regardless of solver

[Greg4cr]

The Z3 solver supports non-constant multiplication (in an incomplete form - it may return "unknown"), but JKind will still reject any non-linear expressions when Z3 is selected as the solver.

Could JKind be updated to allow non-linear multiplication and division if the Z3 solver is being used?

Thanks!

[agacek]

Ok. I committed a change to handle this. In this case Z3 may return 'unknown' but I was not able to find any simple examples that illustrated this. Currently such a response would cause an exception in JKind. When we find an example, we can give it better behavior.

[Greg4cr]

Thanks for making the change. I'll let you know if I break it.

[agacek]

Yes, that would be very useful in this case. I was never able to get z3 to say 'unknown', instead it just ran indefinitely.

On Wed, Mar 26, 2014 at 2:22 PM, Gregory Gay notifications@github.comwrote:

Thanks for making the change. I'll let you know if I break it.

Reply to this email directly or view it on GitHubhttps://github.com/agacek/jkind/issues/16#issuecomment-38727840 .

[Greg4cr]

No issues with multiplication so far, but I think that there may still be an issue with jkind.analysis.evaluation.DivisionChecker.

For a non-linear division statement of the form: x = y div z; I get the following exception/stack trace: java.lang.IllegalArgumentException at jkind.analysis.evaluation.DivisionChecker.signum(DivisionChecker.java:75) at jkind.analysis.evaluation.DivisionChecker.visit(DivisionChecker.java:48) at jkind.lustre.ExprIterVisitor.visit(ExprIterVisitor.java:1) at jkind.lustre.BinaryExpr.accept(BinaryExpr.java:21) at jkind.analysis.evaluation.DivisionChecker.visitNode(DivisionChecker.java:38) at jkind.analysis.evaluation.DivisionChecker.visitProgram(DivisionChecker.java:31) at jkind.analysis.evaluation.DivisionChecker.check(DivisionChecker.java:21) at jkind.analysis.StaticAnalyzer.checkErrors(StaticAnalyzer.java:47) at jkind.analysis.StaticAnalyzer.check(StaticAnalyzer.java:27) at jkind.JKind.main(JKind.java:36) at jkind.Main.main(Main.java:47) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:483) at org.eclipse.jdt.internal.jarinjarloader.JarRsrcLoader.main(JarRsrcLoader.java:58)

I can send the actual Lustre model if needed.

[agacek]

The problem now is that we allow division by zero when using z3 since we can't check for it statically. We also allow integer division and modulus by negative numbers, which solvers give different results for. Thus the particular semantics of division by zero or by negative numbers is subject to the change in the future. For now it's just z3's semantics. I'm pasting in here an email I wrote earlier addressing some of these issues:

It looks like there are some problems/worries with integer division in JKind. First, integer division is all well and good for positive numerators and denominators, but for negatives things fragment. According to [1]:

That paper distinguishes three main possibilities, all of which satisfy the remainder law for all nonzero divisors:

x = y * (x div y) + x mod y

but otherwise differ as follows:

T-definition: x div y = trunc(x / y), i.e. rounded towards zero
F-definition: x div y = floor(x / y), i.e. rounded towards -infinity
E-definition: 0 <= x mod y < |y|

My investigations seem to indicate that:

• Most interactive theorem provers use the F-definition
• Most programming languages and/or hardware use the T-definition

Yices seems to use the F-definition, while SMT-LIB2 (z3, cvc4) seems to use the E-definition. That means that JKind has different results based on the backend you use. As some example:

1 div 3 a) 0 in all systems

-1 div 3 a) -1 in yices, z3,cvc4 b) 0 in java, c, etc

1 div -3 a) -1 in z3, cvc4 b) 0 in yices, java, c, etc

-1 div -3 a) 0 in yices, java, c, etc b) 1 in z3, cvc4

I understand the reasoning behind the E-definition, but the consequences are a bit strange. Negation does not distribute over integer division since -(1 div 3) != -1 div -3. Furthermore, -1 div 3 != 1 div -3.

So this leaves JKind in an awkward spot. SMT-LIB2 is the latest standard, so we should probably follow that. I don't know if there is a good way to correct for the different way that yices treats division. I think my solution for now will be to just add an error if you try to do integer division by a negative number. I don't think anybody will get too bent out of shape about that.

Finally, that still leaves JKind different from most programming languages when the numerator is negative. That's not great, but differing from the SMT-LIB2 / theorem proving world would be bad too. Perhaps I just need to clearly document it somewhere.

[1] http://www.cs.nyu.edu/pipermail/smt-lib/2008/000259.html

[Greg4cr]

Very interesting, I had no idea about those particulars. Thanks for letting me know.