(logic QF_RDL
:smt-lib-version 2.6
:smt-lib-release "2017-11-24"
:written-by "Cesare Tinelli"
:date "2010-04-30"
:last-updated "2015-04-25"
:update-history
"Note: history only accounts for content changes, not release changes.
2015-04-25 Updated to Version 2.5.
2010-12-16 Replaced erroneous ''n > 0'' with ''n > 1'' in language attribute.
"
:theories (Reals)
:language
"Closed quantifier-free formulas with atoms of the form:
- p
- (op (- x y) c),
- (op x y),
- (op (- (+ x ... x) (+ y ... y)) c) with n > 1 occurrences of x and of y,
where
- p is a variable or free constant symbol of sort Bool,
- c is an expression of the form m or (- m) for some numeral m,
- op is <, <=, >, >=, =, or distinct,
- x, y are free constant symbols of sort Real.
"
:extensions
"The expression (op (- x y) (/ c n)) where n is a numeral other than 0 and
c is an expression of the form m or (- m) for some numeral m,
abbreviates the expression
(op (- (+ x ... x) (+ y ... y)) c) with n occurrences of x and y.
"
)
