summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2012-05-08 21:54:55 +0000
committerLiana Hadarean <lianahady@gmail.com>2012-05-08 21:54:55 +0000
commit8a0c0562cb8d0e26ea019ff782b25c1997a49a0b (patch)
tree28239db9bcb26b03d893ad61dd1a7ea099391fbe /src/theory/theory_engine.h
parent5082cb8349efbb287084293cd4bc6c3fa5a34f26 (diff)
Merging in bvprop branch, with proper bit-vector propagation.
This should also fix bug 325.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2b4fd24d1..0a0778ebc 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -499,6 +499,16 @@ private:
*/
Node ppTheoryRewrite(TNode term);
+ /**
+ * Queue of nodes for pre-registration.
+ */
+ std::queue<TNode> d_preregisterQueue;
+
+ /**
+ * Boolean flag denoting we are in pre-registration.
+ */
+ bool d_inPreregister;
+
public:
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback