GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/builtin/type_enumerator.cpp Lines: 1 15 6.7 %
Date: 2021-03-23 Branches: 2 56 3.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 "theory/builtin/type_enumerator.h"
18
19
#include "theory/builtin/theory_builtin_rewriter.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace builtin {
24
25
FunctionEnumerator::FunctionEnumerator(TypeNode type,
26
                                       TypeEnumeratorProperties* tep)
27
    : TypeEnumeratorBase<FunctionEnumerator>(type),
28
      d_arrayEnum(TheoryBuiltinRewriter::getArrayTypeForFunctionType(type), tep)
29
{
30
  Assert(type.getKind() == kind::FUNCTION_TYPE);
31
  d_bvl = NodeManager::currentNM()->getBoundVarListForFunctionType(type);
32
}
33
34
Node FunctionEnumerator::operator*()
35
{
36
  if (isFinished())
37
  {
38
    throw NoMoreValuesException(getType());
39
  }
40
  Node a = *d_arrayEnum;
41
  return TheoryBuiltinRewriter::getLambdaForArrayRepresentation(a, d_bvl);
42
}
43
44
FunctionEnumerator& FunctionEnumerator::operator++()
45
{
46
  ++d_arrayEnum;
47
  return *this;
48
}
49
50
} /* CVC4::theory::builtin namespace */
51
} /* CVC4::theory namespace */
52
26685
} /* CVC4 namespace */