GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/lazy_trie.cpp Lines: 73 78 93.6 %
Date: 2021-03-22 Branches: 124 314 39.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file lazy_trie.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, 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 Implementation of lazy trie
13
 **/
14
15
#include "theory/quantifiers/lazy_trie.h"
16
17
namespace CVC4 {
18
namespace theory {
19
namespace quantifiers {
20
21
9716
Node LazyTrie::add(Node n,
22
                   LazyTrieEvaluator* ev,
23
                   unsigned index,
24
                   unsigned ntotal,
25
                   bool forceKeep)
26
{
27
9716
  LazyTrie* lt = this;
28
167118
  while (lt != NULL)
29
  {
30
88417
    if (index == ntotal)
31
    {
32
      // lazy child holds the leaf data
33
8660
      if (lt->d_lazy_child.isNull() || forceKeep)
34
      {
35
1351
        lt->d_lazy_child = n;
36
      }
37
18376
      return lt->d_lazy_child;
38
    }
39
79757
    if (lt->d_children.empty())
40
    {
41
26576
      if (lt->d_lazy_child.isNull())
42
      {
43
        // no one has been here, we are done
44
1056
        lt->d_lazy_child = n;
45
1056
        return lt->d_lazy_child;
46
      }
47
      // evaluate the lazy child
48
51040
      Node e_lc = ev->evaluate(lt->d_lazy_child, index);
49
      // store at next level
50
25520
      lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
51
      // replace
52
25520
      lt->d_lazy_child = Node::null();
53
    }
54
    // recurse
55
157402
    Node e = ev->evaluate(n, index);
56
78701
    lt = &lt->d_children[e];
57
78701
    index = index + 1;
58
  }
59
  return Node::null();
60
}
61
62
1326
void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal)
63
{
64
2652
  Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1
65
1326
                           << "\n";
66
2652
  std::vector<IndTriePair> visit;
67
1326
  unsigned index = 0;
68
  LazyTrie* trie;
69
1326
  visit.push_back(IndTriePair(0, &d_trie));
70
3994
  while (!visit.empty())
71
  {
72
1334
    index = visit.back().first;
73
1334
    trie = visit.back().second;
74
1334
    visit.pop_back();
75
    // not at (previous) last level, traverse children
76
1334
    if (index < ntotal)
77
    {
78
12
      for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
79
      {
80
8
        visit.push_back(IndTriePair(index + 1, &p_nt.second));
81
      }
82
8
      continue;
83
    }
84
1330
    Assert(trie->d_children.empty());
85
    // if last level and no element at leaf, ignore
86
1330
    if (trie->d_lazy_child.isNull())
87
    {
88
      continue;
89
    }
90
    // apply new classifier
91
1330
    Assert(d_rep_to_class.find(trie->d_lazy_child) != d_rep_to_class.end());
92
2660
    std::vector<Node> prev_sep_class = d_rep_to_class[trie->d_lazy_child];
93
1330
    if (Trace.isOn("lazy-trie-multi"))
94
    {
95
      Trace("lazy-trie-multi") << "...last level. Prev sep class: \n";
96
      for (const Node& n : prev_sep_class)
97
      {
98
        Trace("lazy-trie-multi") << "...... " << n << "\n";
99
      }
100
    }
101
    // make new sepclass of lc a singleton with itself
102
1330
    d_rep_to_class.erase(trie->d_lazy_child);
103
    // replace
104
1330
    trie->d_lazy_child = Node::null();
105
5320
    for (const Node& n : prev_sep_class)
106
    {
107
6230
      Node eval = ev->evaluate(n, index);
108
3990
      std::map<Node, LazyTrie>::iterator it = trie->d_children.find(eval);
109
5740
      if (it != trie->d_children.end())
110
      {
111
        // add n to to map of item in next level
112
3500
        Trace("lazy-trie-multi") << "...add " << n << " to the class of "
113
1750
                                 << it->second.d_lazy_child << "\n";
114
1750
        d_rep_to_class[it->second.d_lazy_child].push_back(n);
115
1750
        continue;
116
      }
117
      // store at next level
118
2240
      trie->d_children[eval].d_lazy_child = n;
119
      // create new map
120
2240
      Trace("lazy-trie-multi") << "...create new class for : " << n << "\n";
121
2240
      Assert(d_rep_to_class.find(n) == d_rep_to_class.end());
122
2240
      d_rep_to_class[n].clear();
123
2240
      d_rep_to_class[n].push_back(n);
124
    }
125
  }
126
1326
}
127
128
8322
Node LazyTrieMulti::add(Node f, LazyTrieEvaluator* ev, unsigned ntotal)
129
{
130
8322
  Trace("lazy-trie-multi") << "LazyTrieM: Adding " << f << "\n";
131
8322
  Node res = d_trie.add(f, ev, 0, ntotal, false);
132
  // f was added to the separation class with representative res
133
8322
  if (res != f)
134
  {
135
13976
    Trace("lazy-trie-multi") << "... added " << f << " to the sepclass of "
136
6988
                             << res << "\n";
137
6988
    Assert(d_rep_to_class.find(res) != d_rep_to_class.end());
138
6988
    Assert(!d_rep_to_class[res].empty());
139
6988
    d_rep_to_class[res].push_back(f);
140
6988
    return res;
141
  }
142
  // f is the representatitve of a singleton seperation class
143
2668
  Trace("lazy-trie-multi") << "... added " << f
144
1334
                           << " as the rep of the sepclass with itself\n";
145
1334
  Assert(d_rep_to_class.find(res) == d_rep_to_class.end());
146
1334
  d_rep_to_class[res].clear();
147
1334
  d_rep_to_class[res].push_back(f);
148
1334
  return res;
149
}
150
151
1334
void LazyTrieMulti::clear()
152
{
153
1334
  d_trie.clear();
154
1334
  d_rep_to_class.clear();
155
1334
}
156
157
} /* CVC4::theory::quantifiers namespace */
158
} /* CVC4::theory namespace */
159
26676
} /* CVC4 namespace */