summaryrefslogtreecommitdiff
path: root/test/unit/theory/logic_info_white.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/theory/logic_info_white.h')
-rw-r--r--test/unit/theory/logic_info_white.h99
1 files changed, 59 insertions, 40 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index f5ef8e15e..427bcc34d 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -457,27 +457,41 @@ public:
LogicInfo info;
TS_ASSERT( !info.isLocked() );
- TS_ASSERT_THROWS( info.getLogicString(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAYS ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAYS ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( !info.isLinear(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS(info.getLogicString(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BUILTIN),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BOOL),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_UF),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_ARITH),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_ARRAYS),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BV),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_DATATYPES),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_QUANTIFIERS),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_BUILTIN),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_BOOL),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_UF), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_ARITH),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_ARRAYS),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_BV), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_DATATYPES),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isPure(THEORY_QUANTIFIERS),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isQuantified(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areIntegersUsed(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areRealsUsed(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(!info.isLinear(), CVC4::IllegalArgumentException&);
info.lock();
TS_ASSERT( info.isLocked() );
@@ -505,15 +519,20 @@ public:
TS_ASSERT(info.areTranscendentalsUsed());
TS_ASSERT( !info.isLinear() );
- TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.enableIntegers(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.disableReals(), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::IllegalArgumentException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS(info.arithOnlyLinear(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.disableIntegers(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.disableQuantifiers(),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.disableTheory(THEORY_BV),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.disableTheory(THEORY_DATATYPES),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.enableIntegers(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.disableReals(), CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.disableTheory(THEORY_ARITH),
+ CVC4::IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.disableTheory(THEORY_UF),
+ CVC4::IllegalArgumentException&);
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
@@ -565,11 +584,11 @@ public:
TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
- TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException );
- TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
- TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
- TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
- TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
+ TS_ASSERT_THROWS(info.isLinear(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areIntegersUsed(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isDifferenceLogic(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areRealsUsed(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException&);
// check copy is unchanged
info = info.getUnlockedCopy();
@@ -585,11 +604,11 @@ public:
TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
- TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException );
- TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
- TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
- TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
- TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
+ TS_ASSERT_THROWS(info.isLinear(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areIntegersUsed(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.isDifferenceLogic(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areRealsUsed(), IllegalArgumentException&);
+ TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException&);
// check all-included logic
info = info.getUnlockedCopy();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback