1 /********************* */
2 /*! \file bounded_integers.cpp
4 ** Original author: Andrew Reynolds
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Bounded integers module
14 ** This class manages integer bounds for quantifiers
17 #include "theory/quantifiers/bounded_integers.h"
18 #include "theory/quantifiers/quant_util.h"
19 #include "theory/quantifiers/first_order_model.h"
20 #include "theory/quantifiers/model_engine.h"
21 #include "theory/quantifiers/term_database.h"
25 using namespace CVC4::theory
;
26 using namespace CVC4::theory::quantifiers
;
27 using namespace CVC4::kind
;
29 void BoundedIntegers::RangeModel::initialize() {
30 //add initial split lemma
31 Node ltr
= NodeManager::currentNM()->mkNode( LT
, d_range
, NodeManager::currentNM()->mkConst( Rational(0) ) );
32 ltr
= Rewriter::rewrite( ltr
);
33 Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr
<< std::endl
;
34 d_bi
->getQuantifiersEngine()->getOutputChannel().split( ltr
);
35 Node ltr_lit
= ltr
.getKind()==NOT
? ltr
[0] : ltr
;
36 d_range_literal
[-1] = ltr_lit
;
37 d_lit_to_range
[ltr_lit
] = -1;
38 d_lit_to_pol
[ltr_lit
] = ltr
.getKind()!=NOT
;
39 //register with bounded integers
40 Trace("bound-int-debug") << "Literal " << ltr_lit
<< " is literal for " << d_range
<< std::endl
;
41 d_bi
->addLiteralFromRange(ltr_lit
, d_range
);
44 void BoundedIntegers::RangeModel::assertNode(Node n
) {
45 bool pol
= n
.getKind()!=NOT
;
46 Node nlit
= n
.getKind()==NOT
? n
[0] : n
;
47 if( d_lit_to_range
.find( nlit
)!=d_lit_to_range
.end() ){
48 Trace("bound-int-assert") << "With polarity = " << pol
<< " (req "<< d_lit_to_pol
[nlit
] << ")";
49 Trace("bound-int-assert") << ", found literal " << nlit
;
50 Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range
[nlit
] << " for " << d_range
<< std::endl
;
51 d_range_assertions
[nlit
] = (pol
==d_lit_to_pol
[nlit
]);
52 if( pol
!=d_lit_to_pol
[nlit
] ){
53 //check if we need a new split?
55 bool needsRange
= true;
56 for( std::map
< Node
, int >::iterator it
= d_lit_to_range
.begin(); it
!= d_lit_to_range
.end(); ++it
){
57 if( d_range_assertions
.find( it
->first
)==d_range_assertions
.end() ){
67 if (!d_has_range
|| d_lit_to_range
[nlit
]<d_curr_range
){
68 Trace("bound-int-bound") << "Successfully bound " << d_range
<< " to " << d_lit_to_range
[nlit
] << std::endl
;
69 d_curr_range
= d_lit_to_range
[nlit
];
75 Message() << "Could not find literal " << nlit
<< " for range " << d_range
<< std::endl
;
80 void BoundedIntegers::RangeModel::allocateRange() {
82 int newBound
= d_curr_max
;
83 Trace("bound-int-proc") << "Allocate range bound " << newBound
<< " for " << d_range
<< std::endl
;
84 //TODO: newBound should be chosen in a smarter way
85 Node ltr
= NodeManager::currentNM()->mkNode( LEQ
, d_range
, NodeManager::currentNM()->mkConst( Rational(newBound
) ) );
86 ltr
= Rewriter::rewrite( ltr
);
87 Trace("bound-int-lemma") << " *** bound int: split on " << ltr
<< std::endl
;
88 d_bi
->getQuantifiersEngine()->getOutputChannel().split( ltr
);
89 Node ltr_lit
= ltr
.getKind()==NOT
? ltr
[0] : ltr
;
90 d_range_literal
[newBound
] = ltr_lit
;
91 d_lit_to_range
[ltr_lit
] = newBound
;
92 d_lit_to_pol
[ltr_lit
] = ltr
.getKind()!=NOT
;
93 //register with bounded integers
94 d_bi
->addLiteralFromRange(ltr_lit
, d_range
);
97 Node
BoundedIntegers::RangeModel::getNextDecisionRequest() {
98 //request the current cardinality as a decision literal, if not already asserted
99 for( std::map
< Node
, int >::iterator it
= d_lit_to_range
.begin(); it
!= d_lit_to_range
.end(); ++it
){
101 if( !d_has_range
|| i
<d_curr_range
){
103 Assert( !rn
.isNull() );
104 if( d_range_assertions
.find( rn
)==d_range_assertions
.end() ){
105 if (!d_lit_to_pol
[it
->first
]) {
108 Trace("bound-int-dec-debug") << "For " << d_range
<< ", make decision " << rn
<< " to make range " << i
<< std::endl
;
117 BoundedIntegers::BoundedIntegers(context::Context
* c
, QuantifiersEngine
* qe
) :
118 QuantifiersModule(qe
), d_assertions(c
){
122 bool BoundedIntegers::isBound( Node f
, Node v
) {
123 return std::find( d_set
[f
].begin(), d_set
[f
].end(), v
)!=d_set
[f
].end();
126 bool BoundedIntegers::hasNonBoundVar( Node f
, Node b
) {
127 if( b
.getKind()==BOUND_VARIABLE
){
128 if( !isBound( f
, b
) ){
132 for( unsigned i
=0; i
<b
.getNumChildren(); i
++ ){
133 if( hasNonBoundVar( f
, b
[i
] ) ){
141 void BoundedIntegers::processLiteral( Node f
, Node lit
, bool pol
,
142 std::map
< int, std::map
< Node
, Node
> >& bound_lit_map
,
143 std::map
< int, std::map
< Node
, bool > >& bound_lit_pol_map
) {
144 if( lit
.getKind()==GEQ
&& lit
[0].getType().isInteger() ){
145 std::map
< Node
, Node
> msum
;
146 if (QuantArith::getMonomialSumLit( lit
, msum
)){
147 Trace("bound-int-debug") << "Literal (polarity = " << pol
<< ") " << lit
<< " is monomial sum : " << std::endl
;
148 for(std::map
< Node
, Node
>::iterator it
= msum
.begin(); it
!= msum
.end(); ++it
){
149 Trace("bound-int-debug") << " ";
150 if( !it
->second
.isNull() ){
151 Trace("bound-int-debug") << it
->second
;
152 if( !it
->first
.isNull() ){
153 Trace("bound-int-debug") << " * ";
156 if( !it
->first
.isNull() ){
157 Trace("bound-int-debug") << it
->first
;
159 Trace("bound-int-debug") << std::endl
;
161 Trace("bound-int-debug") << std::endl
;
162 for( std::map
< Node
, Node
>::iterator it
= msum
.begin(); it
!= msum
.end(); ++it
){
163 if ( !it
->first
.isNull() && it
->first
.getKind()==BOUND_VARIABLE
&& !isBound( f
, it
->first
) ){
165 if( QuantArith::isolate( it
->first
, msum
, veq
, GEQ
) ){
172 if( n1
.getKind()==BOUND_VARIABLE
){
173 n2
= QuantArith::offset( n2
, 1 );
175 n1
= QuantArith::offset( n1
, -1 );
177 veq
= NodeManager::currentNM()->mkNode( GEQ
, n1
, n2
);
179 Trace("bound-int-debug") << "Isolated for " << it
->first
<< " : (" << n1
<< " >= " << n2
<< ")" << std::endl
;
180 Node t
= n1
==it
->first
? n2
: n1
;
181 if( !hasNonBoundVar( f
, t
) ) {
182 Trace("bound-int-debug") << "The bound is relevant." << std::endl
;
183 int loru
= n1
==it
->first
? 0 : 1;
184 d_bounds
[loru
][f
][it
->first
] = t
;
185 bound_lit_map
[loru
][it
->first
] = lit
;
186 bound_lit_pol_map
[loru
][it
->first
] = pol
;
188 Trace("bound-int-debug") << "The term " << t
<< " has non-bound variable." << std::endl
;
194 }else if( lit
.getKind()==LEQ
|| lit
.getKind()==LT
|| lit
.getKind()==GT
) {
195 Message() << "BoundedIntegers : Bad kind for literal : " << lit
<< std::endl
;
199 void BoundedIntegers::process( Node f
, Node n
, bool pol
,
200 std::map
< int, std::map
< Node
, Node
> >& bound_lit_map
,
201 std::map
< int, std::map
< Node
, bool > >& bound_lit_pol_map
){
202 if( (n
.getKind()==OR
&& pol
) || (n
.getKind()==AND
&& !pol
) ){
203 for( unsigned i
=0; i
<n
.getNumChildren(); i
++) {
204 process( f
, n
[i
], pol
, bound_lit_map
, bound_lit_pol_map
);
206 }else if( n
.getKind()==NOT
){
207 process( f
, n
[0], !pol
, bound_lit_map
, bound_lit_pol_map
);
209 processLiteral( f
, n
, pol
, bound_lit_map
, bound_lit_pol_map
);
213 void BoundedIntegers::check( Theory::Effort e
) {
218 void BoundedIntegers::addLiteralFromRange( Node lit
, Node r
) {
219 d_lit_to_ranges
[lit
].push_back(r
);
220 //check if it is already asserted?
221 if(d_assertions
.find(lit
)!=d_assertions
.end()){
222 d_rms
[r
]->assertNode( d_assertions
[lit
] ? lit
: lit
.negate() );
226 void BoundedIntegers::registerQuantifier( Node f
) {
227 Trace("bound-int") << "Register quantifier " << f
<< std::endl
;
228 bool hasIntType
= false;
230 std::map
< Node
, int > numMap
;
231 for( unsigned i
=0; i
<f
[0].getNumChildren(); i
++) {
233 if( f
[0][i
].getType().isInteger() ){
236 else if( f
[0][i
].getType().isSort() || f
[0][i
].getType().getCardinality().isFinite() ){
243 std::map
< int, std::map
< Node
, Node
> > bound_lit_map
;
244 std::map
< int, std::map
< Node
, bool > > bound_lit_pol_map
;
246 process( f
, f
[1], true, bound_lit_map
, bound_lit_pol_map
);
247 for( std::map
< Node
, Node
>::iterator it
= d_bounds
[0][f
].begin(); it
!= d_bounds
[0][f
].end(); ++it
){
250 if( d_bounds
[1][f
].find(v
)!=d_bounds
[1][f
].end() ){
251 d_set
[f
].push_back(v
);
252 d_set_nums
[f
].push_back(numMap
[v
]);
254 //set Attributes on literals
255 for( unsigned b
=0; b
<2; b
++ ){
256 Assert( bound_lit_map
[b
].find( v
)!=bound_lit_map
[b
].end() );
257 Assert( bound_lit_pol_map
[b
].find( v
)!=bound_lit_pol_map
[b
].end() );
258 BoundIntLitAttribute bila
;
259 bound_lit_map
[b
][v
].setAttribute( bila
, bound_lit_pol_map
[b
][v
] ? 1 : 0 );
261 Trace("bound-int") << "Variable " << v
<< " is bound because of literals " << bound_lit_map
[0][v
] << " and " << bound_lit_map
[1][v
] << std::endl
;
266 Trace("bound-int") << "Bounds are : " << std::endl
;
267 for( unsigned i
=0; i
<d_set
[f
].size(); i
++) {
268 Node v
= d_set
[f
][i
];
269 Node r
= NodeManager::currentNM()->mkNode( MINUS
, d_bounds
[1][f
][v
], d_bounds
[0][f
][v
] );
270 d_range
[f
][v
] = Rewriter::rewrite( r
);
271 Trace("bound-int") << " " << d_bounds
[0][f
][v
] << " <= " << v
<< " <= " << d_bounds
[1][f
][v
] << " (range is " << d_range
[f
][v
] << ")" << std::endl
;
273 if( d_set
[f
].size()==(f
[0].getNumChildren()-finiteTypes
) ){
274 d_bound_quants
.push_back( f
);
275 for( unsigned i
=0; i
<d_set
[f
].size(); i
++) {
276 Node v
= d_set
[f
][i
];
277 Node r
= d_range
[f
][v
];
278 if( r
.hasBoundVar() ){
279 //introduce a new bound
280 Node new_range
= NodeManager::currentNM()->mkSkolem( "bir", r
.getType(), "bound for term" );
281 d_nground_range
[f
][v
] = d_range
[f
][v
];
282 d_range
[f
][v
] = new_range
;
285 if( r
.getKind()!=CONST_RATIONAL
){
286 if( std::find(d_ranges
.begin(), d_ranges
.end(), r
)==d_ranges
.end() ){
287 Trace("bound-int") << "For " << v
<< ", bounded Integer Module will try to minimize : " << r
<< " " << r
.getKind() << std::endl
;
288 d_ranges
.push_back( r
);
289 d_rms
[r
] = new RangeModel(this, r
, d_quantEngine
->getSatContext() );
290 d_rms
[r
]->initialize();
295 Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f
<< std::endl
;
296 //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl;
301 void BoundedIntegers::assertNode( Node n
) {
302 Trace("bound-int-assert") << "Assert " << n
<< std::endl
;
303 Node nlit
= n
.getKind()==NOT
? n
[0] : n
;
304 if( d_lit_to_ranges
.find(nlit
)!=d_lit_to_ranges
.end() ){
305 Trace("bound-int-assert") << "This is the bounding literal for " << d_lit_to_ranges
[nlit
].size() << " ranges." << std::endl
;
306 for( unsigned i
=0; i
<d_lit_to_ranges
[nlit
].size(); i
++) {
307 Node r
= d_lit_to_ranges
[nlit
][i
];
308 Trace("bound-int-assert") << " ...this is a bounding literal for " << r
<< std::endl
;
309 d_rms
[r
]->assertNode( n
);
312 d_assertions
[nlit
] = n
.getKind()!=NOT
;
315 Node
BoundedIntegers::getNextDecisionRequest() {
316 Trace("bound-int-dec-debug") << "bi: Get next decision request?" << std::endl
;
317 for( unsigned i
=0; i
<d_ranges
.size(); i
++) {
318 Node d
= d_rms
[d_ranges
[i
]]->getNextDecisionRequest();
320 bool polLit
= d
.getKind()!=NOT
;
321 Node lit
= d
.getKind()==NOT
? d
[0] : d
;
323 if( d_quantEngine
->getValuation().hasSatValue( lit
, value
) ) {
325 Trace("bound-int-dec-debug") << "...already asserted properly." << std::endl
;
326 //already true, we're already fine
328 Trace("bound-int-dec-debug") << "...already asserted with wrong polarity, re-assert." << std::endl
;
329 assertNode( d
.negate() );
333 Trace("bound-int-dec") << "Bounded Integers : Decide " << d
<< std::endl
;
341 void BoundedIntegers::getBounds( Node f
, Node v
, RepSetIterator
* rsi
, Node
& l
, Node
& u
) {
342 l
= d_bounds
[0][f
][v
];
343 u
= d_bounds
[1][f
][v
];
344 if( d_nground_range
[f
].find(v
)!=d_nground_range
[f
].end() ){
345 //must create substitution
346 std::vector
< Node
> vars
;
347 std::vector
< Node
> subs
;
348 Trace("bound-int-rsi") << "Get bound value in model of variable " << v
<< std::endl
;
349 for( unsigned i
=0; i
<d_set
[f
].size(); i
++) {
350 if( d_set
[f
][i
]!=v
){
351 Trace("bound-int-rsi") << "Look up the value for " << d_set
[f
][i
] << " " << rsi
->d_var_order
[d_set_nums
[f
][i
]] << std::endl
;
352 Trace("bound-int-rsi") << "term : " << rsi
->getTerm(rsi
->d_var_order
[d_set_nums
[f
][i
]]) << std::endl
;
353 vars
.push_back(d_set
[f
][i
]);
354 subs
.push_back(rsi
->getTerm(rsi
->d_var_order
[d_set_nums
[f
][i
]]));
359 Trace("bound-int-rsi") << "Do substitution..." << std::endl
;
360 //check if it has been instantiated
361 if (!vars
.empty() && !d_bnd_it
[f
][v
].hasInstantiated(subs
)){
363 Node nn
= d_nground_range
[f
][v
];
364 nn
= nn
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
365 Node lem
= NodeManager::currentNM()->mkNode( LEQ
, nn
, d_range
[f
][v
] );
366 Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem
<< std::endl
;
367 d_quantEngine
->getOutputChannel().lemma(lem
, false, true);
372 u
= u
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
373 l
= l
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
378 void BoundedIntegers::getBoundValues( Node f
, Node v
, RepSetIterator
* rsi
, Node
& l
, Node
& u
) {
379 getBounds( f
, v
, rsi
, l
, u
);
380 Trace("bound-int-rsi") << "Get value in model for..." << l
<< " and " << u
<< std::endl
;
381 l
= d_quantEngine
->getModel()->getCurrentModelValue( l
);
382 u
= d_quantEngine
->getModel()->getCurrentModelValue( u
);
383 Trace("bound-int-rsi") << "Value is " << l
<< " ... " << u
<< std::endl
;
387 bool BoundedIntegers::isGroundRange(Node f
, Node v
) {
388 return isBoundVar(f
,v
) && !getLowerBound(f
,v
).hasBoundVar() && !getUpperBound(f
,v
).hasBoundVar();