Support for integer division in SMT solvers

Question

I have executed z3 and CVC4 on the following SMT input. Both return unknown.

;!(a,b,c).(0<=a & 0<=b & 1<=c
;               =>
;               (a+(b mod c)) mod c = (a+b) mod c)
;
;
(set-logic NIA)
(set-option :print-success false)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(assert (<= 0 a))
(assert (<= 1 c))
(assert (<= 0 b))

(assert (! (not (= (mod (+ a (mod b c)) c) (mod (+ a b) c))) :named goal))
(check-sat)
(exit)

Is there any fundamental reason why they are not able to decide satisfiability?
Which options or other solvers would be suitable to address this kind of problems?

alias alias · Accepted Answer · 2020-07-27T14:07:42

Yes, there's a fundamental reason why non-linear integer arithmetic is difficult for SMT solvers. Leo explains this thoroughly in https://stackoverflow.com/a/13898524/936310

So, expecting SMT solvers to do well in this domain is simply unreasonable. The recommendation is to use proper theorem provers like Isabelle, Coq, Lean, ACL2, HOL, HOL-Light etc. Of course, the proofs are then mostly manual, but these systems usually have connections to SMT solvers to discharge many of the goals, giving you the best of both worlds so far as decidability is concerned.

Note that even the (check-sat-using qfnra-nlsat) trick that Leo describes wouldn't work for your problem, since the interpretation of mod over real's isn't going to help you here at all. (In general, the qfnra-nlsat trick can find models, but will not ever produce unsat as it is mostly a model-search strategy.)

The best you can do out-of-the box is prove instances of your problem, by making c concrete. i.e., add an assertion of the form:

(assert (= c 12))

and you'll see z3 instantly returns unsat. Of course this is hardly sufficient, but you can't do any better with a push-button solver (unless they add "custom" heuristics for this very problem!) for the time being.

Support for integer division in SMT solvers

1 Answers