diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-11-02 15:01:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-02 22:01:01 +0000 |
commit | 217a258f4b52d8776c344f9c3d0d9e79aec060a5 (patch) | |
tree | 4d79f8e5543f5620b3975155c3f6229899e5a461 | |
parent | 0c16abf2d7fe9a18494d3c9867567c43a1655200 (diff) |
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.
-rw-r--r-- | src/theory/bv/bv_solver_bitblast_internal.cpp | 11 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_bitblast_internal.h | 2 |
2 files changed, 11 insertions, 2 deletions
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 {} |