Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_registry.cpp	Lines:	94	103	91.3 %
Date:	2021-11-07	Branches:	114	338	33.7 %


/******************************************************************************
 * 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;
  }
  Assert(q.getKind() == kind::FORALL);
  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);
  std::vector<Node>& vars = d_vars.at(q);
  std::vector<Node>& consts = d_inst_constants.at(q);
  Assert(vars.size() == q[0].getNumChildren());
  Assert(vars.size() == consts.size());
  return n.substitute(vars.begin(), vars.end(), consts.begin(), consts.end());
}

Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
                                                                  Node q)
{
  registerQuantifier(q);
  std::vector<Node>& vars = d_vars.at(q);
  std::vector<Node>& consts = d_inst_constants.at(q);
  Assert(vars.size() == q[0].getNumChildren());
  Assert(vars.size() == consts.size());
  return n.substitute(consts.begin(), consts.end(), vars.begin(), vars.end());
}

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

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