From 735bf7daa07b016aa7964cabdcef27a918d4a96a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 28 May 2013 13:29:59 -0400 Subject: 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. --- test/unit/theory/logic_info_white.h | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'test/unit/theory/logic_info_white.h') 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(); -- cgit v1.2.3