(logic QF_LRA
:written_by {Cesare Tinelli}
:date {08/04/05}
:theory Reals
:language
"Closed quantifier-free formulas built over an arbitrary expansion of
the Reals signature with free constant symbols, but containing only
linear atoms, that is, atoms with no occurrences of the function
symbol * (but see the notational conventions below).
Formulas in ite terms must satisfy the same restriction as well
with the exception that they need not be closed.
"
:extensions
"The syntax (+ t_1 ... t_n) with n>2 is allowed as an abbreviation
of the term (+ t_1 (+ t_2 (+ t_3 ... ))).
"
:extensions
"Terms with positive integer coefficients are allowed, that is, expressions
of the form (* n t) or (* t n) for some numeral n, both of which abbreviate
the term (+ t ... t) having n occurrences of t.
"
:extensions
"Terms with negative integer coefficients are also allowed, that is,
expressions of the form (* (~ n) t) or (* t (~ n)) for some numeral n,
both of which abbreviate the term (~ (* n t)).
"
:extensions
"In addition to 0 and 1, numerals n > 1 are allowed also as arguments of
atoms or of +. In that case, they abbreviate the term (+ 1 ... 1) with
n occurrences of 1.
"
:extensions
"Also allowed are rational coefficients: expressions of the form:
(/ m n) where n is a numeral other than 0 and m is either a numeral
or an expression of the form (~ i) for some numeral i,
An atom with rational coefficients is syntactic sugar for any equivalent
atom with integer coefficients obtained by applying standard arithmetic
transformations.
"
)