bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)

When we eagerly bitblast to the main SAT solver, we have to make sure that we don't use the equality engine in order to not start propagating equalities below BITVECTOR_EAGER_ATOM predicates.

Fixes the nightly failure.

diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp
index 0c43cddbf3118900218775fd2375e615757bf33d..1d864e72a1fc3a17cfd69dd474df72df6297ffb7 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast_internal.cpp
+++ b/src/theory/bv/bv_solver_bitblast_internal.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/bv/bv_solver_bitblast_internal.h"
 
+#include "options/bv_options.h"
 #include "proof/conv_proof_generator.h"
 #include "theory/bv/bitblast/bitblast_proof_generator.h"
 #include "theory/bv/theory_bv.h"
@@ -103,6 +104,12 @@ void BVSolverBitblastInternal::addBBLemma(TNode fact)
   }
 }
 
+bool BVSolverBitblastInternal::needsEqualityEngine(EeSetupInfo& esi)
+{
+  // Disable equality engine if --bitblast=eager is enabled.
+  return options().bv.bitblastMode != options::BitblastMode::EAGER;
+}
+
 bool BVSolverBitblastInternal::preNotifyFact(
     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 {
@@ -141,7 +148,9 @@ bool BVSolverBitblastInternal::preNotifyFact(
     }
   }
 
-  return false;  // Return false to enable equality engine reasoning in Theory.
+  // Disable the equality engine in --bitblast=eager mode. Otherwise return
+  // false to enable equality engine reasoning in Theory.
+  return options().bv.bitblastMode == options::BitblastMode::EAGER;
 }
 
 TrustNode BVSolverBitblastInternal::explain(TNode n)

diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h
index 2c53b9056de290fbd95bd52d119a8a00b1004d8b..08c618880f0aeb4f04f790b8b95125e30e0d12d0 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast_internal.h
+++ b/src/theory/bv/bv_solver_bitblast_internal.h
@@ -44,7 +44,7 @@ class BVSolverBitblastInternal : public BVSolver
                            ProofNodeManager* pnm);
   ~BVSolverBitblastInternal() = default;
 
-  bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
 
   void preRegisterTerm(TNode n) override {}