summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.h
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-03-16 15:48:51 -0400
committerlianah <lianahady@gmail.com>2013-03-16 15:48:51 -0400
commit25ac2c8f4b45e2b299895e97a30790fbf46cf79f (patch)
treed7b52003d7157073be554bd9818230f1c3b439d3 /src/theory/bv/theory_bv.h
parent3fcdb18fe92e5213aa708285c0d7d5e55633492b (diff)
started work on the inequality bv subtheory
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r--src/theory/bv/theory_bv.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 3e14584ed..d457571e2 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -44,8 +44,8 @@ class TheoryBV : public Theory {
context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
- Slicer d_slicer;
BitblastSolver d_bitblastSolver;
+ // TODO generalize to multiple subtheories
CoreSolver d_coreSolver;
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback