diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-20 01:08:32 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-20 01:08:32 +0000 |
commit | 1b30b256a0ec40ff431b83296bfe5aa0e099eb2e (patch) | |
tree | 91fb063e9cfcf360d601e21a19996995576ece7d /src/theory/bv/theory_bv.h | |
parent | 9eaf94708275337a4749b7ef2f44bf1c6746d8fc (diff) |
bitvector rewriting for the core theory and testcases
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 537e7f5fe..ee331af02 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -33,12 +33,12 @@ public: TheoryBV(int id, context::Context* c, OutputChannel& out) : Theory(id, c, out) { } - - void preRegisterTerm(TNode n) { Unimplemented(); } - void registerTerm(TNode n) { Unimplemented(); } + void preRegisterTerm(TNode n) { } + void registerTerm(TNode n) { } void check(Effort e) {} void propagate(Effort e) {} - void explain(TNode n, Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { } + RewriteResponse postRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */ |