(logic LRA :written_by {Cesare Tinelli} :date {02/07/09} :theory Reals :language "Closed 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. " )