(logic AUFLIRA
:smt-lib-version 2.6
:smt-lib-release "2017-11-24"
:written-by "Cesare Tinelli and Clark Barrett"
:date "2010-05-05"
: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.
2011-06-03 Replaced ""(* c x), or (* x c)"" with ""c, (* c x), or (* x c)""
in :extensions.
(The missing case was had been left out unintentionally.)
"
:theories (Reals_Ints ArraysEx)
:language
"Closed formulas built over arbitrary expansions of the Reals_Ints and
ArraysEx signatures with free sort and function symbols, but with the
following restrictions:
- all terms of sort Int are linear, that is, have no occurrences of the
function symbols *, /, div, mod, and abs, except as specified in the
:extensions attributes;
- all terms of sort Real are linear, that is, have no occurrences of the
function symbols * and /, except as specified in the
:extensions attribute;
- all array terms have sort
(Array Int Real) or
(Array Int (Array Int Real)).
"
:extensions
"For every operator op with declaration (op Real Real s) for some sort s,
and every term t1, t2 of sort Int and t of sort Real, the expression
- (op t1 t) is syntactic sugar for (op (to_real t1) t)
- (op t t1) is syntactic sugar for (op t (to_real t1))
- (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
"
:extensions
"Real or Int terms with _concrete_ coefficients are also allowed, that is,
terms of the form c, (* c x), or (* x c) where
x is a free constant of sort Int or Real and
c is an integer or rational coefficient, respectively.
- An integer coefficient is a term of the form m or (- m) for some
numeral m.
- A rational coefficient is a term of the form d, (- d) or (/ c n)
for some decimal d, integer coefficient c and numeral n other than 0.
"
)
