#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"
*/
ArithRewriter d_rewriter;
+ ArithUnatePropagator d_propagator;
public:
TheoryArith(context::Context* c, OutputChannel& out);
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(){ }
IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
Statistics();
+ ~Statistics();
};
Statistics d_statistics;