Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/inst_match_trie.cpp	Lines:	70	155	45.2 %
Date:	2021-09-16	Branches:	82	390	21.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, 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.
 * ****************************************************************************
 *
 * Implementation of inst match trie class.
 */

#include "theory/quantifiers/inst_match_trie.h"

#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
#include "theory/uf/equality_engine_iterator.h"

using namespace cvc5::context;

namespace cvc5 {
namespace theory {
namespace quantifiers {

bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
                                    Node q,
                                    const std::vector<Node>& m,
                                    bool modEq,
                                    ImtIndexOrder* imtio,
                                    unsigned index)
{
  return !addInstMatch(qs, q, m, modEq, imtio, true, index);
}

bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
                                 Node f,
                                 const std::vector<Node>& m,
                                 bool modEq,
                                 ImtIndexOrder* imtio,
                                 bool onlyExist,
                                 unsigned index)
{
  if (index == f[0].getNumChildren()
      || (imtio && index == imtio->d_order.size()))
  {
    return false;
  }
  unsigned i_index = imtio ? imtio->d_order[index] : index;
  Node n = m[i_index];
  std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
  if (it != d_data.end())
  {
    bool ret =
        it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1);
    if (!onlyExist || !ret)
    {
      return ret;
    }
  }
  if (modEq)
  {
    // check modulo equality if any other instantiation match exists
    if (!n.isNull() && qs.hasTerm(n))
    {
      eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
      while (!eqc.isFinished())
      {
        Node en = (*eqc);
        if (en != n)
        {
          std::map<Node, InstMatchTrie>::iterator itc = d_data.find(en);
          if (itc != d_data.end())
          {
            if (itc->second.addInstMatch(
                    qs, f, m, modEq, imtio, true, index + 1))
            {
              return false;
            }
          }
        }
        ++eqc;
      }
    }
  }
  if (!onlyExist)
  {
    d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1);
  }
  return true;
}

bool InstMatchTrie::removeInstMatch(Node q,
                                    const std::vector<Node>& m,
                                    ImtIndexOrder* imtio,
                                    unsigned index)
{
  Assert(index < q[0].getNumChildren());
  Assert(!imtio || index < imtio->d_order.size());
  unsigned i_index = imtio ? imtio->d_order[index] : index;
  Node n = m[i_index];
  std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
  if (it != d_data.end())
  {
    if ((index + 1) == q[0].getNumChildren()
        || (imtio && (index + 1) == imtio->d_order.size()))
    {
      d_data.erase(n);
      return true;
    }
    return it->second.removeInstMatch(q, m, imtio, index + 1);
  }
  return false;
}

void InstMatchTrie::print(std::ostream& out,
                          Node q,
                          std::vector<TNode>& terms) const
{
  if (terms.size() == q[0].getNumChildren())
  {
    out << "  ( ";
    for (unsigned i = 0, size = terms.size(); i < size; i++)
    {
      if (i > 0)
      {
        out << ", ";
      }
      out << terms[i];
    }
    out << " )" << std::endl;
  }
  else
  {
    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
    {
      terms.push_back(d.first);
      d.second.print(out, q, terms);
      terms.pop_back();
    }
  }
}

void InstMatchTrie::getInstantiations(
    Node q, std::vector<std::vector<Node>>& insts) const
{
  std::vector<Node> terms;
  getInstantiations(q, insts, terms);
}

void InstMatchTrie::getInstantiations(Node q,
                                      std::vector<std::vector<Node>>& insts,
                                      std::vector<Node>& terms) const
{
  if (terms.size() == q[0].getNumChildren())
  {
    insts.push_back(terms);
  }
  else
  {
    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
    {
      terms.push_back(d.first);
      d.second.getInstantiations(q, insts, terms);
      terms.pop_back();
    }
  }
}

void InstMatchTrie::clear() { d_data.clear(); }

void InstMatchTrie::print(std::ostream& out, Node q) const
{
  std::vector<TNode> terms;
  print(out, q, terms);
}

CDInstMatchTrie::~CDInstMatchTrie()
{
  for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
  {
    CDInstMatchTrie* current = d.second;
    delete current;
  }
  d_data.clear();
}

bool CDInstMatchTrie::existsInstMatch(context::Context* context,
                                      quantifiers::QuantifiersState& qs,
                                      Node q,
                                      const std::vector<Node>& m,
                                      bool modEq,
                                      unsigned index)
{
  return !addInstMatch(context, qs, q, m, modEq, index, true);
}

bool CDInstMatchTrie::addInstMatch(context::Context* context,
                                   quantifiers::QuantifiersState& qs,
                                   Node f,
                                   const std::vector<Node>& m,
                                   bool modEq,
                                   unsigned index,
                                   bool onlyExist)
{
  bool reset = false;
  if (!d_valid.get())
  {
    if (onlyExist)
    {
      return true;
    }
    else
    {
      d_valid.set(true);
      reset = true;
    }
  }
  if (index == f[0].getNumChildren())
  {
    return reset;
  }
  Node n = m[index];
  std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
  if (it != d_data.end())
  {
    bool ret =
        it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist);
    if (!onlyExist || !ret)
    {
      return reset || ret;
    }
  }
  if (modEq)
  {
    // check modulo equality if any other instantiation match exists
    if (!n.isNull() && qs.hasTerm(n))
    {
      eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
      while (!eqc.isFinished())
      {
        Node en = (*eqc);
        if (en != n)
        {
          std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
          if (itc != d_data.end())
          {
            if (itc->second->addInstMatch(
                    context, qs, f, m, modEq, index + 1, true))
            {
              return false;
            }
          }
        }
        ++eqc;
      }
    }
  }

  if (!onlyExist)
  {
    CDInstMatchTrie* imt = new CDInstMatchTrie(context);
    Assert(d_data.find(n) == d_data.end());
    d_data[n] = imt;
    imt->addInstMatch(context, qs, f, m, modEq, index + 1, false);
  }
  return true;
}

bool CDInstMatchTrie::removeInstMatch(Node q,
                                      const std::vector<Node>& m,
                                      unsigned index)
{
  if (index == q[0].getNumChildren())
  {
    if (d_valid.get())
    {
      d_valid.set(false);
      return true;
    }
    return false;
  }
  std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
  if (it != d_data.end())
  {
    return it->second->removeInstMatch(q, m, index + 1);
  }
  return false;
}

void CDInstMatchTrie::print(std::ostream& out,
                            Node q,
                            std::vector<TNode>& terms) const
{
  if (d_valid.get())
  {
    if (terms.size() == q[0].getNumChildren())
    {
      out << "  ( ";
      for (unsigned i = 0; i < terms.size(); i++)
      {
        if (i > 0) out << " ";
        out << terms[i];
      }
      out << " )" << std::endl;
    }
    else
    {
      for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
      {
        terms.push_back(d.first);
        d.second->print(out, q, terms);
        terms.pop_back();
      }
    }
  }
}

void CDInstMatchTrie::getInstantiations(
    Node q, std::vector<std::vector<Node>>& insts) const
{
  std::vector<Node> terms;
  getInstantiations(q, insts, terms);
}

void CDInstMatchTrie::getInstantiations(Node q,
                                        std::vector<std::vector<Node>>& insts,
                                        std::vector<Node>& terms) const
{
  if (!d_valid.get())
  {
    // do nothing
  }
  else if (terms.size() == q[0].getNumChildren())
  {
    insts.push_back(terms);
  }
  else
  {
    for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
    {
      terms.push_back(d.first);
      d.second->getInstantiations(q, insts, terms);
      terms.pop_back();
    }
  }
}

void CDInstMatchTrie::print(std::ostream& out, Node q) const
{
  std::vector<TNode> terms;
  print(out, q, terms);
}

bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs,
                                        Node q,
                                        const std::vector<Node>& m,
                                        bool modEq)
{
  return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
}

bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
                                           Node q,
                                           const std::vector<Node>& m,
                                           bool modEq)
{
  return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, 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		* Implementation of inst match trie class.
14		*/
15
16		#include "theory/quantifiers/inst_match_trie.h"
17
18		#include "theory/quantifiers/instantiate.h"
19		#include "theory/quantifiers/quant_util.h"
20		#include "theory/quantifiers/quantifiers_state.h"
21		#include "theory/quantifiers/term_database.h"
22		#include "theory/uf/equality_engine_iterator.h"
23
24		using namespace cvc5::context;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29
30		bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
31		Node q,
32		const std::vector<Node>& m,
33		bool modEq,
34		ImtIndexOrder* imtio,
35		unsigned index)
36		{
37		return !addInstMatch(qs, q, m, modEq, imtio, true, index);
38		}
39
40	242953	bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
41		Node f,
42		const std::vector<Node>& m,
43		bool modEq,
44		ImtIndexOrder* imtio,
45		bool onlyExist,
46		unsigned index)
47		{
48	728859	if (index == f[0].getNumChildren()
49	728859	\|\| (imtio && index == imtio->d_order.size()))
50		{
51	71657	return false;
52		}
53	171296	unsigned i_index = imtio ? imtio->d_order[index] : index;
54	342592	Node n = m[i_index];
55	171296	std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
56	171296	if (it != d_data.end())
57		{
58		bool ret =
59	97611	it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1);
60	97611	if (!onlyExist \|\| !ret)
61		{
62	97611	return ret;
63		}
64		}
65	73685	if (modEq)
66		{
67		// check modulo equality if any other instantiation match exists
68		if (!n.isNull() && qs.hasTerm(n))
69		{
70		eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
71		while (!eqc.isFinished())
72		{
73		Node en = (*eqc);
74		if (en != n)
75		{
76		std::map<Node, InstMatchTrie>::iterator itc = d_data.find(en);
77		if (itc != d_data.end())
78		{
79		if (itc->second.addInstMatch(
80		qs, f, m, modEq, imtio, true, index + 1))
81		{
82		return false;
83		}
84		}
85		}
86		++eqc;
87		}
88		}
89		}
90	73685	if (!onlyExist)
91		{
92	73685	d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1);
93		}
94	73685	return true;
95		}
96
97		bool InstMatchTrie::removeInstMatch(Node q,
98		const std::vector<Node>& m,
99		ImtIndexOrder* imtio,
100		unsigned index)
101		{
102		Assert(index < q[0].getNumChildren());
103		Assert(!imtio \|\| index < imtio->d_order.size());
104		unsigned i_index = imtio ? imtio->d_order[index] : index;
105		Node n = m[i_index];
106		std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
107		if (it != d_data.end())
108		{
109		if ((index + 1) == q[0].getNumChildren()
110		\|\| (imtio && (index + 1) == imtio->d_order.size()))
111		{
112		d_data.erase(n);
113		return true;
114		}
115		return it->second.removeInstMatch(q, m, imtio, index + 1);
116		}
117		return false;
118		}
119
120		void InstMatchTrie::print(std::ostream& out,
121		Node q,
122		std::vector<TNode>& terms) const
123		{
124		if (terms.size() == q[0].getNumChildren())
125		{
126		out << " ( ";
127		for (unsigned i = 0, size = terms.size(); i < size; i++)
128		{
129		if (i > 0)
130		{
131		out << ", ";
132		}
133		out << terms[i];
134		}
135		out << " )" << std::endl;
136		}
137		else
138		{
139		for (const std::pair<const Node, InstMatchTrie>& d : d_data)
140		{
141		terms.push_back(d.first);
142		d.second.print(out, q, terms);
143		terms.pop_back();
144		}
145		}
146		}
147
148	49	void InstMatchTrie::getInstantiations(
149		Node q, std::vector<std::vector<Node>>& insts) const
150		{
151	98	std::vector<Node> terms;
152	49	getInstantiations(q, insts, terms);
153	49	}
154
155	440	void InstMatchTrie::getInstantiations(Node q,
156		std::vector<std::vector<Node>>& insts,
157		std::vector<Node>& terms) const
158		{
159	440	if (terms.size() == q[0].getNumChildren())
160		{
161	111	insts.push_back(terms);
162		}
163		else
164		{
165	720	for (const std::pair<const Node, InstMatchTrie>& d : d_data)
166		{
167	391	terms.push_back(d.first);
168	391	d.second.getInstantiations(q, insts, terms);
169	391	terms.pop_back();
170		}
171		}
172	440	}
173
174		void InstMatchTrie::clear() { d_data.clear(); }
175
176		void InstMatchTrie::print(std::ostream& out, Node q) const
177		{
178		std::vector<TNode> terms;
179		print(out, q, terms);
180		}
181
182	15560	CDInstMatchTrie::~CDInstMatchTrie()
183		{
184	14849	for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
185		{
186	7069	CDInstMatchTrie* current = d.second;
187	7069	delete current;
188		}
189	7780	d_data.clear();
190	7780	}
191
192		bool CDInstMatchTrie::existsInstMatch(context::Context* context,
193		quantifiers::QuantifiersState& qs,
194		Node q,
195		const std::vector<Node>& m,
196		bool modEq,
197		unsigned index)
198		{
199		return !addInstMatch(context, qs, q, m, modEq, index, true);
200		}
201
202	22143	bool CDInstMatchTrie::addInstMatch(context::Context* context,
203		quantifiers::QuantifiersState& qs,
204		Node f,
205		const std::vector<Node>& m,
206		bool modEq,
207		unsigned index,
208		bool onlyExist)
209		{
210	22143	bool reset = false;
211	22143	if (!d_valid.get())
212		{
213	7964	if (onlyExist)
214		{
215		return true;
216		}
217		else
218		{
219	7964	d_valid.set(true);
220	7964	reset = true;
221		}
222		}
223	22143	if (index == f[0].getNumChildren())
224		{
225	8201	return reset;
226		}
227	27884	Node n = m[index];
228	13942	std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
229	13942	if (it != d_data.end())
230		{
231		bool ret =
232	6873	it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist);
233	6873	if (!onlyExist \|\| !ret)
234		{
235	6873	return reset \|\| ret;
236		}
237		}
238	7069	if (modEq)
239		{
240		// check modulo equality if any other instantiation match exists
241		if (!n.isNull() && qs.hasTerm(n))
242		{
243		eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
244		while (!eqc.isFinished())
245		{
246		Node en = (*eqc);
247		if (en != n)
248		{
249		std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
250		if (itc != d_data.end())
251		{
252		if (itc->second->addInstMatch(
253		context, qs, f, m, modEq, index + 1, true))
254		{
255		return false;
256		}
257		}
258		}
259		++eqc;
260		}
261		}
262		}
263
264	7069	if (!onlyExist)
265		{
266	7069	CDInstMatchTrie* imt = new CDInstMatchTrie(context);
267	7069	Assert(d_data.find(n) == d_data.end());
268	7069	d_data[n] = imt;
269	7069	imt->addInstMatch(context, qs, f, m, modEq, index + 1, false);
270		}
271	7069	return true;
272		}
273
274		bool CDInstMatchTrie::removeInstMatch(Node q,
275		const std::vector<Node>& m,
276		unsigned index)
277		{
278		if (index == q[0].getNumChildren())
279		{
280		if (d_valid.get())
281		{
282		d_valid.set(false);
283		return true;
284		}
285		return false;
286		}
287		std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
288		if (it != d_data.end())
289		{
290		return it->second->removeInstMatch(q, m, index + 1);
291		}
292		return false;
293		}
294
295		void CDInstMatchTrie::print(std::ostream& out,
296		Node q,
297		std::vector<TNode>& terms) const
298		{
299		if (d_valid.get())
300		{
301		if (terms.size() == q[0].getNumChildren())
302		{
303		out << " ( ";
304		for (unsigned i = 0; i < terms.size(); i++)
305		{
306		if (i > 0) out << " ";
307		out << terms[i];
308		}
309		out << " )" << std::endl;
310		}
311		else
312		{
313		for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
314		{
315		terms.push_back(d.first);
316		d.second->print(out, q, terms);
317		terms.pop_back();
318		}
319		}
320		}
321		}
322
323	4	void CDInstMatchTrie::getInstantiations(
324		Node q, std::vector<std::vector<Node>>& insts) const
325		{
326	8	std::vector<Node> terms;
327	4	getInstantiations(q, insts, terms);
328	4	}
329
330	10	void CDInstMatchTrie::getInstantiations(Node q,
331		std::vector<std::vector<Node>>& insts,
332		std::vector<Node>& terms) const
333		{
334	10	if (!d_valid.get())
335		{
336		// do nothing
337		}
338	8	else if (terms.size() == q[0].getNumChildren())
339		{
340	4	insts.push_back(terms);
341		}
342		else
343		{
344	10	for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
345		{
346	6	terms.push_back(d.first);
347	6	d.second->getInstantiations(q, insts, terms);
348	6	terms.pop_back();
349		}
350		}
351	10	}
352
353		void CDInstMatchTrie::print(std::ostream& out, Node q) const
354		{
355		std::vector<TNode> terms;
356		print(out, q, terms);
357		}
358
359	308	bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs,
360		Node q,
361		const std::vector<Node>& m,
362		bool modEq)
363		{
364	308	return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
365		}
366
367		bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
368		Node q,
369		const std::vector<Node>& m,
370		bool modEq)
371		{
372		return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
373		}
374
375		} // namespace quantifiers
376		} // namespace theory
377	29577	} // namespace cvc5