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.

1 files changed, 5 insertions, 4 deletions

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 08d223137..e22be81e3 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -69,11 +69,12 @@ void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
 void InferenceManager::addPendingArithLemma(const Node& lemma,
                                             InferenceId inftype,
                                             ProofGenerator* pg,
-                                            bool isWaiting)
+                                            bool isWaiting,
+                                            LemmaProperty p)
 {
-  addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(
-                           lemma, LemmaProperty::NONE, pg, inftype)),
-                       isWaiting);
+  addPendingArithLemma(
+      std::unique_ptr<ArithLemma>(new ArithLemma(lemma, p, pg, inftype)),
+      isWaiting);
 }
 
 void InferenceManager::flushWaitingLemmas()