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 /test | |
| 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 'test')
| -rw-r--r-- | test/unit/theory/logic_info_white.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index a0d415296..39d8aadb1 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -555,10 +555,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areRealsUsed() ); + TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException ); // check copy is unchanged info = info.getUnlockedCopy(); @@ -574,10 +574,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areRealsUsed() ); + TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException ); // check all-included logic info = info.getUnlockedCopy(); |