Fixing an issue with LogicInfo::isPure() that turned off simplification in QF_UF...

diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 560b7250970997a6b8915ce48c61f50714e87d97..d5b8be58d2913691b39d96a8fbd1f79b459f649e 100644 (file)
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -110,10 +110,11 @@ public:
    * use "isPure(theory) && !isQuantified()".
    */
   bool isPure(theory::TheoryId theory) const {
-    // the third conjuct is really just to rule out the misleading case where you ask
-    // isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
+    // the third and fourth conjucts are really just to rule out the misleading
+    // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
     return isTheoryEnabled(theory) && !isSharingEnabled() &&
-      ( !isTrueTheory(theory) || d_sharingTheories == 1 );
+      ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
+      ( isTrueTheory(theory) || d_sharingTheories == 0 );
   }
 
   // these are for arithmetic

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 77d18bd728881eec6d97fec197d98447c7a65b4e..8bb3b52df0d0e891c9b24cadaf8eb0d5b209073b 100644 (file)
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -37,6 +37,7 @@ public:
     TS_ASSERT( !info.isQuantified() );
 
     info.setLogicString("AUFLIA");
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -50,6 +51,7 @@ public:
     TS_ASSERT( !info.areRealsUsed() );
 
     info.setLogicString("AUFLIRA");
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -63,6 +65,7 @@ public:
     TS_ASSERT( info.areRealsUsed() );
 
     info.setLogicString("AUFNIRA");
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -76,6 +79,7 @@ public:
     TS_ASSERT( info.areRealsUsed() );
 
     info.setLogicString("LRA");
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -90,6 +94,7 @@ public:
     TS_ASSERT( info.areRealsUsed() );
 
     info.setLogicString("QF_ABV");
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -228,6 +233,7 @@ public:
     TS_ASSERT( info.areRealsUsed() );
 
     info.setLogicString("QF_UF");
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );