summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-11-16 21:11:11 +0000
committerTim King <taking@cs.nyu.edu>2010-11-16 21:11:11 +0000
commitbb2a0e0e12f39a1b4dea8fb0c990decba4708a1c (patch)
tree6e5824f8cf1b0f1cb32e6cae5cbd214b1b48d965 /src/theory/bv
parente66924cb0f425ca70969058532340e68c9c17a54 (diff)
Added Theory::presolve().
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/theory_bv.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c673a56b4..f6073eff9 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -71,6 +71,10 @@ public:
void check(Effort e);
+ void presolve(){
+ Unimplemented();
+ }
+
void propagate(Effort e) {}
void explain(TNode n, Effort e) { }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback