diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
| commit | 488ae3f42d9d3e06978e11a42d1d47e76072f797 (patch) | |
| tree | f466859889ceee9947e20d695fd35f99065277f8 /src/theory/arith/kinds | |
| parent | fe2088f892af594765fc50d8cc9f2b4f87286b7c (diff) | |
This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.
Diffstat (limited to 'src/theory/arith/kinds')
| -rw-r--r-- | src/theory/arith/kinds | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 95d7d6ed1..e00d8dc5e 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -31,7 +31,7 @@ sort REAL_TYPE \ sort INTEGER_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(Integer(0))" \ + "NodeManager::currentNM()->mkConst(Rational(0))" \ "expr/node_manager.h" \ "Integer type" sort PSEUDOBOOLEAN_TYPE \ @@ -59,11 +59,7 @@ constant CONST_RATIONAL \ ::CVC4::RationalHashStrategy \ "util/rational.h" \ "a multiple-precision rational constant" -constant CONST_INTEGER \ - ::CVC4::Integer \ - ::CVC4::IntegerHashStrategy \ - "util/integer.h" \ - "a multiple-precision integer constant" + constant CONST_PSEUDOBOOLEAN \ ::CVC4::Pseudoboolean \ ::CVC4::PseudobooleanHashStrategy \ @@ -83,7 +79,6 @@ typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule -typerule CONST_INTEGER ::CVC4::theory::arith::ArithConstantTypeRule typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule |