diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-05-27 20:34:18 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-05-27 20:34:18 +0000 |
| commit | d1acfe81a013d1f8960bd0267dcd685185ffc785 (patch) | |
| tree | 70870c5ccbea9fff7edf5ba26c5f8e68fe16c20e /src/theory/arith/theory_arith.h | |
| parent | e5c77b0674a9cb698e6012ccc1950fef9bee4f8d (diff) | |
Preregistration has been turned on. Highly experimental eager splitting support has been added. Also a few bug fixes to Tableau.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
| -rw-r--r-- | src/theory/arith/theory_arith.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 7bfa535a8..1d6cca5cc 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -38,6 +38,10 @@ class TheoryArith : public Theory { private: /* Chopping block begins */ + std::vector<Node> d_splits; + //This stores the eager splits sent out of the theory. + //TODO get rid of this. + context::CDList<Node> d_preprocessed; //TODO This is currently needed to save preprocessed nodes that may not //currently have an outisde reference. Get rid of when preprocessing is occuring @@ -65,7 +69,7 @@ public: Node rewrite(TNode n); - void preRegisterTerm(TNode n) { Unimplemented(); } + void preRegisterTerm(TNode n); void registerTerm(TNode n); void check(Effort e); void propagate(Effort e) { Unimplemented(); } |