Add bitwise refinement mode for IAND (#5328)

Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits.

For example, with a 1-bit granularity, you might learn a lemma like:

((_ iand 4) x y), value = 1
  actual (2, 3) = 2
  bv-value = #b0001
  bv-actual (#b0010, #b0011) = #b0010
IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y))) 
         (and (and true 
                  (= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0))) 
                  (= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0)))) 
        ; BITWISE_REFINE

which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.

2 files changed, 6 insertions, 8 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index f14eafcc4..8539e639d 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -424,10 +424,10 @@ Node BVToInt::translateWithChildren(Node original,
         // Construct a sum of ites, based on granularity.
         Assert(translated_children.size() == 2);
         returnNode =
-            d_iandTable.createBitwiseNode(translated_children[0],
-                                          translated_children[1],
-                                          bvsize,
-                                          options::BVAndIntegerGranularity());
+            d_iandUtils.createSumNode(translated_children[0],
+                                      translated_children[1],
+                                      bvsize,
+                                      options::BVAndIntegerGranularity());
       }
       break;
     }
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index 0f6a6a4bb..dd830d7cf 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -47,8 +47,6 @@
  ** Tr((bvand s t)) =
  ** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g)
  **
- ** More details and examples for this case are described next to
- ** the function createBitwiseNode.
  ** Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor.
  **
  ** Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of
@@ -75,7 +73,7 @@
 #include "context/context.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "theory/arith/nl/iand_table.h"
+#include "theory/arith/nl/iand_utils.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -284,7 +282,7 @@ class BVToInt : public PreprocessingPass
   Node d_one;
   
   /** helper class for handeling bvand translation */
-  theory::arith::nl::IAndTable d_iandTable;
+  theory::arith::nl::IAndUtils d_iandUtils;
 };
 
 }  // namespace passes