diff options
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 25 |
1 files changed, 4 insertions, 21 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e9ff06adb..c95ca6cc4 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -94,31 +94,14 @@ private: */ Tableau d_tableau; - /** - * The rewriter module for arithmetic. - */ - ArithRewriter d_rewriter; - ArithUnatePropagator d_propagator; SimplexDecisionProcedure d_simplex; public: - TheoryArith(int id, context::Context* c, OutputChannel& out); + TheoryArith(context::Context* c, OutputChannel& out); ~TheoryArith(); /** - * Rewriting optimizations. - */ - RewriteResponse preRewrite(TNode n, bool topLevel); - - /** - * Plug in old rewrite to the new (pre,post)rewrite interface. - */ - RewriteResponse postRewrite(TNode n, bool topLevel) { - return d_rewriter.postRewrite(n); - } - - /** * Does non-context dependent setup for a node connected to a theory. */ void preRegisterTerm(TNode n); @@ -128,7 +111,9 @@ public: void check(Effort e); void propagate(Effort e); - void explain(TNode n, Effort e); + void explain(TNode n); + + void notifyEq(TNode lhs, TNode rhs); Node getValue(TNode n, TheoryEngine* engine); @@ -144,8 +129,6 @@ public: private: - bool isTheoryLeaf(TNode x) const; - ArithVar determineLeftVariable(TNode assertion, Kind simpleKind); |