GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/builtin/theory_builtin_type_rules.cpp Lines: 8 8 100.0 %
Date: 2021-03-23 Branches: 15 42 35.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_builtin_type_rules.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Type rules for the builtin theory
13
 **
14
 ** Type rules for the builtin theory.
15
 **/
16
17
#include "theory/builtin/theory_builtin_type_rules.h"
18
19
#include "expr/attribute.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace builtin {
24
25
/**
26
 * Attribute for caching the ground term for each type. Maps TypeNode to the
27
 * skolem to return for mkGroundTerm.
28
 */
29
struct GroundTermAttributeId
30
{
31
};
32
typedef expr::Attribute<GroundTermAttributeId, Node> GroundTermAttribute;
33
34
265
Node SortProperties::mkGroundTerm(TypeNode type)
35
{
36
265
  Assert(type.getKind() == kind::SORT_TYPE);
37
  GroundTermAttribute gta;
38
265
  if (type.hasAttribute(gta))
39
  {
40
244
    return type.getAttribute(gta);
41
  }
42
  Node k = NodeManager::currentNM()->mkSkolem(
43
42
      "groundTerm", type, "a ground term created for type " + type.toString());
44
21
  type.setAttribute(gta, k);
45
21
  return k;
46
}
47
48
}  // namespace builtin
49
}  // namespace theory
50
26685
}  // namespace CVC4