GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/builtin/type_enumerator.h Lines: 24 27 88.9 %
Date: 2021-03-22 Branches: 35 84 41.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Tim King
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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 Enumerator for uninterpreted sorts and functions.
13
 **
14
 ** Enumerator for uninterpreted sorts and functions.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
20
#define CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
21
22
#include "expr/kind.h"
23
#include "expr/type_node.h"
24
#include "expr/uninterpreted_constant.h"
25
#include "theory/type_enumerator.h"
26
#include "util/integer.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace builtin {
31
32
7620
class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortEnumerator> {
33
  Integer d_count;
34
  bool d_has_fixed_bound;
35
  Integer d_fixed_bound;
36
37
 public:
38
3330
  UninterpretedSortEnumerator(TypeNode type,
39
                              TypeEnumeratorProperties* tep = nullptr)
40
3330
      : TypeEnumeratorBase<UninterpretedSortEnumerator>(type), d_count(0)
41
  {
42
3330
    Assert(type.getKind() == kind::SORT_TYPE);
43
3330
    d_has_fixed_bound = false;
44
3330
    Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl;
45
3330
    if( tep && tep->d_fixed_usort_card ){
46
2675
      d_has_fixed_bound = true;
47
2675
      std::map< TypeNode, Integer >::iterator it = tep->d_fixed_card.find( type );
48
2675
      if( it!=tep->d_fixed_card.end() ){
49
2675
        d_fixed_bound = it->second;
50
      }else{
51
        d_fixed_bound = Integer(1);
52
      }
53
2675
      Trace("uf-type-enum") << "...fixed bound : " << d_fixed_bound << std::endl;
54
    }
55
3330
  }
56
57
19526
  Node operator*() override
58
  {
59
19526
    if(isFinished()) {
60
976
      throw NoMoreValuesException(getType());
61
    }
62
    return NodeManager::currentNM()->mkConst(
63
18550
        UninterpretedConstant(getType(), d_count));
64
  }
65
66
6420
  UninterpretedSortEnumerator& operator++() override
67
  {
68
6420
    d_count += 1;
69
6420
    return *this;
70
  }
71
72
45274
  bool isFinished() override
73
  {
74
45274
    if( d_has_fixed_bound ){
75
34973
      return d_count>=d_fixed_bound;
76
    }else{
77
10301
      return false;
78
    }
79
  }
80
81
};/* class UninterpretedSortEnumerator */
82
83
/** FunctionEnumerator
84
* This enumerates function values, based on the enumerator for the
85
* array type corresponding to the given function type.
86
*/
87
class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator>
88
{
89
 public:
90
  FunctionEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
91
  /** Get the current term of the enumerator. */
92
  Node operator*() override;
93
  /** Increment the enumerator. */
94
  FunctionEnumerator& operator++() override;
95
  /** is the enumerator finished? */
96
  bool isFinished() override { return d_arrayEnum.isFinished(); }
97
 private:
98
  /** Enumerates arrays, which we convert to functions. */
99
  TypeEnumerator d_arrayEnum;
100
  /** The bound variable list for the function type we are enumerating.
101
  * All terms output by this enumerator are of the form (LAMBDA d_bvl t) for
102
  * some term t.
103
  */
104
  Node d_bvl;
105
}; /* class FunctionEnumerator */
106
107
}/* CVC4::theory::builtin namespace */
108
}/* CVC4::theory namespace */
109
}/* CVC4 namespace */
110
111
#endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */