GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/trigger_trie.cpp Lines: 29 29 100.0 %
Date: 2021-03-23 Branches: 25 42 59.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file trigger_trie.cpp
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 Implementation of trigger trie class
13
 **/
14
15
#include "theory/quantifiers/ematching/trigger_trie.h"
16
17
namespace CVC4 {
18
namespace theory {
19
namespace inst {
20
21
27158
TriggerTrie::TriggerTrie() {}
22
23
54310
TriggerTrie::~TriggerTrie()
24
{
25
43777
  for (size_t i = 0, ntriggers = d_tr.size(); i < ntriggers; i++)
26
  {
27
16622
    delete d_tr[i];
28
  }
29
27155
}
30
31
12943
inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
32
{
33
25886
  std::vector<Node> temp;
34
12943
  temp.insert(temp.begin(), nodes.begin(), nodes.end());
35
12943
  std::sort(temp.begin(), temp.end());
36
12943
  TriggerTrie* tt = this;
37
13037
  for (const Node& n : temp)
38
  {
39
12993
    std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n);
40
12993
    if (itt == tt->d_children.end())
41
    {
42
12899
      return nullptr;
43
    }
44
    else
45
    {
46
94
      tt = &(itt->second);
47
    }
48
  }
49
44
  return tt->d_tr.empty() ? nullptr : tt->d_tr[0];
50
}
51
52
16622
void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
53
{
54
33244
  std::vector<Node> temp(nodes.begin(), nodes.end());
55
16622
  std::sort(temp.begin(), temp.end());
56
16622
  TriggerTrie* tt = this;
57
34796
  for (const Node& n : temp)
58
  {
59
18174
    std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n);
60
18174
    if (itt == tt->d_children.end())
61
    {
62
18161
      TriggerTrie* ttn = &tt->d_children[n];
63
18161
      tt = ttn;
64
    }
65
    else
66
    {
67
13
      tt = &(itt->second);
68
    }
69
  }
70
16622
  tt->d_tr.push_back(t);
71
16622
}
72
73
}  // namespace inst
74
}  // namespace theory
75
26685
}  // namespace CVC4