What are the limits of reasoning in quantified arithmetic in SMT?
cvc4, smt, z3
Solution
Pad is correct, the `qe` preprocessor can be quite expensive. Moreover, it is not effective in formulas coming from software verification tools such as VCC, Poirot, Dafny, VeriFast, Why3, and ESCJava2. It is not effective because the formulas produced by these applications also contain uninterpreted functions, arrays, etc.
As Pad's answer suggests, Z3 is a collection of engines. It provides APIs and commands that allow users to select which engine (or combination of engines) will be used to solve a problem. When the user just says `(check-sat)` is tries to guess what is the best engine for solving the input formula. The guess is based on the structure of input formula and annotations provided by the user (example: the `set-logic` command). We are continuously expanding the set of fragments that are automatically detected, and the set of engines we provide.
That being said, it is embarrassing that Z3 missed a fragment such as `LIA` and did not automatically applied the `qe` procedure to it. For `LIA` formulas, `qe` is usually the best option. Alternatives based on E-matching or MBQI are not effective since they are meant for completely different fragments.
I just committed code that detects `LIA` (even when `set-logic` is not used). The change is already available in the `unstable` (working-in-progress) branch. It will be available tomorrow in the nightly builds, and in the next official release.
Problem
I have tried several SMT solvers (CVC3, CVC4 and Z3) on the following seemingly trivial benchmark: ``` (set-logic LIA) (set-info :smt-lib-version 2.0) (assert (forall (( x Int)) (forall ((y Int)) (= y x)))) (check-sat) (exit) ``` The solvers all return unknown. I understand that this is an undecidable fragment (well non-linear) but I was expecting there would be some simple instantiation heuristics that could solve it. I also tried adding some extra assertions with constants but it didn't help. Is there a way to attack these problems and what are the limits of reasoning in quantified arithmetic in SMT?