diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-28 13:29:59 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-28 16:30:14 -0400 |
| commit | 735bf7daa07b016aa7964cabdcef27a918d4a96a (patch) | |
| tree | 2b322d405693ceea219b70ddcf3dc3e14e47b283 /src/decision | |
| parent | 7709fff002e3345bd727eaef2677e28830efb84d (diff) | |
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.
Diffstat (limited to 'src/decision')
0 files changed, 0 insertions, 0 deletions