1 /********************* */
2 /*! \file bounded_integers.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Andres Noetzli, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Bounded integers module
13 **
14 ** This class manages integer bounds for quantifiers
15 **/
16
17 #include "theory/quantifiers/fmf/bounded_integers.h"
18
19 #include "expr/node_algorithm.h"
20 #include "options/quantifiers_options.h"
21 #include "theory/arith/arith_msum.h"
22 #include "theory/quantifiers/first_order_model.h"
23 #include "theory/quantifiers/fmf/model_engine.h"
24 #include "theory/quantifiers/term_enumeration.h"
25 #include "theory/quantifiers/term_util.h"
26 #include "theory/theory_engine.h"
27
28 using namespace CVC4;
29 using namespace std;
30 using namespace CVC4::theory;
31 using namespace CVC4::theory::quantifiers;
32 using namespace CVC4::kind;
33
IntRangeDecisionHeuristic(Node r,context::Context * c,context::Context * u,Valuation valuation,bool isProxy)34 BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
35 Node r,
36 context::Context* c,
37 context::Context* u,
38 Valuation valuation,
39 bool isProxy)
40 : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u)
41 {
42 if( options::fmfBoundLazy() ){
43 d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
44 }else{
45 d_proxy_range = r;
46 }
47 if( !isProxy ){
48 Trace("bound-int") << "Introduce proxy " << d_proxy_range << " for " << d_range << std::endl;
49 }
50 }
mkLiteral(unsigned n)51 Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n)
52 {
53 NodeManager* nm = NodeManager::currentNM();
54 Node cn = nm->mkConst(Rational(n == 0 ? 0 : n - 1));
55 return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn);
56 }
57
proxyCurrentRangeLemma()58 Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
59 {
60 if (d_range == d_proxy_range)
61 {
62 return Node::null();
63 }
64 unsigned curr = 0;
65 if (!getAssertedLiteralIndex(curr))
66 {
67 return Node::null();
68 }
69 if (d_ranges_proxied.find(curr) != d_ranges_proxied.end())
70 {
71 return Node::null();
72 }
73 d_ranges_proxied[curr] = true;
74 NodeManager* nm = NodeManager::currentNM();
75 Node currLit = getLiteral(curr);
76 Node lem =
77 nm->mkNode(EQUAL,
78 currLit,
79 nm->mkNode(curr == 0 ? LT : LEQ,
80 d_range,
81 nm->mkConst(Rational(curr == 0 ? 0 : curr - 1))));
82 return lem;
83 }
84
BoundedIntegers(context::Context * c,QuantifiersEngine * qe)85 BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe)
86 : QuantifiersModule(qe)
87 {
88 }
89
~BoundedIntegers()90 BoundedIntegers::~BoundedIntegers() {}
91
presolve()92 void BoundedIntegers::presolve() {
93 d_bnd_it.clear();
94 }
95
isBound(Node f,Node v)96 bool BoundedIntegers::isBound( Node f, Node v ) {
97 return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
98 }
99
hasNonBoundVar(Node f,Node b,std::map<Node,bool> & visited)100 bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) {
101 if( visited.find( b )==visited.end() ){
102 visited[b] = true;
103 if( b.getKind()==BOUND_VARIABLE ){
104 if( !isBound( f, b ) ){
105 return true;
106 }
107 }else{
108 for( unsigned i=0; i<b.getNumChildren(); i++ ){
109 if( hasNonBoundVar( f, b[i], visited ) ){
110 return true;
111 }
112 }
113 }
114 }
115 return false;
116 }
hasNonBoundVar(Node f,Node b)117 bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
118 std::map< Node, bool > visited;
119 return hasNonBoundVar( f, b, visited );
120 }
121
processEqDisjunct(Node q,Node n,Node & v,std::vector<Node> & v_cases)122 bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ) {
123 if( n.getKind()==EQUAL ){
124 for( unsigned i=0; i<2; i++ ){
125 Node t = n[i];
126 if( !hasNonBoundVar( q, n[1-i] ) ){
127 if( t==v ){
128 v_cases.push_back( n[1-i] );
129 return true;
130 }else if( v.isNull() && t.getKind()==BOUND_VARIABLE ){
131 v = t;
132 v_cases.push_back( n[1-i] );
133 return true;
134 }
135 }
136 }
137 }
138 return false;
139 }
140
processMatchBoundVars(Node q,Node n,std::vector<Node> & bvs,std::map<Node,bool> & visited)141 void BoundedIntegers::processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ){
142 if( visited.find( n )==visited.end() ){
143 visited[n] = true;
144 if( n.getKind()==BOUND_VARIABLE && !isBound( q, n ) ){
145 bvs.push_back( n );
146 //injective operators
147 }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
148 for( unsigned i=0; i<n.getNumChildren(); i++ ){
149 processMatchBoundVars( q, n[i], bvs, visited );
150 }
151 }
152 }
153 }
154
process(Node q,Node n,bool pol,std::map<Node,unsigned> & bound_lit_type_map,std::map<int,std::map<Node,Node>> & bound_lit_map,std::map<int,std::map<Node,bool>> & bound_lit_pol_map,std::map<int,std::map<Node,Node>> & bound_int_range_term,std::map<Node,std::vector<Node>> & bound_fixed_set)155 void BoundedIntegers::process( Node q, Node n, bool pol,
156 std::map< Node, unsigned >& bound_lit_type_map,
157 std::map< int, std::map< Node, Node > >& bound_lit_map,
158 std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
159 std::map< int, std::map< Node, Node > >& bound_int_range_term,
160 std::map< Node, std::vector< Node > >& bound_fixed_set ){
161 if( n.getKind()==OR || n.getKind()==AND ){
162 if( (n.getKind()==OR)==pol ){
163 for( unsigned i=0; i<n.getNumChildren(); i++) {
164 process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
165 }
166 }else{
167 //if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn }
168 Node conj = n;
169 if( !pol ){
170 conj = TermUtil::simpleNegate( conj );
171 }
172 Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl;
173 Assert( conj.getKind()==AND );
174 Node v;
175 std::vector< Node > v_cases;
176 bool success = true;
177 for( unsigned i=0; i<conj.getNumChildren(); i++ ){
178 if( conj[i].getKind()==NOT && processEqDisjunct( q, conj[i][0], v, v_cases ) ){
179 //continue
180 }else{
181 Trace("bound-int-debug") << "...failed due to " << conj[i] << std::endl;
182 success = false;
183 break;
184 }
185 }
186 if( success && !isBound( q, v ) ){
187 Trace("bound-int-debug") << "Success with variable " << v << std::endl;
188 bound_lit_type_map[v] = BOUND_FIXED_SET;
189 bound_lit_map[3][v] = n;
190 bound_lit_pol_map[3][v] = pol;
191 bound_fixed_set[v].clear();
192 bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() );
193 }
194 }
195 }else if( n.getKind()==EQUAL ){
196 if( !pol ){
197 // non-applied DER on x != t, x can be bound to { t }
198 Node v;
199 std::vector< Node > v_cases;
200 if( processEqDisjunct( q, n, v, v_cases ) ){
201 if( !isBound( q, v ) ){
202 bound_lit_type_map[v] = BOUND_FIXED_SET;
203 bound_lit_map[3][v] = n;
204 bound_lit_pol_map[3][v] = pol;
205 Assert( v_cases.size()==1 );
206 bound_fixed_set[v].clear();
207 bound_fixed_set[v].push_back( v_cases[0] );
208 }
209 }
210 }
211 }else if( n.getKind()==NOT ){
212 process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
213 }else if( n.getKind()==GEQ ){
214 if( n[0].getType().isInteger() ){
215 std::map< Node, Node > msum;
216 if (ArithMSum::getMonomialSumLit(n, msum))
217 {
218 Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is monomial sum : " << std::endl;
219 ArithMSum::debugPrintMonomialSum(msum, "bound-int-debug");
220 for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
221 if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){
222 //if not bound in another way
223 if( bound_lit_type_map.find( it->first )==bound_lit_type_map.end() || bound_lit_type_map[it->first] == BOUND_INT_RANGE ){
224 Node veq;
225 if (ArithMSum::isolate(it->first, msum, veq, GEQ) != 0)
226 {
227 Node n1 = veq[0];
228 Node n2 = veq[1];
229 if(pol){
230 //flip
231 n1 = veq[1];
232 n2 = veq[0];
233 if( n1.getKind()==BOUND_VARIABLE ){
234 n2 = ArithMSum::offset(n2, 1);
235 }else{
236 n1 = ArithMSum::offset(n1, -1);
237 }
238 veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
239 }
240 Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
241 Node t = n1==it->first ? n2 : n1;
242 if( !hasNonBoundVar( q, t ) ) {
243 Trace("bound-int-debug") << "The bound is relevant." << std::endl;
244 int loru = n1==it->first ? 0 : 1;
245 bound_lit_type_map[it->first] = BOUND_INT_RANGE;
246 bound_int_range_term[loru][it->first] = t;
247 bound_lit_map[loru][it->first] = n;
248 bound_lit_pol_map[loru][it->first] = pol;
249 }else{
250 Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
251 }
252 }
253 }
254 }
255 }
256 }
257 }
258 }else if( n.getKind()==MEMBER ){
259 if( !pol && !hasNonBoundVar( q, n[1] ) ){
260 std::vector< Node > bound_vars;
261 std::map< Node, bool > visited;
262 processMatchBoundVars( q, n[0], bound_vars, visited );
263 for( unsigned i=0; i<bound_vars.size(); i++ ){
264 Node v = bound_vars[i];
265 Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
266 bound_lit_type_map[v] = BOUND_SET_MEMBER;
267 bound_lit_map[2][v] = n;
268 bound_lit_pol_map[2][v] = pol;
269 }
270 }
271 }else{
272 Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT );
273 }
274 }
275
needsCheck(Theory::Effort e)276 bool BoundedIntegers::needsCheck( Theory::Effort e ) {
277 return e==Theory::EFFORT_LAST_CALL;
278 }
279
check(Theory::Effort e,QEffort quant_e)280 void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
281 {
282 if (quant_e != QEFFORT_STANDARD)
283 {
284 return;
285 }
286 Trace("bint-engine") << "---Bounded Integers---" << std::endl;
287 bool addedLemma = false;
288 // make sure proxies are up-to-date with range
289 for (const Node& r : d_ranges)
290 {
291 Node prangeLem = d_rms[r]->proxyCurrentRangeLemma();
292 if (!prangeLem.isNull())
293 {
294 Trace("bound-int-lemma")
295 << "*** bound int : proxy lemma : " << prangeLem << std::endl;
296 d_quantEngine->addLemma(prangeLem);
297 addedLemma = true;
298 }
299 }
300 Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl;
301 }
setBoundedVar(Node q,Node v,unsigned bound_type)302 void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
303 d_bound_type[q][v] = bound_type;
304 d_set_nums[q][v] = d_set[q].size();
305 d_set[q].push_back( v );
306 Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl;
307 }
308
checkOwnership(Node f)309 void BoundedIntegers::checkOwnership(Node f)
310 {
311 //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
312 Trace("bound-int") << "check ownership quantifier " << f << std::endl;
313 NodeManager* nm = NodeManager::currentNM();
314
315 bool success;
316 do{
317 std::map< Node, unsigned > bound_lit_type_map;
318 std::map< int, std::map< Node, Node > > bound_lit_map;
319 std::map< int, std::map< Node, bool > > bound_lit_pol_map;
320 std::map< int, std::map< Node, Node > > bound_int_range_term;
321 std::map< Node, std::vector< Node > > bound_fixed_set;
322 success = false;
323 process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
324 //for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
325 for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){
326 Node v = it->first;
327 if( !isBound( f, v ) ){
328 bool setBoundVar = false;
329 if( it->second==BOUND_INT_RANGE ){
330 //must have both
331 std::map<Node, Node>& blm0 = bound_lit_map[0];
332 std::map<Node, Node>& blm1 = bound_lit_map[1];
333 if (blm0.find(v) != blm0.end() && blm1.find(v) != blm1.end())
334 {
335 setBoundedVar( f, v, BOUND_INT_RANGE );
336 setBoundVar = true;
337 for( unsigned b=0; b<2; b++ ){
338 //set the bounds
339 Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() );
340 d_bounds[b][f][v] = bound_int_range_term[b][v];
341 }
342 Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]);
343 d_range[f][v] = Rewriter::rewrite(r);
344 Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
345 }
346 }else if( it->second==BOUND_SET_MEMBER ){
347 // only handles infinite element types currently (cardinality is not
348 // supported for finite element types #1123). Regardless, this is
349 // typically not a limitation since this variable can be bound in a
350 // standard way below since its type is finite.
351 if (!v.getType().isInterpretedFinite())
352 {
353 setBoundedVar(f, v, BOUND_SET_MEMBER);
354 setBoundVar = true;
355 d_setm_range[f][v] = bound_lit_map[2][v][1];
356 d_setm_range_lit[f][v] = bound_lit_map[2][v];
357 d_range[f][v] = nm->mkNode(CARD, d_setm_range[f][v]);
358 Trace("bound-int") << "Variable " << v
359 << " is bound because of set membership literal "
360 << bound_lit_map[2][v] << std::endl;
361 }
362 }else if( it->second==BOUND_FIXED_SET ){
363 setBoundedVar(f, v, BOUND_FIXED_SET);
364 setBoundVar = true;
365 for (unsigned i = 0; i < bound_fixed_set[v].size(); i++)
366 {
367 Node t = bound_fixed_set[v][i];
368 if (expr::hasBoundVar(t))
369 {
370 d_fixed_set_ngr_range[f][v].push_back(t);
371 }
372 else
373 {
374 d_fixed_set_gr_range[f][v].push_back(t);
375 }
376 }
377 Trace("bound-int") << "Variable " << v
378 << " is bound because of disequality conjunction "
379 << bound_lit_map[3][v] << std::endl;
380 }
381 if( setBoundVar ){
382 success = true;
383 //set Attributes on literals
384 for( unsigned b=0; b<2; b++ ){
385 std::map<Node, Node>& blm = bound_lit_map[b];
386 if (blm.find(v) != blm.end())
387 {
388 std::map<Node, bool>& blmp = bound_lit_pol_map[b];
389 // WARNING_CANDIDATE:
390 // This assertion may fail. We intentionally do not enable this in
391 // production as it is considered safe for this to fail. We fail
392 // the assertion in debug mode to have this instance raised to
393 // our attention.
394 Assert(blmp.find(v) != blmp.end());
395 BoundIntLitAttribute bila;
396 bound_lit_map[b][v].setAttribute(bila, blmp[v] ? 1 : 0);
397 }
398 else
399 {
400 Assert( it->second!=BOUND_INT_RANGE );
401 }
402 }
403 }
404 }
405 }
406 if( !success ){
407 //resort to setting a finite bound on a variable
408 for( unsigned i=0; i<f[0].getNumChildren(); i++) {
409 if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
410 TypeNode tn = f[0][i].getType();
411 if (tn.isSort()
412 || d_quantEngine->getTermEnumeration()->mayComplete(tn))
413 {
414 success = true;
415 setBoundedVar( f, f[0][i], BOUND_FINITE );
416 break;
417 }
418 }
419 }
420 }
421 }while( success );
422
423 if( Trace.isOn("bound-int") ){
424 Trace("bound-int") << "Bounds are : " << std::endl;
425 for( unsigned i=0; i<f[0].getNumChildren(); i++) {
426 Node v = f[0][i];
427 if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){
428 Assert( d_bound_type[f].find( v )!=d_bound_type[f].end() );
429 if( d_bound_type[f][v]==BOUND_INT_RANGE ){
430 Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
431 }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
432 if( d_setm_range_lit[f][v][0]==v ){
433 Trace("bound-int") << " " << v << " in " << d_setm_range[f][v] << std::endl;
434 }else{
435 Trace("bound-int") << " " << v << " unifiable in " << d_setm_range_lit[f][v] << std::endl;
436 }
437 }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
438 Trace("bound-int") << " " << v << " in { ";
439 for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){
440 Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " ";
441 }
442 for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){
443 Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " ";
444 }
445 Trace("bound-int") << "}" << std::endl;
446 }else if( d_bound_type[f][v]==BOUND_FINITE ){
447 Trace("bound-int") << " " << v << " has small finite type." << std::endl;
448 }else{
449 Trace("bound-int") << " " << v << " has unknown bound." << std::endl;
450 Assert( false );
451 }
452 }else{
453 Trace("bound-int") << " " << "*** " << v << " is unbounded." << std::endl;
454 }
455 }
456 }
457
458 bool bound_success = true;
459 for( unsigned i=0; i<f[0].getNumChildren(); i++) {
460 if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
461 Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl;
462 bound_success = false;
463 break;
464 }
465 }
466
467 if( bound_success ){
468 d_bound_quants.push_back( f );
469 for( unsigned i=0; i<d_set[f].size(); i++) {
470 Node v = d_set[f][i];
471 std::map< Node, Node >::iterator itr = d_range[f].find( v );
472 if( itr != d_range[f].end() ){
473 Node r = itr->second;
474 Assert( !r.isNull() );
475 bool isProxy = false;
476 if (expr::hasBoundVar(r))
477 {
478 // introduce a new bound
479 Node new_range = NodeManager::currentNM()->mkSkolem(
480 "bir", r.getType(), "bound for term");
481 d_nground_range[f][v] = r;
482 d_range[f][v] = new_range;
483 r = new_range;
484 isProxy = true;
485 }
486 if( !r.isConst() ){
487 if (d_rms.find(r) == d_rms.end())
488 {
489 Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
490 d_ranges.push_back( r );
491 d_rms[r].reset(
492 new IntRangeDecisionHeuristic(r,
493 d_quantEngine->getSatContext(),
494 d_quantEngine->getUserContext(),
495 d_quantEngine->getValuation(),
496 isProxy));
497 d_quantEngine->getTheoryEngine()
498 ->getDecisionManager()
499 ->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
500 d_rms[r].get());
501 }
502 }
503 }
504 }
505 }
506 }
507
getBoundVarType(Node q,Node v)508 unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) {
509 std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v );
510 if( it==d_bound_type[q].end() ){
511 return BOUND_NONE;
512 }else{
513 return it->second;
514 }
515 }
516
getBounds(Node f,Node v,RepSetIterator * rsi,Node & l,Node & u)517 void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
518 l = d_bounds[0][f][v];
519 u = d_bounds[1][f][v];
520 if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){
521 //get the substitution
522 std::vector< Node > vars;
523 std::vector< Node > subs;
524 if( getRsiSubsitution( f, v, vars, subs, rsi ) ){
525 u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
526 l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
527 }else{
528 u = Node::null();
529 l = Node::null();
530 }
531 }
532 }
533
getBoundValues(Node f,Node v,RepSetIterator * rsi,Node & l,Node & u)534 void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
535 getBounds( f, v, rsi, l, u );
536 Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
537 if( !l.isNull() ){
538 l = d_quantEngine->getModel()->getValue( l );
539 }
540 if( !u.isNull() ){
541 u = d_quantEngine->getModel()->getValue( u );
542 }
543 Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
544 return;
545 }
546
isGroundRange(Node q,Node v)547 bool BoundedIntegers::isGroundRange(Node q, Node v)
548 {
549 if (isBoundVar(q, v))
550 {
551 if (d_bound_type[q][v] == BOUND_INT_RANGE)
552 {
553 return !expr::hasBoundVar(getLowerBound(q, v))
554 && !expr::hasBoundVar(getUpperBound(q, v));
555 }
556 else if (d_bound_type[q][v] == BOUND_SET_MEMBER)
557 {
558 return !expr::hasBoundVar(d_setm_range[q][v]);
559 }
560 else if (d_bound_type[q][v] == BOUND_FIXED_SET)
561 {
562 return !d_fixed_set_ngr_range[q][v].empty();
563 }
564 }
565 return false;
566 }
567
getSetRange(Node q,Node v,RepSetIterator * rsi)568 Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) {
569 Node sr = d_setm_range[q][v];
570 if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){
571 Trace("bound-int-rsi-debug")
572 << sr << " is non-ground, apply substitution..." << std::endl;
573 //get the substitution
574 std::vector< Node > vars;
575 std::vector< Node > subs;
576 if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
577 Trace("bound-int-rsi-debug")
578 << " apply " << vars << " -> " << subs << std::endl;
579 sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
580 }else{
581 sr = Node::null();
582 }
583 }
584 return sr;
585 }
586
getSetRangeValue(Node q,Node v,RepSetIterator * rsi)587 Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
588 Node sr = getSetRange( q, v, rsi );
589 if (sr.isNull())
590 {
591 return sr;
592 }
593 Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
594 Assert(!expr::hasFreeVar(sr));
595 Node sro = sr;
596 sr = d_quantEngine->getModel()->getValue(sr);
597 // if non-constant, then sr does not occur in the model, we fail
598 if (!sr.isConst())
599 {
600 return Node::null();
601 }
602 Trace("bound-int-rsi") << "Value is " << sr << std::endl;
603 if (sr.getKind() == EMPTYSET)
604 {
605 return sr;
606 }
607 NodeManager* nm = NodeManager::currentNM();
608 Node nsr;
609 TypeNode tne = sr.getType().getSetElementType();
610
611 // we can use choice functions for canonical symbolic instantiations
612 unsigned srCard = 0;
613 while (sr.getKind() == UNION)
614 {
615 srCard++;
616 sr = sr[0];
617 }
618 Assert(sr.getKind() == SINGLETON);
619 srCard++;
620 // choices[i] stores the canonical symbolic representation of the (i+1)^th
621 // element of sro
622 std::vector<Node> choices;
623 Node srCardN = nm->mkNode(CARD, sro);
624 Node choice_i;
625 for (unsigned i = 0; i < srCard; i++)
626 {
627 if (i == d_setm_choice[sro].size())
628 {
629 choice_i = nm->mkBoundVar(tne);
630 choices.push_back(choice_i);
631 Node cBody = nm->mkNode(MEMBER, choice_i, sro);
632 if (choices.size() > 1)
633 {
634 cBody = nm->mkNode(AND, cBody, nm->mkNode(DISTINCT, choices));
635 }
636 choices.pop_back();
637 Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i);
638 Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i)));
639 choice_i = nm->mkNode(CHOICE, bvl, nm->mkNode(OR, cMinCard, cBody));
640 d_setm_choice[sro].push_back(choice_i);
641 }
642 Assert(i < d_setm_choice[sro].size());
643 choice_i = d_setm_choice[sro][i];
644 choices.push_back(choice_i);
645 Node sChoiceI = nm->mkNode(SINGLETON, choice_i);
646 if (nsr.isNull())
647 {
648 nsr = sChoiceI;
649 }
650 else
651 {
652 nsr = nm->mkNode(UNION, nsr, sChoiceI);
653 }
654 }
655 // turns the concrete model value of sro into a canonical representation
656 // e.g.
657 // singleton(0) union singleton(1)
658 // becomes
659 // C1 union ( choice y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
660 // where C1 = ( choice x. card(S)<=0 OR x in S ).
661 Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
662 return nsr;
663 }
664
getRsiSubsitution(Node q,Node v,std::vector<Node> & vars,std::vector<Node> & subs,RepSetIterator * rsi)665 bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) {
666
667 Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
668 Assert( d_set_nums[q].find( v )!=d_set_nums[q].end() );
669 int vindex = d_set_nums[q][v];
670 Assert( d_set_nums[q][v]==vindex );
671 Trace("bound-int-rsi-debug") << " index order is " << vindex << std::endl;
672 //must take substitution for all variables that are iterating at higher level
673 for( int i=0; i<vindex; i++) {
674 Assert( d_set_nums[q][d_set[q][i]]==i );
675 Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
676 int v = rsi->getVariableOrder( i );
677 Assert( q[0][v]==d_set[q][i] );
678 Node t = rsi->getCurrentTerm(v, true);
679 Trace("bound-int-rsi") << "term : " << t << std::endl;
680 vars.push_back( d_set[q][i] );
681 subs.push_back( t );
682 }
683
684 //check if it has been instantiated
685 if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){
686 if( d_bound_type[q][v]==BOUND_INT_RANGE || d_bound_type[q][v]==BOUND_SET_MEMBER ){
687 //must add the lemma
688 Node nn = d_nground_range[q][v];
689 nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
690 Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
691 Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
692 d_quantEngine->getOutputChannel().lemma(lem, false, true);
693 }
694 return false;
695 }else{
696 return true;
697 }
698 }
699
matchBoundVar(Node v,Node t,Node e)700 Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
701 if( t==v ){
702 return e;
703 }else if( t.getKind()==kind::APPLY_CONSTRUCTOR ){
704 if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
705 if( t.getOperator() != e.getOperator() ) {
706 return Node::null();
707 }
708 }
709 const Datatype& dt = Datatype::datatypeOf( t.getOperator().toExpr() );
710 unsigned index = Datatype::indexOf( t.getOperator().toExpr() );
711 for( unsigned i=0; i<t.getNumChildren(); i++ ){
712 Node u;
713 if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
714 u = matchBoundVar( v, t[i], e[i] );
715 }else{
716 Node se = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index].getSelectorInternal( e.getType().toType(), i ) ), e );
717 u = matchBoundVar( v, t[i], se );
718 }
719 if( !u.isNull() ){
720 return u;
721 }
722 }
723 }
724 return Node::null();
725 }
726
getBoundElements(RepSetIterator * rsi,bool initial,Node q,Node v,std::vector<Node> & elements)727 bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
728 if( initial || !isGroundRange( q, v ) ){
729 elements.clear();
730 unsigned bvt = getBoundVarType( q, v );
731 if( bvt==BOUND_INT_RANGE ){
732 Node l, u;
733 getBoundValues( q, v, rsi, l, u );
734 if( l.isNull() || u.isNull() ){
735 Trace("bound-int-warn") << "WARNING: Could not find integer bounds in model for " << v << " in " << q << std::endl;
736 //failed, abort the iterator
737 return false;
738 }else{
739 Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl;
740 Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
741 Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
742 Node tl = l;
743 Node tu = u;
744 getBounds( q, v, rsi, tl, tu );
745 Assert( !tl.isNull() && !tu.isNull() );
746 if( ra==d_quantEngine->getTermUtil()->d_true ){
747 long rr = range.getConst<Rational>().getNumerator().getLong()+1;
748 Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
749 for( unsigned k=0; k<rr; k++ ){
750 Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) );
751 t = Rewriter::rewrite( t );
752 elements.push_back( t );
753 }
754 return true;
755 }else{
756 Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << v << "." << std::endl;
757 return false;
758 }
759 }
760 }else if( bvt==BOUND_SET_MEMBER ){
761 Node srv = getSetRangeValue( q, v, rsi );
762 if( srv.isNull() ){
763 Trace("bound-int-warn") << "WARNING: Could not find set bound in model for " << v << " in " << q << std::endl;
764 return false;
765 }else{
766 Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
767 if( srv.getKind()!=EMPTYSET ){
768 //collect the elements
769 while( srv.getKind()==UNION ){
770 Assert( srv[1].getKind()==kind::SINGLETON );
771 elements.push_back( srv[1][0] );
772 srv = srv[0];
773 }
774 Assert( srv.getKind()==kind::SINGLETON );
775 elements.push_back( srv[0] );
776 //check if we need to do matching, for literals like ( tuple( v ) in S )
777 Node t = d_setm_range_lit[q][v][0];
778 if( t!=v ){
779 std::vector< Node > elements_tmp;
780 elements_tmp.insert( elements_tmp.end(), elements.begin(), elements.end() );
781 elements.clear();
782 for( unsigned i=0; i<elements_tmp.size(); i++ ){
783 //do matching to determine v -> u
784 Node u = matchBoundVar( v, t, elements_tmp[i] );
785 Trace("bound-int-rsi-debug") << " unification : " << elements_tmp[i] << " = " << t << " yields " << v << " -> " << u << std::endl;
786 if( !u.isNull() ){
787 elements.push_back( u );
788 }
789 }
790 }
791 }
792 return true;
793 }
794 }else if( bvt==BOUND_FIXED_SET ){
795 std::map< Node, std::vector< Node > >::iterator it = d_fixed_set_gr_range[q].find( v );
796 if( it!=d_fixed_set_gr_range[q].end() ){
797 for( unsigned i=0; i<it->second.size(); i++ ){
798 elements.push_back( it->second[i] );
799 }
800 }
801 it = d_fixed_set_ngr_range[q].find( v );
802 if( it!=d_fixed_set_ngr_range[q].end() ){
803 std::vector< Node > vars;
804 std::vector< Node > subs;
805 if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
806 for( unsigned i=0; i<it->second.size(); i++ ){
807 Node t = it->second[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
808 elements.push_back( t );
809 }
810 return true;
811 }else{
812 return false;
813 }
814 }else{
815 return true;
816 }
817 }else{
818 return false;
819 }
820 }else{
821 //no change required
822 return true;
823 }
824 }
825