Standardize SMT-LIBv2 set of logics to use LogicInfo.
authorMorgan Deters <mdeters@cs.nyu.edu>
Tue, 28 May 2013 17:29:59 +0000 (13:29 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Tue, 28 May 2013 20:30:14 +0000 (16:30 -0400)
commit735bf7daa07b016aa7964cabdcef27a918d4a96a
tree2b322d405693ceea219b70ddcf3dc3e14e47b283
parent7709fff002e3345bd727eaef2677e28830efb84d
Standardize SMT-LIBv2 set of logics to use LogicInfo.

Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort.  Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols.  SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/theory/logic_info.h
test/unit/theory/logic_info_white.h