Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/match_trie.cpp	Lines:	107	108	99.1 %
Date:	2021-08-14	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	4737	bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
24		{
25	9474	std::vector<Node> vars;
26	9474	std::vector<Node> subs;
27	9474	std::map<Node, Node> smap;
28
29	9474	std::vector<std::vector<Node> > visit;
30	9474	std::vector<MatchTrie*> visit_trie;
31	9474	std::vector<int> visit_var_index;
32	9474	std::vector<bool> visit_bound_var;
33
34	4737	visit.push_back(std::vector<Node>{n});
35	4737	visit_trie.push_back(this);
36	4737	visit_var_index.push_back(-1);
37	4737	visit_bound_var.push_back(false);
38	85427	while (!visit.empty())
39		{
40	84856	std::vector<Node> cvisit = visit.back();
41	44511	MatchTrie* curr = visit_trie.back();
42	44511	if (cvisit.empty())
43		{
44	4377	Assert(n
45		== curr->d_data.substitute(
46		vars.begin(), vars.end(), subs.begin(), subs.end()));
47	4377	Trace("match-debug") << "notify : " << curr->d_data << std::endl;
48	4377	if (!ntm->notify(n, curr->d_data, vars, subs))
49		{
50	4166	return false;
51		}
52	211	visit.pop_back();
53	211	visit_trie.pop_back();
54	211	visit_var_index.pop_back();
55	211	visit_bound_var.pop_back();
56		}
57		else
58		{
59	80268	Node cn = cvisit.back();
60	80268	Trace("match-debug") << "traverse : " << cn << " at depth "
61	40134	<< visit.size() << std::endl;
62	40134	unsigned index = visit.size() - 1;
63	40134	int vindex = visit_var_index[index];
64	40134	if (vindex == -1)
65		{
66	21950	if (!cn.isVar())
67		{
68	30154	Node op = cn.hasOperator() ? cn.getOperator() : cn;
69	15077	unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
70		std::map<unsigned, MatchTrie>::iterator itu =
71	15077	curr->d_children[op].find(nchild);
72	15077	if (itu != curr->d_children[op].end())
73		{
74		// recurse on the operator or self
75	9036	cvisit.pop_back();
76	9036	if (cn.hasOperator())
77		{
78	23110	for (const Node& cnc : cn)
79		{
80	16251	cvisit.push_back(cnc);
81		}
82		}
83	9036	Trace("match-debug") << "recurse op : " << op << std::endl;
84	9036	visit.push_back(cvisit);
85	9036	visit_trie.push_back(&itu->second);
86	9036	visit_var_index.push_back(-1);
87	9036	visit_bound_var.push_back(false);
88		}
89		}
90	21950	visit_var_index[index]++;
91		}
92		else
93		{
94		// clean up if we previously bound a variable
95	18184	if (visit_bound_var[index])
96		{
97	2522	Assert(!vars.empty());
98	2522	smap.erase(vars.back());
99	2522	vars.pop_back();
100	2522	subs.pop_back();
101	2522	visit_bound_var[index] = false;
102		}
103
104	18184	if (vindex == static_cast<int>(curr->d_vars.size()))
105		{
106	11120	Trace("match-debug")
107	11120	<< "finished checking " << curr->d_vars.size()
108	5560	<< " variables at depth " << visit.size() << std::endl;
109		// finished
110	5560	visit.pop_back();
111	5560	visit_trie.pop_back();
112	5560	visit_var_index.pop_back();
113	5560	visit_bound_var.pop_back();
114		}
115		else
116		{
117	25248	Trace("match-debug") << "check variable #" << vindex << " at depth "
118	12624	<< visit.size() << std::endl;
119	12624	Assert(vindex < static_cast<int>(curr->d_vars.size()));
120		// recurse on variable?
121	25248	Node var = curr->d_vars[vindex];
122	12624	bool recurse = true;
123		// check if it is already bound
124	12624	std::map<Node, Node>::iterator its = smap.find(var);
125	12624	if (its != smap.end())
126		{
127	86	if (its->second != cn)
128		{
129	70	recurse = false;
130		}
131		}
132	12538	else if (!var.getType().isSubtypeOf(cn.getType()))
133		{
134		recurse = false;
135		}
136		else
137		{
138	12538	vars.push_back(var);
139	12538	subs.push_back(cn);
140	12538	smap[var] = cn;
141	12538	visit_bound_var[index] = true;
142		}
143	12624	if (recurse)
144		{
145	12554	Trace("match-debug") << "recurse var : " << var << std::endl;
146	12554	cvisit.pop_back();
147	12554	visit.push_back(cvisit);
148	12554	visit_trie.push_back(&curr->d_children[var][0]);
149	12554	visit_var_index.push_back(-1);
150	12554	visit_bound_var.push_back(false);
151		}
152	12624	visit_var_index[index]++;
153		}
154		}
155		}
156		}
157	571	return true;
158		}
159
160	600	void MatchTrie::addTerm(Node n)
161		{
162	600	Assert(!n.isNull());
163	1200	std::vector<Node> visit;
164	600	visit.push_back(n);
165	600	MatchTrie* curr = this;
166	9210	while (!visit.empty())
167		{
168	8610	Node cn = visit.back();
169	4305	visit.pop_back();
170	4305	if (cn.hasOperator())
171		{
172	1546	curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
173	5251	for (const Node& cnc : cn)
174		{
175	3705	visit.push_back(cnc);
176		}
177		}
178		else
179		{
180	5518	if (cn.isVar()
181	5759	&& std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
182	5759	== curr->d_vars.end())
183		{
184	783	curr->d_vars.push_back(cn);
185		}
186	2759	curr = &(curr->d_children[cn][0]);
187		}
188		}
189	600	curr->d_data = n;
190	600	}
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	29340	} // namespace cvc5