summaryrefslogtreecommitdiff
path: root/src/theory/booleans/theory_bool.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-05-27 20:34:18 +0000
committerTim King <taking@cs.nyu.edu>2010-05-27 20:34:18 +0000
commitd1acfe81a013d1f8960bd0267dcd685185ffc785 (patch)
tree70870c5ccbea9fff7edf5ba26c5f8e68fe16c20e /src/theory/booleans/theory_bool.h
parente5c77b0674a9cb698e6012ccc1950fef9bee4f8d (diff)
Preregistration has been turned on. Highly experimental eager splitting support has been added. Also a few bug fixes to Tableau.
Diffstat (limited to 'src/theory/booleans/theory_bool.h')
-rw-r--r--src/theory/booleans/theory_bool.h11
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index eb6e84c39..b39663449 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -31,11 +31,18 @@ public:
Theory(c, out) {
}
- void preRegisterTerm(TNode n) { Unimplemented(); }
- void registerTerm(TNode n) { Unimplemented(); }
+ void preRegisterTerm(TNode n) {
+ Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
+ Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
+ }
+ void registerTerm(TNode n) {
+ Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
+ Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
+ }
void check(Effort e) { Unimplemented(); }
void propagate(Effort e) { Unimplemented(); }
void explain(TNode n, Effort e) { Unimplemented(); }
+
};
}/* CVC4::theory::booleans namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback