dd6db951da1c0a084bcaa296e0692ab0d5b8fb2f
1 /********************* */
2 /*! \file ambqi_builder.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
12 ** \brief Implementation of abstract MBQI builder
16 #include "options/quantifiers_options.h"
17 #include "theory/quantifiers/ambqi_builder.h"
18 #include "theory/quantifiers/term_database.h"
22 using namespace CVC4::kind
;
23 using namespace CVC4::context
;
24 using namespace CVC4::theory
;
25 using namespace CVC4::theory::quantifiers
;
27 void AbsDef::construct_func( FirstOrderModelAbs
* m
, std::vector
< TNode
>& fapps
, unsigned depth
) {
29 Assert( !fapps
.empty() );
30 if( depth
==fapps
[0].getNumChildren() ){
31 //if( fapps.size()>1 ){
32 // for( unsigned i=0; i<fapps.size(); i++ ){
33 // std::cout << "...." << fapps[i] << " -> " << m->getRepresentativeId( fapps[i] ) << std::endl;
36 //get representative in model for this term
37 d_value
= m
->getRepresentativeId( fapps
[0] );
38 Assert( d_value
!=val_none
);
40 TypeNode tn
= fapps
[0][depth
].getType();
41 std::map
< unsigned, std::vector
< TNode
> > fapp_child
;
43 //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
44 for( unsigned i
=0; i
<fapps
.size(); i
++ ){
45 unsigned r
= m
->getRepresentativeId( fapps
[i
][depth
] );
47 fapp_child
[r
].push_back( fapps
[i
] );
51 std::map
< unsigned, unsigned > fapp_child_index
;
52 unsigned def
= m
->d_domain
[ tn
];
53 unsigned minSize
= fapp_child
.begin()->second
.size();
54 unsigned minSizeIndex
= fapp_child
.begin()->first
;
55 for( std::map
< unsigned, std::vector
< TNode
> >::iterator it
= fapp_child
.begin(); it
!= fapp_child
.end(); ++it
){
56 fapp_child_index
[it
->first
] = ( 1 << it
->first
);
57 def
= def
& ~( 1 << it
->first
);
58 if( it
->second
.size()<minSize
){
59 minSize
= it
->second
.size();
60 minSizeIndex
= it
->first
;
63 fapp_child_index
[minSizeIndex
] |= def
;
64 d_default
= fapp_child_index
[minSizeIndex
];
67 for( std::map
< unsigned, std::vector
< TNode
> >::iterator it
= fapp_child
.begin(); it
!= fapp_child
.end(); ++it
){
68 Trace("abs-model-debug") << "Construct " << it
->first
<< " : " << fapp_child_index
[it
->first
] << " : ";
69 debugPrintUInt( "abs-model-debug", m
->d_rep_set
.d_type_reps
[tn
].size(), fapp_child_index
[it
->first
] );
70 Trace("abs-model-debug") << " : " << it
->second
.size() << " terms." << std::endl
;
71 d_def
[fapp_child_index
[it
->first
]].construct_func( m
, it
->second
, depth
+1 );
76 void AbsDef::simplify( FirstOrderModelAbs
* m
, TNode q
, TNode n
, unsigned depth
) {
77 if( d_value
==val_none
&& !d_def
.empty() ){
79 std::map
< unsigned, AbsDef
>::iterator defd
= d_def
.find( d_default
);
80 Assert( defd
!=d_def
.end() );
81 unsigned newDef
= d_default
;
82 std::vector
< unsigned > to_erase
;
83 defd
->second
.simplify( m
, q
, n
, depth
+1 );
84 int defVal
= defd
->second
.d_value
;
85 bool isConstant
= ( defVal
!=val_none
);
87 for( std::map
< unsigned, AbsDef
>::iterator it
= d_def
.begin(); it
!= d_def
.end(); ++it
){
88 if( it
->first
!=d_default
){
89 it
->second
.simplify( m
, q
, n
, depth
+1 );
90 if( it
->second
.d_value
==defVal
&& it
->second
.d_value
!=val_none
){
91 newDef
= newDef
| it
->first
;
92 to_erase
.push_back( it
->first
);
98 if( !to_erase
.empty() ){
100 int defVal
= defd
->second
.d_value
;
101 d_def
.erase( d_default
);
104 d_def
[d_default
].construct_def_entry( m
, q
, n
, defVal
, depth
+1 );
105 //erase redundant entries
106 for( unsigned i
=0; i
<to_erase
.size(); i
++ ){
107 d_def
.erase( to_erase
[i
] );
110 //if constant, propagate the value upwards
119 void AbsDef::debugPrintUInt( const char * c
, unsigned dSize
, unsigned u
) const{
120 for( unsigned i
=0; i
<dSize
; i
++ ){
121 Trace(c
) << ( ( u
& ( 1 << i
) )!=0 ? "1" : "0");
124 //for( unsigned i=0; i<32; i++ ){
125 // Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
130 void AbsDef::debugPrint( const char * c
, FirstOrderModelAbs
* m
, TNode f
, unsigned depth
) const{
132 if( depth
==f
.getNumChildren() ){
133 for( unsigned i
=0; i
<depth
; i
++ ){ Trace(c
) << " ";}
134 Trace(c
) << "V[" << d_value
<< "]" << std::endl
;
136 TypeNode tn
= f
[depth
].getType();
137 unsigned dSize
= m
->d_rep_set
.getNumRepresentatives( tn
);
139 for( std::map
< unsigned, AbsDef
>::const_iterator it
= d_def
.begin(); it
!= d_def
.end(); ++it
){
140 for( unsigned i
=0; i
<depth
; i
++ ){ Trace(c
) << " ";}
141 debugPrintUInt( c
, dSize
, it
->first
);
142 if( it
->first
==d_default
){
145 if( it
->second
.d_value
!=val_none
){
146 Trace(c
) << " -> V[" << it
->second
.d_value
<< "]";
148 Trace(c
) << std::endl
;
149 it
->second
.debugPrint( c
, m
, f
, depth
+1 );
155 bool AbsDef::addInstantiations( FirstOrderModelAbs
* m
, QuantifiersEngine
* qe
, TNode q
, std::vector
< Node
>& terms
, int& inst
, unsigned depth
) {
156 if( inst
==0 || !options::fmfOneInstPerRound() ){
158 //instantiations are all true : ignore this
161 if( depth
==q
[0].getNumChildren() ){
162 if( qe
->addInstantiation( q
, terms
) ){
163 Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl
;
167 Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl
;
172 bool osuccess
= true;
173 TypeNode tn
= m
->getVariable( q
, depth
).getType();
174 for( std::map
< unsigned, AbsDef
>::iterator it
= d_def
.begin(); it
!= d_def
.end(); ++it
){
180 index
= getId( it
->first
, index
);
182 Assert( index
<m
->d_rep_set
.d_type_reps
[tn
].size() );
183 terms
[m
->d_var_order
[q
][depth
]] = m
->d_rep_set
.d_type_reps
[tn
][index
];
184 //terms[depth] = m->d_rep_set.d_type_reps[tn][index];
185 if( !it
->second
.addInstantiations( m
, qe
, q
, terms
, inst
, depth
+1 ) && inst
==0 ){
186 //if we are incomplete, and have not yet added an instantiation, keep trying
188 Trace("ambqi-inst-debug") << "At depth " << depth
<< ", failed branch, no instantiations and incomplete, increment index : " << index
<< std::endl
;
193 }while( !qe
->inConflict() && !success
&& index
<32 );
194 //mark if we are incomplete
195 osuccess
= osuccess
&& success
;
205 void AbsDef::construct_entry( std::vector
< unsigned >& entry
, std::vector
< bool >& entry_def
, int v
, unsigned depth
) {
206 if( depth
==entry
.size() ){
209 d_def
[entry
[depth
]].construct_entry( entry
, entry_def
, v
, depth
+1 );
210 if( entry_def
[depth
] ){
211 d_default
= entry
[depth
];
216 void AbsDef::get_defs( unsigned u
, std::vector
< AbsDef
* >& defs
) {
217 for( std::map
< unsigned, AbsDef
>::iterator it
= d_def
.begin(); it
!= d_def
.end(); ++it
){
218 if( ( u
& it
->first
)!=0 ){
219 Assert( (u
& it
->first
)==u
);
220 defs
.push_back( &it
->second
);
225 void AbsDef::construct_normalize( FirstOrderModelAbs
* m
, TNode q
, std::vector
< AbsDef
* >& defs
, unsigned depth
) {
226 if( depth
==q
[0].getNumChildren() ){
227 Assert( defs
.size()==1 );
228 d_value
= defs
[0]->d_value
;
230 TypeNode tn
= m
->getVariable( q
, depth
).getType();
231 unsigned def
= m
->d_domain
[tn
];
232 for( unsigned i
=0; i
<defs
.size(); i
++ ){
233 //process each simple child
234 for( std::map
< unsigned, AbsDef
>::iterator itd
= defs
[i
]->d_def
.begin(); itd
!= defs
[i
]->d_def
.end(); ++itd
){
235 if( isSimple( itd
->first
) && ( def
& itd
->first
)!=0 ){
236 def
&= ~( itd
->first
);
238 std::vector
< AbsDef
* > cdefs
;
239 for( unsigned j
=0; j
<defs
.size(); j
++ ){
240 defs
[j
]->get_defs( itd
->first
, cdefs
);
242 d_def
[itd
->first
].construct_normalize( m
, q
, cdefs
, depth
+1 );
244 d_default
= itd
->first
;
255 //process the default
256 std::vector
< AbsDef
* > cdefs
;
257 for( unsigned j
=0; j
<defs
.size(); j
++ ){
258 defs
[j
]->get_defs( d_default
, cdefs
);
260 d_def
[d_default
].construct_normalize( m
, q
, cdefs
, depth
+1 );
265 void AbsDef::construct_def_entry( FirstOrderModelAbs
* m
, TNode q
, TNode n
, int v
, unsigned depth
) {
267 if( depth
<n
.getNumChildren() ){
268 TypeNode tn
= q
.isNull() ? n
[depth
].getType() : m
->getVariable( q
, depth
).getType();
269 unsigned dom
= m
->d_domain
[tn
] ;
270 d_def
[dom
].construct_def_entry( m
, q
, n
, v
, depth
+1 );
275 void AbsDef::apply_ucompose( FirstOrderModelAbs
* m
, TNode q
,
276 std::vector
< unsigned >& entry
, std::vector
< bool >& entry_def
,
277 std::vector
< int >& terms
, std::map
< unsigned, int >& vchildren
,
278 AbsDef
* a
, unsigned depth
) {
279 if( depth
==terms
.size() ){
280 if( Trace
.isOn("ambqi-check-debug2") ){
281 Trace("ambqi-check-debug2") << "Add entry ( ";
282 for( unsigned i
=0; i
<entry
.size(); i
++ ){
283 unsigned dSize
= m
->d_rep_set
.d_type_reps
[m
->getVariable( q
, i
).getType()].size();
284 debugPrintUInt( "ambqi-check-debug2", dSize
, entry
[i
] );
285 Trace("ambqi-check-debug2") << " ";
287 Trace("ambqi-check-debug2") << ")" << std::endl
;
289 a
->construct_entry( entry
, entry_def
, d_value
);
292 if( terms
[depth
]==val_none
){
294 std::map
< unsigned, int >::iterator itv
= vchildren
.find( depth
);
295 Assert( itv
!=vchildren
.end() );
296 unsigned prev_v
= entry
[itv
->second
];
297 bool prev_vd
= entry_def
[itv
->second
];
298 for( std::map
< unsigned, AbsDef
>::iterator it
= d_def
.begin(); it
!= d_def
.end(); ++it
){
299 entry
[itv
->second
] = it
->first
& prev_v
;
300 entry_def
[itv
->second
] = ( it
->first
==d_default
) && prev_vd
;
301 if( entry
[itv
->second
]!=0 ){
302 it
->second
.apply_ucompose( m
, q
, entry
, entry_def
, terms
, vchildren
, a
, depth
+1 );
305 entry
[itv
->second
] = prev_v
;
306 entry_def
[itv
->second
] = prev_vd
;
308 id
= (unsigned)terms
[depth
];
310 unsigned fid
= 1 << id
;
311 std::map
< unsigned, AbsDef
>::iterator it
= d_def
.find( fid
);
312 if( it
!=d_def
.end() ){
313 it
->second
.apply_ucompose( m
, q
, entry
, entry_def
, terms
, vchildren
, a
, depth
+1 );
315 d_def
[d_default
].apply_ucompose( m
, q
, entry
, entry_def
, terms
, vchildren
, a
, depth
+1 );
321 void AbsDef::construct_var_eq( FirstOrderModelAbs
* m
, TNode q
, unsigned v1
, unsigned v2
, int curr
, int currv
, unsigned depth
) {
322 if( depth
==q
[0].getNumChildren() ){
323 Assert( currv
!=val_none
);
326 TypeNode tn
= m
->getVariable( q
, depth
).getType();
327 unsigned dom
= m
->d_domain
[tn
];
328 int vindex
= depth
==v1
? 0 : ( depth
==v2
? 1 : val_none
);
329 if( vindex
==val_none
){
330 d_def
[dom
].construct_var_eq( m
, q
, v1
, v2
, curr
, currv
, depth
+1 );
333 Assert( currv
==val_none
);
334 if( curr
==val_none
){
335 unsigned numReps
= m
->d_rep_set
.getNumRepresentatives( tn
);
336 Assert( numReps
< 32 );
337 for( unsigned i
=0; i
<numReps
; i
++ ){
339 d_def
[curr
].construct_var_eq( m
, q
, v1
, v2
, curr
, currv
, depth
+1 );
343 d_def
[curr
].construct_var_eq( m
, q
, v1
, v2
, curr
, 1, depth
+1 );
345 d_def
[dom
].construct_var_eq( m
, q
, v1
, v2
, curr
, 0, depth
+1 );
352 void AbsDef::construct_var( FirstOrderModelAbs
* m
, TNode q
, unsigned v
, int currv
, unsigned depth
) {
353 if( depth
==q
[0].getNumChildren() ){
354 Assert( currv
!=val_none
);
357 TypeNode tn
= m
->getVariable( q
, depth
).getType();
359 unsigned numReps
= m
->d_rep_set
.d_type_reps
[tn
].size();
360 Assert( numReps
>0 && numReps
< 32 );
361 for( unsigned i
=0; i
<numReps
; i
++ ){
362 d_def
[ 1 << i
].construct_var( m
, q
, v
, i
, depth
+1 );
364 d_default
= 1 << (numReps
- 1);
366 unsigned dom
= m
->d_domain
[tn
];
367 d_def
[dom
].construct_var( m
, q
, v
, currv
, depth
+1 );
373 void AbsDef::construct_compose( FirstOrderModelAbs
* m
, TNode q
, TNode n
, AbsDef
* f
,
374 std::map
< unsigned, AbsDef
* >& children
,
375 std::map
< unsigned, int >& bchildren
, std::map
< unsigned, int >& vchildren
,
376 std::vector
< unsigned >& entry
, std::vector
< bool >& entry_def
) {
377 if( n
.getKind()==OR
|| n
.getKind()==AND
){
379 for( std::map
< unsigned, AbsDef
* >::iterator it
= children
.begin(); it
!= children
.end(); ++it
){
380 if( ( it
->second
->d_value
==0 && n
.getKind()==AND
) ||
381 ( it
->second
->d_value
==1 && n
.getKind()==OR
) ){
382 //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl;
383 unsigned count
= q
[0].getNumChildren() - entry
.size();
384 for( unsigned i
=0; i
<count
; i
++ ){
385 entry
.push_back( m
->d_domain
[m
->getVariable( q
, entry
.size() ).getType()] );
386 entry_def
.push_back( true );
388 construct_entry( entry
, entry_def
, it
->second
->d_value
);
389 for( unsigned i
=0; i
<count
; i
++ ){
391 entry_def
.pop_back();
397 if( entry
.size()==q
[0].getNumChildren() ){
399 if( Trace
.isOn("ambqi-check-debug2") ){
400 for( unsigned i
=0; i
<entry
.size(); i
++ ){ Trace("ambqi-check-debug2") << " "; }
401 Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl
;
403 //we are composing with an uninterpreted function
404 std::vector
< int > values
;
405 values
.resize( n
.getNumChildren(), val_none
);
406 for( std::map
< unsigned, AbsDef
* >::iterator it
= children
.begin(); it
!= children
.end(); ++it
){
407 values
[it
->first
] = it
->second
->d_value
;
409 for( std::map
< unsigned, int >::iterator it
= bchildren
.begin(); it
!= bchildren
.end(); ++it
){
410 values
[it
->first
] = it
->second
;
413 f
->apply_ucompose( m
, q
, entry
, entry_def
, values
, vchildren
, this );
415 bool incomplete
= false;
416 //we are composing with an interpreted function
417 std::vector
< TNode
> values
;
418 values
.resize( n
.getNumChildren(), TNode::null() );
419 for( std::map
< unsigned, AbsDef
* >::iterator it
= children
.begin(); it
!= children
.end(); ++it
){
420 Trace("ambqi-check-debug2") << "composite : " << it
->first
<< " : " << it
->second
->d_value
;
421 if( it
->second
->d_value
>=0 ){
422 if( it
->second
->d_value
>=(int)m
->d_rep_set
.d_type_reps
[n
[it
->first
].getType()].size() ){
423 std::cout
<< it
->second
->d_value
<< " " << n
[it
->first
] << " " << n
[it
->first
].getType() << " " << m
->d_rep_set
.d_type_reps
[n
[it
->first
].getType()].size() << std::endl
;
425 Assert( it
->second
->d_value
<(int)m
->d_rep_set
.d_type_reps
[n
[it
->first
].getType()].size() );
426 values
[it
->first
] = m
->d_rep_set
.d_type_reps
[n
[it
->first
].getType()][it
->second
->d_value
];
430 Trace("ambqi-check-debug2") << " ->> " << values
[it
->first
] << std::endl
;
432 for( std::map
< unsigned, int >::iterator it
= bchildren
.begin(); it
!= bchildren
.end(); ++it
){
433 Trace("ambqi-check-debug2") << " basic : " << it
->first
<< " : " << it
->second
;
435 Assert( it
->second
<(int)m
->d_rep_set
.d_type_reps
[n
[it
->first
].getType()].size() );
436 values
[it
->first
] = m
->d_rep_set
.d_type_reps
[n
[it
->first
].getType()][it
->second
];
440 Trace("ambqi-check-debug2") << " ->> " << values
[it
->first
] << std::endl
;
442 Assert( vchildren
.empty() );
444 Trace("ambqi-check-debug2") << "Construct incomplete entry." << std::endl
;
446 //if a child is unknown, we must return unknown
447 construct_entry( entry
, entry_def
, val_unk
);
449 if( Trace
.isOn("ambqi-check-debug2") ){
450 for( unsigned i
=0; i
<entry
.size(); i
++ ){ Trace("ambqi-check-debug2") << " "; }
451 Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( ";
452 for( unsigned i
=0; i
<values
.size(); i
++ ){
453 Assert( !values
[i
].isNull() );
454 Trace("ambqi-check-debug2") << values
[i
] << " ";
456 Trace("ambqi-check-debug2") << ")..." << std::endl
;
459 Node vv
= NodeManager::currentNM()->mkNode( n
.getKind(), values
);
460 vv
= Rewriter::rewrite( vv
);
461 int v
= m
->getRepresentativeId( vv
);
462 construct_entry( entry
, entry_def
, v
);
466 //take product of arguments
467 TypeNode tn
= m
->getVariable( q
, entry
.size() ).getType();
468 Assert( m
->isValidType( tn
) );
469 unsigned def
= m
->d_domain
[tn
];
470 if( Trace
.isOn("ambqi-check-debug2") ){
471 for( unsigned i
=0; i
<entry
.size(); i
++ ){ Trace("ambqi-check-debug2") << " "; }
472 Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl
;
474 for( std::map
< unsigned, AbsDef
* >::iterator it
= children
.begin(); it
!= children
.end(); ++it
){
475 Assert( it
->second
!=NULL
);
477 for( std::map
< unsigned, AbsDef
>::iterator itd
= it
->second
->d_def
.begin(); itd
!= it
->second
->d_def
.end(); ++itd
){
478 if( itd
->first
!=it
->second
->d_default
&& ( def
& itd
->first
)!=0 ){
479 def
&= ~( itd
->first
);
481 std::map
< unsigned, AbsDef
* > cchildren
;
482 for( std::map
< unsigned, AbsDef
* >::iterator it2
= children
.begin(); it2
!= children
.end(); ++it2
){
483 Assert( it2
->second
!=NULL
);
484 std::map
< unsigned, AbsDef
>::iterator itdf
= it2
->second
->d_def
.find( itd
->first
);
485 if( itdf
!=it2
->second
->d_def
.end() ){
486 cchildren
[it2
->first
] = &itdf
->second
;
488 Assert( it2
->second
->getDefault()!=NULL
);
489 cchildren
[it2
->first
] = it2
->second
->getDefault();
492 if( Trace
.isOn("ambqi-check-debug2") ){
493 for( unsigned i
=0; i
<entry
.size(); i
++ ){ Trace("ambqi-check-debug2") << " "; }
494 Trace("ambqi-check-debug2") << "...process : ";
495 debugPrintUInt("ambqi-check-debug2", m
->d_rep_set
.d_type_reps
[tn
].size(), itd
->first
);
496 Trace("ambqi-check-debug2") << " " << children
.size() << " " << cchildren
.size() << std::endl
;
498 entry
.push_back( itd
->first
);
499 entry_def
.push_back( def
==0 );
500 construct_compose( m
, q
, n
, f
, cchildren
, bchildren
, vchildren
, entry
, entry_def
);
501 entry_def
.pop_back();
513 if( Trace
.isOn("ambqi-check-debug2") ){
514 for( unsigned i
=0; i
<entry
.size(); i
++ ){ Trace("ambqi-check-debug2") << " "; }
515 Trace("ambqi-check-debug2") << "Make default argument" << std::endl
;
517 std::map
< unsigned, AbsDef
* > cdchildren
;
518 for( std::map
< unsigned, AbsDef
* >::iterator it
= children
.begin(); it
!= children
.end(); ++it
){
519 Assert( it
->second
->getDefault()!=NULL
);
520 cdchildren
[it
->first
] = it
->second
->getDefault();
522 if( Trace
.isOn("ambqi-check-debug2") ){
523 for( unsigned i
=0; i
<entry
.size(); i
++ ){ Trace("ambqi-check-debug2") << " "; }
524 Trace("ambqi-check-debug2") << "...process default : ";
525 debugPrintUInt("ambqi-check-debug2", m
->d_rep_set
.getNumRepresentatives( tn
), def
);
526 Trace("ambqi-check-debug2") << " " << children
.size() << " " << cdchildren
.size() << std::endl
;
528 entry
.push_back( def
);
529 entry_def
.push_back( true );
530 construct_compose( m
, q
, n
, f
, cdchildren
, bchildren
, vchildren
, entry
, entry_def
);
531 entry_def
.pop_back();
537 bool AbsDef::construct( FirstOrderModelAbs
* m
, TNode q
, TNode n
, AbsDef
* f
,
538 std::map
< unsigned, AbsDef
* >& children
,
539 std::map
< unsigned, int >& bchildren
, std::map
< unsigned, int >& vchildren
,
541 if( Trace
.isOn("ambqi-check-debug3") ){
542 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
543 Trace("ambqi-check-debug3") << i
<< " : ";
544 Trace("ambqi-check-debug3") << ((children
.find( i
)!=children
.end()) ? "X" : ".");
545 if( bchildren
.find( i
)!=bchildren
.end() ){
546 Trace("ambqi-check-debug3") << bchildren
[i
];
548 Trace("ambqi-check-debug3") << ".";
550 if( vchildren
.find( i
)!=vchildren
.end() ){
551 Trace("ambqi-check-debug3") << vchildren
[i
];
553 Trace("ambqi-check-debug3") << ".";
555 Trace("ambqi-check-debug3") << std::endl
;
557 Trace("ambqi-check-debug3") << "varChCount : " << varChCount
<< std::endl
;
559 if( varChCount
==0 || f
){
561 if( n
.getKind()==AND
|| n
.getKind()==OR
){
562 for( std::map
< unsigned, int >::iterator it
= bchildren
.begin(); it
!=bchildren
.end(); ++it
){
563 if( ( it
->second
==0 && n
.getKind()==AND
) ||
564 ( it
->second
==1 && n
.getKind()==OR
) ){
565 construct_def_entry( m
, q
, q
[0], it
->second
);
570 Trace("ambqi-check-debug2") << "Construct compose..." << std::endl
;
571 std::vector
< unsigned > entry
;
572 std::vector
< bool > entry_def
;
573 if( f
&& varChCount
>0 ){
575 unorm
.construct_compose( m
, q
, n
, f
, children
, bchildren
, vchildren
, entry
, entry_def
);
577 std::vector
< AbsDef
* > defs
;
578 defs
.push_back( &unorm
);
579 construct_normalize( m
, q
, defs
);
581 construct_compose( m
, q
, n
, f
, children
, bchildren
, vchildren
, entry
, entry_def
);
583 Assert( is_normalized() );
584 //if( !is_normalized() ){
585 // std::cout << "NON NORMALIZED DEFINITION" << std::endl;
589 }else if( varChCount
==1 && n
.getKind()==EQUAL
){
590 Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl
;
591 //expand the variable based on its finite domain
593 a
.construct_var( m
, q
, vchildren
.begin()->second
, val_none
);
594 children
[vchildren
.begin()->first
] = &a
;
596 std::vector
< unsigned > entry
;
597 std::vector
< bool > entry_def
;
598 Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl
;
599 construct_compose( m
, q
, n
, f
, children
, bchildren
, vchildren
, entry
, entry_def
);
601 }else if( varChCount
==2 && n
.getKind()==EQUAL
){
602 Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl
;
603 //efficient expansion of the equality
604 construct_var_eq( m
, q
, vchildren
[0], vchildren
[1], val_none
, val_none
);
611 void AbsDef::negate() {
612 for( std::map
< unsigned, AbsDef
>::iterator it
= d_def
.begin(); it
!= d_def
.end(); ++it
){
617 }else if( d_value
==1 ){
622 Node
AbsDef::getFunctionValue( FirstOrderModelAbs
* m
, TNode op
, std::vector
< Node
>& vars
, unsigned depth
) {
623 if( depth
==vars
.size() ){
624 TypeNode tn
= op
.getType();
625 if( tn
.getNumChildren()>0 ){
626 tn
= tn
[tn
.getNumChildren() - 1];
629 Assert( d_value
<(int)m
->d_rep_set
.d_type_reps
[tn
].size() );
630 if( tn
.isBoolean() ){
631 return NodeManager::currentNM()->mkConst( d_value
==1 );
633 return m
->d_rep_set
.d_type_reps
[tn
][d_value
];
639 TypeNode tn
= vars
[depth
].getType();
641 curr
= d_def
[d_default
].getFunctionValue( m
, op
, vars
, depth
+1 );
642 for( std::map
< unsigned, AbsDef
>::iterator it
= d_def
.begin(); it
!= d_def
.end(); ++it
){
643 if( it
->first
!=d_default
){
644 unsigned id
= getId( it
->first
);
645 Assert( id
<m
->d_rep_set
.d_type_reps
[tn
].size() );
646 TNode n
= m
->d_rep_set
.d_type_reps
[tn
][id
];
647 Node fv
= it
->second
.getFunctionValue( m
, op
, vars
, depth
+1 );
648 if( !curr
.isNull() && !fv
.isNull() ){
649 curr
= NodeManager::currentNM()->mkNode( ITE
, vars
[depth
].eqNode( n
), fv
, curr
);
659 bool AbsDef::isSimple( unsigned n
) {
660 return (n
& (n
- 1))==0;
663 unsigned AbsDef::getId( unsigned n
, unsigned start
, unsigned end
) {
665 while( (n
& ( 1 << start
)) == 0 ){
674 Node
AbsDef::evaluate( FirstOrderModelAbs
* m
, TypeNode retTyp
, std::vector
< Node
>& args
) {
675 std::vector
< unsigned > iargs
;
676 for( unsigned i
=0; i
<args
.size(); i
++ ){
677 unsigned v
= 1 << m
->getRepresentativeId( args
[i
] );
678 iargs
.push_back( v
);
680 return evaluate( m
, retTyp
, iargs
, 0 );
683 Node
AbsDef::evaluate( FirstOrderModelAbs
* m
, TypeNode retTyp
, std::vector
< unsigned >& iargs
, unsigned depth
) {
684 if( d_value
!=val_none
){
685 if( d_value
==val_unk
){
688 Assert( d_value
>=0 && d_value
<(int)m
->d_rep_set
.d_type_reps
[retTyp
].size() );
689 return m
->d_rep_set
.d_type_reps
[retTyp
][d_value
];
692 std::map
< unsigned, AbsDef
>::iterator it
= d_def
.find( iargs
[depth
] );
693 if( it
==d_def
.end() ){
694 return d_def
[d_default
].evaluate( m
, retTyp
, iargs
, depth
+1 );
696 return it
->second
.evaluate( m
, retTyp
, iargs
, depth
+1 );
701 bool AbsDef::is_normalized() {
702 for( std::map
< unsigned, AbsDef
>::iterator it1
= d_def
.begin(); it1
!= d_def
.end(); ++it1
){
703 if( !it1
->second
.is_normalized() ){
706 for( std::map
< unsigned, AbsDef
>::iterator it2
= d_def
.begin(); it2
!= d_def
.end(); ++it2
){
707 if( it1
->first
!=it2
->first
&& (( it1
->first
& it2
->first
)!=0) ){
715 AbsMbqiBuilder::AbsMbqiBuilder( context::Context
* c
, QuantifiersEngine
* qe
) :
716 QModelBuilder( c
, qe
){
717 d_true
= NodeManager::currentNM()->mkConst( true );
718 d_false
= NodeManager::currentNM()->mkConst( false );
722 //------------------------model construction----------------------------
724 void AbsMbqiBuilder::processBuildModel(TheoryModel
* m
, bool fullModel
) {
725 Trace("ambqi-debug") << "process build model " << fullModel
<< std::endl
;
726 FirstOrderModel
* f
= (FirstOrderModel
*)m
;
727 FirstOrderModelAbs
* fm
= f
->asFirstOrderModelAbs();
729 Trace("ambqi-model") << "Construct model representation..." << std::endl
;
730 //make function values
731 for( std::map
<Node
, AbsDef
* >::iterator it
= fm
->d_models
.begin(); it
!= fm
->d_models
.end(); ++it
) {
732 if( it
->first
.getType().getNumChildren()>1 ){
733 Trace("ambqi-model") << "Construct for " << it
->first
<< "..." << std::endl
;
734 m
->d_uf_models
[ it
->first
] = fm
->getFunctionValue( it
->first
, "$x" );
737 TheoryEngineModelBuilder::processBuildModel( m
, fullModel
);
738 //mark that the model has been set
744 //process representatives
745 fm
->d_rep_id
.clear();
746 fm
->d_domain
.clear();
748 //initialize boolean sort
749 TypeNode b
= d_true
.getType();
750 fm
->d_rep_set
.d_type_reps
[b
].clear();
751 fm
->d_rep_set
.d_type_reps
[b
].push_back( d_false
);
752 fm
->d_rep_set
.d_type_reps
[b
].push_back( d_true
);
753 fm
->d_rep_id
[d_false
] = 0;
754 fm
->d_rep_id
[d_true
] = 1;
756 //initialize unintpreted sorts
757 Trace("ambqi-model") << std::endl
<< "Making representatives..." << std::endl
;
758 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= fm
->d_rep_set
.d_type_reps
.begin();
759 it
!= fm
->d_rep_set
.d_type_reps
.end(); ++it
){
760 if( it
->first
.isSort() ){
761 Assert( !it
->second
.empty() );
763 fm
->d_domain
[it
->first
] = 0;
764 Trace("ambqi-model") << "Representatives for " << it
->first
<< " : " << std::endl
;
765 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
767 fm
->d_domain
[it
->first
] |= ( 1 << i
);
769 Trace("ambqi-model") << i
<< " : " << it
->second
[i
] << std::endl
;
770 fm
->d_rep_id
[it
->second
[i
]] = i
;
772 if( it
->second
.size()>=32 ){
773 fm
->d_domain
.erase( it
->first
);
778 Trace("ambqi-model") << std::endl
<< "Making function definitions..." << std::endl
;
779 //construct the models for functions
780 for( std::map
<Node
, AbsDef
* >::iterator it
= fm
->d_models
.begin(); it
!= fm
->d_models
.end(); ++it
) {
782 Trace("ambqi-model-debug") << "Building Model for " << f
<< std::endl
;
785 //get all (non-redundant) f-applications
786 std::vector
< TNode
> fapps
;
787 Trace("ambqi-model-debug") << "Initial terms: " << std::endl
;
788 for( size_t i
=0; i
<fm
->d_uf_terms
[f
].size(); i
++ ){
789 Node n
= fm
->d_uf_terms
[f
][i
];
790 if( !n
.getAttribute(NoMatchAttribute()) ){
791 Trace("ambqi-model-debug") << " " << n
<< " -> " << fm
->getRepresentativeId( n
) << std::endl
;
792 fapps
.push_back( n
);
796 //choose arbitrary value
797 Node mbt
= d_qe
->getTermDatabase()->getModelBasisOpTerm(f
);
798 Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt
<< std::endl
;
799 fapps
.push_back( mbt
);
802 for( unsigned i
=0; i
<fapps
[0].getNumChildren(); i
++ ){
803 if( fm
->d_domain
.find( fapps
[0][i
].getType() )==fm
->d_domain
.end() ){
804 Trace("ambqi-model") << "Interpretation of " << f
<< " is not valid.";
805 Trace("ambqi-model") << " (domain for " << fapps
[0][i
].getType() << " is too large)." << std::endl
;
810 fm
->d_models_valid
[f
] = fValid
;
812 //construct the ambqi model
813 it
->second
->construct_func( fm
, fapps
);
814 Trace("ambqi-model-debug") << "Interpretation of " << f
<< " : " << std::endl
;
815 it
->second
->debugPrint("ambqi-model-debug", fm
, fapps
[0] );
816 Trace("ambqi-model-debug") << "Simplifying " << f
<< "..." << std::endl
;
817 it
->second
->simplify( fm
, TNode::null(), fapps
[0] );
818 Trace("ambqi-model") << "(Simplified) interpretation of " << f
<< " : " << std::endl
;
819 it
->second
->debugPrint("ambqi-model", fm
, fapps
[0] );
822 if( Debug.isOn("ambqi-model-debug") ){
823 for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
824 Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
825 Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
826 Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
836 //--------------------model checking---------------------------------------
838 //do exhaustive instantiation
839 bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel
* fm
, Node q
, int effort
) {
840 Trace("ambqi-check") << "Exhaustive instantiation " << q
<< " " << effort
<< std::endl
;
842 FirstOrderModelAbs
* fma
= fm
->asFirstOrderModelAbs();
843 bool quantValid
= true;
844 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
845 if( !fma
->isValidType( q
[0][i
].getType() ) ){
847 Trace("ambqi-inst") << "Interpretation of " << q
<< " is not valid because of type " << q
[0][i
].getType() << std::endl
;
852 Trace("ambqi-check") << "Compute interpretation..." << std::endl
;
854 doCheck( fma
, q
, ad
, q
[1] );
855 //now process entries
856 Trace("ambqi-inst-debug") << "...Current : " << d_addedLemmas
<< std::endl
;
857 Trace("ambqi-inst") << "Interpretation of " << q
<< " is : " << std::endl
;
858 ad
.debugPrint( "ambqi-inst", fma
, q
[0] );
859 Trace("ambqi-inst") << std::endl
;
860 Trace("ambqi-check") << "Add instantiations..." << std::endl
;
862 quantValid
= ad
.addInstantiations( fma
, d_qe
, q
, lem
);
863 Trace("ambqi-inst") << "...Added " << lem
<< " lemmas." << std::endl
;
865 //if we were incomplete but added at least one lemma, we are ok
868 d_addedLemmas
+= lem
;
869 Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas
<< std::endl
;
876 bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs
* m
, TNode q
, AbsDef
& ad
, TNode n
) {
877 Assert( n
.getKind()!=FORALL
);
878 if( n
.getKind()==NOT
&& n
[0].getKind()!=FORALL
){
879 doCheck( m
, q
, ad
, n
[0] );
883 std::map
< unsigned, AbsDef
> children
;
884 std::map
< unsigned, int > bchildren
;
885 std::map
< unsigned, int > vchildren
;
887 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
888 if( n
[i
].getKind()==FORALL
){
889 bchildren
[i
] = AbsDef::val_unk
;
890 }else if( n
[i
].getKind() == BOUND_VARIABLE
){
892 vchildren
[i
] = m
->d_var_index
[q
][ m
->getVariableId( q
, n
[i
] ) ];
893 //vchildren[i] = m->getVariableId( q, n[i] );
894 }else if( m
->hasTerm( n
[i
] ) ){
895 bchildren
[i
] = m
->getRepresentativeId( n
[i
] );
897 if( !doCheck( m
, q
, children
[i
], n
[i
] ) ){
898 bchildren
[i
] = AbsDef::val_unk
;
903 //convert to pointers
904 std::map
< unsigned, AbsDef
* > pchildren
;
905 for( std::map
< unsigned, AbsDef
>::iterator it
= children
.begin(); it
!= children
.end(); ++it
){
906 pchildren
[it
->first
] = &it
->second
;
908 //construct the interpretation
909 Trace("ambqi-check-debug") << "Compute Interpretation of " << n
<< " " << n
.getKind() << std::endl
;
910 if( n
.getKind() == APPLY_UF
|| n
.getKind() == VARIABLE
|| n
.getKind() == SKOLEM
){
912 if( n
.getKind() == APPLY_UF
){
913 op
= n
.getOperator();
917 //uninterpreted compose
918 if( m
->d_models_valid
[op
] ){
919 ad
.construct( m
, q
, n
, m
->d_models
[op
], pchildren
, bchildren
, vchildren
, varChCount
);
921 Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n
<< " (no function model)" << std::endl
;
924 }else if( !ad
.construct( m
, q
, n
, NULL
, pchildren
, bchildren
, vchildren
, varChCount
) ){
925 Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n
<< " (variables are children of interpreted symbol)" << std::endl
;
928 Trace("ambqi-check-try") << "Interpretation for " << n
<< " is : " << std::endl
;
929 ad
.debugPrint("ambqi-check-try", m
, q
[0] );
930 ad
.simplify( m
, q
, q
[0] );
931 Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n
<< " is : " << std::endl
;
932 ad
.debugPrint("ambqi-check-debug", m
, q
[0] );
933 Trace("ambqi-check-debug") << std::endl
;