src/theory/arith/type_enumerator.h

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