summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/theory/logic_info_white.h52
1 files changed, 52 insertions, 0 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 069f99d0b..a2f61f5d2 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -36,6 +36,8 @@ public:
TS_ASSERT( !info.isSharingEnabled() );
TS_ASSERT( info.isPure( THEORY_BOOL ) );
TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( info.hasNothing() );
info = LogicInfo("AUFLIA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -51,6 +53,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("AUFLIRA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -66,6 +70,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("AUFNIRA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -81,6 +87,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("LRA");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -97,6 +105,8 @@ public:
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_ABV");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -109,6 +119,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_AUFBV");
TS_ASSERT( !info.isQuantified() );
@@ -120,6 +132,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_AUFLIA");
TS_ASSERT( !info.isQuantified() );
@@ -135,6 +149,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_AX");
TS_ASSERT( !info.isQuantified() );
@@ -146,6 +162,8 @@ public:
TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_BV");
TS_ASSERT( !info.isQuantified() );
@@ -157,6 +175,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_IDL");
TS_ASSERT( !info.isQuantified() );
@@ -172,6 +192,8 @@ public:
TS_ASSERT( info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_LIA");
TS_ASSERT( !info.isQuantified() );
@@ -187,6 +209,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_LRA");
TS_ASSERT( !info.isQuantified() );
@@ -202,6 +226,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_NIA");
TS_ASSERT( !info.isQuantified() );
@@ -217,6 +243,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_NRA");
TS_ASSERT( !info.isQuantified() );
@@ -232,6 +260,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_RDL");
TS_ASSERT( !info.isQuantified() );
@@ -247,6 +277,8 @@ public:
TS_ASSERT( info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UF");
TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -259,6 +291,8 @@ public:
TS_ASSERT( info.isPure( THEORY_UF ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFBV");
TS_ASSERT( !info.isQuantified() );
@@ -271,6 +305,8 @@ public:
TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFIDL");
TS_ASSERT( !info.isQuantified() );
@@ -286,6 +322,8 @@ public:
TS_ASSERT( info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFLIA");
TS_ASSERT( !info.isQuantified() );
@@ -301,6 +339,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFLRA");
TS_ASSERT( !info.isQuantified() );
@@ -315,6 +355,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_UFNRA");
TS_ASSERT( !info.isQuantified() );
@@ -330,6 +372,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("UFLRA");
TS_ASSERT( info.isQuantified() );
@@ -345,6 +389,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( !info.areIntegersUsed() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("UFNIA");
TS_ASSERT( info.isQuantified() );
@@ -360,6 +406,8 @@ public:
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("QF_ALL_SUPPORTED");
TS_ASSERT( info.isLocked() );
@@ -376,6 +424,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( !info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
info = LogicInfo("ALL_SUPPORTED");
TS_ASSERT( info.isLocked() );
@@ -392,6 +442,8 @@ public:
TS_ASSERT( info.areIntegersUsed() );
TS_ASSERT( !info.isDifferenceLogic() );
TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( info.hasEverything() );
+ TS_ASSERT( !info.hasNothing() );
}
void testDefaultLogic() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback