Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/index_trie.cpp	Lines:	42	43	97.7 %
Date:	2021-09-15	Branches:	55	98	56.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   MikolasJanota
 *
 * 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 a trie that store subsets of tuples of term indices
 * that are not yielding  useful instantiations. of quantifier instantiation.
 * This is used in the term_tuple_enumerator.
 */
#include "theory/quantifiers/index_trie.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

void IndexTrie::add(const std::vector<bool>& mask,
                    const std::vector<size_t>& values)
{
  const size_t cardinality = std::count(mask.begin(), mask.end(), true);
  if (d_ignoreFullySpecified && cardinality == mask.size())
  {
    return;
  }

  d_root = addRec(d_root, 0, cardinality, mask, values);
}

void IndexTrie::freeRec(IndexTrieNode* n)
{
  if (!n)
  {
    return;
  }
  for (auto c : n->d_children)
  {
    freeRec(c.second);
  }
  freeRec(n->d_blank);
  delete n;
}

bool IndexTrie::findRec(const IndexTrieNode* n,
                        size_t index,
                        const std::vector<size_t>& members,
                        size_t& nonBlankLength) const
{
  if (!n || index >= members.size())
  {
    return true;  // all elements of members matched
  }
  if (n->d_blank && findRec(n->d_blank, index + 1, members, nonBlankLength))
  {
    return true;  // found in the blank branch
  }
  nonBlankLength = index + 1;
  for (const auto& c : n->d_children)
  {
    if (c.first == members[index]
        && findRec(c.second, index + 1, members, nonBlankLength))
    {
      return true;  // found in the matching subtree
    }
  }
  return false;
}

IndexTrieNode* IndexTrie::addRec(IndexTrieNode* n,
                                 size_t index,
                                 size_t cardinality,
                                 const std::vector<bool>& mask,
                                 const std::vector<size_t>& values)
{
  if (!n)
  {
    return nullptr;  // this tree matches everything, no point to add
  }
  if (cardinality == 0)  // all blanks, all strings match
  {
    freeRec(n);
    return nullptr;
  }

  Assert(index < mask.size());

  if (!mask[index])  // blank position in the added vector
  {
    auto blank = n->d_blank ? n->d_blank : new IndexTrieNode();
    n->d_blank = addRec(blank, index + 1, cardinality, mask, values);
    return n;
  }
  Assert(cardinality);

  for (auto& edge : n->d_children)
  {
    if (edge.first == values[index])
    {
      // value already amongst the children
      edge.second =
          addRec(edge.second, index + 1, cardinality - 1, mask, values);
      return n;
    }
  }
  // new child needs to be added
  auto child =
      addRec(new IndexTrieNode(), index + 1, cardinality - 1, mask, values);
  n->d_children.push_back(std::make_pair(values[index], child));
  return n;
}
}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* MikolasJanota
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 a trie that store subsets of tuples of term indices
14		* that are not yielding useful instantiations. of quantifier instantiation.
15		* This is used in the term_tuple_enumerator.
16		*/
17		#include "theory/quantifiers/index_trie.h"
18
19		namespace cvc5 {
20		namespace theory {
21		namespace quantifiers {
22
23	2644	void IndexTrie::add(const std::vector<bool>& mask,
24		const std::vector<size_t>& values)
25		{
26	2644	const size_t cardinality = std::count(mask.begin(), mask.end(), true);
27	2644	if (d_ignoreFullySpecified && cardinality == mask.size())
28		{
29	2301	return;
30		}
31
32	343	d_root = addRec(d_root, 0, cardinality, mask, values);
33		}
34
35	6493	void IndexTrie::freeRec(IndexTrieNode* n)
36		{
37	6493	if (!n)
38		{
39	3399	return;
40		}
41	4861	for (auto c : n->d_children)
42		{
43	1767	freeRec(c.second);
44		}
45	3094	freeRec(n->d_blank);
46	3094	delete n;
47		}
48
49	6029	bool IndexTrie::findRec(const IndexTrieNode* n,
50		size_t index,
51		const std::vector<size_t>& members,
52		size_t& nonBlankLength) const
53		{
54	6029	if (!n \|\| index >= members.size())
55		{
56	280	return true; // all elements of members matched
57		}
58	5749	if (n->d_blank && findRec(n->d_blank, index + 1, members, nonBlankLength))
59		{
60	76	return true; // found in the blank branch
61		}
62	5673	nonBlankLength = index + 1;
63	8079	for (const auto& c : n->d_children)
64		{
65	7732	if (c.first == members[index]
66	3866	&& findRec(c.second, index + 1, members, nonBlankLength))
67		{
68	1460	return true; // found in the matching subtree
69		}
70		}
71	4213	return false;
72		}
73
74	2589	IndexTrieNode* IndexTrie::addRec(IndexTrieNode* n,
75		size_t index,
76		size_t cardinality,
77		const std::vector<bool>& mask,
78		const std::vector<size_t>& values)
79		{
80	2589	if (!n)
81		{
82		return nullptr; // this tree matches everything, no point to add
83		}
84	2589	if (cardinality == 0) // all blanks, all strings match
85		{
86	343	freeRec(n);
87	343	return nullptr;
88		}
89
90	2246	Assert(index < mask.size());
91
92	2246	if (!mask[index]) // blank position in the added vector
93		{
94	62	auto blank = n->d_blank ? n->d_blank : new IndexTrieNode();
95	62	n->d_blank = addRec(blank, index + 1, cardinality, mask, values);
96	62	return n;
97		}
98	2184	Assert(cardinality);
99
100	2276	for (auto& edge : n->d_children)
101		{
102	509	if (edge.first == values[index])
103		{
104		// value already amongst the children
105	417	edge.second =
106	417	addRec(edge.second, index + 1, cardinality - 1, mask, values);
107	417	return n;
108		}
109		}
110		// new child needs to be added
111		auto child =
112	1767	addRec(new IndexTrieNode(), index + 1, cardinality - 1, mask, values);
113	1767	n->d_children.push_back(std::make_pair(values[index], child));
114	1767	return n;
115		}
116		} // namespace quantifiers
117		} // namespace theory
118		} // namespace cvc5