(logic AUFNIRA
:smt-lib-version 2.6
:smt-lib-release "2017-11-24"
:written-by "Cesare Tinelli and Clark Barrett"
:date "2010-05-12"
: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.
2012-09-26 Clarified in :notes in what way AUFNIRA extendes AUFLIRA.
"
:theories (Reals_Ints ArraysEx)
:language
"Closed formulas built over arbitrary expansions of the Reals_Ints and
ArraysEx signatures with free sort and function symbols.
"
: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))
"
:notes
"This logic properly extends the logic AUFLIRA by allowing
- non-linear (integer/real) operators such as *, /, div, mod, and abs, and
- allowing terms with an arbitrary array sort (as opposed to just
(Array Int Real) and (Array Int (Array Int Real)) ).
"
)
