Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Implementation of relevant domain class.
14 : : */
15 : :
16 : : #include "theory/quantifiers/relevant_domain.h"
17 : :
18 : : #include "expr/term_context.h"
19 : : #include "expr/term_context_stack.h"
20 : : #include "theory/arith/arith_msum.h"
21 : : #include "theory/quantifiers/first_order_model.h"
22 : : #include "theory/quantifiers/quantifiers_registry.h"
23 : : #include "theory/quantifiers/quantifiers_state.h"
24 : : #include "theory/quantifiers/term_database.h"
25 : : #include "theory/quantifiers/instantiate.h"
26 : : #include "theory/quantifiers/term_registry.h"
27 : : #include "theory/quantifiers/term_util.h"
28 : : #include "util/rational.h"
29 : :
30 : : using namespace cvc5::internal::kind;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace quantifiers {
35 : :
36 : 30567 : void RelevantDomain::RDomain::merge( RDomain * r ) {
37 [ - + ][ - + ]: 30567 : Assert(!d_parent);
[ - - ]
38 [ - + ][ - + ]: 30567 : Assert(!r->d_parent);
[ - - ]
39 : 30567 : d_parent = r;
40 [ + + ]: 31934 : for( unsigned i=0; i<d_terms.size(); i++ ){
41 : 1367 : r->addTerm( d_terms[i] );
42 : : }
43 : 30567 : d_terms.clear();
44 : 30567 : }
45 : :
46 : 32453 : void RelevantDomain::RDomain::addTerm( Node t ) {
47 [ + + ]: 32453 : if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
48 : 7476 : d_terms.push_back( t );
49 : : }
50 : 32453 : }
51 : :
52 : 1060640 : RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
53 [ + + ]: 1060640 : if( !d_parent ){
54 : 532144 : return this;
55 : : }else{
56 : 528498 : RDomain * p = d_parent->getParent();
57 : 528498 : d_parent = p;
58 : 528498 : return p;
59 : : }
60 : : }
61 : :
62 : 3174 : void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
63 : : {
64 : 6348 : std::map< Node, Node > rterms;
65 [ + + ]: 9283 : for( unsigned i=0; i<d_terms.size(); i++ ){
66 : 12218 : Node r = d_terms[i];
67 [ + - ]: 6109 : if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
68 : 6109 : r = qs.getRepresentative(d_terms[i]);
69 : : }
70 [ + + ]: 6109 : if( rterms.find( r )==rterms.end() ){
71 : 4699 : rterms[r] = d_terms[i];
72 : : }
73 : : }
74 : 3174 : d_terms.clear();
75 [ + + ]: 7873 : for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){
76 : 4699 : d_terms.push_back( it->second );
77 : : }
78 : 3174 : }
79 : :
80 : 334 : RelevantDomain::RelevantDomain(Env& env,
81 : : QuantifiersState& qs,
82 : : QuantifiersRegistry& qr,
83 : 334 : TermRegistry& tr)
84 : 334 : : QuantifiersUtil(env), d_qs(qs), d_qreg(qr), d_treg(tr)
85 : : {
86 : 334 : d_is_computed = false;
87 : 334 : }
88 : :
89 : 668 : RelevantDomain::~RelevantDomain() {
90 [ + + ]: 2722 : for (auto& r : d_rel_doms)
91 : : {
92 [ + + ]: 14748 : for (auto& rr : r.second)
93 : : {
94 : 12360 : RDomain* current = rr.second;
95 [ - + ][ - + ]: 12360 : Assert(current != NULL);
96 [ + - ]: 12360 : delete current;
97 : : }
98 : : }
99 : 668 : }
100 : :
101 : 497328 : RelevantDomain::RDomain* RelevantDomain::getRDomain(Node n,
102 : : size_t i,
103 : : bool getParent)
104 : : {
105 [ + + ][ + + ]: 497328 : if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
[ + + ]
106 : 12360 : d_rel_doms[n][i] = new RDomain;
107 : : }
108 [ + + ]: 497328 : return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
109 : : }
110 : :
111 : 4135 : bool RelevantDomain::reset( Theory::Effort e ) {
112 : 4135 : d_is_computed = false;
113 : 4135 : return true;
114 : : }
115 : :
116 : 13608 : void RelevantDomain::registerQuantifier(Node q) {}
117 : 466 : void RelevantDomain::compute(){
118 [ + - ]: 466 : if( !d_is_computed ){
119 : 466 : d_is_computed = true;
120 [ + + ]: 3904 : for (auto& r : d_rel_doms)
121 : : {
122 [ + + ]: 25045 : for (auto& rr : r.second)
123 : : {
124 : 21607 : rr.second->reset();
125 : : }
126 : : }
127 : 466 : FirstOrderModel* fm = d_treg.getModel();
128 [ + + ]: 4007 : for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
129 : 7082 : Node q = fm->getAssertedQuantifier( i );
130 : 3541 : Node icf = d_qreg.getInstConstantBody(q);
131 [ + - ]: 3541 : Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
132 : 3541 : computeRelevantDomain(q);
133 : : }
134 : :
135 [ + - ]: 466 : Trace("rel-dom-debug") << "account for ground terms" << std::endl;
136 : 466 : TermDb* db = d_treg.getTermDatabase();
137 [ + + ]: 2588 : for (unsigned k = 0; k < db->getNumOperators(); k++)
138 : : {
139 : 4244 : Node op = db->getOperator(k);
140 : 2122 : unsigned sz = db->getNumGroundTerms( op );
141 [ + + ]: 12480 : for( unsigned i=0; i<sz; i++ ){
142 : 20716 : Node n = db->getGroundTerm(op, i);
143 : : //if it is a non-redundant term
144 [ + + ]: 10358 : if( db->isTermActive( n ) ){
145 [ + + ]: 34873 : for( unsigned j=0; j<n.getNumChildren(); j++ ){
146 : 27886 : RDomain * rf = getRDomain( op, j );
147 : 27886 : rf->addTerm( n[j] );
148 [ + - ][ - + ]: 27886 : Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl;
[ - - ]
149 : : }
150 : : }
151 : : }
152 : : }
153 : : // print debug and verify types are correct
154 : 466 : NodeManager* nm = nodeManager();
155 [ + + ]: 6177 : for (std::pair<const Node, std::map<size_t, RDomain*> >& d : d_rel_doms)
156 : : {
157 [ + - ]: 11422 : Trace("rel-dom") << "Relevant domain for " << d.first << " : "
158 : 5711 : << std::endl;
159 [ + + ]: 39452 : for (std::pair<const size_t, RDomain*>& dd : d.second)
160 : : {
161 [ + - ]: 33741 : Trace("rel-dom") << " " << dd.first << " : ";
162 : 33741 : RDomain* r = dd.second;
163 : 33741 : RDomain * rp = r->getParent();
164 [ + + ]: 33741 : if( r==rp ){
165 : 3174 : r->removeRedundantTerms(d_qs);
166 [ + - ]: 3174 : Trace("rel-dom") << r->d_terms;
167 : : }else{
168 [ + - ]: 30567 : Trace("rel-dom") << "Dom( " << d.first << ", " << dd.first << " ) ";
169 : : }
170 [ + - ]: 33741 : Trace("rel-dom") << std::endl;
171 [ + + ]: 33741 : if (d.first.getKind() == Kind::FORALL)
172 : : {
173 : 67515 : TypeNode expectedType = d.first[0][dd.first].getType();
174 [ + + ]: 22886 : for (Node& t : r->d_terms)
175 : : {
176 : 762 : TypeNode tt = t.getType();
177 [ - + ]: 381 : if (tt != expectedType)
178 : : {
179 : : // Computation may merge Int with Real due to inequalities. We
180 : : // correct this here.
181 : 0 : if (tt.isInteger() && expectedType.isReal())
182 : : {
183 : 0 : t = nm->mkNode(Kind::TO_REAL, t);
184 : : }
185 : : else
186 : : {
187 : 0 : Assert(false) << "Relevant domain: bad type " << t.getType()
188 : 0 : << ", expected " << expectedType;
189 : : }
190 : : }
191 : : }
192 : : }
193 : : }
194 : : }
195 : : }
196 : 466 : }
197 : :
198 : 3541 : void RelevantDomain::computeRelevantDomain(Node q)
199 : : {
200 [ - + ][ - + ]: 3541 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
201 : 7082 : Node n = d_qreg.getInstConstantBody(q);
202 : : // we care about polarity in the traversal, so we use a polarity term context
203 : 7082 : PolarityTermContext tc;
204 : 7082 : TCtxStack ctx(&tc);
205 : 3541 : ctx.pushInitial(n);
206 : : std::unordered_set<std::pair<Node, uint32_t>,
207 : : PairHashFunction<Node, uint32_t, std::hash<Node> > >
208 : 7082 : visited;
209 : 7082 : std::pair<Node, uint32_t> curr;
210 : 7082 : Node node;
211 : : uint32_t nodeVal;
212 : : std::unordered_set<
213 : : std::pair<Node, uint32_t>,
214 : 3541 : PairHashFunction<Node, uint32_t, std::hash<Node> > >::const_iterator itc;
215 : : bool hasPol, pol;
216 [ + + ]: 236602 : while (!ctx.empty())
217 : : {
218 : 233061 : curr = ctx.getCurrent();
219 : 233061 : itc = visited.find(curr);
220 : 233061 : ctx.pop();
221 [ + + ]: 233061 : if (itc == visited.end())
222 : : {
223 : 76922 : visited.insert(curr);
224 : 76922 : node = curr.first;
225 : : // if not a quantified formula
226 [ + + ]: 76922 : if (!node.isClosure())
227 : : {
228 : 76490 : nodeVal = curr.second;
229 : : // get the polarity of the current term and process it
230 : 76490 : PolarityTermContext::getFlags(nodeVal, hasPol, pol);
231 : 76490 : computeRelevantDomainNode(q, node, hasPol, pol);
232 : : // traverse the children
233 : 76490 : ctx.pushChildren(node, nodeVal);
234 : : }
235 : : }
236 : : }
237 : 3541 : }
238 : :
239 : 76490 : void RelevantDomain::computeRelevantDomainNode(Node q,
240 : : Node n,
241 : : bool hasPol,
242 : : bool pol)
243 : : {
244 [ + - ]: 76490 : Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
245 : 76490 : Node op = d_treg.getTermDatabase()->getMatchOperator(n);
246 : : // Relevant domain only makes sense for non-parametric operators, thus we
247 : : // check op==n.getOperator() here. This otherwise would lead to bad types
248 : : // for terms in the relevant domain.
249 [ + + ][ + + ]: 76490 : if (!op.isNull() && op == n.getOperator())
[ + + ][ + + ]
[ - - ]
250 : : {
251 [ + + ]: 200828 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
252 : : {
253 : 176791 : RDomain * rf = getRDomain( op, i );
254 [ + + ]: 176791 : if (n[i].getKind() == Kind::ITE)
255 : : {
256 [ + + ]: 12 : for( unsigned j=1; j<=2; j++ ){
257 : 8 : computeRelevantDomainOpCh( rf, n[i][j] );
258 : : }
259 : : }
260 : : else
261 : : {
262 : 176787 : computeRelevantDomainOpCh( rf, n[i] );
263 : : }
264 : : }
265 : : }
266 : :
267 : 79095 : if (((n.getKind() == Kind::EQUAL && !n[0].getType().isBoolean())
268 [ + + ]: 73969 : || n.getKind() == Kind::GEQ)
269 [ + + ][ + - ]: 152980 : && TermUtil::hasInstConstAttr(n))
[ + + ][ + + ]
[ - - ]
270 : : {
271 : : //compute the information for what this literal does
272 : 3003 : computeRelevantDomainLit( q, hasPol, pol, n );
273 : 3003 : RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
274 [ + + ]: 3003 : if (rdl.d_merge)
275 : : {
276 [ + - ][ + - ]: 810 : Assert(rdl.d_rd[0] != nullptr && rdl.d_rd[1] != nullptr);
[ - + ][ - - ]
277 : 405 : RDomain* rd1 = rdl.d_rd[0]->getParent();
278 : 405 : RDomain* rd2 = rdl.d_rd[1]->getParent();
279 [ + + ]: 405 : if( rd1!=rd2 ){
280 : 319 : rd1->merge( rd2 );
281 : : }
282 : : }
283 : : else
284 : : {
285 [ + + ]: 2598 : if (rdl.d_rd[0] != nullptr)
286 : : {
287 : 1087 : RDomain* rd = rdl.d_rd[0]->getParent();
288 [ + + ]: 2176 : for (unsigned i = 0; i < rdl.d_val.size(); i++)
289 : : {
290 : 1089 : rd->addTerm(rdl.d_val[i]);
291 : : }
292 : : }
293 : : }
294 : : }
295 [ + - ]: 76490 : Trace("rel-dom-debug") << "...finished Compute relevant domain " << n << std::endl;
296 : 76490 : }
297 : :
298 : 176795 : void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
299 [ + + ]: 176795 : if (n.getKind() == Kind::INST_CONSTANT)
300 : : {
301 : 348110 : Node q = TermUtil::getInstConstAttr(n);
302 : : //merge the RDomains
303 : 174055 : size_t id = n.getAttribute(InstVarNumAttribute());
304 [ - + ][ - + ]: 174055 : Assert(q[0][id].getType() == n.getType());
[ - - ]
305 [ + - ]: 174055 : Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
306 : 348110 : Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
307 : 174055 : << std::endl;
308 : 174055 : RDomain * rq = getRDomain( q, id );
309 [ + + ]: 174055 : if( rf!=rq ){
310 : 30248 : rq->merge( rf );
311 : : }
312 : : }
313 [ + + ]: 2740 : else if (!TermUtil::hasInstConstAttr(n))
314 : : {
315 [ + - ]: 2111 : Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
316 : : //term to add
317 : 2111 : rf->addTerm( n );
318 : : }
319 : 176795 : }
320 : :
321 : 3003 : void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
322 [ + + ]: 3003 : if (d_rel_dom_lit[hasPol][pol].find(n) != d_rel_dom_lit[hasPol][pol].end())
323 : : {
324 : 1790 : return;
325 : : }
326 : 1321 : NodeManager* nm = nodeManager();
327 : 1321 : RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
328 : 1321 : rdl.d_merge = false;
329 : 1321 : size_t varCount = 0;
330 : 1321 : size_t varCh = 0;
331 [ - + ][ - + ]: 1321 : Assert(n.getNumChildren() == 2);
[ - - ]
332 [ + + ]: 3963 : for (size_t i = 0; i < 2; i++)
333 : : {
334 [ + + ]: 2642 : if (n[i].getKind() == Kind::INST_CONSTANT)
335 : : {
336 : : // must get the quantified formula this belongs to, which may be
337 : : // different from q
338 : 742 : Node qi = TermUtil::getInstConstAttr(n[i]);
339 : 742 : unsigned id = n[i].getAttribute(InstVarNumAttribute());
340 : 742 : rdl.d_rd[i] = getRDomain(qi, id, false);
341 : 742 : varCount++;
342 : 742 : varCh = i;
343 : : }
344 : : else
345 : : {
346 : 1900 : rdl.d_rd[i] = nullptr;
347 : : }
348 : : }
349 : :
350 : 1321 : Node rAdd;
351 : 1321 : Node rVar;
352 : 1321 : bool varLhs = true;
353 [ + + ]: 1321 : if (varCount == 2)
354 : : {
355 : : // don't merge Int and Real
356 : 87 : rdl.d_merge = (n[0].getType() == n[1].getType());
357 : : }
358 [ + + ]: 1234 : else if (varCount == 1)
359 : : {
360 : 568 : rVar = n[varCh];
361 : 568 : rAdd = n[1 - varCh];
362 : 568 : varLhs = (varCh == 0);
363 : 568 : rdl.d_rd[0] = rdl.d_rd[varCh];
364 : 568 : rdl.d_rd[1] = nullptr;
365 : : }
366 [ + + ]: 666 : else if (n[0].getType().isRealOrInt())
367 : : {
368 : : // solve the inequality for one/two variables, if possible
369 : 762 : std::map<Node, Node> msum;
370 [ + - ]: 381 : if (ArithMSum::getMonomialSumLit(n, msum))
371 : : {
372 : 762 : Node var;
373 : 762 : Node var2;
374 : 381 : bool hasNonVar = false;
375 [ + + ]: 1174 : for (std::pair<const Node, Node>& m : msum)
376 : : {
377 [ + + ]: 684 : if (!m.first.isNull() && m.first.getKind() == Kind::INST_CONSTANT
378 : 1477 : && TermUtil::getInstConstAttr(m.first) == q)
379 : : {
380 [ + + ]: 137 : if (var.isNull())
381 : : {
382 : 95 : var = m.first;
383 : : }
384 [ + - ]: 42 : else if (var2.isNull())
385 : : {
386 : 42 : var2 = m.first;
387 : : }
388 : : else
389 : : {
390 : 0 : hasNonVar = true;
391 : : }
392 : : }
393 : : else
394 : : {
395 : 656 : hasNonVar = true;
396 : : }
397 : : }
398 [ + - ]: 762 : Trace("rel-dom") << "Process lit " << n << ", var/var2=" << var << "/"
399 : 381 : << var2 << std::endl;
400 [ + + ]: 381 : if (!var.isNull())
401 : : {
402 [ - + ][ - + ]: 95 : Assert(var.hasAttribute(InstVarNumAttribute()));
[ - - ]
403 [ + + ]: 95 : if (var2.isNull())
404 : : {
405 : : // single variable solve
406 : 106 : Node veq_c;
407 : 106 : Node val;
408 : 53 : int ires = ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
409 [ + - ]: 53 : if (ires != 0)
410 : : {
411 [ + + ]: 53 : if (veq_c.isNull())
412 : : {
413 : 38 : rVar = var;
414 : 38 : rAdd = val;
415 : 38 : varLhs = (ires == 1);
416 : 38 : rdl.d_rd[0] =
417 : 38 : getRDomain(q, var.getAttribute(InstVarNumAttribute()), false);
418 : 38 : rdl.d_rd[1] = nullptr;
419 : : }
420 : : }
421 : : }
422 [ + + ]: 42 : else if (!hasNonVar)
423 : : {
424 [ - + ][ - + ]: 21 : Assert(var2.hasAttribute(InstVarNumAttribute()));
[ - - ]
425 : : // merge the domains
426 : 21 : rdl.d_rd[0] =
427 : 21 : getRDomain(q, var.getAttribute(InstVarNumAttribute()), false);
428 : 21 : rdl.d_rd[1] =
429 : 21 : getRDomain(q, var2.getAttribute(InstVarNumAttribute()), false);
430 : 21 : rdl.d_merge = true;
431 : : }
432 : : }
433 : : }
434 : : }
435 [ + + ]: 1321 : if (rdl.d_merge)
436 : : {
437 : : // do not merge if constant negative polarity
438 [ + + ][ + + ]: 108 : if (hasPol && !pol)
439 : : {
440 : 21 : rdl.d_merge = false;
441 : : }
442 : 108 : return;
443 : : }
444 [ + + ]: 1213 : if (!rAdd.isNull())
445 : : {
446 : : // Ensure that rAdd has the same type as the variable. This is necessary
447 : : // since GEQ may mix Int and Real, as well as the equality solving above
448 : : // may introduce mixed Int and Real.
449 : 606 : rAdd = TermUtil::ensureType(rAdd, rVar.getType());
450 : : }
451 [ + + ][ + + ]: 1213 : if (!rAdd.isNull() && !TermUtil::hasInstConstAttr(rAdd))
[ + + ][ + + ]
[ - - ]
452 : : {
453 [ + - ]: 1032 : Trace("rel-dom-debug") << "...add term " << rAdd << ", pol = " << pol
454 : 516 : << ", kind = " << n.getKind() << std::endl;
455 : : // the negative occurrence adds the term to the domain
456 [ + + ][ + + ]: 516 : if (!hasPol || !pol)
457 : : {
458 : 421 : rdl.d_val.push_back(rAdd);
459 : : }
460 : : // the positive occurrence adds other terms
461 : 516 : if ((!hasPol || pol) && n[0].getType().isInteger())
462 : : {
463 [ + + ]: 103 : if (n.getKind() == Kind::EQUAL)
464 : : {
465 [ + + ]: 45 : for (size_t i = 0; i < 2; i++)
466 : : {
467 : : Node roff = nm->mkNode(
468 [ + + ]: 90 : Kind::ADD, rAdd, nm->mkConstInt(Rational(i == 0 ? 1 : -1)));
469 : 30 : rdl.d_val.push_back(roff);
470 : : }
471 : : }
472 [ + - ]: 88 : else if (n.getKind() == Kind::GEQ)
473 : : {
474 : : Node roff = nm->mkNode(
475 [ + - ]: 264 : Kind::ADD, rAdd, nm->mkConstInt(Rational(varLhs ? 1 : -1)));
476 : 88 : rdl.d_val.push_back(roff);
477 : : }
478 : : }
479 : : }
480 : : else
481 : : {
482 : 697 : rdl.d_rd[0] = nullptr;
483 : 697 : rdl.d_rd[1] = nullptr;
484 : : }
485 : : }
486 : :
487 : : } // namespace quantifiers
488 : : } // namespace theory
489 : : } // namespace cvc5::internal
|
