(logic QF_RDL
:written_by {Cesare Tinelli}
:date {08/04/05}
:last_modified {30/05/05}
:theory Reals
:language
"Closed quantifier-free formulas with atoms of the form:
- (see SMT-LIB concrete syntax)
- (op (- x y) c),
- (op (- x y) (~ c)),
- (op x y),
- (op (- (+ x ... x) (+ y ... y)) c) with n>0 occurrences of x and y,
- (op (- (+ x ... x) (+ y ... y)) (~ c)) with n>0 occurrences of x and y
where
- op is <, <=, >, >=, =, or distinct
- x, y are free constant symbols,
- c is 0, 1, or a term of the form (+ 1 ... (+ 1 1)) with n>1 ones.
"
:extensions
"Sums (+ 1 ... (+ 1 1)) of n ones can be abbreviated by the numeral n.
For instance, (+ 1 (+ 1 1)) can be abbreviated by 3.
"
:extensions
"The expression (op (- x y) (/ c n)) where n is a numeral other than 0 and
c is either a numeral or an expression of the form (~ m) for some numeral m,
abbreviates the expression
(op (- (+ x ... x) (+ y ... y)) m) with n occurrences of x and y.
"
)