Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_registry.cpp	Lines:	80	95	84.2 %
Date:	2021-08-16	Branches:	82	216	38.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * The quantifiers registry.
 */

#include "theory/quantifiers/quantifiers_registry.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/term_util.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

QuantifiersRegistry::QuantifiersRegistry()
    : d_quantAttr(),
      d_quantBoundInf(options::fmfTypeCompletionThresh(),
                      options::finiteModelFind())
{
}

void QuantifiersRegistry::registerQuantifier(Node q)
{
  if (d_inst_constants.find(q) != d_inst_constants.end())
  {
    return;
  }
  NodeManager* nm = NodeManager::currentNM();
  Debug("quantifiers-engine")
      << "Instantiation constants for " << q << " : " << std::endl;
  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
  {
    d_vars[q].push_back(q[0][i]);
    // make instantiation constants
    Node ic = nm->mkInstConstant(q[0][i].getType());
    d_inst_constants_map[ic] = q;
    d_inst_constants[q].push_back(ic);
    Debug("quantifiers-engine") << "  " << ic << std::endl;
    // set the var number attribute
    InstVarNumAttribute ivna;
    ic.setAttribute(ivna, i);
    InstConstantAttribute ica;
    ic.setAttribute(ica, q);
  }
  // compute attributes
  d_quantAttr.computeAttributes(q);
}

bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }

std::string QuantifiersRegistry::identify() const
{
  return "QuantifiersRegistry";
}

QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
{
  std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
  if (it == d_owner.end())
  {
    return nullptr;
  }
  return it->second;
}

void QuantifiersRegistry::setOwner(Node q,
                                   QuantifiersModule* m,
                                   int32_t priority)
{
  QuantifiersModule* mo = getOwner(q);
  if (mo == m)
  {
    return;
  }
  if (mo != nullptr)
  {
    if (priority <= d_owner_priority[q])
    {
      Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
                          << (m ? m->identify() : "null")
                          << ", but already has owner " << mo->identify()
                          << " with higher priority!" << std::endl;
      return;
    }
  }
  d_owner[q] = m;
  d_owner_priority[q] = priority;
}

bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
{
  QuantifiersModule* mo = getOwner(q);
  return mo == m || mo == nullptr;
}

Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
{
  std::map<Node, std::vector<Node> >::const_iterator it =
      d_inst_constants.find(q);
  if (it != d_inst_constants.end())
  {
    return it->second[i];
  }
  return Node::null();
}

size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
{
  std::map<Node, std::vector<Node> >::const_iterator it =
      d_inst_constants.find(q);
  if (it != d_inst_constants.end())
  {
    return it->second.size();
  }
  return 0;
}

Node QuantifiersRegistry::getInstConstantBody(Node q)
{
  std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
  if (it == d_inst_const_body.end())
  {
    Node n = substituteBoundVariablesToInstConstants(q[1], q);
    d_inst_const_body[q] = n;
    return n;
  }
  return it->second;
}

Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
                                                                  Node q)
{
  registerQuantifier(q);
  return n.substitute(d_vars[q].begin(),
                      d_vars[q].end(),
                      d_inst_constants[q].begin(),
                      d_inst_constants[q].end());
}

Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
                                                                  Node q)
{
  registerQuantifier(q);
  return n.substitute(d_inst_constants[q].begin(),
                      d_inst_constants[q].end(),
                      d_vars[q].begin(),
                      d_vars[q].end());
}

Node QuantifiersRegistry::substituteBoundVariables(Node n,
                                                   Node q,
                                                   std::vector<Node>& terms)
{
  registerQuantifier(q);
  Assert(d_vars[q].size() == terms.size());
  return n.substitute(
      d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end());
}

Node QuantifiersRegistry::substituteInstConstants(Node n,
                                                  Node q,
                                                  std::vector<Node>& terms)
{
  registerQuantifier(q);
  Assert(d_inst_constants[q].size() == terms.size());
  return n.substitute(d_inst_constants[q].begin(),
                      d_inst_constants[q].end(),
                      terms.begin(),
                      terms.end());
}

QuantAttributes& QuantifiersRegistry::getQuantAttributes()
{
  return d_quantAttr;
}

QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
{
  return d_quantBoundInf;
}

Node QuantifiersRegistry::getNameForQuant(Node q) const
{
  Node name = d_quantAttr.getQuantName(q);
  if (!name.isNull())
  {
    return name;
  }
  return q;
}

bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
{
  name = getNameForQuant(q);
  // if we have a name, or we did not require one
  return name != q || !req;
}

}  // 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
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		* The quantifiers registry.
14		*/
15
16		#include "theory/quantifiers/quantifiers_registry.h"
17
18		#include "options/quantifiers_options.h"
19		#include "theory/quantifiers/quant_module.h"
20		#include "theory/quantifiers/term_util.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace quantifiers {
25
26	9853	QuantifiersRegistry::QuantifiersRegistry()
27		: d_quantAttr(),
28	9853	d_quantBoundInf(options::fmfTypeCompletionThresh(),
29	19706	options::finiteModelFind())
30		{
31	9853	}
32
33	76230	void QuantifiersRegistry::registerQuantifier(Node q)
34		{
35	76230	if (d_inst_constants.find(q) != d_inst_constants.end())
36		{
37	51251	return;
38		}
39	24979	NodeManager* nm = NodeManager::currentNM();
40	49958	Debug("quantifiers-engine")
41	24979	<< "Instantiation constants for " << q << " : " << std::endl;
42	83655	for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
43		{
44	58676	d_vars[q].push_back(q[0][i]);
45		// make instantiation constants
46	117352	Node ic = nm->mkInstConstant(q[0][i].getType());
47	58676	d_inst_constants_map[ic] = q;
48	58676	d_inst_constants[q].push_back(ic);
49	58676	Debug("quantifiers-engine") << " " << ic << std::endl;
50		// set the var number attribute
51		InstVarNumAttribute ivna;
52	58676	ic.setAttribute(ivna, i);
53		InstConstantAttribute ica;
54	58676	ic.setAttribute(ica, q);
55		}
56		// compute attributes
57	24979	d_quantAttr.computeAttributes(q);
58		}
59
60	28528	bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }
61
62	28528	std::string QuantifiersRegistry::identify() const
63		{
64	28528	return "QuantifiersRegistry";
65		}
66
67	495154	QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
68		{
69	495154	std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
70	495154	if (it == d_owner.end())
71		{
72	440805	return nullptr;
73		}
74	54349	return it->second;
75		}
76
77	2901	void QuantifiersRegistry::setOwner(Node q,
78		QuantifiersModule* m,
79		int32_t priority)
80		{
81	2901	QuantifiersModule* mo = getOwner(q);
82	2901	if (mo == m)
83		{
84		return;
85		}
86	2901	if (mo != nullptr)
87		{
88		if (priority <= d_owner_priority[q])
89		{
90		Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
91		<< (m ? m->identify() : "null")
92		<< ", but already has owner " << mo->identify()
93		<< " with higher priority!" << std::endl;
94		return;
95		}
96		}
97	2901	d_owner[q] = m;
98	2901	d_owner_priority[q] = priority;
99		}
100
101	439735	bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
102		{
103	439735	QuantifiersModule* mo = getOwner(q);
104	439735	return mo == m \|\| mo == nullptr;
105		}
106
107	62311	Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
108		{
109		std::map<Node, std::vector<Node> >::const_iterator it =
110	62311	d_inst_constants.find(q);
111	62311	if (it != d_inst_constants.end())
112		{
113	62311	return it->second[i];
114		}
115		return Node::null();
116		}
117
118	26581	size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
119		{
120		std::map<Node, std::vector<Node> >::const_iterator it =
121	26581	d_inst_constants.find(q);
122	26581	if (it != d_inst_constants.end())
123		{
124	26581	return it->second.size();
125		}
126		return 0;
127		}
128
129	159720	Node QuantifiersRegistry::getInstConstantBody(Node q)
130		{
131	159720	std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
132	159720	if (it == d_inst_const_body.end())
133		{
134	46510	Node n = substituteBoundVariablesToInstConstants(q[1], q);
135	23255	d_inst_const_body[q] = n;
136	23255	return n;
137		}
138	136465	return it->second;
139		}
140
141	32894	Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
142		Node q)
143		{
144	32894	registerQuantifier(q);
145	32894	return n.substitute(d_vars[q].begin(),
146	32894	d_vars[q].end(),
147	32894	d_inst_constants[q].begin(),
148	131576	d_inst_constants[q].end());
149		}
150
151	18351	Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
152		Node q)
153		{
154	18351	registerQuantifier(q);
155	18351	return n.substitute(d_inst_constants[q].begin(),
156	18351	d_inst_constants[q].end(),
157	18351	d_vars[q].begin(),
158	73404	d_vars[q].end());
159		}
160
161	16	Node QuantifiersRegistry::substituteBoundVariables(Node n,
162		Node q,
163		std::vector<Node>& terms)
164		{
165	16	registerQuantifier(q);
166	16	Assert(d_vars[q].size() == terms.size());
167		return n.substitute(
168	16	d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end());
169		}
170
171		Node QuantifiersRegistry::substituteInstConstants(Node n,
172		Node q,
173		std::vector<Node>& terms)
174		{
175		registerQuantifier(q);
176		Assert(d_inst_constants[q].size() == terms.size());
177		return n.substitute(d_inst_constants[q].begin(),
178		d_inst_constants[q].end(),
179		terms.begin(),
180		terms.end());
181		}
182
183	73340	QuantAttributes& QuantifiersRegistry::getQuantAttributes()
184		{
185	73340	return d_quantAttr;
186		}
187
188	27348	QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
189		{
190	27348	return d_quantBoundInf;
191		}
192
193	34	Node QuantifiersRegistry::getNameForQuant(Node q) const
194		{
195	68	Node name = d_quantAttr.getQuantName(q);
196	34	if (!name.isNull())
197		{
198	10	return name;
199		}
200	24	return q;
201		}
202
203	34	bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
204		{
205	34	name = getNameForQuant(q);
206		// if we have a name, or we did not require one
207	34	return name != q \|\| !req;
208		}
209
210		} // namespace quantifiers
211		} // namespace theory
212	29340	} // namespace cvc5