Spec errors on the difference logic benchmarks of the SMT-LIB

[hra687261]

Running dolmen on the difference logic benchmarks of the SMT-LIB resulted in the following errors:

In QF_IDL, the files in the folder bcnscheduling seem to contain terms of the form (let (... (v (+ x 15)) ...) ...) but dolmen outputs the following message when executed of one of those files:

Error Non-linear expressions are forbidden by the logic.
Hint: addition is not allowed in integer difference logic

So in this case dolmen seems to be too restrictive.

In UFIDL, when running dolmen on the following files:

• boogie/Arrays_P1-noinfer.smt2
• boogie/Arrays_Q1-noinfer.smt2

It outputs what seems to be an incorrect error message that says the following:

Error Non-linear expressions are forbidden by the logic.
Hint: subtraction in difference logic (QF_UFIDL version) expects all but at
  most one of its arguments to be numerals

While there are no subtractions in the files in question, the terms that triggers the error are of the form (+ x (select2 _ _ _)) with (declare-fun select2 (Int Int Int) Int)

The same message is printed for the files in sledgehammer/TypeSafe but for terms of the form (+ x y), where x and y are quantified variables and their addition is an argument to an uninterpreted function.

boogie.zip bcnscheduling.zip TypeSafe.zip

[Gbury]

I'll look at that when I'm back from holidays, but note that : 1) there are many different flavours of difference logic and 2) difference logic is really restrictive: for instance, difference logic forbids any use of the addition, according to the spec, and lastly 3) it is known that especially for difference logic, the benchmarks from the smtlib are not all conforming to the spec.

[Gbury]

Ok, so I had some free time, here's a response.

QF_IDL/bcnscheduling

There is no error here: as one can read in the spec, addition is not allowed to appear in atoms (which is reasonable given the name "difference" logic). That being said, the error message could be clearer/more explicit, I'll work on that.

Lastly, these benchmarks, while not conforming to the standard spec, actually respect the spirit of the spec: indeed, if one substitutes the let-bound variables and performs some arithmetic simplification/re-ordering of terms, then the benchmark only contains subtractions and no additions, which is why solvers do not complain about them, however it's outside the scope of dolmen to perform such computations currently.

UFIDL problems

Here, indeed as you point out, the error message is the wrong one (but the problems are nonetheless not spec-conforming). I'll fix that asap.