From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 17 May 2012 20:45:32 +0000 (+0000)
Subject: Fixing an issue with LogicInfo::isPure() that turned off simplification in QF_UF... 
X-Git-Tag: cvc5-1.0.0~8157
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f49378f9acb65b78ab29d89d37c644d0b203ebae;p=cvc5.git

Fixing an issue with LogicInfo::isPure() that turned off simplification in QF_UF and maybe others
---

diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 560b72509..d5b8be58d 100644
--- 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 77d18bd72..8bb3b52df 100644
--- 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 ) );