Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_registry.cpp	Lines:	89	98	90.8 %
Date:	2021-09-29	Branches:	99	218	45.4 %


/******************************************************************************
 * 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(Env& env)
    : QuantifiersUtil(env),
      d_quantAttr(),
      d_quantBoundInf(options::fmfTypeCompletionThresh(),
                      options::finiteModelFind()),
      d_quantPreproc(env)
{
}

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;
}
QuantifiersPreprocess& QuantifiersRegistry::getPreprocess()
{
  return d_quantPreproc;
}

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	6271	QuantifiersRegistry::QuantifiersRegistry(Env& env)
27		: QuantifiersUtil(env),
28		d_quantAttr(),
29	6271	d_quantBoundInf(options::fmfTypeCompletionThresh(),
30	6271	options::finiteModelFind()),
31	18813	d_quantPreproc(env)
32		{
33	6271	}
34
35	30539	void QuantifiersRegistry::registerQuantifier(Node q)
36		{
37	30539	if (d_inst_constants.find(q) != d_inst_constants.end())
38		{
39	20015	return;
40		}
41	10524	NodeManager* nm = NodeManager::currentNM();
42	21048	Debug("quantifiers-engine")
43	10524	<< "Instantiation constants for " << q << " : " << std::endl;
44	34292	for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
45		{
46	23768	d_vars[q].push_back(q[0][i]);
47		// make instantiation constants
48	47536	Node ic = nm->mkInstConstant(q[0][i].getType());
49	23768	d_inst_constants_map[ic] = q;
50	23768	d_inst_constants[q].push_back(ic);
51	23768	Debug("quantifiers-engine") << " " << ic << std::endl;
52		// set the var number attribute
53		InstVarNumAttribute ivna;
54	23768	ic.setAttribute(ivna, i);
55		InstConstantAttribute ica;
56	23768	ic.setAttribute(ica, q);
57		}
58		// compute attributes
59	10524	d_quantAttr.computeAttributes(q);
60		}
61
62	19493	bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }
63
64	19493	std::string QuantifiersRegistry::identify() const
65		{
66	19493	return "QuantifiersRegistry";
67		}
68
69	235853	QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
70		{
71	235853	std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
72	235853	if (it == d_owner.end())
73		{
74	208035	return nullptr;
75		}
76	27818	return it->second;
77		}
78
79	1797	void QuantifiersRegistry::setOwner(Node q,
80		QuantifiersModule* m,
81		int32_t priority)
82		{
83	1797	QuantifiersModule* mo = getOwner(q);
84	1797	if (mo == m)
85		{
86		return;
87		}
88	1797	if (mo != nullptr)
89		{
90	1	if (priority <= d_owner_priority[q])
91		{
92	2	Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
93	2	<< (m ? m->identify() : "null")
94	2	<< ", but already has owner " << mo->identify()
95	1	<< " with higher priority!" << std::endl;
96	1	return;
97		}
98		}
99	1796	d_owner[q] = m;
100	1796	d_owner_priority[q] = priority;
101		}
102
103	210613	bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
104		{
105	210613	QuantifiersModule* mo = getOwner(q);
106	210613	return mo == m \|\| mo == nullptr;
107		}
108
109	25997	Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
110		{
111		std::map<Node, std::vector<Node> >::const_iterator it =
112	25997	d_inst_constants.find(q);
113	25997	if (it != d_inst_constants.end())
114		{
115	25997	return it->second[i];
116		}
117		return Node::null();
118		}
119
120	11642	size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
121		{
122		std::map<Node, std::vector<Node> >::const_iterator it =
123	11642	d_inst_constants.find(q);
124	11642	if (it != d_inst_constants.end())
125		{
126	11642	return it->second.size();
127		}
128		return 0;
129		}
130
131	44420	Node QuantifiersRegistry::getInstConstantBody(Node q)
132		{
133	44420	std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
134	44420	if (it == d_inst_const_body.end())
135		{
136	19596	Node n = substituteBoundVariablesToInstConstants(q[1], q);
137	9798	d_inst_const_body[q] = n;
138	9798	return n;
139		}
140	34622	return it->second;
141		}
142
143	13273	Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
144		Node q)
145		{
146	13273	registerQuantifier(q);
147	13273	return n.substitute(d_vars[q].begin(),
148	13273	d_vars[q].end(),
149	13273	d_inst_constants[q].begin(),
150	53092	d_inst_constants[q].end());
151		}
152
153	6746	Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
154		Node q)
155		{
156	6746	registerQuantifier(q);
157	6746	return n.substitute(d_inst_constants[q].begin(),
158	6746	d_inst_constants[q].end(),
159	6746	d_vars[q].begin(),
160	26984	d_vars[q].end());
161		}
162
163	4	Node QuantifiersRegistry::substituteBoundVariables(Node n,
164		Node q,
165		std::vector<Node>& terms)
166		{
167	4	registerQuantifier(q);
168	4	Assert(d_vars[q].size() == terms.size());
169		return n.substitute(
170	4	d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end());
171		}
172
173		Node QuantifiersRegistry::substituteInstConstants(Node n,
174		Node q,
175		std::vector<Node>& terms)
176		{
177		registerQuantifier(q);
178		Assert(d_inst_constants[q].size() == terms.size());
179		return n.substitute(d_inst_constants[q].begin(),
180		d_inst_constants[q].end(),
181		terms.begin(),
182		terms.end());
183		}
184
185	34203	QuantAttributes& QuantifiersRegistry::getQuantAttributes()
186		{
187	34203	return d_quantAttr;
188		}
189
190	19321	QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
191		{
192	19321	return d_quantBoundInf;
193		}
194	17613	QuantifiersPreprocess& QuantifiersRegistry::getPreprocess()
195		{
196	17613	return d_quantPreproc;
197		}
198
199	12	Node QuantifiersRegistry::getNameForQuant(Node q) const
200		{
201	24	Node name = d_quantAttr.getQuantName(q);
202	12	if (!name.isNull())
203		{
204	4	return name;
205		}
206	8	return q;
207		}
208
209	12	bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
210		{
211	12	name = getNameForQuant(q);
212		// if we have a name, or we did not require one
213	12	return name != q \|\| !req;
214		}
215
216		} // namespace quantifiers
217		} // namespace theory
218	22746	} // namespace cvc5