1

Closed

AUFLIRA front-end problem with rational constants

description

Using z3 v4.3.1 (master branch), compiled on 64bit Scientific Linux 6.3, I provide the SMTLIB 2 input
(set-logic AUFLIRA)
(assert (< 0 (/ 1 2)))
and get the response
(error "line 2 column 21: logic does not support nonlinear arithmetic")
This seems specific to AUFLIRA. I don't see this problem with AUFNIRA or LRA.
Closed Jan 24, 2013 at 8:56 PM by leodemoura
Problem has been fixed.

comments

leodemoura wrote Jan 24, 2013 at 8:55 PM

Paul, thanks for reporting the problem.
I fixed it: http://z3.codeplex.com/SourceControl/changeset/7eaa5562d8a9

Note that, (/ 1 2) is not really compliant with SMT 2.0 standard.
It should be (/ 1.0 2.0).
Z3 automatically adds a coercion.
After the fix, it will also accept (/ 1 2). However, other SMT solvers may refuse the input.

The fix is already available in the "unstable" (work-in-progress) branch, and will be available in the next release. If you don't want to use non officially released code. You can workaround the problem by using (/ 1.0 2.0) instead of (/ 1 2).

PaulJackson wrote Jan 25, 2013 at 12:03 PM

(/ 1 2) is fully compliant with the current version of SMTLIB 2.0.

Specifically, for AUFLIRA, see

http://smtlib.cs.uiowa.edu/logics/AUFLIRA.smt2

There it says:
 :extensions
 "For every operator op with declaration (op Real Real s) for some sort s,
  and every term t1, t2 of sort Int and t of sort Real, the expression 
  - (op t1 t) is syntactic sugar for (op (to_real t1) t)
  - (op t t1) is syntactic sugar for (op t (to_real t1))
  - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
 "
AUFNIRA has the same.

The SMTLIB 2 theory and logic definitions do seem to need some tidying up on this issue. While the Reals_Ints theory that AUFLIRA and AUFNIRA use does not allow (/ 1 2), the Reals theory does (in general, only when numerator and denominator have no common factors), and the *LRA logics that use Reals relax the common factor requirement, allowing (/ c n) for any integer c and positive integer n. However the *NRA logic do not include this relaxation.

leodemoura wrote Jan 25, 2013 at 4:43 PM

My bad, I have not seen the extensions.