(logic QF_LIA
:written_by {Cesare Tinelli}
:date {08/04/05}
:theory Ints
:language
"Closed quantifier-free formulas built over an arbitrary expansion of
the Ints 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.
"
)