Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/inst_match_trie.cpp	Lines:	70	155	45.2 %
Date:	2021-08-01	Branches:	83	394	21.1 %


/******************************************************************************
 * 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(quantifiers::QuantifiersState& qs,
                                      Node q,
                                      const std::vector<Node>& m,
                                      bool modEq,
                                      unsigned index)
{
  return !addInstMatch(qs, q, m, modEq, index, true);
}

bool CDInstMatchTrie::addInstMatch(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(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(qs, f, m, modEq, index + 1, true))
            {
              return false;
            }
          }
        }
        ++eqc;
      }
    }
  }

  if (!onlyExist)
  {
    CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext());
    Assert(d_data.find(n) == d_data.end());
    d_data[n] = imt;
    imt->addInstMatch(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	254972	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	764916	if (index == f[0].getNumChildren()
49	764916	\|\| (imtio && index == imtio->d_order.size()))
50		{
51	75804	return false;
52		}
53	179168	unsigned i_index = imtio ? imtio->d_order[index] : index;
54	358336	Node n = m[i_index];
55	179168	std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
56	179168	if (it != d_data.end())
57		{
58		bool ret =
59	106439	it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1);
60	106439	if (!onlyExist \|\| !ret)
61		{
62	106439	return ret;
63		}
64		}
65	72729	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	72729	if (!onlyExist)
91		{
92	72729	d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1);
93		}
94	72729	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	48	void InstMatchTrie::getInstantiations(
149		Node q, std::vector<std::vector<Node>>& insts) const
150		{
151	96	std::vector<Node> terms;
152	48	getInstantiations(q, insts, terms);
153	48	}
154
155	388	void InstMatchTrie::getInstantiations(Node q,
156		std::vector<std::vector<Node>>& insts,
157		std::vector<Node>& terms) const
158		{
159	388	if (terms.size() == q[0].getNumChildren())
160		{
161	116	insts.push_back(terms);
162		}
163		else
164		{
165	612	for (const std::pair<const Node, InstMatchTrie>& d : d_data)
166		{
167	340	terms.push_back(d.first);
168	340	d.second.getInstantiations(q, insts, terms);
169	340	terms.pop_back();
170		}
171		}
172	388	}
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	14008	CDInstMatchTrie::~CDInstMatchTrie()
183		{
184	13306	for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
185		{
186	6302	CDInstMatchTrie* current = d.second;
187	6302	delete current;
188		}
189	7004	d_data.clear();
190	7004	}
191
192		bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
193		Node q,
194		const std::vector<Node>& m,
195		bool modEq,
196		unsigned index)
197		{
198		return !addInstMatch(qs, q, m, modEq, index, true);
199		}
200
201	18613	bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
202		Node f,
203		const std::vector<Node>& m,
204		bool modEq,
205		unsigned index,
206		bool onlyExist)
207		{
208	18613	bool reset = false;
209	18613	if (!d_valid.get())
210		{
211	7187	if (onlyExist)
212		{
213		return true;
214		}
215		else
216		{
217	7187	d_valid.set(true);
218	7187	reset = true;
219		}
220		}
221	18613	if (index == f[0].getNumChildren())
222		{
223	7032	return reset;
224		}
225	23162	Node n = m[index];
226	11581	std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
227	11581	if (it != d_data.end())
228		{
229	5279	bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist);
230	5279	if (!onlyExist \|\| !ret)
231		{
232	5279	return reset \|\| ret;
233		}
234		}
235	6302	if (modEq)
236		{
237		// check modulo equality if any other instantiation match exists
238		if (!n.isNull() && qs.hasTerm(n))
239		{
240		eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
241		while (!eqc.isFinished())
242		{
243		Node en = (*eqc);
244		if (en != n)
245		{
246		std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
247		if (itc != d_data.end())
248		{
249		if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true))
250		{
251		return false;
252		}
253		}
254		}
255		++eqc;
256		}
257		}
258		}
259
260	6302	if (!onlyExist)
261		{
262	6302	CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext());
263	6302	Assert(d_data.find(n) == d_data.end());
264	6302	d_data[n] = imt;
265	6302	imt->addInstMatch(qs, f, m, modEq, index + 1, false);
266		}
267	6302	return true;
268		}
269
270		bool CDInstMatchTrie::removeInstMatch(Node q,
271		const std::vector<Node>& m,
272		unsigned index)
273		{
274		if (index == q[0].getNumChildren())
275		{
276		if (d_valid.get())
277		{
278		d_valid.set(false);
279		return true;
280		}
281		return false;
282		}
283		std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
284		if (it != d_data.end())
285		{
286		return it->second->removeInstMatch(q, m, index + 1);
287		}
288		return false;
289		}
290
291		void CDInstMatchTrie::print(std::ostream& out,
292		Node q,
293		std::vector<TNode>& terms) const
294		{
295		if (d_valid.get())
296		{
297		if (terms.size() == q[0].getNumChildren())
298		{
299		out << " ( ";
300		for (unsigned i = 0; i < terms.size(); i++)
301		{
302		if (i > 0) out << " ";
303		out << terms[i];
304		}
305		out << " )" << std::endl;
306		}
307		else
308		{
309		for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
310		{
311		terms.push_back(d.first);
312		d.second->print(out, q, terms);
313		terms.pop_back();
314		}
315		}
316		}
317		}
318
319	4	void CDInstMatchTrie::getInstantiations(
320		Node q, std::vector<std::vector<Node>>& insts) const
321		{
322	8	std::vector<Node> terms;
323	4	getInstantiations(q, insts, terms);
324	4	}
325
326	10	void CDInstMatchTrie::getInstantiations(Node q,
327		std::vector<std::vector<Node>>& insts,
328		std::vector<Node>& terms) const
329		{
330	10	if (!d_valid.get())
331		{
332		// do nothing
333		}
334	8	else if (terms.size() == q[0].getNumChildren())
335		{
336	4	insts.push_back(terms);
337		}
338		else
339		{
340	10	for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
341		{
342	6	terms.push_back(d.first);
343	6	d.second->getInstantiations(q, insts, terms);
344	6	terms.pop_back();
345		}
346		}
347	10	}
348
349		void CDInstMatchTrie::print(std::ostream& out, Node q) const
350		{
351		std::vector<TNode> terms;
352		print(out, q, terms);
353		}
354
355	308	bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs,
356		Node q,
357		const std::vector<Node>& m,
358		bool modEq)
359		{
360	308	return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
361		}
362
363		bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
364		Node q,
365		const std::vector<Node>& m,
366		bool modEq)
367		{
368		return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
369		}
370
371		} // namespace quantifiers
372		} // namespace theory
373	29280	} // namespace cvc5