From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 2 Nov 2021 22:01:01 +0000 (-0700)
Subject: bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)
X-Git-Tag: cvc5-1.0.0~904
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=217a258f4b52d8776c344f9c3d0d9e79aec060a5;p=cvc5.git

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 0c43cddbf..1d864e72a 100644
--- 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 2c53b9056..08c618880 100644
--- 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 {}