summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r--src/theory/arith/theory_arith.h7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index aff60f651..c76923bee 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -30,6 +30,7 @@
#include "theory/arith/tableau.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/partial_model.h"
+#include "theory/arith/arith_propagator.h"
#include "util/stats.h"
@@ -96,6 +97,7 @@ private:
*/
ArithRewriter d_rewriter;
+ ArithUnatePropagator d_propagator;
public:
TheoryArith(context::Context* c, OutputChannel& out);
@@ -115,8 +117,8 @@ public:
void registerTerm(TNode n);
void check(Effort e);
- void propagate(Effort e) { Unimplemented(); }
- void explain(TNode n, Effort e) { Unimplemented(); }
+ void propagate(Effort e);
+ void explain(TNode n, Effort e);
void shutdown(){ }
@@ -242,6 +244,7 @@ private:
IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
Statistics();
+ ~Statistics();
};
Statistics d_statistics;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback