1 /********************* */
2 /*! \file type_enumerator.h
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
14 ** \brief Enumerators for rationals and integers
16 ** Enumerators for rationals and integers.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
22 #define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
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"
34 class RationalEnumerator
: public TypeEnumeratorBase
<RationalEnumerator
> {
39 RationalEnumerator(TypeNode type
) throw(AssertionException
) :
40 TypeEnumeratorBase
<RationalEnumerator
>(type
),
42 Assert(type
.getKind() == kind::TYPE_CONSTANT
&&
43 type
.getConst
<TypeConstant
>() == REAL_TYPE
);
46 Node
operator*() throw() {
47 return NodeManager::currentNM()->mkConst(d_rat
);
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, ...)
56 } else if(d_rat
< 0) {
58 Integer num
= d_rat
.getNumerator();
59 Integer den
= d_rat
.getDenominator();
67 d_rat
= Rational(num
, den
);
68 } while(d_rat
.getNumerator() != num
);
75 };/* class RationalEnumerator */
77 class IntegerEnumerator
: public TypeEnumeratorBase
<IntegerEnumerator
> {
82 IntegerEnumerator(TypeNode type
) throw(AssertionException
) :
83 TypeEnumeratorBase
<IntegerEnumerator
>(type
),
85 Assert(type
.getKind() == kind::TYPE_CONSTANT
&&
86 type
.getConst
<TypeConstant
>() == INTEGER_TYPE
);
89 Node
operator*() throw() {
90 return NodeManager::currentNM()->mkConst(Rational(d_int
));
93 IntegerEnumerator
& operator++() throw() {
94 // sequence is 0, 1, -1, 2, -2, 3, -3, ...
103 };/* class IntegerEnumerator */
105 }/* CVC4::theory::arith namespace */
106 }/* CVC4::theory namespace */
107 }/* CVC4 namespace */
109 #endif /* __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */