src/theory/arith/type_enumerator.h

   1 /*********************                                                        */
   2 /*! \file type_enumerator.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Enumerators for rationals and integers
  15  **
  16  ** Enumerators for rationals and integers.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
  22 #define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
  23
  24 #include "util/integer.h"
  25 #include "util/rational.h"
  26 #include "theory/type_enumerator.h"
  27 #include "expr/type_node.h"
  28 #include "expr/kind.h"
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace arith {
  33
  34 class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
  35   Rational d_rat;
  36
  37 public:
  38
  39   RationalEnumerator(TypeNode type) throw(AssertionException) :
  40     TypeEnumeratorBase(type),
  41     d_rat(0) {
  42     Assert(type.getKind() == kind::TYPE_CONSTANT &&
  43            type.getConst<TypeConstant>() == REAL_TYPE);
  44   }
  45
  46   Node operator*() throw() {
  47     return NodeManager::currentNM()->mkConst(d_rat);
  48   }
  49
  50   RationalEnumerator& operator++() throw() {
  51     // sequence is 0, then diagonal with negatives interleaved
  52     // ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3,
  53     // 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...)
  54     if(d_rat == 0) {
  55       d_rat = 1;
  56     } else if(d_rat < 0) {
  57       d_rat = -d_rat;
  58       Integer num = d_rat.getNumerator();
  59       Integer den = d_rat.getDenominator();
  60       do {
  61         num -= 1;
  62         den += 1;
  63         if(num == 0) {
  64           num = den;
  65           den = 1;
  66         }
  67         d_rat = Rational(num, den);
  68       } while(d_rat.getNumerator() != num);
  69     } else {
  70       d_rat = -d_rat;
  71     }
  72     return *this;
  73   }
  74
  75 };/* class RationalEnumerator */
  76
  77 class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
  78   Integer d_int;
  79
  80 public:
  81
  82   IntegerEnumerator(TypeNode type) throw(AssertionException) :
  83     TypeEnumeratorBase(type),
  84     d_int(0) {
  85     Assert(type.getKind() == kind::TYPE_CONSTANT &&
  86            type.getConst<TypeConstant>() == INTEGER_TYPE);
  87   }
  88
  89   Node operator*() throw() {
  90     return NodeManager::currentNM()->mkConst(Rational(d_int));
  91   }
  92
  93   IntegerEnumerator& operator++() throw() {
  94     // sequence is 0, 1, -1, 2, -2, 3, -3, ...
  95     if(d_int <= 0) {
  96       d_int = -d_int + 1;
  97     } else {
  98       d_int = -d_int;
  99     }
 100     return *this;
 101   }
 102
 103 };/* class IntegerEnumerator */
 104
 105 }/* CVC4::theory::arith namespace */
 106 }/* CVC4::theory namespace */
 107 }/* CVC4 namespace */
 108
 109 #endif /* __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */