diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src/theory/bv/theory_bv.h | |
parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f6073eff9..dfae3b965 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -61,8 +61,8 @@ private: public: - TheoryBV(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out), d_eqEngine(*this, c), d_assertions(c) { + TheoryBV(context::Context* c, OutputChannel& out) : + Theory(THEORY_BV, c, out), d_eqEngine(*this, c), d_assertions(c) { } void preRegisterTerm(TNode n); @@ -71,18 +71,14 @@ public: void check(Effort e); - void presolve(){ - Unimplemented(); - } + void presolve() { } - void propagate(Effort e) {} + void propagate(Effort e) { } - void explain(TNode n, Effort e) { } + void explain(TNode n) { } Node getValue(TNode n, TheoryEngine* engine); - RewriteResponse postRewrite(TNode n, bool topLevel); - std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */ |