Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/match_trie.cpp	Lines:	107	108	99.1 %
Date:	2021-05-21	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	4625	bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
24		{
25	9250	std::vector<Node> vars;
26	9250	std::vector<Node> subs;
27	9250	std::map<Node, Node> smap;
28
29	9250	std::vector<std::vector<Node> > visit;
30	9250	std::vector<MatchTrie*> visit_trie;
31	9250	std::vector<int> visit_var_index;
32	9250	std::vector<bool> visit_bound_var;
33
34	4625	visit.push_back(std::vector<Node>{n});
35	4625	visit_trie.push_back(this);
36	4625	visit_var_index.push_back(-1);
37	4625	visit_bound_var.push_back(false);
38	84171	while (!visit.empty())
39		{
40	83592	std::vector<Node> cvisit = visit.back();
41	43819	MatchTrie* curr = visit_trie.back();
42	43819	if (cvisit.empty())
43		{
44	4207	Assert(n
45		== curr->d_data.substitute(
46		vars.begin(), vars.end(), subs.begin(), subs.end()));
47	4207	Trace("match-debug") << "notify : " << curr->d_data << std::endl;
48	4207	if (!ntm->notify(n, curr->d_data, vars, subs))
49		{
50	4046	return false;
51		}
52	161	visit.pop_back();
53	161	visit_trie.pop_back();
54	161	visit_var_index.pop_back();
55	161	visit_bound_var.pop_back();
56		}
57		else
58		{
59	79224	Node cn = cvisit.back();
60	79224	Trace("match-debug") << "traverse : " << cn << " at depth "
61	39612	<< visit.size() << std::endl;
62	39612	unsigned index = visit.size() - 1;
63	39612	int vindex = visit_var_index[index];
64	39612	if (vindex == -1)
65		{
66	21487	if (!cn.isVar())
67		{
68	29666	Node op = cn.hasOperator() ? cn.getOperator() : cn;
69	14833	unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
70		std::map<unsigned, MatchTrie>::iterator itu =
71	14833	curr->d_children[op].find(nchild);
72	14833	if (itu != curr->d_children[op].end())
73		{
74		// recurse on the operator or self
75	8825	cvisit.pop_back();
76	8825	if (cn.hasOperator())
77		{
78	22602	for (const Node& cnc : cn)
79		{
80	15907	cvisit.push_back(cnc);
81		}
82		}
83	8825	Trace("match-debug") << "recurse op : " << op << std::endl;
84	8825	visit.push_back(cvisit);
85	8825	visit_trie.push_back(&itu->second);
86	8825	visit_var_index.push_back(-1);
87	8825	visit_bound_var.push_back(false);
88		}
89		}
90	21487	visit_var_index[index]++;
91		}
92		else
93		{
94		// clean up if we previously bound a variable
95	18125	if (visit_bound_var[index])
96		{
97	2523	Assert(!vars.empty());
98	2523	smap.erase(vars.back());
99	2523	vars.pop_back();
100	2523	subs.pop_back();
101	2523	visit_bound_var[index] = false;
102		}
103
104	18125	if (vindex == static_cast<int>(curr->d_vars.size()))
105		{
106	11606	Trace("match-debug")
107	11606	<< "finished checking " << curr->d_vars.size()
108	5803	<< " variables at depth " << visit.size() << std::endl;
109		// finished
110	5803	visit.pop_back();
111	5803	visit_trie.pop_back();
112	5803	visit_var_index.pop_back();
113	5803	visit_bound_var.pop_back();
114		}
115		else
116		{
117	24644	Trace("match-debug") << "check variable #" << vindex << " at depth "
118	12322	<< visit.size() << std::endl;
119	12322	Assert(vindex < static_cast<int>(curr->d_vars.size()));
120		// recurse on variable?
121	24644	Node var = curr->d_vars[vindex];
122	12322	bool recurse = true;
123		// check if it is already bound
124	12322	std::map<Node, Node>::iterator its = smap.find(var);
125	12322	if (its != smap.end())
126		{
127	108	if (its->second != cn)
128		{
129	78	recurse = false;
130		}
131		}
132	12214	else if (!var.getType().isSubtypeOf(cn.getType()))
133		{
134		recurse = false;
135		}
136		else
137		{
138	12214	vars.push_back(var);
139	12214	subs.push_back(cn);
140	12214	smap[var] = cn;
141	12214	visit_bound_var[index] = true;
142		}
143	12322	if (recurse)
144		{
145	12244	Trace("match-debug") << "recurse var : " << var << std::endl;
146	12244	cvisit.pop_back();
147	12244	visit.push_back(cvisit);
148	12244	visit_trie.push_back(&curr->d_children[var][0]);
149	12244	visit_var_index.push_back(-1);
150	12244	visit_bound_var.push_back(false);
151		}
152	12322	visit_var_index[index]++;
153		}
154		}
155		}
156		}
157	579	return true;
158		}
159
160	610	void MatchTrie::addTerm(Node n)
161		{
162	610	Assert(!n.isNull());
163	1220	std::vector<Node> visit;
164	610	visit.push_back(n);
165	610	MatchTrie* curr = this;
166	9944	while (!visit.empty())
167		{
168	9334	Node cn = visit.back();
169	4667	visit.pop_back();
170	4667	if (cn.hasOperator())
171		{
172	1670	curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
173	5727	for (const Node& cnc : cn)
174		{
175	4057	visit.push_back(cnc);
176		}
177		}
178		else
179		{
180	5994	if (cn.isVar()
181	6149	&& std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
182	6149	== curr->d_vars.end())
183		{
184	818	curr->d_vars.push_back(cn);
185		}
186	2997	curr = &(curr->d_children[cn][0]);
187		}
188		}
189	610	curr->d_data = n;
190	610	}
191
192	22	void MatchTrie::clear()
193		{
194	22	d_children.clear();
195	22	d_vars.clear();
196	22	d_data = Node::null();
197	22	}
198
199		} // namespace expr
200	27735	} // namespace cvc5