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 : 51329 : QuantifiersRegistry::QuantifiersRegistry(Env& env)
24 : : : QuantifiersUtil(env),
25 : 51329 : d_quantAttr(userContext()),
26 : 51329 : d_quantBoundInf(options().quantifiers.fmfTypeCompletionThresh,
27 : 51329 : options().quantifiers.finiteModelFind),
28 : 102658 : d_quantPreproc(env)
29 : : {
30 : 51329 : }
31 : :
32 : 162972 : void QuantifiersRegistry::registerQuantifier(Node q)
33 : : {
34 [ + + ]: 162972 : if (d_inst_constants.find(q) != d_inst_constants.end())
35 : : {
36 : 109076 : return;
37 : : }
38 [ - + ][ - + ]: 53896 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
39 : 53896 : NodeManager* nm = nodeManager();
40 [ + - ]: 107792 : Trace("quantifiers-engine")
41 : 53896 : << "Instantiation constants for " << q << " : " << std::endl;
42 [ + + ]: 172345 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
43 : : {
44 : 118449 : d_vars[q].push_back(q[0][i]);
45 : : // make instantiation constants
46 : 236898 : Node ic = nm->mkInstConstant(q[0][i].getType());
47 : 118449 : d_inst_constants_map[ic] = q;
48 : 118449 : d_inst_constants[q].push_back(ic);
49 [ + - ]: 118449 : Trace("quantifiers-engine") << " " << ic << std::endl;
50 : : // set the var number attribute
51 : : InstVarNumAttribute ivna;
52 : 118449 : ic.setAttribute(ivna, i);
53 : : InstConstantAttribute ica;
54 : 118449 : ic.setAttribute(ica, q);
55 : 118449 : }
56 : : // compute attributes
57 : 53896 : d_quantAttr.computeAttributes(q);
58 : : }
59 : :
60 : 71241 : 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 : 952290 : QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
68 : : {
69 : 952290 : std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
70 [ + + ]: 952290 : if (it == d_owner.end())
71 : : {
72 : 871930 : return nullptr;
73 : : }
74 : 80360 : return it->second;
75 : : }
76 : :
77 : 5407 : void QuantifiersRegistry::setOwner(Node q,
78 : : QuantifiersModule* m,
79 : : int32_t priority)
80 : : {
81 : 5407 : QuantifiersModule* mo = getOwner(q);
82 [ - + ]: 5407 : if (mo == m)
83 : : {
84 : 0 : return;
85 : : }
86 [ + + ]: 5407 : 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 : 5400 : d_owner[q] = m;
98 : 5400 : d_owner_priority[q] = priority;
99 : : }
100 : :
101 : 826983 : bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
102 : : {
103 : 826983 : QuantifiersModule* mo = getOwner(q);
104 [ + + ][ + + ]: 826983 : return mo == m || mo == nullptr;
105 : : }
106 : :
107 : 128984 : Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
108 : : {
109 : : std::map<Node, std::vector<Node> >::const_iterator it =
110 : 128984 : d_inst_constants.find(q);
111 [ + - ]: 128984 : if (it != d_inst_constants.end())
112 : : {
113 : 128984 : return it->second[i];
114 : : }
115 : 0 : return Node::null();
116 : : }
117 : :
118 : 57429 : size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
119 : : {
120 : : std::map<Node, std::vector<Node> >::const_iterator it =
121 : 57429 : d_inst_constants.find(q);
122 [ + - ]: 57429 : if (it != d_inst_constants.end())
123 : : {
124 : 57429 : return it->second.size();
125 : : }
126 : 0 : return 0;
127 : : }
128 : :
129 : 135271 : Node QuantifiersRegistry::getInstConstantBody(Node q)
130 : : {
131 : 135271 : std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
132 [ + + ]: 135271 : if (it == d_inst_const_body.end())
133 : : {
134 : 99344 : Node n = substituteBoundVariablesToInstConstants(q[1], q);
135 : 49672 : d_inst_const_body[q] = n;
136 : 49672 : return n;
137 : 49672 : }
138 : 85599 : return it->second;
139 : : }
140 : :
141 : 68350 : Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
142 : : Node q)
143 : : {
144 : 68350 : registerQuantifier(q);
145 : 68350 : std::vector<Node>& vars = d_vars.at(q);
146 : 68350 : std::vector<Node>& consts = d_inst_constants.at(q);
147 [ - + ][ - + ]: 68350 : Assert(vars.size() == q[0].getNumChildren());
[ - - ]
148 [ - + ][ - + ]: 68350 : Assert(vars.size() == consts.size());
[ - - ]
149 : 68350 : return n.substitute(vars.begin(), vars.end(), consts.begin(), consts.end());
150 : : }
151 : :
152 : 40743 : Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
153 : : Node q)
154 : : {
155 : 40743 : registerQuantifier(q);
156 : 40743 : std::vector<Node>& vars = d_vars.at(q);
157 : 40743 : std::vector<Node>& consts = d_inst_constants.at(q);
158 [ - + ][ - + ]: 40743 : Assert(vars.size() == q[0].getNumChildren());
[ - - ]
159 [ - + ][ - + ]: 40743 : Assert(vars.size() == consts.size());
[ - - ]
160 : 40743 : 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 : 231689 : QuantAttributes& QuantifiersRegistry::getQuantAttributes()
184 : : {
185 : 231689 : return d_quantAttr;
186 : : }
187 : :
188 : 86095 : QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
189 : : {
190 : 86095 : return d_quantBoundInf;
191 : : }
192 : 107649 : QuantifiersPreprocess& QuantifiersRegistry::getPreprocess()
193 : : {
194 : 107649 : 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
|
