GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_trie.cpp Lines: 20 27 74.1 %
Date: 2021-03-22 Branches: 36 94 38.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_trie.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 Implementation of a trie class for Nodes and TNodes.
13
 **/
14
15
#include "expr/node_trie.h"
16
17
namespace CVC4 {
18
namespace theory {
19
20
template <bool ref_count>
21
1898055
NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::existsTerm(
22
    const std::vector<NodeTemplate<ref_count>>& reps) const
23
{
24
1898055
  const NodeTemplateTrie<ref_count>* tnt = this;
25
  typename std::map<NodeTemplate<ref_count>,
26
1898055
                    NodeTemplateTrie<ref_count>>::const_iterator it;
27
5102159
  for (const NodeTemplate<ref_count>& r : reps)
28
  {
29
3828285
    it = tnt->d_data.find(r);
30
3828285
    if (it == tnt->d_data.end())
31
    {
32
      // didn't find this child, return null
33
624181
      return Node::null();
34
    }
35
3204104
    tnt = &it->second;
36
  }
37
1273874
  if (tnt->d_data.empty())
38
  {
39
1167
    return Node::null();
40
  }
41
1272707
  return tnt->d_data.begin()->first;
42
}
43
44
template TNode NodeTemplateTrie<false>::existsTerm(
45
    const std::vector<TNode>& reps) const;
46
template Node NodeTemplateTrie<true>::existsTerm(
47
    const std::vector<Node>& reps) const;
48
49
template <bool ref_count>
50
1769566
NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::addOrGetTerm(
51
    NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
52
{
53
1769566
  NodeTemplateTrie<ref_count>* tnt = this;
54
4787015
  for (const NodeTemplate<ref_count>& r : reps)
55
  {
56
3017449
    tnt = &(tnt->d_data[r]);
57
  }
58
1769566
  if (tnt->d_data.empty())
59
  {
60
    // Store n in d_data. This should be interpretted as the "data" and not as a
61
    // reference to a child.
62
1336926
    tnt->d_data[n].clear();
63
1336926
    return n;
64
  }
65
432640
  return tnt->d_data.begin()->first;
66
}
67
68
template TNode NodeTemplateTrie<false>::addOrGetTerm(
69
    TNode n, const std::vector<TNode>& reps);
70
template Node NodeTemplateTrie<true>::addOrGetTerm(
71
    Node n, const std::vector<Node>& reps);
72
73
template <bool ref_count>
74
void NodeTemplateTrie<ref_count>::debugPrint(const char* c,
75
                                             unsigned depth) const
76
{
77
  for (const std::pair<const NodeTemplate<ref_count>,
78
                       NodeTemplateTrie<ref_count>>& p : d_data)
79
  {
80
    for (unsigned i = 0; i < depth; i++)
81
    {
82
      Trace(c) << "  ";
83
    }
84
    Trace(c) << p.first << std::endl;
85
    p.second.debugPrint(c, depth + 1);
86
  }
87
}
88
89
template void NodeTemplateTrie<false>::debugPrint(const char* c,
90
                                                  unsigned depth) const;
91
template void NodeTemplateTrie<true>::debugPrint(const char* c,
92
                                                 unsigned depth) const;
93
94
}  // namespace theory
95
26676
}  // namespace CVC4