Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/match_trie.cpp	Lines:	107	108	99.1 %
Date:	2021-05-22	Branches:	160	326	49.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implements a match trie, also known as a discrimination tree.
 */

#include "expr/match_trie.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace expr {

bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
{
  std::vector<Node> vars;
  std::vector<Node> subs;
  std::map<Node, Node> smap;

  std::vector<std::vector<Node> > visit;
  std::vector<MatchTrie*> visit_trie;
  std::vector<int> visit_var_index;
  std::vector<bool> visit_bound_var;

  visit.push_back(std::vector<Node>{n});
  visit_trie.push_back(this);
  visit_var_index.push_back(-1);
  visit_bound_var.push_back(false);
  while (!visit.empty())
  {
    std::vector<Node> cvisit = visit.back();
    MatchTrie* curr = visit_trie.back();
    if (cvisit.empty())
    {
      Assert(n
             == curr->d_data.substitute(
                 vars.begin(), vars.end(), subs.begin(), subs.end()));
      Trace("match-debug") << "notify : " << curr->d_data << std::endl;
      if (!ntm->notify(n, curr->d_data, vars, subs))
      {
        return false;
      }
      visit.pop_back();
      visit_trie.pop_back();
      visit_var_index.pop_back();
      visit_bound_var.pop_back();
    }
    else
    {
      Node cn = cvisit.back();
      Trace("match-debug") << "traverse : " << cn << " at depth "
                           << visit.size() << std::endl;
      unsigned index = visit.size() - 1;
      int vindex = visit_var_index[index];
      if (vindex == -1)
      {
        if (!cn.isVar())
        {
          Node op = cn.hasOperator() ? cn.getOperator() : cn;
          unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
          std::map<unsigned, MatchTrie>::iterator itu =
              curr->d_children[op].find(nchild);
          if (itu != curr->d_children[op].end())
          {
            // recurse on the operator or self
            cvisit.pop_back();
            if (cn.hasOperator())
            {
              for (const Node& cnc : cn)
              {
                cvisit.push_back(cnc);
              }
            }
            Trace("match-debug") << "recurse op : " << op << std::endl;
            visit.push_back(cvisit);
            visit_trie.push_back(&itu->second);
            visit_var_index.push_back(-1);
            visit_bound_var.push_back(false);
          }
        }
        visit_var_index[index]++;
      }
      else
      {
        // clean up if we previously bound a variable
        if (visit_bound_var[index])
        {
          Assert(!vars.empty());
          smap.erase(vars.back());
          vars.pop_back();
          subs.pop_back();
          visit_bound_var[index] = false;
        }

        if (vindex == static_cast<int>(curr->d_vars.size()))
        {
          Trace("match-debug")
              << "finished checking " << curr->d_vars.size()
              << " variables at depth " << visit.size() << std::endl;
          // finished
          visit.pop_back();
          visit_trie.pop_back();
          visit_var_index.pop_back();
          visit_bound_var.pop_back();
        }
        else
        {
          Trace("match-debug") << "check variable #" << vindex << " at depth "
                               << visit.size() << std::endl;
          Assert(vindex < static_cast<int>(curr->d_vars.size()));
          // recurse on variable?
          Node var = curr->d_vars[vindex];
          bool recurse = true;
          // check if it is already bound
          std::map<Node, Node>::iterator its = smap.find(var);
          if (its != smap.end())
          {
            if (its->second != cn)
            {
              recurse = false;
            }
          }
          else if (!var.getType().isSubtypeOf(cn.getType()))
          {
            recurse = false;
          }
          else
          {
            vars.push_back(var);
            subs.push_back(cn);
            smap[var] = cn;
            visit_bound_var[index] = true;
          }
          if (recurse)
          {
            Trace("match-debug") << "recurse var : " << var << std::endl;
            cvisit.pop_back();
            visit.push_back(cvisit);
            visit_trie.push_back(&curr->d_children[var][0]);
            visit_var_index.push_back(-1);
            visit_bound_var.push_back(false);
          }
          visit_var_index[index]++;
        }
      }
    }
  }
  return true;
}

void MatchTrie::addTerm(Node n)
{
  Assert(!n.isNull());
  std::vector<Node> visit;
  visit.push_back(n);
  MatchTrie* curr = this;
  while (!visit.empty())
  {
    Node cn = visit.back();
    visit.pop_back();
    if (cn.hasOperator())
    {
      curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
      for (const Node& cnc : cn)
      {
        visit.push_back(cnc);
      }
    }
    else
    {
      if (cn.isVar()
          && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
                 == curr->d_vars.end())
      {
        curr->d_vars.push_back(cn);
      }
      curr = &(curr->d_children[cn][0]);
    }
  }
  curr->d_data = n;
}

void MatchTrie::clear()
{
  d_children.clear();
  d_vars.clear();
  d_data = Node::null();
}

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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