Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/nary_match_trie.cpp	Lines:	1	143	0.7 %
Date:	2021-09-17	Branches:	2	451	0.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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 n-ary match trie
 */

#include "expr/nary_match_trie.h"

#include <sstream>
#include "expr/nary_term_util.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace expr {

class NaryMatchFrame
{
 public:
  NaryMatchFrame(const std::vector<Node>& syms, const NaryMatchTrie* t)
      : d_syms(syms), d_trie(t), d_index(0), d_variant(0), d_boundVar(false)
  {
  }
  /** Symbols to match */
  std::vector<Node> d_syms;
  /** The match trie */
  const NaryMatchTrie* d_trie;
  /** The index we are considering, 0 = operator, n>0 = variable # (n-1) */
  size_t d_index;
  /** List length considering */
  size_t d_variant;
  /** Whether we just bound a variable */
  bool d_boundVar;
};

bool NaryMatchTrie::getMatches(Node n, NotifyMatch* ntm) const
{
  NodeManager* nm = NodeManager::currentNM();
  std::vector<Node> vars;
  std::vector<Node> subs;
  std::map<Node, Node> smap;

  std::map<Node, NaryMatchTrie>::const_iterator itc;

  std::vector<NaryMatchFrame> visit;
  visit.push_back(NaryMatchFrame({n}, this));

  while (!visit.empty())
  {
    NaryMatchFrame& curr = visit.back();
    // currently, copy the symbols from previous frame TODO: improve?
    std::vector<Node> syms = curr.d_syms;
    const NaryMatchTrie* mt = curr.d_trie;
    if (syms.empty())
    {
      // if we matched, there must be a data member at this node
      Assert(!mt->d_data.isNull());
      // notify match?
      Assert(n == expr::narySubstitute(mt->d_data, vars, subs));
      Trace("match-debug") << "notify : " << mt->d_data << std::endl;
      if (!ntm->notify(n, mt->d_data, vars, subs))
      {
        return false;
      }
      visit.pop_back();
      continue;
    }

    // clean up if we previously bound a variable
    if (curr.d_boundVar)
    {
      Assert(!vars.empty());
      Assert(smap.find(vars.back()) != smap.end());
      smap.erase(vars.back());
      vars.pop_back();
      subs.pop_back();
      curr.d_boundVar = false;
    }

    if (curr.d_index == 0)
    {
      curr.d_index++;
      // finished matching variables, try to match the operator
      Node next = syms.back();
      Node op =
          (!next.isNull() && next.hasOperator()) ? next.getOperator() : next;
      itc = mt->d_children.find(op);
      if (itc != mt->d_children.end())
      {
        syms.pop_back();
        // push the children + null termination marker, in reverse order
        if (NodeManager::isNAryKind(next.getKind()))
        {
          syms.push_back(Node::null());
        }
        if (next.hasOperator())
        {
          syms.insert(syms.end(), next.rbegin(), next.rend());
        }
        // new frame
        visit.push_back(NaryMatchFrame(syms, &itc->second));
      }
    }
    else if (curr.d_index <= mt->d_vars.size())
    {
      // try to match the next (variable, length)
      Node var;
      Node next;
      do
      {
        var = mt->d_vars[curr.d_index - 1];
        Assert(mt->d_children.find(var) != mt->d_children.end());
        std::vector<Node> currChildren;
        if (isListVar(var))
        {
          // get the length of the list we want to consider
          size_t l = curr.d_variant;
          curr.d_variant++;
          // match with l, or increment d_index otherwise
          bool foundChildren = true;
          // We are in a state where the children of an n-ary child
          // have been pused to syms. We try to extract l children here. If
          // we encounter the null symbol, then we do not have sufficient
          // children to match for this variant and fail.
          for (size_t i = 0; i < l; i++)
          {
            Assert(!syms.empty());
            Node s = syms.back();
            if (s.isNull())
            {
              foundChildren = false;
              break;
            }
            currChildren.push_back(s);
            syms.pop_back();
          }
          if (foundChildren)
          {
            // we are matching the next list
            next = nm->mkNode(SEXPR, currChildren);
          }
          else
          {
            // otherwise, we have run out of variants, go to next variable
            curr.d_index++;
            curr.d_variant = 0;
          }
        }
        else
        {
          next = syms.back();
          curr.d_index++;
          // we could be at the end of an n-ary operator, in which case we
          // do not match
          if (!next.isNull())
          {
            currChildren.push_back(next);
            syms.pop_back();
            // check subtyping in the (non-list) case
            if (!var.getType().isSubtypeOf(next.getType()))
            {
              next = Node::null();
            }
          }
        }
        if (!next.isNull())
        {
          // check if it is already bound, do the binding if necessary
          std::map<Node, Node>::iterator its = smap.find(var);
          if (its != smap.end())
          {
            if (its->second != next)
            {
              // failed to match
              next = Node::null();
            }
            // otherwise, successfully matched, nothing to do
          }
          else
          {
            // add to binding
            vars.push_back(var);
            subs.push_back(next);
            smap[var] = next;
            curr.d_boundVar = true;
          }
        }
        if (next.isNull())
        {
          // if we failed, revert changes to syms
          syms.insert(syms.end(), currChildren.rbegin(), currChildren.rend());
        }
      } while (next.isNull() && curr.d_index <= mt->d_vars.size());
      if (next.isNull())
      {
        // we are out of variables to match, finished with this frame
        visit.pop_back();
        continue;
      }
      Trace("match-debug") << "recurse var : " << var << std::endl;
      itc = mt->d_children.find(var);
      Assert(itc != mt->d_children.end());
      visit.push_back(NaryMatchFrame(syms, &itc->second));
    }
    else
    {
      // no variables to match, we are done
      visit.pop_back();
    }
  }
  return true;
}

void NaryMatchTrie::addTerm(Node n)
{
  Assert(!n.isNull());
  std::vector<Node> visit;
  visit.push_back(n);
  NaryMatchTrie* curr = this;
  while (!visit.empty())
  {
    Node cn = visit.back();
    visit.pop_back();
    if (cn.isNull())
    {
      curr = &(curr->d_children[cn]);
    }
    else if (cn.hasOperator())
    {
      curr = &(curr->d_children[cn.getOperator()]);
      // add null terminator if an n-ary kind
      if (NodeManager::isNAryKind(cn.getKind()))
      {
        visit.push_back(Node::null());
      }
      // note children are processed left to right
      visit.insert(visit.end(), cn.rbegin(), cn.rend());
    }
    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]);
    }
  }
  curr->d_data = n;
}

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

std::string NaryMatchTrie::debugPrint() const
{
  std::stringstream ss;
  std::vector<std::tuple<const NaryMatchTrie*, size_t, Node>> visit;
  visit.emplace_back(this, 0, Node::null());
  do
  {
    std::tuple<const NaryMatchTrie*, size_t, Node> curr = visit.back();
    visit.pop_back();
    size_t indent = std::get<1>(curr);
    for (size_t i = 0; i < indent; i++)
    {
      ss << "  ";
    }
    Node n = std::get<2>(curr);
    if (indent == 0)
    {
      ss << ".";
    }
    else
    {
      ss << n;
    }
    ss << ((!n.isNull() && isListVar(n)) ? " [*]" : "");
    ss << std::endl;
    const NaryMatchTrie* mt = std::get<0>(curr);
    for (const std::pair<const Node, NaryMatchTrie>& c : mt->d_children)
    {
      visit.emplace_back(&c.second, indent + 1, c.first);
    }
  } while (!visit.empty());
  return ss.str();
}

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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 n-ary match trie
14		*/
15
16		#include "expr/nary_match_trie.h"
17
18		#include <sstream>
19		#include "expr/nary_term_util.h"
20
21		using namespace cvc5::kind;
22
23		namespace cvc5 {
24		namespace expr {
25
26		class NaryMatchFrame
27		{
28		public:
29		NaryMatchFrame(const std::vector<Node>& syms, const NaryMatchTrie* t)
30		: d_syms(syms), d_trie(t), d_index(0), d_variant(0), d_boundVar(false)
31		{
32		}
33		/** Symbols to match */
34		std::vector<Node> d_syms;
35		/** The match trie */
36		const NaryMatchTrie* d_trie;
37		/** The index we are considering, 0 = operator, n>0 = variable # (n-1) */
38		size_t d_index;
39		/** List length considering */
40		size_t d_variant;
41		/** Whether we just bound a variable */
42		bool d_boundVar;
43		};
44
45		bool NaryMatchTrie::getMatches(Node n, NotifyMatch* ntm) const
46		{
47		NodeManager* nm = NodeManager::currentNM();
48		std::vector<Node> vars;
49		std::vector<Node> subs;
50		std::map<Node, Node> smap;
51
52		std::map<Node, NaryMatchTrie>::const_iterator itc;
53
54		std::vector<NaryMatchFrame> visit;
55		visit.push_back(NaryMatchFrame({n}, this));
56
57		while (!visit.empty())
58		{
59		NaryMatchFrame& curr = visit.back();
60		// currently, copy the symbols from previous frame TODO: improve?
61		std::vector<Node> syms = curr.d_syms;
62		const NaryMatchTrie* mt = curr.d_trie;
63		if (syms.empty())
64		{
65		// if we matched, there must be a data member at this node
66		Assert(!mt->d_data.isNull());
67		// notify match?
68		Assert(n == expr::narySubstitute(mt->d_data, vars, subs));
69		Trace("match-debug") << "notify : " << mt->d_data << std::endl;
70		if (!ntm->notify(n, mt->d_data, vars, subs))
71		{
72		return false;
73		}
74		visit.pop_back();
75		continue;
76		}
77
78		// clean up if we previously bound a variable
79		if (curr.d_boundVar)
80		{
81		Assert(!vars.empty());
82		Assert(smap.find(vars.back()) != smap.end());
83		smap.erase(vars.back());
84		vars.pop_back();
85		subs.pop_back();
86		curr.d_boundVar = false;
87		}
88
89		if (curr.d_index == 0)
90		{
91		curr.d_index++;
92		// finished matching variables, try to match the operator
93		Node next = syms.back();
94		Node op =
95		(!next.isNull() && next.hasOperator()) ? next.getOperator() : next;
96		itc = mt->d_children.find(op);
97		if (itc != mt->d_children.end())
98		{
99		syms.pop_back();
100		// push the children + null termination marker, in reverse order
101		if (NodeManager::isNAryKind(next.getKind()))
102		{
103		syms.push_back(Node::null());
104		}
105		if (next.hasOperator())
106		{
107		syms.insert(syms.end(), next.rbegin(), next.rend());
108		}
109		// new frame
110		visit.push_back(NaryMatchFrame(syms, &itc->second));
111		}
112		}
113		else if (curr.d_index <= mt->d_vars.size())
114		{
115		// try to match the next (variable, length)
116		Node var;
117		Node next;
118		do
119		{
120		var = mt->d_vars[curr.d_index - 1];
121		Assert(mt->d_children.find(var) != mt->d_children.end());
122		std::vector<Node> currChildren;
123		if (isListVar(var))
124		{
125		// get the length of the list we want to consider
126		size_t l = curr.d_variant;
127		curr.d_variant++;
128		// match with l, or increment d_index otherwise
129		bool foundChildren = true;
130		// We are in a state where the children of an n-ary child
131		// have been pused to syms. We try to extract l children here. If
132		// we encounter the null symbol, then we do not have sufficient
133		// children to match for this variant and fail.
134		for (size_t i = 0; i < l; i++)
135		{
136		Assert(!syms.empty());
137		Node s = syms.back();
138		if (s.isNull())
139		{
140		foundChildren = false;
141		break;
142		}
143		currChildren.push_back(s);
144		syms.pop_back();
145		}
146		if (foundChildren)
147		{
148		// we are matching the next list
149		next = nm->mkNode(SEXPR, currChildren);
150		}
151		else
152		{
153		// otherwise, we have run out of variants, go to next variable
154		curr.d_index++;
155		curr.d_variant = 0;
156		}
157		}
158		else
159		{
160		next = syms.back();
161		curr.d_index++;
162		// we could be at the end of an n-ary operator, in which case we
163		// do not match
164		if (!next.isNull())
165		{
166		currChildren.push_back(next);
167		syms.pop_back();
168		// check subtyping in the (non-list) case
169		if (!var.getType().isSubtypeOf(next.getType()))
170		{
171		next = Node::null();
172		}
173		}
174		}
175		if (!next.isNull())
176		{
177		// check if it is already bound, do the binding if necessary
178		std::map<Node, Node>::iterator its = smap.find(var);
179		if (its != smap.end())
180		{
181		if (its->second != next)
182		{
183		// failed to match
184		next = Node::null();
185		}
186		// otherwise, successfully matched, nothing to do
187		}
188		else
189		{
190		// add to binding
191		vars.push_back(var);
192		subs.push_back(next);
193		smap[var] = next;
194		curr.d_boundVar = true;
195		}
196		}
197		if (next.isNull())
198		{
199		// if we failed, revert changes to syms
200		syms.insert(syms.end(), currChildren.rbegin(), currChildren.rend());
201		}
202		} while (next.isNull() && curr.d_index <= mt->d_vars.size());
203		if (next.isNull())
204		{
205		// we are out of variables to match, finished with this frame
206		visit.pop_back();
207		continue;
208		}
209		Trace("match-debug") << "recurse var : " << var << std::endl;
210		itc = mt->d_children.find(var);
211		Assert(itc != mt->d_children.end());
212		visit.push_back(NaryMatchFrame(syms, &itc->second));
213		}
214		else
215		{
216		// no variables to match, we are done
217		visit.pop_back();
218		}
219		}
220		return true;
221		}
222
223		void NaryMatchTrie::addTerm(Node n)
224		{
225		Assert(!n.isNull());
226		std::vector<Node> visit;
227		visit.push_back(n);
228		NaryMatchTrie* curr = this;
229		while (!visit.empty())
230		{
231		Node cn = visit.back();
232		visit.pop_back();
233		if (cn.isNull())
234		{
235		curr = &(curr->d_children[cn]);
236		}
237		else if (cn.hasOperator())
238		{
239		curr = &(curr->d_children[cn.getOperator()]);
240		// add null terminator if an n-ary kind
241		if (NodeManager::isNAryKind(cn.getKind()))
242		{
243		visit.push_back(Node::null());
244		}
245		// note children are processed left to right
246		visit.insert(visit.end(), cn.rbegin(), cn.rend());
247		}
248		else
249		{
250		if (cn.isVar()
251		&& std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
252		== curr->d_vars.end())
253		{
254		curr->d_vars.push_back(cn);
255		}
256		curr = &(curr->d_children[cn]);
257		}
258		}
259		curr->d_data = n;
260		}
261
262		void NaryMatchTrie::clear()
263		{
264		d_children.clear();
265		d_vars.clear();
266		d_data = Node::null();
267		}
268
269		std::string NaryMatchTrie::debugPrint() const
270		{
271		std::stringstream ss;
272		std::vector<std::tuple<const NaryMatchTrie*, size_t, Node>> visit;
273		visit.emplace_back(this, 0, Node::null());
274		do
275		{
276		std::tuple<const NaryMatchTrie*, size_t, Node> curr = visit.back();
277		visit.pop_back();
278		size_t indent = std::get<1>(curr);
279		for (size_t i = 0; i < indent; i++)
280		{
281		ss << " ";
282		}
283		Node n = std::get<2>(curr);
284		if (indent == 0)
285		{
286		ss << ".";
287		}
288		else
289		{
290		ss << n;
291		}
292		ss << ((!n.isNull() && isListVar(n)) ? " [*]" : "");
293		ss << std::endl;
294		const NaryMatchTrie* mt = std::get<0>(curr);
295		for (const std::pair<const Node, NaryMatchTrie>& c : mt->d_children)
296		{
297		visit.emplace_back(&c.second, indent + 1, c.first);
298		}
299		} while (!visit.empty());
300		return ss.str();
301		}
302
303		} // namespace expr
304	29577	} // namespace cvc5