diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-16 22:41:07 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-16 22:41:07 +0000 |
commit | 958b0b56aad79df431376344420106115ab23778 (patch) | |
tree | 803931308136c01077f67c3a6092920c045ebf8d /test/unit | |
parent | 7b624d5052e196eb7d465a1979263fa1e3376f65 (diff) |
The SmtEngine now ensures that setLogicInternal() is called even if there is no explicit setLogic(). This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses. setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.
This means that the CVC language can now take advantage of statistics.
Also added the ability to set the logic from CVC presentation language via (e.g.)
OPTION "logic" "QF_UFLIA";
Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality. Kshitij may have a fix (I warned him about this commit).
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/logic_info_white.h | 52 |
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() { |