diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-18 20:20:58 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-18 20:20:58 +0000 |
commit | 3b93d45dab9513195d5604a069423ed13e173f49 (patch) | |
tree | 96497114c06755a14efe0d30c680703c9aa5380b /src/theory/arith/theory_arith.h | |
parent | 76b8bdc51693af0867de94fe6002e8a8bec9e5f9 (diff) |
This commit removes the dead psuedoboolean code.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 4aac76eac..431c82476 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -112,31 +112,25 @@ private: /** * (For the moment) the type hierarchy goes as: - * PsuedoBoolean <: Integer <: Real + * Integer <: Real * The type number of a variable is an integer representing the most specific * type of the variable. The possible values of type number are: */ enum ArithType { ATReal = 0, - ATInteger = 1, - ATPsuedoBoolean = 2 + ATInteger = 1 }; std::vector<ArithType> d_variableTypes; inline ArithType nodeToArithType(TNode x) const { - return x.getType().isPseudoboolean() ? ATPsuedoBoolean : - (x.getType().isInteger() ? ATInteger : ATReal); + return (x.getType().isInteger() ? ATInteger : ATReal); } - /** Returns true if x is of type Integer or PsuedoBoolean. */ + /** Returns true if x is of type Integer. */ inline bool isInteger(ArithVar x) const { return d_variableTypes[x] >= ATInteger; } - /** Returns true if x is of type PsuedoBoolean. */ - inline bool isPsuedoBoolean(ArithVar x) const { - return d_variableTypes[x] == ATPsuedoBoolean; - } /** This is the set of variables initially introduced as slack variables. */ std::vector<bool> d_slackVars; |