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

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds, Morgan Deters, Tim King
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Implementation of trigger trie class.
14
 */
15
16
#include "theory/quantifiers/ematching/trigger_trie.h"
17
18
namespace cvc5 {
19
namespace theory {
20
namespace quantifiers {
21
namespace inst {
22
23
24832
TriggerTrie::TriggerTrie() {}
24
25
49664
TriggerTrie::~TriggerTrie()
26
{
27
41682
  for (size_t i = 0, ntriggers = d_tr.size(); i < ntriggers; i++)
28
  {
29
16850
    delete d_tr[i];
30
  }
31
24832
}
32
33
12849
inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
34
{
35
25698
  std::vector<Node> temp;
36
12849
  temp.insert(temp.begin(), nodes.begin(), nodes.end());
37
12849
  std::sort(temp.begin(), temp.end());
38
12849
  TriggerTrie* tt = this;
39
12933
  for (const Node& n : temp)
40
  {
41
12894
    std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n);
42
12894
    if (itt == tt->d_children.end())
43
    {
44
12810
      return nullptr;
45
    }
46
    else
47
    {
48
84
      tt = &(itt->second);
49
    }
50
  }
51
39
  return tt->d_tr.empty() ? nullptr : tt->d_tr[0];
52
}
53
54
16850
void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
55
{
56
33700
  std::vector<Node> temp(nodes.begin(), nodes.end());
57
16850
  std::sort(temp.begin(), temp.end());
58
16850
  TriggerTrie* tt = this;
59
35201
  for (const Node& n : temp)
60
  {
61
18351
    std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n);
62
18351
    if (itt == tt->d_children.end())
63
    {
64
18329
      TriggerTrie* ttn = &tt->d_children[n];
65
18329
      tt = ttn;
66
    }
67
    else
68
    {
69
22
      tt = &(itt->second);
70
    }
71
  }
72
16850
  tt->d_tr.push_back(t);
73
16850
}
74
75
}  // namespace inst
76
}  // namespace quantifiers
77
}  // namespace theory
78
29322
}  // namespace cvc5