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).

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() {