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/kinds | |
| parent | 76b8bdc51693af0867de94fe6002e8a8bec9e5f9 (diff) | |
This commit removes the dead psuedoboolean code.
Diffstat (limited to 'src/theory/arith/kinds')
| -rw-r--r-- | src/theory/arith/kinds | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index e00d8dc5e..8ffe68376 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -34,12 +34,6 @@ sort INTEGER_TYPE \ "NodeManager::currentNM()->mkConst(Rational(0))" \ "expr/node_manager.h" \ "Integer type" -sort PSEUDOBOOLEAN_TYPE \ - 2 \ - well-founded \ - "NodeManager::currentNM()->mkConst(Pseudoboolean(0))" \ - "expr/node_manager.h" \ - "Pseudoboolean type" constant SUBRANGE_TYPE \ ::CVC4::SubrangeBounds \ @@ -60,12 +54,6 @@ constant CONST_RATIONAL \ "util/rational.h" \ "a multiple-precision rational constant" -constant CONST_PSEUDOBOOLEAN \ - ::CVC4::Pseudoboolean \ - ::CVC4::PseudobooleanHashStrategy \ - "util/pseudoboolean.h" \ - "a pseudoboolean constant" - operator LT 2 "less than, x < y" operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" |