src/theory/arith/type_enumerator.h

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