Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/match_trie.cpp	Lines:	107	108	99.1 %
Date:	2021-11-07	Branches:	160	324	49.4 %


/******************************************************************************
 * 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	4873	bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
24		{
25	9746	std::vector<Node> vars;
26	9746	std::vector<Node> subs;
27	9746	std::map<Node, Node> smap;
28
29	9746	std::vector<std::vector<Node> > visit;
30	9746	std::vector<MatchTrie*> visit_trie;
31	9746	std::vector<int> visit_var_index;
32	9746	std::vector<bool> visit_bound_var;
33
34	4873	visit.push_back(std::vector<Node>{n});
35	4873	visit_trie.push_back(this);
36	4873	visit_var_index.push_back(-1);
37	4873	visit_bound_var.push_back(false);
38	87715	while (!visit.empty())
39		{
40	87081	std::vector<Node> cvisit = visit.back();
41	45660	MatchTrie* curr = visit_trie.back();
42	45660	if (cvisit.empty())
43		{
44	4491	Assert(n
45		== curr->d_data.substitute(
46		vars.begin(), vars.end(), subs.begin(), subs.end()));
47	4491	Trace("match-debug") << "notify : " << curr->d_data << std::endl;
48	4491	if (!ntm->notify(n, curr->d_data, vars, subs))
49		{
50	4239	return false;
51		}
52	252	visit.pop_back();
53	252	visit_trie.pop_back();
54	252	visit_var_index.pop_back();
55	252	visit_bound_var.pop_back();
56		}
57		else
58		{
59	82338	Node cn = cvisit.back();
60	82338	Trace("match-debug") << "traverse : " << cn << " at depth "
61	41169	<< visit.size() << std::endl;
62	41169	unsigned index = visit.size() - 1;
63	41169	int vindex = visit_var_index[index];
64	41169	if (vindex == -1)
65		{
66	22473	if (!cn.isVar())
67		{
68	30726	Node op = cn.hasOperator() ? cn.getOperator() : cn;
69	15363	unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
70		std::map<unsigned, MatchTrie>::iterator itu =
71	15363	curr->d_children[op].find(nchild);
72	15363	if (itu != curr->d_children[op].end())
73		{
74		// recurse on the operator or self
75	9244	cvisit.pop_back();
76	9244	if (cn.hasOperator())
77		{
78	23712	for (const Node& cnc : cn)
79		{
80	16645	cvisit.push_back(cnc);
81		}
82		}
83	9244	Trace("match-debug") << "recurse op : " << op << std::endl;
84	9244	visit.push_back(cvisit);
85	9244	visit_trie.push_back(&itu->second);
86	9244	visit_var_index.push_back(-1);
87	9244	visit_bound_var.push_back(false);
88		}
89		}
90	22473	visit_var_index[index]++;
91		}
92		else
93		{
94		// clean up if we previously bound a variable
95	18696	if (visit_bound_var[index])
96		{
97	2613	Assert(!vars.empty());
98	2613	smap.erase(vars.back());
99	2613	vars.pop_back();
100	2613	subs.pop_back();
101	2613	visit_bound_var[index] = false;
102		}
103
104	18696	if (vindex == static_cast<int>(curr->d_vars.size()))
105		{
106	11488	Trace("match-debug")
107	11488	<< "finished checking " << curr->d_vars.size()
108	5744	<< " variables at depth " << visit.size() << std::endl;
109		// finished
110	5744	visit.pop_back();
111	5744	visit_trie.pop_back();
112	5744	visit_var_index.pop_back();
113	5744	visit_bound_var.pop_back();
114		}
115		else
116		{
117	25904	Trace("match-debug") << "check variable #" << vindex << " at depth "
118	12952	<< visit.size() << std::endl;
119	12952	Assert(vindex < static_cast<int>(curr->d_vars.size()));
120		// recurse on variable?
121	25904	Node var = curr->d_vars[vindex];
122	12952	bool recurse = true;
123		// check if it is already bound
124	12952	std::map<Node, Node>::iterator its = smap.find(var);
125	12952	if (its != smap.end())
126		{
127	129	if (its->second != cn)
128		{
129	105	recurse = false;
130		}
131		}
132	12823	else if (!var.getType().isSubtypeOf(cn.getType()))
133		{
134		recurse = false;
135		}
136		else
137		{
138	12823	vars.push_back(var);
139	12823	subs.push_back(cn);
140	12823	smap[var] = cn;
141	12823	visit_bound_var[index] = true;
142		}
143	12952	if (recurse)
144		{
145	12847	Trace("match-debug") << "recurse var : " << var << std::endl;
146	12847	cvisit.pop_back();
147	12847	visit.push_back(cvisit);
148	12847	visit_trie.push_back(&curr->d_children[var][0]);
149	12847	visit_var_index.push_back(-1);
150	12847	visit_bound_var.push_back(false);
151		}
152	12952	visit_var_index[index]++;
153		}
154		}
155		}
156		}
157	634	return true;
158		}
159
160	682	void MatchTrie::addTerm(Node n)
161		{
162	682	Assert(!n.isNull());
163	1364	std::vector<Node> visit;
164	682	visit.push_back(n);
165	682	MatchTrie* curr = this;
166	9980	while (!visit.empty())
167		{
168	9298	Node cn = visit.back();
169	4649	visit.pop_back();
170	4649	if (cn.hasOperator())
171		{
172	1686	curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
173	5653	for (const Node& cnc : cn)
174		{
175	3967	visit.push_back(cnc);
176		}
177		}
178		else
179		{
180	5926	if (cn.isVar()
181	6355	&& std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
182	6355	== curr->d_vars.end())
183		{
184	948	curr->d_vars.push_back(cn);
185		}
186	2963	curr = &(curr->d_children[cn][0]);
187		}
188		}
189	682	curr->d_data = n;
190	682	}
191
192	28	void MatchTrie::clear()
193		{
194	28	d_children.clear();
195	28	d_vars.clear();
196	28	d_data = Node::null();
197	28	}
198
199		} // namespace expr
200	31137	} // namespace cvc5