diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-02-19 00:22:34 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-02-19 00:22:34 +0000 |
| commit | 0db4ec99a2f289b66878d0ca3be9d43492eff3ad (patch) | |
| tree | cdcb1badb92bf405c2be4f15a19bec05ea716c32 /src/theory/arith/theory_arith.h | |
| parent | 005066130a774c9e4aa838ca500d5fd3137909be (diff) | |
Changes:
- The Tableau is now in charge of managing what variables are basic in a unified manner. Specifically, TheoryArith::d_basicManager was merged into Tableau::d_basicVariables.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
| -rw-r--r-- | src/theory/arith/theory_arith.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index efd1adde4..60d24708c 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -89,7 +89,9 @@ private: */ ArithPartialModel d_partialModel; - ArithVarSet d_basicManager; + /** + * Set of ArithVars that were introduced via preregisteration. + */ ArithVarSet d_userVariables; /** @@ -100,7 +102,6 @@ private: inline bool hasArithVar(TNode x) const { return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); - //return x.hasAttribute(ArithVarAttr()); } inline ArithVar asArithVar(TNode x) const{ |