GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/index_trie.cpp Lines: 42 43 97.7 %
Date: 2021-03-23 Branches: 55 98 56.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file index_trie.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mikolas Janota
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2020 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 that store subsets of tuples of term indices
13
 ** that are not yielding  useful instantiations. of quantifier instantiation.
14
 ** This is used in the term_tuple_enumerator.
15
 **/
16
#include "theory/quantifiers/index_trie.h"
17
18
namespace CVC4 {
19
namespace theory {
20
namespace quantifiers {
21
22
7810
void IndexTrie::add(const std::vector<bool>& mask,
23
                    const std::vector<size_t>& values)
24
{
25
7810
  const size_t cardinality = std::count(mask.begin(), mask.end(), true);
26
7810
  if (d_ignoreFullySpecified && cardinality == mask.size())
27
  {
28
7288
    return;
29
  }
30
31
522
  d_root = addRec(d_root, 0, cardinality, mask, values);
32
}
33
34
8242
void IndexTrie::freeRec(IndexTrieNode* n)
35
{
36
8242
  if (!n)
37
  {
38
4329
    return;
39
  }
40
5755
  for (auto c : n->d_children)
41
  {
42
1842
    freeRec(c.second);
43
  }
44
3913
  freeRec(n->d_blank);
45
3913
  delete n;
46
}
47
48
13586
bool IndexTrie::findRec(const IndexTrieNode* n,
49
                        size_t index,
50
                        const std::vector<size_t>& members,
51
                        size_t& nonBlankLength) const
52
{
53
13586
  if (!n || index >= members.size())
54
  {
55
743
    return true;  // all elements of members matched
56
  }
57
12843
  if (n->d_blank && findRec(n->d_blank, index + 1, members, nonBlankLength))
58
  {
59
613
    return true;  // found in the blank branch
60
  }
61
12230
  nonBlankLength = index + 1;
62
16721
  for (const auto& c : n->d_children)
63
  {
64
13926
    if (c.first == members[index]
65
6963
        && findRec(c.second, index + 1, members, nonBlankLength))
66
    {
67
2472
      return true;  // found in the matching subtree
68
    }
69
  }
70
9758
  return false;
71
}
72
73
3158
IndexTrieNode* IndexTrie::addRec(IndexTrieNode* n,
74
                                 size_t index,
75
                                 size_t cardinality,
76
                                 const std::vector<bool>& mask,
77
                                 const std::vector<size_t>& values)
78
{
79
3158
  if (!n)
80
  {
81
    return nullptr;  // this tree matches everything, no point to add
82
  }
83
3158
  if (cardinality == 0)  // all blanks, all strings match
84
  {
85
522
    freeRec(n);
86
522
    return nullptr;
87
  }
88
89
2636
  Assert(index < mask.size());
90
91
2636
  if (!mask[index])  // blank position in the added vector
92
  {
93
249
    auto blank = n->d_blank ? n->d_blank : new IndexTrieNode();
94
249
    n->d_blank = addRec(blank, index + 1, cardinality, mask, values);
95
249
    return n;
96
  }
97
2387
  Assert(cardinality);
98
99
2662
  for (auto& edge : n->d_children)
100
  {
101
820
    if (edge.first == values[index])
102
    {
103
      // value already amongst the children
104
545
      edge.second =
105
545
          addRec(edge.second, index + 1, cardinality - 1, mask, values);
106
545
      return n;
107
    }
108
  }
109
  // new child needs to be added
110
  auto child =
111
1842
      addRec(new IndexTrieNode(), index + 1, cardinality - 1, mask, values);
112
1842
  n->d_children.push_back(std::make_pair(values[index], child));
113
1842
  return n;
114
}
115
}  // namespace quantifiers
116
}  // namespace theory
117
}  // namespace CVC4