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 : : * Implementation of QuantifiersAttributes class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/quantifiers_attributes.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "options/quantifiers_options.h"
17 : : #include "smt/print_benchmark.h"
18 : : #include "theory/arith/arith_msum.h"
19 : : #include "theory/quantifiers/fmf/bounded_integers.h"
20 : : #include "theory/quantifiers/sygus/synth_engine.h"
21 : : #include "theory/quantifiers/term_util.h"
22 : : #include "util/rational.h"
23 : : #include "util/string.h"
24 : :
25 : : using namespace std;
26 : : using namespace cvc5::internal::kind;
27 : : using namespace cvc5::context;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace quantifiers {
32 : :
33 : : /**
34 : : * Mapping from terms to their "instantiation level", for details see
35 : : * QuantAttributes::getInstantiationLevel.
36 : : */
37 : : struct InstLevelAttributeId
38 : : {
39 : : };
40 : : using InstLevelAttribute = expr::Attribute<InstLevelAttributeId, uint64_t>;
41 : :
42 : : /** Attribute true for quantifiers we are doing quantifier elimination on */
43 : : struct QuantElimAttributeId
44 : : {
45 : : };
46 : : using QuantElimAttribute = expr::Attribute<QuantElimAttributeId, bool>;
47 : :
48 : : /** Attribute true for quantifiers we which to preserve structure for, including
49 : : * those that we are doing quantifier elimination on */
50 : : struct PreserveStructureAttributeId
51 : : {
52 : : };
53 : : using PreserveStructureAttribute =
54 : : expr::Attribute<PreserveStructureAttributeId, bool>;
55 : :
56 : 4220924 : bool QAttributes::isStandard() const
57 : : {
58 [ + + ][ + + ]: 4161410 : return !d_sygus && !d_preserveStructure && !isFunDef() && !isOracleInterface()
[ + + ]
59 [ + + ][ + + ]: 8382334 : && !d_isQuantBounded && !d_hasPool;
[ + + ]
60 : : }
61 : :
62 : 49952 : QuantAttributes::QuantAttributes() {}
63 : :
64 : 2622 : void QuantAttributes::setUserAttribute(const std::string& attr,
65 : : TNode n,
66 : : const std::vector<Node>& nodeValues)
67 : : {
68 [ + - ]: 2622 : Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
69 [ - + ]: 2622 : if (attr == "fun-def")
70 : : {
71 [ - - ]: 0 : Trace("quant-attr-debug") << "Set function definition " << n << std::endl;
72 : : FunDefAttribute fda;
73 : 0 : n.setAttribute( fda, true );
74 : : }
75 [ + + ]: 2622 : else if (attr == "qid")
76 : : {
77 : : // using z3 syntax "qid"
78 [ + - ]: 2363 : Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
79 : : QuantNameAttribute qna;
80 : 2363 : n.setAttribute(qna, true);
81 [ - + ]: 259 : }else if( attr=="quant-inst-max-level" ){
82 : 0 : Assert(nodeValues.size() == 1);
83 : 0 : uint64_t lvl = nodeValues[0].getConst<Rational>().getNumerator().getLong();
84 [ - - ]: 0 : Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
85 : : QuantInstLevelAttribute qila;
86 : 0 : n.setAttribute( qila, lvl );
87 [ + + ]: 259 : }else if( attr=="quant-elim" ){
88 [ + - ]: 254 : Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
89 : : QuantElimAttribute qea;
90 : 254 : n.setAttribute( qea, true );
91 [ + - ]: 5 : }else if( attr=="quant-elim-partial" ){
92 [ + - ]: 5 : Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl;
93 : : QuantElimPartialAttribute qepa;
94 : 5 : n.setAttribute( qepa, true );
95 : : }
96 : 2622 : }
97 : :
98 : 765 : Node QuantAttributes::getFunDefHead( Node q ) {
99 : : //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
100 [ + + ][ + + ]: 765 : if (q.getKind() == Kind::FORALL && q.getNumChildren() == 3)
[ + + ]
101 : : {
102 : 292 : Node ipl = q[2];
103 [ + + ]: 294 : for (unsigned i = 0; i < ipl.getNumChildren(); i++)
104 : : {
105 [ + + ][ - - ]: 292 : if (ipl[i].getKind() == Kind::INST_ATTRIBUTE
106 : 292 : && ipl[i][0].getAttribute(FunDefAttribute()))
107 : : {
108 : 290 : return ipl[i][0];
109 : : }
110 : : }
111 [ + + ]: 292 : }
112 : 475 : return Node::null();
113 : : }
114 : 145 : Node QuantAttributes::getFunDefBody( Node q ) {
115 : 145 : Node h = getFunDefHead( q );
116 [ + - ]: 145 : if( !h.isNull() ){
117 [ + + ]: 145 : if (q[1].getKind() == Kind::EQUAL)
118 : : {
119 [ + + ]: 143 : if( q[1][0]==h ){
120 : 117 : return q[1][1];
121 [ + + ]: 26 : }else if( q[1][1]==h ){
122 : 25 : return q[1][0];
123 : : }
124 [ + - ]: 1 : else if (q[1][0].getType().isRealOrInt())
125 : : {
126 : : // solve for h in the equality
127 : 1 : std::map<Node, Node> msum;
128 [ + - ]: 1 : if (ArithMSum::getMonomialSumLit(q[1], msum))
129 : : {
130 : 1 : Node veq;
131 : 1 : int res = ArithMSum::isolate(h, msum, veq, Kind::EQUAL);
132 [ + - ]: 1 : if (res != 0)
133 : : {
134 [ - + ][ - + ]: 1 : Assert(veq.getKind() == Kind::EQUAL);
[ - - ]
135 [ + - ]: 1 : return res == 1 ? veq[1] : veq[0];
136 : : }
137 [ - + ]: 1 : }
138 [ - + ]: 1 : }
139 : : }
140 : : else
141 : : {
142 [ + - ][ + - ]: 4 : Node atom = q[1].getKind() == Kind::NOT ? q[1][0] : q[1];
[ - - ]
143 : 2 : bool pol = q[1].getKind() != Kind::NOT;
144 [ + - ]: 2 : if( atom==h ){
145 : 2 : return q.getNodeManager()->mkConst(pol);
146 : : }
147 [ - + ]: 2 : }
148 : : }
149 : 0 : return Node::null();
150 : 145 : }
151 : :
152 : 11479 : bool QuantAttributes::checkSygusConjecture( Node q ) {
153 [ + + ]: 1668 : return (q.getKind() == Kind::FORALL && q.getNumChildren() == 3)
154 [ + + ][ + + ]: 24626 : ? checkSygusConjectureAnnotation(q[2])
[ - - ]
155 [ + + ]: 22958 : : false;
156 : : }
157 : :
158 : 1513 : bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){
159 [ + - ]: 1513 : if( !ipl.isNull() ){
160 [ + + ]: 1641 : for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
161 [ + - ]: 1513 : if (ipl[i].getKind() == Kind::INST_ATTRIBUTE)
162 : : {
163 : 1513 : Node avar = ipl[i][0];
164 [ + + ]: 1513 : if( avar.getAttribute(SygusAttribute()) ){
165 : 1385 : return true;
166 : : }
167 [ + + ]: 1513 : }
168 : : }
169 : : }
170 : 128 : return false;
171 : : }
172 : :
173 : 7661 : bool QuantAttributes::hasPattern(Node q)
174 : : {
175 [ - + ][ - + ]: 7661 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
176 [ + + ]: 7661 : if (q.getNumChildren() != 3)
177 : : {
178 : 7492 : return false;
179 : : }
180 [ + + ]: 227 : for (const Node& qc : q[2])
181 : : {
182 : 169 : if (qc.getKind() == Kind::INST_PATTERN
183 [ + + ][ - + ]: 169 : || qc.getKind() == Kind::INST_NO_PATTERN)
[ + + ]
184 : : {
185 : 111 : return true;
186 : : }
187 [ + + ][ + + ]: 338 : }
188 : 58 : return false;
189 : : }
190 : :
191 : 53205 : void QuantAttributes::computeAttributes( Node q ) {
192 : 53205 : computeQuantAttributes( q, d_qattr[q] );
193 : 53205 : QAttributes& qa = d_qattr[q];
194 [ + + ]: 53205 : if (qa.isFunDef())
195 : : {
196 : 1004 : Node f = qa.d_fundef_f;
197 [ - + ]: 1004 : if( d_fun_defs.find( f )!=d_fun_defs.end() ){
198 : 0 : AlwaysAssert(false) << "Cannot define function " << f
199 : 0 : << " more than once." << std::endl;
200 : : }
201 : 1004 : d_fun_defs[f] = true;
202 : 1004 : }
203 : 53205 : }
204 : :
205 : 559135 : void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
206 [ + - ]: 559135 : Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
207 [ + + ]: 559135 : if( q.getNumChildren()==3 ){
208 : 83762 : NodeManager* nm = q.getNodeManager();
209 : 83762 : qa.d_ipl = q[2];
210 [ + + ]: 174780 : for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
211 : 91018 : Kind k = q[2][i].getKind();
212 [ + - ]: 182036 : Trace("quant-attr-debug")
213 : 91018 : << "Check : " << q[2][i] << " " << k << std::endl;
214 [ + + ][ + + ]: 91018 : if (k == Kind::INST_PATTERN || k == Kind::INST_NO_PATTERN)
215 : : {
216 : 52966 : qa.d_hasPattern = true;
217 : : }
218 [ + + ][ + + ]: 38052 : else if (k == Kind::INST_POOL || k == Kind::INST_ADD_TO_POOL
219 [ + + ]: 37416 : || k == Kind::SKOLEM_ADD_TO_POOL)
220 : : {
221 : 758 : qa.d_hasPool = true;
222 : : }
223 [ + - ]: 37294 : else if (k == Kind::INST_ATTRIBUTE)
224 : : {
225 : 37294 : Node avar;
226 : : // We support two use cases of INST_ATTRIBUTE:
227 : : // (1) where the user constructs a term of the form
228 : : // (INST_ATTRIBUTE "keyword" [nodeValues])
229 : : // (2) where we internally generate nodes of the form
230 : : // (INST_ATTRIBUTE v) where v has an internal attribute set on it.
231 : : // We distinguish these two cases by checking the kind of the first
232 : : // child.
233 [ + + ]: 37294 : if (q[2][i][0].getKind() == Kind::CONST_STRING)
234 : : {
235 : : // make a dummy variable to be used below
236 : 2622 : avar = NodeManager::mkBoundVar(nm->booleanType());
237 : 2622 : std::vector<Node> nodeValues(q[2][i].begin() + 1, q[2][i].end());
238 : : // set user attribute on the dummy variable
239 : 5244 : setUserAttribute(
240 : 5244 : q[2][i][0].getConst<String>().toString(), avar, nodeValues);
241 : 2622 : }
242 : : else
243 : : {
244 : : // assume the dummy variable has already had its attributes set
245 : 34672 : avar = q[2][i][0];
246 : : }
247 [ + + ]: 37294 : if( avar.getAttribute(FunDefAttribute()) ){
248 [ + - ]: 7070 : Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
249 : : //get operator directly from pattern
250 : 7070 : qa.d_fundef_f = q[2][i][0].getOperator();
251 : : }
252 [ + + ]: 37294 : if( avar.getAttribute(SygusAttribute()) ){
253 : : //not necessarily nested existential
254 : : //Assert( q[1].getKind()==NOT );
255 : : //Assert( q[1][0].getKind()==FORALL );
256 [ + - ]: 11087 : Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
257 : 11087 : qa.d_sygus = true;
258 : : }
259 : : // oracles are specified by a distinguished variable kind
260 [ + + ]: 37294 : if (avar.getKind() == Kind::ORACLE)
261 : : {
262 : 2282 : qa.d_oracle = avar;
263 [ + - ]: 4564 : Trace("quant-attr")
264 : 2282 : << "Attribute : oracle interface : " << q << std::endl;
265 : : }
266 [ + + ]: 37294 : if (avar.hasAttribute(SygusSideConditionAttribute()))
267 : : {
268 : : qa.d_sygusSideCondition =
269 : 3535 : avar.getAttribute(SygusSideConditionAttribute());
270 [ + - ]: 7070 : Trace("quant-attr")
271 : 0 : << "Attribute : sygus side condition : "
272 : 3535 : << qa.d_sygusSideCondition << " : " << q << std::endl;
273 : : }
274 [ + + ]: 37294 : if (avar.getAttribute(QuantNameAttribute()))
275 : : {
276 : : // only set the name if there is a value
277 [ + - ]: 2363 : if (q[2][i].getNumChildren() > 1)
278 : : {
279 : 4726 : std::string name = q[2][i][1].getName();
280 : : // mark that this symbol should not be printed with the print
281 : : // benchmark utility
282 : 4726 : Node sym = q[2][i][1];
283 : 2363 : smt::PrintBenchmark::markNoPrint(sym);
284 [ + - ]: 4726 : Trace("quant-attr") << "Attribute : quantifier name : " << name
285 : 2363 : << " for " << q << std::endl;
286 : : // assign the name to a variable with the given name (to avoid
287 : : // enclosing the name in quotes)
288 : 2363 : qa.d_name = NodeManager::mkBoundVar(name, nm->booleanType());
289 : 2363 : }
290 : : else
291 : : {
292 [ - - ]: 0 : Warning() << "Missing name for qid attribute";
293 : : }
294 : : }
295 [ - + ]: 37294 : if( avar.hasAttribute(QuantInstLevelAttribute()) ){
296 : 0 : qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
297 [ - - ]: 0 : Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
298 : : }
299 [ + + ]: 37294 : if (avar.getAttribute(PreserveStructureAttribute()))
300 : : {
301 [ + - ]: 5632 : Trace("quant-attr")
302 : 2816 : << "Attribute : preserve structure : " << q << std::endl;
303 : 2816 : qa.d_preserveStructure = true;
304 : : }
305 [ + + ]: 37294 : if( avar.getAttribute(QuantElimAttribute()) ){
306 [ + - ]: 696 : Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
307 : 696 : qa.d_preserveStructure = true;
308 : 696 : qa.d_quant_elim = true;
309 : : //don't set owner, should happen naturally
310 : : }
311 [ + + ]: 37294 : if( avar.getAttribute(QuantElimPartialAttribute()) ){
312 [ + - ]: 5 : Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
313 : 5 : qa.d_preserveStructure = true;
314 : 5 : qa.d_quant_elim = true;
315 : 5 : qa.d_quant_elim_partial = true;
316 : : //don't set owner, should happen naturally
317 : : }
318 [ + + ]: 37294 : if (BoundedIntegers::isBoundedForallAttribute(avar))
319 : : {
320 [ + - ]: 13720 : Trace("quant-attr")
321 : 6860 : << "Attribute : bounded quantifiers : " << q << std::endl;
322 : 6860 : qa.d_isQuantBounded = true;
323 : : }
324 [ + + ]: 37294 : if( avar.hasAttribute(QuantIdNumAttribute()) ){
325 : 81 : qa.d_qid_num = avar;
326 [ + - ]: 81 : Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
327 : : }
328 : 37294 : }
329 : : }
330 : : }
331 : 559135 : }
332 : :
333 : 303 : bool QuantAttributes::isFunDef( Node q ) {
334 : 303 : std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
335 [ - + ]: 303 : if( it==d_qattr.end() ){
336 : 0 : return false;
337 : : }
338 : 303 : return it->second.isFunDef();
339 : : }
340 : :
341 : 4548 : bool QuantAttributes::isSygus( Node q ) {
342 : 4548 : std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
343 [ - + ]: 4548 : if( it==d_qattr.end() ){
344 : 0 : return false;
345 : : }
346 : 4548 : return it->second.d_sygus;
347 : : }
348 : :
349 : 652 : bool QuantAttributes::isOracleInterface(Node q)
350 : : {
351 : 652 : std::map<Node, QAttributes>::iterator it = d_qattr.find(q);
352 [ - + ]: 652 : if (it == d_qattr.end())
353 : : {
354 : 0 : return false;
355 : : }
356 : 652 : return it->second.isOracleInterface();
357 : : }
358 : :
359 : 1114 : int64_t QuantAttributes::getQuantInstLevel(Node q)
360 : : {
361 : 1114 : std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
362 [ - + ]: 1114 : if( it==d_qattr.end() ){
363 : 0 : return -1;
364 : : }else{
365 : 1114 : return it->second.d_qinstLevel;
366 : : }
367 : : }
368 : :
369 : 33046 : bool QuantAttributes::isQuantElim(Node q) const
370 : : {
371 : 33046 : std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
372 [ - + ]: 33046 : if (it == d_qattr.end())
373 : : {
374 : 0 : return false;
375 : : }
376 : 33046 : return it->second.d_quant_elim;
377 : : }
378 : 15527 : bool QuantAttributes::isQuantElimPartial(Node q) const
379 : : {
380 : 15527 : std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
381 [ - + ]: 15527 : if( it==d_qattr.end() ){
382 : 0 : return false;
383 : : }
384 : 15527 : return it->second.d_quant_elim_partial;
385 : : }
386 : :
387 : 170172 : bool QuantAttributes::isQuantBounded(Node q) const
388 : : {
389 : 170172 : std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
390 [ + - ]: 170172 : if (it != d_qattr.end())
391 : : {
392 : 170172 : return it->second.d_isQuantBounded;
393 : : }
394 : 0 : return false;
395 : : }
396 : :
397 : 95 : Node QuantAttributes::getQuantName(Node q) const
398 : : {
399 : 95 : std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
400 [ + - ]: 95 : if (it != d_qattr.end())
401 : : {
402 : 95 : return it->second.d_name;
403 : : }
404 : 0 : return Node::null();
405 : : }
406 : :
407 : 0 : std::string QuantAttributes::quantToString(Node q) const
408 : : {
409 : 0 : std::stringstream ss;
410 : 0 : Node name = getQuantName(q);
411 [ - - ]: 0 : ss << (name.isNull() ? q : name);
412 : 0 : return ss.str();
413 : 0 : }
414 : :
415 : 0 : int QuantAttributes::getQuantIdNum( Node q ) {
416 : 0 : std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
417 [ - - ]: 0 : if( it!=d_qattr.end() ){
418 [ - - ]: 0 : if( !it->second.d_qid_num.isNull() ){
419 : 0 : return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
420 : : }
421 : : }
422 : 0 : return -1;
423 : : }
424 : :
425 : 0 : Node QuantAttributes::getQuantIdNumNode( Node q ) {
426 : 0 : std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
427 [ - - ]: 0 : if( it==d_qattr.end() ){
428 : 0 : return Node::null();
429 : : }else{
430 : 0 : return it->second.d_qid_num;
431 : : }
432 : : }
433 : :
434 : 767 : Node QuantAttributes::mkAttrPreserveStructure(NodeManager* nm)
435 : : {
436 : 767 : Node nattr = mkAttrInternal(nm, AttrType::ATTR_PRESERVE_STRUCTURE);
437 : : PreserveStructureAttribute psa;
438 : 767 : nattr[0].setAttribute(psa, true);
439 : 1534 : return nattr;
440 : 0 : }
441 : :
442 : 76 : Node QuantAttributes::mkAttrQuantifierElimination(NodeManager* nm)
443 : : {
444 : 76 : Node nattr = mkAttrInternal(nm, AttrType::ATTR_QUANT_ELIM);
445 : : QuantElimAttribute qea;
446 : 76 : nattr[0].setAttribute(qea, true);
447 : 152 : return nattr;
448 : 0 : }
449 : 843 : Node QuantAttributes::mkAttrInternal(NodeManager* nm, AttrType at)
450 : : {
451 : 843 : SkolemManager* sm = nm->getSkolemManager();
452 : : // use internal skolem id so that this method is deterministic
453 : 843 : Node id = nm->mkConstInt(Rational(static_cast<uint32_t>(at)));
454 : 843 : Node nattr = sm->mkInternalSkolemFunction(
455 : : InternalSkolemId::QUANTIFIERS_ATTRIBUTE_INTERNAL,
456 : 1686 : nm->booleanType(),
457 : 2529 : {id});
458 : 843 : nattr = nm->mkNode(Kind::INST_ATTRIBUTE, nattr);
459 : 1686 : return nattr;
460 : 843 : }
461 : :
462 : 6703 : void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
463 : : {
464 : : InstLevelAttribute ila;
465 [ + + ]: 6703 : if (!n.hasAttribute(ila))
466 : : {
467 : 3019 : n.setAttribute(ila, level);
468 [ + - ]: 6038 : Trace("inst-level-debug") << "Set instantiation level " << n << " to "
469 : 3019 : << level << std::endl;
470 [ + + ]: 8931 : for (unsigned i = 0; i < n.getNumChildren(); i++)
471 : : {
472 : 5912 : setInstantiationLevelAttr(n[i], level);
473 : : }
474 : : }
475 : 6703 : }
476 : :
477 : 6161 : bool QuantAttributes::getInstantiationLevel(const Node& n, uint64_t& level)
478 : : {
479 : : InstLevelAttribute ila;
480 [ + + ]: 6161 : if (n.hasAttribute(ila))
481 : : {
482 : 2175 : level = n.getAttribute(ila);
483 : 2175 : return true;
484 : : }
485 : 3986 : return false;
486 : : }
487 : :
488 : 0 : Node mkNamedQuant(Kind k, Node bvl, Node body, const std::string& name)
489 : : {
490 : 0 : NodeManager* nm = bvl.getNodeManager();
491 : : Node v = NodeManager::mkDummySkolem(
492 : 0 : name, nm->booleanType(), SkolemFlags::SKOLEM_EXACT_NAME);
493 : 0 : Node attr = nm->mkConst(String("qid"));
494 : 0 : Node ip = nm->mkNode(Kind::INST_ATTRIBUTE, attr, v);
495 : 0 : Node ipl = nm->mkNode(Kind::INST_PATTERN_LIST, ip);
496 : 0 : return nm->mkNode(k, bvl, body, ipl);
497 : 0 : }
498 : :
499 : : } // namespace quantifiers
500 : : } // namespace theory
501 : : } // namespace cvc5::internal
|
