diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-02-13 06:08:37 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-13 08:08:37 -0600 |
| commit | 10f6aae991a550e2b970c6234ebdd75742d078dd (patch) | |
| tree | 22c10c1451d8d880e17e17884a1c676111cd7f45 /src/theory/bv/theory_bv.h | |
| parent | d47a8708171f1cf488fe9ce05f56f2566db53093 (diff) | |
Properly set up equality engine for BV bitblast solver. (#5905)
Theory BV now sets up the default equality engine for BV solvers that do not use their own equality engine like e.g. the BV bitblast solver. This commit also adds the missing equality engine pieces to the BV bitblast solver (getEqualityStatus, explain).
Diffstat (limited to 'src/theory/bv/theory_bv.h')
| -rw-r--r-- | src/theory/bv/theory_bv.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 306b1ff93..2aa722e48 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -23,6 +23,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/theory.h" +#include "theory/theory_eq_notify.h" namespace CVC4 { namespace theory { @@ -130,7 +131,10 @@ class TheoryBV : public Theory TheoryState d_state; /** A (default) theory inference manager. */ - TheoryInferenceManager d_inferMgr; + TheoryInferenceManager d_im; + + /** The notify class for equality engine. */ + TheoryEqNotifyClass d_notify; }; /* class TheoryBV */ |