Commit 8be3a9a2 authored by Cristina Serban's avatar Cristina Serban
Browse files

Add new logics and theories

parent 0568ca51
(logic ALIA
:theories (Ints ArraysEx)
)
(logic LIA
:theories (Ints)
)
(logic NIA
:smt-lib-version 2.5
:written-by "Cesare Tinelli"
:date "2010-05-12"
:last-updated "2015-04-25"
:update-history
"2015-04-25 Updated to Version 2.5.
"
:theories ( Ints )
:language
"Closed formulas built over an arbitrary expansion of the
Ints signature with free constant symbols.
"
)
(logic NRA
:theories ( Reals )
)
(logic ALIA
:theories (Ints ArraysEx)
)
(logic UFNIA
:smt-lib-version 2.5
:written-by "Cesare Tinelli"
:date "2011-06-11"
:last-updated "2015-04-25"
:update-history
"2015-04-25 Updated to Version 2.5.
"
:theories ( Ints )
:language
"Closed formulas built over an arbitrary expansion of the Ints signature
with free sort and function symbols."
)
(logic SL
:theories (SepLogic)
)
(logic UF
:theories () ; includes just Core theory
)
(logic UFIDL
:theories (Ints)
)
(logic UFLIA
:theories ( Ints )
)
(theory SepLogic
:sorts ((Ref 1))
:funs ((emp Bool)
(sep Bool Bool Bool :left-assoc)
(par (A) (pto (Ref A) A Bool))
(par (A) (nil (Ref A)))
)
)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment