Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The quantifiers registry.
11 : : */
12 : :
13 : : #include "theory/quantifiers/quantifiers_registry.h"
14 : :
15 : : #include "options/quantifiers_options.h"
16 : : #include "theory/quantifiers/quant_module.h"
17 : : #include "theory/quantifiers/term_util.h"
18 : :
19 : : namespace cvc5::internal {
20 : : namespace theory {
21 : : namespace quantifiers {
22 : :
23 : 51004 : QuantifiersRegistry::QuantifiersRegistry(Env& env)
24 : : : QuantifiersUtil(env),
25 : 51004 : d_quantAttr(),
26 : 51004 : d_quantBoundInf(options().quantifiers.fmfTypeCompletionThresh,
27 : 51004 : options().quantifiers.finiteModelFind),
28 : 102008 : d_quantPreproc(env)
29 : : {
30 : 51004 : }
31 : :
32 : 162472 : void QuantifiersRegistry::registerQuantifier(Node q)
33 : : {
34 [ + + ]: 162472 : if (d_inst_constants.find(q) != d_inst_constants.end())
35 : : {
36 : 108761 : return;
37 : : }
38 [ - + ][ - + ]: 53711 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
39 : 53711 : NodeManager* nm = nodeManager();
40 [ + - ]: 107422 : Trace("quantifiers-engine")
41 : 53711 : << "Instantiation constants for " << q << " : " << std::endl;
42 [ + + ]: 171674 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
43 : : {
44 : 117963 : d_vars[q].push_back(q[0][i]);
45 : : // make instantiation constants
46 : 235926 : Node ic = nm->mkInstConstant(q[0][i].getType());
47 : 117963 : d_inst_constants_map[ic] = q;
48 : 117963 : d_inst_constants[q].push_back(ic);
49 [ + - ]: 117963 : Trace("quantifiers-engine") << " " << ic << std::endl;
50 : : // set the var number attribute
51 : : InstVarNumAttribute ivna;
52 : 117963 : ic.setAttribute(ivna, i);
53 : : InstConstantAttribute ica;
54 : 117963 : ic.setAttribute(ica, q);
55 : 117963 : }
56 : : // compute attributes
57 : 53711 : d_quantAttr.computeAttributes(q);
58 : : }
59 : :
60 : 68681 : bool QuantifiersRegistry::reset(CVC5_UNUSED Theory::Effort e) { return true; }
61 : :
62 : 0 : std::string QuantifiersRegistry::identify() const
63 : : {
64 : 0 : return "QuantifiersRegistry";
65 : : }
66 : :
67 : 941771 : QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
68 : : {
69 : 941771 : std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
70 [ + + ]: 941771 : if (it == d_owner.end())
71 : : {
72 : 863331 : return nullptr;
73 : : }
74 : 78440 : return it->second;
75 : : }
76 : :
77 : 5396 : void QuantifiersRegistry::setOwner(Node q,
78 : : QuantifiersModule* m,
79 : : int32_t priority)
80 : : {
81 : 5396 : QuantifiersModule* mo = getOwner(q);
82 [ - + ]: 5396 : if (mo == m)
83 : : {
84 : 0 : return;
85 : : }
86 [ + + ]: 5396 : if (mo != nullptr)
87 : : {
88 [ + + ]: 12 : if (priority <= d_owner_priority[q])
89 : : {
90 [ + - ]: 14 : Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
91 : 7 : << (m ? m->identify() : "null")
92 [ - + ][ - + ]: 7 : << ", but already has owner " << mo->identify()
[ - - ]
93 : 7 : << " with higher priority!" << std::endl;
94 : 7 : return;
95 : : }
96 : : }
97 : 5389 : d_owner[q] = m;
98 : 5389 : d_owner_priority[q] = priority;
99 : : }
100 : :
101 : 817654 : bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
102 : : {
103 : 817654 : QuantifiersModule* mo = getOwner(q);
104 [ + + ][ + + ]: 817654 : return mo == m || mo == nullptr;
105 : : }
106 : :
107 : 128533 : Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
108 : : {
109 : : std::map<Node, std::vector<Node> >::const_iterator it =
110 : 128533 : d_inst_constants.find(q);
111 [ + - ]: 128533 : if (it != d_inst_constants.end())
112 : : {
113 : 128533 : return it->second[i];
114 : : }
115 : 0 : return Node::null();
116 : : }
117 : :
118 : 57236 : size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
119 : : {
120 : : std::map<Node, std::vector<Node> >::const_iterator it =
121 : 57236 : d_inst_constants.find(q);
122 [ + - ]: 57236 : if (it != d_inst_constants.end())
123 : : {
124 : 57236 : return it->second.size();
125 : : }
126 : 0 : return 0;
127 : : }
128 : :
129 : 134727 : Node QuantifiersRegistry::getInstConstantBody(Node q)
130 : : {
131 : 134727 : std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
132 [ + + ]: 134727 : if (it == d_inst_const_body.end())
133 : : {
134 : 98996 : Node n = substituteBoundVariablesToInstConstants(q[1], q);
135 : 49498 : d_inst_const_body[q] = n;
136 : 49498 : return n;
137 : 49498 : }
138 : 85229 : return it->second;
139 : : }
140 : :
141 : 68140 : Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
142 : : Node q)
143 : : {
144 : 68140 : registerQuantifier(q);
145 : 68140 : std::vector<Node>& vars = d_vars.at(q);
146 : 68140 : std::vector<Node>& consts = d_inst_constants.at(q);
147 [ - + ][ - + ]: 68140 : Assert(vars.size() == q[0].getNumChildren());
[ - - ]
148 [ - + ][ - + ]: 68140 : Assert(vars.size() == consts.size());
[ - - ]
149 : 68140 : return n.substitute(vars.begin(), vars.end(), consts.begin(), consts.end());
150 : : }
151 : :
152 : 40638 : Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
153 : : Node q)
154 : : {
155 : 40638 : registerQuantifier(q);
156 : 40638 : std::vector<Node>& vars = d_vars.at(q);
157 : 40638 : std::vector<Node>& consts = d_inst_constants.at(q);
158 [ - + ][ - + ]: 40638 : Assert(vars.size() == q[0].getNumChildren());
[ - - ]
159 [ - + ][ - + ]: 40638 : Assert(vars.size() == consts.size());
[ - - ]
160 : 40638 : return n.substitute(consts.begin(), consts.end(), vars.begin(), vars.end());
161 : : }
162 : :
163 : 0 : Node QuantifiersRegistry::substituteBoundVariables(
164 : : Node n, Node q, const std::vector<Node>& terms)
165 : : {
166 : 0 : registerQuantifier(q);
167 : 0 : std::vector<Node>& vars = d_vars.at(q);
168 : 0 : Assert(vars.size() == q[0].getNumChildren());
169 : 0 : Assert(vars.size() == terms.size());
170 : 0 : return n.substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
171 : : }
172 : :
173 : 0 : Node QuantifiersRegistry::substituteInstConstants(
174 : : Node n, Node q, const std::vector<Node>& terms)
175 : : {
176 : 0 : registerQuantifier(q);
177 : 0 : std::vector<Node>& consts = d_inst_constants.at(q);
178 : 0 : Assert(consts.size() == q[0].getNumChildren());
179 : 0 : Assert(consts.size() == terms.size());
180 : 0 : return n.substitute(consts.begin(), consts.end(), terms.begin(), terms.end());
181 : : }
182 : :
183 : 228499 : QuantAttributes& QuantifiersRegistry::getQuantAttributes()
184 : : {
185 : 228499 : return d_quantAttr;
186 : : }
187 : :
188 : 85398 : QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
189 : : {
190 : 85398 : return d_quantBoundInf;
191 : : }
192 : 174601 : QuantifiersPreprocess& QuantifiersRegistry::getPreprocess()
193 : : {
194 : 174601 : return d_quantPreproc;
195 : : }
196 : :
197 : 95 : Node QuantifiersRegistry::getNameForQuant(Node q) const
198 : : {
199 : 95 : Node name = d_quantAttr.getQuantName(q);
200 [ + + ]: 95 : if (!name.isNull())
201 : : {
202 : 10 : return name;
203 : : }
204 : 85 : return q;
205 : 95 : }
206 : :
207 : 95 : bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
208 : : {
209 : 95 : name = getNameForQuant(q);
210 : : // if we have a name, or we did not require one
211 [ + + ][ + - ]: 95 : return name != q || !req;
212 : : }
213 : :
214 : : } // namespace quantifiers
215 : : } // namespace theory
216 : : } // namespace cvc5::internal
|
