diff options
| author | lianah <lianahady@gmail.com> | 2013-03-13 13:44:33 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-03-13 13:44:33 -0400 |
| commit | 3fcdb18fe92e5213aa708285c0d7d5e55633492b (patch) | |
| tree | bbbd57efd9a8063a976a55afa7c384fb67db9b17 /src/theory/bv/theory_bv.h | |
| parent | 267ad0ceb6808bd4c05d7c4bb04a7886efc19eab (diff) | |
| parent | 9817df56827b4ee0ee67a33361f8619c5d1df6ed (diff) | |
post failed attempts at getting the incremental solver to work
Diffstat (limited to 'src/theory/bv/theory_bv.h')
| -rw-r--r-- | src/theory/bv/theory_bv.h | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ec72f40e1..3e14584ed 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -25,7 +25,6 @@ #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" -#include "context/cdqueue.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/bv_subtheory_eq.h" #include "theory/bv/bv_subtheory_core.h" @@ -46,11 +45,8 @@ class TheoryBV : public Theory { context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; Slicer d_slicer; - - context::CDQueue<TNode> d_bitblastAssertionsQueue; - BitblastSolver d_bitblastSolver; - CoreSolver d_coreSolver; + CoreSolver d_coreSolver; public: |