GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/match_trie.cpp Lines: 102 108 94.4 %
Date: 2021-03-23 Branches: 158 326 48.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file match_trie.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Implements a match trie, also known as a discrimination tree.
13
 **/
14
15
#include "expr/match_trie.h"
16
17
using namespace CVC4::kind;
18
19
namespace CVC4 {
20
namespace expr {
21
22
163
bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
23
{
24
326
  std::vector<Node> vars;
25
326
  std::vector<Node> subs;
26
326
  std::map<Node, Node> smap;
27
28
326
  std::vector<std::vector<Node> > visit;
29
326
  std::vector<MatchTrie*> visit_trie;
30
326
  std::vector<int> visit_var_index;
31
326
  std::vector<bool> visit_bound_var;
32
33
163
  visit.push_back(std::vector<Node>{n});
34
163
  visit_trie.push_back(this);
35
163
  visit_var_index.push_back(-1);
36
163
  visit_bound_var.push_back(false);
37
3291
  while (!visit.empty())
38
  {
39
3131
    std::vector<Node> cvisit = visit.back();
40
1567
    MatchTrie* curr = visit_trie.back();
41
1567
    if (cvisit.empty())
42
    {
43
120
      Assert(n
44
             == curr->d_data.substitute(
45
                 vars.begin(), vars.end(), subs.begin(), subs.end()));
46
120
      Trace("match-debug") << "notify : " << curr->d_data << std::endl;
47
120
      if (!ntm->notify(n, curr->d_data, vars, subs))
48
      {
49
3
        return false;
50
      }
51
117
      visit.pop_back();
52
117
      visit_trie.pop_back();
53
117
      visit_var_index.pop_back();
54
117
      visit_bound_var.pop_back();
55
    }
56
    else
57
    {
58
2894
      Node cn = cvisit.back();
59
2894
      Trace("match-debug") << "traverse : " << cn << " at depth "
60
1447
                           << visit.size() << std::endl;
61
1447
      unsigned index = visit.size() - 1;
62
1447
      int vindex = visit_var_index[index];
63
1447
      if (vindex == -1)
64
      {
65
532
        if (!cn.isVar())
66
        {
67
652
          Node op = cn.hasOperator() ? cn.getOperator() : cn;
68
326
          unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
69
          std::map<unsigned, MatchTrie>::iterator itu =
70
326
              curr->d_children[op].find(nchild);
71
326
          if (itu != curr->d_children[op].end())
72
          {
73
            // recurse on the operator or self
74
196
            cvisit.pop_back();
75
196
            if (cn.hasOperator())
76
            {
77
591
              for (const Node& cnc : cn)
78
              {
79
395
                cvisit.push_back(cnc);
80
              }
81
            }
82
196
            Trace("match-debug") << "recurse op : " << op << std::endl;
83
196
            visit.push_back(cvisit);
84
196
            visit_trie.push_back(&itu->second);
85
196
            visit_var_index.push_back(-1);
86
196
            visit_bound_var.push_back(false);
87
          }
88
        }
89
532
        visit_var_index[index]++;
90
      }
91
      else
92
      {
93
        // clean up if we previously bound a variable
94
915
        if (visit_bound_var[index])
95
        {
96
263
          Assert(!vars.empty());
97
263
          smap.erase(vars.back());
98
263
          vars.pop_back();
99
263
          subs.pop_back();
100
263
          visit_bound_var[index] = false;
101
        }
102
103
915
        if (vindex == static_cast<int>(curr->d_vars.size()))
104
        {
105
1034
          Trace("match-debug")
106
1034
              << "finished checking " << curr->d_vars.size()
107
517
              << " variables at depth " << visit.size() << std::endl;
108
          // finished
109
517
          visit.pop_back();
110
517
          visit_trie.pop_back();
111
517
          visit_var_index.pop_back();
112
517
          visit_bound_var.pop_back();
113
        }
114
        else
115
        {
116
796
          Trace("match-debug") << "check variable #" << vindex << " at depth "
117
398
                               << visit.size() << std::endl;
118
398
          Assert(vindex < static_cast<int>(curr->d_vars.size()));
119
          // recurse on variable?
120
796
          Node var = curr->d_vars[vindex];
121
398
          bool recurse = true;
122
          // check if it is already bound
123
398
          std::map<Node, Node>::iterator its = smap.find(var);
124
398
          if (its != smap.end())
125
          {
126
129
            if (its->second != cn)
127
            {
128
105
              recurse = false;
129
            }
130
          }
131
269
          else if (!var.getType().isSubtypeOf(cn.getType()))
132
          {
133
            recurse = false;
134
          }
135
          else
136
          {
137
269
            vars.push_back(var);
138
269
            subs.push_back(cn);
139
269
            smap[var] = cn;
140
269
            visit_bound_var[index] = true;
141
          }
142
398
          if (recurse)
143
          {
144
293
            Trace("match-debug") << "recurse var : " << var << std::endl;
145
293
            cvisit.pop_back();
146
293
            visit.push_back(cvisit);
147
293
            visit_trie.push_back(&curr->d_children[var][0]);
148
293
            visit_var_index.push_back(-1);
149
293
            visit_bound_var.push_back(false);
150
          }
151
398
          visit_var_index[index]++;
152
        }
153
      }
154
    }
155
  }
156
160
  return true;
157
}
158
159
210
void MatchTrie::addTerm(Node n)
160
{
161
210
  Assert(!n.isNull());
162
420
  std::vector<Node> visit;
163
210
  visit.push_back(n);
164
210
  MatchTrie* curr = this;
165
2066
  while (!visit.empty())
166
  {
167
1856
    Node cn = visit.back();
168
928
    visit.pop_back();
169
928
    if (cn.hasOperator())
170
    {
171
371
      curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
172
1089
      for (const Node& cnc : cn)
173
      {
174
718
        visit.push_back(cnc);
175
      }
176
    }
177
    else
178
    {
179
1114
      if (cn.isVar()
180
1601
          && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
181
1601
                 == curr->d_vars.end())
182
      {
183
433
        curr->d_vars.push_back(cn);
184
      }
185
557
      curr = &(curr->d_children[cn][0]);
186
    }
187
  }
188
210
  curr->d_data = n;
189
210
}
190
191
void MatchTrie::clear()
192
{
193
  d_children.clear();
194
  d_vars.clear();
195
  d_data = Node::null();
196
}
197
198
}  // namespace expr
199
26685
}  // namespace CVC4