Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Morgan Deters
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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::internal {
23 : : namespace theory {
24 : : namespace quantifiers {
25 : :
26 : 50019 : QuantifiersRegistry::QuantifiersRegistry(Env& env)
27 : : : QuantifiersUtil(env),
28 : : d_quantAttr(),
29 : 100038 : d_quantBoundInf(options().quantifiers.fmfTypeCompletionThresh,
30 : 100038 : options().quantifiers.finiteModelFind),
31 : 50019 : d_quantPreproc(env)
32 : : {
33 : 50019 : }
34 : :
35 : 176162 : void QuantifiersRegistry::registerQuantifier(Node q)
36 : : {
37 [ + + ]: 176162 : if (d_inst_constants.find(q) != d_inst_constants.end())
38 : : {
39 : 118255 : return;
40 : : }
41 [ - + ][ - + ]: 57907 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
42 : 57907 : NodeManager* nm = nodeManager();
43 [ + - ]: 115814 : Trace("quantifiers-engine")
44 : 57907 : << "Instantiation constants for " << q << " : " << std::endl;
45 [ + + ]: 187263 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
46 : : {
47 : 129356 : d_vars[q].push_back(q[0][i]);
48 : : // make instantiation constants
49 : 388068 : Node ic = nm->mkInstConstant(q[0][i].getType());
50 : 129356 : d_inst_constants_map[ic] = q;
51 : 129356 : d_inst_constants[q].push_back(ic);
52 [ + - ]: 129356 : Trace("quantifiers-engine") << " " << ic << std::endl;
53 : : // set the var number attribute
54 : : InstVarNumAttribute ivna;
55 : 129356 : ic.setAttribute(ivna, i);
56 : : InstConstantAttribute ica;
57 : 129356 : ic.setAttribute(ica, q);
58 : : }
59 : : // compute attributes
60 : 57907 : d_quantAttr.computeAttributes(q);
61 : : }
62 : :
63 : 58243 : bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }
64 : :
65 : 0 : std::string QuantifiersRegistry::identify() const
66 : : {
67 : 0 : return "QuantifiersRegistry";
68 : : }
69 : :
70 : 973393 : QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
71 : : {
72 : 973393 : std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
73 [ + + ]: 973393 : if (it == d_owner.end())
74 : : {
75 : 898033 : return nullptr;
76 : : }
77 : 75360 : return it->second;
78 : : }
79 : :
80 : 5478 : void QuantifiersRegistry::setOwner(Node q,
81 : : QuantifiersModule* m,
82 : : int32_t priority)
83 : : {
84 : 5478 : QuantifiersModule* mo = getOwner(q);
85 [ - + ]: 5478 : if (mo == m)
86 : : {
87 : 0 : return;
88 : : }
89 [ + + ]: 5478 : if (mo != nullptr)
90 : : {
91 [ + + ]: 14 : if (priority <= d_owner_priority[q])
92 : : {
93 [ + - ]: 16 : Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
94 : 8 : << (m ? m->identify() : "null")
95 [ - + ][ - + ]: 8 : << ", but already has owner " << mo->identify()
[ - - ]
96 : 8 : << " with higher priority!" << std::endl;
97 : 8 : return;
98 : : }
99 : : }
100 : 5470 : d_owner[q] = m;
101 : 5470 : d_owner_priority[q] = priority;
102 : : }
103 : :
104 : 840275 : bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
105 : : {
106 : 840275 : QuantifiersModule* mo = getOwner(q);
107 [ + + ][ + + ]: 840275 : return mo == m || mo == nullptr;
108 : : }
109 : :
110 : 139975 : Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
111 : : {
112 : : std::map<Node, std::vector<Node> >::const_iterator it =
113 : 139975 : d_inst_constants.find(q);
114 [ + - ]: 139975 : if (it != d_inst_constants.end())
115 : : {
116 : 139975 : return it->second[i];
117 : : }
118 : 0 : return Node::null();
119 : : }
120 : :
121 : 61168 : size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
122 : : {
123 : : std::map<Node, std::vector<Node> >::const_iterator it =
124 : 61168 : d_inst_constants.find(q);
125 [ + - ]: 61168 : if (it != d_inst_constants.end())
126 : : {
127 : 61168 : return it->second.size();
128 : : }
129 : 0 : return 0;
130 : : }
131 : :
132 : 137058 : Node QuantifiersRegistry::getInstConstantBody(Node q)
133 : : {
134 : 137058 : std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
135 [ + + ]: 137058 : if (it == d_inst_const_body.end())
136 : : {
137 : 161679 : Node n = substituteBoundVariablesToInstConstants(q[1], q);
138 : 53893 : d_inst_const_body[q] = n;
139 : 53893 : return n;
140 : : }
141 : 83165 : return it->second;
142 : : }
143 : :
144 : 73870 : Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
145 : : Node q)
146 : : {
147 : 73870 : registerQuantifier(q);
148 : 73870 : std::vector<Node>& vars = d_vars.at(q);
149 : 73870 : std::vector<Node>& consts = d_inst_constants.at(q);
150 [ - + ][ - + ]: 73870 : Assert(vars.size() == q[0].getNumChildren());
[ - - ]
151 [ - + ][ - + ]: 73870 : Assert(vars.size() == consts.size());
[ - - ]
152 : 73870 : return n.substitute(vars.begin(), vars.end(), consts.begin(), consts.end());
153 : : }
154 : :
155 : 44404 : Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
156 : : Node q)
157 : : {
158 : 44404 : registerQuantifier(q);
159 : 44404 : std::vector<Node>& vars = d_vars.at(q);
160 : 44404 : std::vector<Node>& consts = d_inst_constants.at(q);
161 [ - + ][ - + ]: 44404 : Assert(vars.size() == q[0].getNumChildren());
[ - - ]
162 [ - + ][ - + ]: 44404 : Assert(vars.size() == consts.size());
[ - - ]
163 : 44404 : return n.substitute(consts.begin(), consts.end(), vars.begin(), vars.end());
164 : : }
165 : :
166 : 0 : Node QuantifiersRegistry::substituteBoundVariables(
167 : : Node n, Node q, const std::vector<Node>& terms)
168 : : {
169 : 0 : registerQuantifier(q);
170 : 0 : std::vector<Node>& vars = d_vars.at(q);
171 : 0 : Assert(vars.size() == q[0].getNumChildren());
172 : 0 : Assert(vars.size() == terms.size());
173 : 0 : return n.substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
174 : : }
175 : :
176 : 0 : Node QuantifiersRegistry::substituteInstConstants(
177 : : Node n, Node q, const std::vector<Node>& terms)
178 : : {
179 : 0 : registerQuantifier(q);
180 : 0 : std::vector<Node>& consts = d_inst_constants.at(q);
181 : 0 : Assert(consts.size() == q[0].getNumChildren());
182 : 0 : Assert(consts.size() == terms.size());
183 : 0 : return n.substitute(consts.begin(), consts.end(), terms.begin(), terms.end());
184 : : }
185 : :
186 : 250797 : QuantAttributes& QuantifiersRegistry::getQuantAttributes()
187 : : {
188 : 250797 : return d_quantAttr;
189 : : }
190 : :
191 : 84504 : QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
192 : : {
193 : 84504 : return d_quantBoundInf;
194 : : }
195 : 82258 : QuantifiersPreprocess& QuantifiersRegistry::getPreprocess()
196 : : {
197 : 82258 : return d_quantPreproc;
198 : : }
199 : :
200 : 95 : Node QuantifiersRegistry::getNameForQuant(Node q) const
201 : : {
202 : 190 : Node name = d_quantAttr.getQuantName(q);
203 [ + + ]: 95 : if (!name.isNull())
204 : : {
205 : 14 : return name;
206 : : }
207 : 81 : return q;
208 : : }
209 : :
210 : 95 : bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
211 : : {
212 : 95 : name = getNameForQuant(q);
213 : : // if we have a name, or we did not require one
214 [ + + ][ + - ]: 95 : return name != q || !req;
215 : : }
216 : :
217 : : } // namespace quantifiers
218 : : } // namespace theory
219 : : } // namespace cvc5::internal
|
