d_def.clear();\r
Assert( !fapps.empty() );\r
if( depth==fapps[0].getNumChildren() ){\r
+ //if( fapps.size()>1 ){\r
+ // for( unsigned i=0; i<fapps.size(); i++ ){\r
+ // std::cout << "...." << fapps[i] << " -> " << m->getRepresentativeId( fapps[i] ) << std::endl;\r
+ // }\r
+ //}\r
//get representative in model for this term\r
- Assert( fapps.size()==1 );\r
d_value = m->getRepresentativeId( fapps[0] );\r
- Assert( d_value!=-1 );\r
+ Assert( d_value!=val_none );\r
}else{\r
TypeNode tn = fapps[0][depth].getType();\r
std::map< unsigned, std::vector< TNode > > fapp_child;\r
}\r
}\r
\r
-void AbsDef::simplify( FirstOrderModelAbs * m, Node q, unsigned depth ) {\r
- if( d_value==-1 ){\r
+void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {\r
+ if( d_value==val_none && !d_def.empty() ){\r
//process the default\r
std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );\r
+ Assert( defd!=d_def.end() );\r
unsigned newDef = d_default;\r
std::vector< unsigned > to_erase;\r
- defd->second.simplify( m, q, depth+1 );\r
- bool isConstant = ( defd->second.d_value!=-1 );\r
+ defd->second.simplify( m, n, depth+1 );\r
+ int defVal = defd->second.d_value;\r
+ bool isConstant = ( defVal!=val_none );\r
//process each child\r
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
if( it->first!=d_default ){\r
- it->second.simplify( m, q, depth+1 );\r
- if( it->second.d_value==defd->second.d_value && it->second.d_value!=-1 ){\r
- newDef = d_default | it->first;\r
+ it->second.simplify( m, n, depth+1 );\r
+ if( it->second.d_value==defVal && it->second.d_value!=val_none ){\r
+ newDef = newDef | it->first;\r
to_erase.push_back( it->first );\r
}else{\r
isConstant = false;\r
d_def.erase( d_default );\r
//set new default\r
d_default = newDef;\r
- d_def[d_default].construct_def_entry( m, q, defVal, depth+1 );\r
+ d_def[d_default].construct_def_entry( m, n, defVal, depth+1 );\r
//erase redundant entries\r
for( unsigned i=0; i<to_erase.size(); i++ ){\r
d_def.erase( to_erase[i] );\r
}\r
//if constant, propagate the value upwards\r
if( isConstant ){\r
- d_value = defd->second.d_value;\r
+ d_value = defVal;\r
+ }else{\r
+ d_value = val_none;\r
}\r
}\r
}\r
\r
-void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) {\r
+void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{\r
for( unsigned i=0; i<dSize; i++ ){\r
Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");\r
}\r
}\r
\r
-void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, Node f, unsigned depth ) {\r
+void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{\r
if( Trace.isOn(c) ){\r
if( depth==f.getNumChildren() ){\r
for( unsigned i=0; i<depth; i++ ){ Trace(c) << " ";}\r
Trace(c) << "V[" << d_value << "]" << std::endl;\r
}else{\r
TypeNode tn = f[depth].getType();\r
- unsigned dSize = m->d_rep_set.d_type_reps[tn].size();\r
+ unsigned dSize = m->d_rep_set.getNumRepresentatives( tn );\r
Assert( dSize<32 );\r
- for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
+ for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
for( unsigned i=0; i<depth; i++ ){ Trace(c) << " ";}\r
debugPrintUInt( c, dSize, it->first );\r
if( it->first==d_default ){\r
Trace(c) << "*";\r
}\r
- if( it->second.d_value!=-1 ){\r
+ if( it->second.d_value!=val_none ){\r
Trace(c) << " -> V[" << it->second.d_value << "]";\r
}\r
Trace(c) << std::endl;\r
}\r
}\r
\r
-int AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, std::vector< Node >& terms, unsigned depth ) {\r
- if( depth==q[0].getNumChildren() ){\r
- if( d_value!=1 ){\r
+bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) {\r
+ if( d_value==1 ){\r
+ //instantiations are all true : ignore this\r
+ return true;\r
+ }else{\r
+ if( depth==q[0].getNumChildren() ){\r
if( qe->addInstantiation( q, terms ) ){\r
- return 1;\r
+ Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;\r
+ inst++;\r
+ return true;\r
+ }else{\r
+ Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;\r
+ //we are incomplete\r
+ return false;\r
}\r
+ }else{\r
+ bool osuccess = true;\r
+ TypeNode tn = q[0][depth].getType();\r
+ for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
+ //get witness term\r
+ unsigned index = 0;\r
+ bool success;\r
+ do {\r
+ success = false;\r
+ index = getId( it->first, index );\r
+ if( index<32 ){\r
+ Assert( index<m->d_rep_set.d_type_reps[tn].size() );\r
+ terms.push_back( m->d_rep_set.d_type_reps[tn][index] );\r
+ if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){\r
+ //if we are incomplete, and have not yet added an instantiation, keep trying\r
+ index++;\r
+ Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;\r
+ }else{\r
+ success = true;\r
+ }\r
+ terms.pop_back();\r
+ }\r
+ }while( !success && index<32 );\r
+ //mark if we are incomplete\r
+ osuccess = osuccess && success;\r
+ }\r
+ return osuccess;\r
}\r
- return 0;\r
- }else{\r
- int sum = 0;\r
- TypeNode tn = q[0][depth].getType();\r
- for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
- //get witness term\r
- int index = getId( it->first );\r
- terms.push_back( m->d_rep_set.d_type_reps[tn][index] );\r
- sum += it->second.addInstantiations( m, qe, q, terms, depth+1 );\r
- terms.pop_back();\r
- }\r
- return sum;\r
}\r
}\r
\r
}\r
}\r
\r
-void AbsDef::construct_def_entry( FirstOrderModelAbs * m, Node q, int v, unsigned depth ) {\r
+void AbsDef::get_defs( unsigned u, std::vector< AbsDef * >& defs ) {\r
+ for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
+ if( ( u & it->first )!=0 ){\r
+ Assert( (u & it->first)==u );\r
+ defs.push_back( &it->second );\r
+ }\r
+ }\r
+}\r
+\r
+void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth ) {\r
if( depth==q[0].getNumChildren() ){\r
- d_value = v;\r
+ Assert( defs.size()==1 );\r
+ d_value = defs[0]->d_value;\r
}else{\r
- unsigned dom = m->d_domain[q[0][depth].getType()];\r
- d_def[dom].construct_def_entry( m, q, v, depth+1 );\r
+ TypeNode tn = q[0][depth].getType();\r
+ unsigned def = m->d_domain[tn];\r
+ for( unsigned i=0; i<defs.size(); i++ ){\r
+ //process each simple child\r
+ for( std::map< unsigned, AbsDef >::iterator itd = defs[i]->d_def.begin(); itd != defs[i]->d_def.end(); ++itd ){\r
+ if( isSimple( itd->first ) && ( def & itd->first )!=0 ){\r
+ def &= ~( itd->first );\r
+ //process this value\r
+ std::vector< AbsDef * > cdefs;\r
+ for( unsigned j=0; j<defs.size(); j++ ){\r
+ defs[j]->get_defs( itd->first, cdefs );\r
+ }\r
+ d_def[itd->first].construct_normalize( m, q, cdefs, depth+1 );\r
+ if( def==0 ){\r
+ d_default = itd->first;\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ if( def==0 ){\r
+ break;\r
+ }\r
+ }\r
+ if( def!=0 ){\r
+ d_default = def;\r
+ //process the default\r
+ std::vector< AbsDef * > cdefs;\r
+ for( unsigned j=0; j<defs.size(); j++ ){\r
+ defs[j]->get_defs( d_default, cdefs );\r
+ }\r
+ d_def[d_default].construct_normalize( m, q, cdefs, depth+1 );\r
+ }\r
+ }\r
+}\r
+\r
+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth ) {\r
+ d_value = v;\r
+ if( depth<n.getNumChildren() ){\r
+ unsigned dom = m->d_domain[n[depth].getType()];\r
+ d_def[dom].construct_def_entry( m, n, v, depth+1 );\r
d_default = dom;\r
}\r
}\r
\r
-void AbsDef::apply_ucompose( std::vector< unsigned >& entry, std::vector< bool >& entry_def,\r
+void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q,\r
+ std::vector< unsigned >& entry, std::vector< bool >& entry_def,\r
std::vector< int >& terms, std::map< unsigned, int >& vchildren,\r
AbsDef * a, unsigned depth ) {\r
if( depth==terms.size() ){\r
+ if( Trace.isOn("ambqi-check-debug2") ){\r
+ Trace("ambqi-check-debug2") << "Add entry ( ";\r
+ for( unsigned i=0; i<entry.size(); i++ ){\r
+ unsigned dSize = m->d_rep_set.d_type_reps[q[0][i].getType()].size();\r
+ debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] );\r
+ Trace("ambqi-check-debug2") << " ";\r
+ }\r
+ Trace("ambqi-check-debug2") << ")" << std::endl;\r
+ }\r
a->construct_entry( entry, entry_def, d_value );\r
}else{\r
unsigned id;\r
- if( terms[depth]==-1 ){\r
+ if( terms[depth]==val_none ){\r
//a variable\r
std::map< unsigned, int >::iterator itv = vchildren.find( depth );\r
Assert( itv!=vchildren.end() );\r
entry[itv->second] = it->first & prev_v;\r
entry_def[itv->second] = ( it->first==d_default ) && prev_vd;\r
if( entry[itv->second]!=0 ){\r
- it->second.apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 );\r
+ it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );\r
}\r
}\r
entry[itv->second] = prev_v;\r
unsigned fid = 1 << id;\r
std::map< unsigned, AbsDef >::iterator it = d_def.find( fid );\r
if( it!=d_def.end() ){\r
- it->second.apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 );\r
+ it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );\r
}else{\r
- d_def[d_default].apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 );\r
+ d_def[d_default].apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );\r
}\r
}\r
}\r
}\r
\r
-void AbsDef::construct_var_eq( FirstOrderModelAbs * m, Node q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) {\r
+void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) {\r
if( depth==q[0].getNumChildren() ){\r
- Assert( currv!=-1 );\r
+ Assert( currv!=val_none );\r
d_value = currv;\r
}else{\r
TypeNode tn = q[0][depth].getType();\r
unsigned dom = m->d_domain[tn];\r
- int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : -1 );\r
- if( vindex==-1 ){\r
+ int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none );\r
+ if( vindex==val_none ){\r
d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );\r
d_default = dom;\r
}else{\r
- Assert( currv==-1 );\r
- if( curr==-1 ){\r
+ Assert( currv==val_none );\r
+ if( curr==val_none ){\r
unsigned numReps = m->d_rep_set.d_type_reps[tn].size();\r
Assert( numReps < 32 );\r
for( unsigned i=0; i<numReps; i++ ){\r
}\r
}\r
\r
-void AbsDef::construct_var( FirstOrderModelAbs * m, Node q, unsigned v, int currv, unsigned depth ) {\r
+void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth ) {\r
if( depth==q[0].getNumChildren() ){\r
- Assert( currv!=-1 );\r
+ Assert( currv!=val_none );\r
d_value = currv;\r
}else{\r
TypeNode tn = q[0][depth].getType();\r
for( unsigned i=0; i<numReps; i++ ){\r
d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );\r
}\r
- d_default = 1 << (numReps-1);\r
+ d_default = 1 << (numReps - 1);\r
}else{\r
unsigned dom = m->d_domain[tn];\r
d_def[dom].construct_var( m, q, v, currv, depth+1 );\r
}\r
}\r
\r
-void AbsDef::construct_compose( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f,\r
+void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,\r
std::map< unsigned, AbsDef * >& children,\r
std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,\r
- std::vector< unsigned >& entry, std::vector< bool >& entry_def,\r
- bool incomplete ) {\r
- if( Trace.isOn("ambqi-check-debug2") ){\r
- for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }\r
- }\r
+ std::vector< unsigned >& entry, std::vector< bool >& entry_def ) {\r
if( n.getKind()==OR || n.getKind()==AND ){\r
// short circuiting\r
for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\r
if( ( it->second->d_value==0 && n.getKind()==AND ) ||\r
( it->second->d_value==1 && n.getKind()==OR ) ){\r
+ //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl;\r
+ unsigned count = q[0].getNumChildren() - entry.size();\r
+ for( unsigned i=0; i<count; i++ ){\r
+ entry.push_back( m->d_domain[q[0][entry.size()].getType()] );\r
+ entry_def.push_back( true );\r
+ }\r
construct_entry( entry, entry_def, it->second->d_value );\r
+ for( unsigned i=0; i<count; i++ ){\r
+ entry.pop_back();\r
+ entry_def.pop_back();\r
+ }\r
return;\r
}\r
}\r
}\r
if( entry.size()==q[0].getNumChildren() ){\r
- if( incomplete ){\r
- //if a child is unknown, we must return unknown\r
- construct_entry( entry, entry_def, -1 );\r
- }else{\r
- if( f ){\r
+ if( f ){\r
+ if( Trace.isOn("ambqi-check-debug2") ){\r
+ for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }\r
Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl;\r
- //we are composing with an uninterpreted function\r
- std::vector< int > values;\r
- values.resize( n.getNumChildren(), -1 );\r
- for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\r
- values[it->first] = it->second->d_value;\r
- }\r
- for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){\r
- values[it->first] = it->second;\r
- }\r
- //look up value(s)\r
- f->apply_ucompose( entry, entry_def, values, vchildren, this );\r
- }else{\r
- //we are composing with an interpreted function\r
- std::vector< TNode > values;\r
- values.resize( n.getNumChildren(), TNode::null() );\r
- for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\r
- Assert( it->second->d_value>=0 && it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );\r
+ }\r
+ //we are composing with an uninterpreted function\r
+ std::vector< int > values;\r
+ values.resize( n.getNumChildren(), val_none );\r
+ for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\r
+ values[it->first] = it->second->d_value;\r
+ }\r
+ for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){\r
+ values[it->first] = it->second;\r
+ }\r
+ //look up value(s)\r
+ f->apply_ucompose( m, q, entry, entry_def, values, vchildren, this );\r
+ }else{\r
+ bool incomplete = false;\r
+ //we are composing with an interpreted function\r
+ std::vector< TNode > values;\r
+ values.resize( n.getNumChildren(), TNode::null() );\r
+ for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\r
+ Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value;\r
+ if( it->second->d_value>=0 ){\r
+ if( it->second->d_value>=(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ){\r
+ 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;\r
+ }\r
+ Assert( it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );\r
values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second->d_value];\r
- Trace("ambqi-check-debug2") << it->first << " : " << it->second->d_value << " ->> " << values[it->first] << std::endl;\r
+ }else{\r
+ incomplete = true;\r
}\r
- for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){\r
- Assert( it->second>=0 && it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );\r
+ Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl;\r
+ }\r
+ for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){\r
+ Trace("ambqi-check-debug2") << " basic : " << it->first << " : " << it->second;\r
+ if( it->second>=0 ){\r
+ Assert( it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );\r
values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second];\r
- Trace("ambqi-check-debug2") << it->first << " : " << it->second << " ->> " << values[it->first] << std::endl;\r
+ }else{\r
+ incomplete = true;\r
}\r
- Assert( vchildren.empty() );\r
+ Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl;\r
+ }\r
+ Assert( vchildren.empty() );\r
+ if( incomplete ){\r
+ Trace("ajr-temp") << "Construct incomplete entry." << std::endl;\r
+\r
+ //if a child is unknown, we must return unknown\r
+ construct_entry( entry, entry_def, val_unk );\r
+ }else{\r
if( Trace.isOn("ambqi-check-debug2") ){\r
+ for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }\r
Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( ";\r
for( unsigned i=0; i<values.size(); i++ ){\r
+ Assert( !values[i].isNull() );\r
Trace("ambqi-check-debug2") << values[i] << " ";\r
}\r
Trace("ambqi-check-debug2") << ")..." << std::endl;\r
}else{\r
//take product of arguments\r
TypeNode tn = q[0][entry.size()].getType();\r
+ Assert( m->isValidType( tn ) );\r
unsigned def = m->d_domain[tn];\r
- Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl;\r
+ if( Trace.isOn("ambqi-check-debug2") ){\r
+ for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }\r
+ Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl;\r
+ }\r
for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\r
+ Assert( it->second!=NULL );\r
//process each child\r
for( std::map< unsigned, AbsDef >::iterator itd = it->second->d_def.begin(); itd != it->second->d_def.end(); ++itd ){\r
if( itd->first!=it->second->d_default && ( def & itd->first )!=0 ){\r
//process this value\r
std::map< unsigned, AbsDef * > cchildren;\r
for( std::map< unsigned, AbsDef * >::iterator it2 = children.begin(); it2 != children.end(); ++it2 ){\r
- std::map< unsigned, AbsDef >::iterator itdf = it->second->d_def.find( itd->first );\r
- if( itdf!=it->second->d_def.end() ){\r
- cchildren[it->first] = &itdf->second;\r
+ Assert( it2->second!=NULL );\r
+ std::map< unsigned, AbsDef >::iterator itdf = it2->second->d_def.find( itd->first );\r
+ if( itdf!=it2->second->d_def.end() ){\r
+ cchildren[it2->first] = &itdf->second;\r
}else{\r
- cchildren[it->first] = it2->second->getDefault();\r
+ Assert( it2->second->getDefault()!=NULL );\r
+ cchildren[it2->first] = it2->second->getDefault();\r
}\r
}\r
if( Trace.isOn("ambqi-check-debug2") ){\r
for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }\r
Trace("ambqi-check-debug2") << "...process : ";\r
debugPrintUInt("ambqi-check-debug2", m->d_rep_set.d_type_reps[tn].size(), itd->first );\r
- Trace("ambqi-check-debug2") << std::endl;\r
+ Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl;\r
}\r
entry.push_back( itd->first );\r
entry_def.push_back( def==0 );\r
- construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def, incomplete );\r
+ construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def );\r
entry_def.pop_back();\r
entry.pop_back();\r
if( def==0 ){\r
}\r
}\r
if( def!=0 ){\r
+ if( Trace.isOn("ambqi-check-debug2") ){\r
+ for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }\r
+ Trace("ambqi-check-debug2") << "Make default argument" << std::endl;\r
+ }\r
std::map< unsigned, AbsDef * > cdchildren;\r
for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\r
+ Assert( it->second->getDefault()!=NULL );\r
cdchildren[it->first] = it->second->getDefault();\r
}\r
if( Trace.isOn("ambqi-check-debug2") ){\r
for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }\r
Trace("ambqi-check-debug2") << "...process default : ";\r
- debugPrintUInt("ambqi-check-debug2", m->d_rep_set.d_type_reps[tn].size(), def );\r
- Trace("ambqi-check-debug2") << std::endl;\r
+ debugPrintUInt("ambqi-check-debug2", m->d_rep_set.getNumRepresentatives( tn ), def );\r
+ Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl;\r
}\r
entry.push_back( def );\r
entry_def.push_back( true );\r
- construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def, incomplete );\r
+ construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def );\r
entry_def.pop_back();\r
entry.pop_back();\r
}\r
}\r
}\r
\r
-bool AbsDef::construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f,\r
+bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,\r
std::map< unsigned, AbsDef * >& children,\r
std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,\r
- int varChCount, bool incomplete ) {\r
+ int varChCount ) {\r
+ if( Trace.isOn("ambqi-check-debug3") ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ Trace("ambqi-check-debug3") << i << " : ";\r
+ Trace("ambqi-check-debug3") << ((children.find( i )!=children.end()) ? "X" : ".");\r
+ if( bchildren.find( i )!=bchildren.end() ){\r
+ Trace("ambqi-check-debug3") << bchildren[i];\r
+ }else{\r
+ Trace("ambqi-check-debug3") << ".";\r
+ }\r
+ if( vchildren.find( i )!=vchildren.end() ){\r
+ Trace("ambqi-check-debug3") << vchildren[i];\r
+ }else{\r
+ Trace("ambqi-check-debug3") << ".";\r
+ }\r
+ Trace("ambqi-check-debug3") << std::endl;\r
+ }\r
+ Trace("ambqi-check-debug3") << "varChCount : " << varChCount << std::endl;\r
+ }\r
if( varChCount==0 || f ){\r
//short-circuit\r
if( n.getKind()==AND || n.getKind()==OR ){\r
for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){\r
if( ( it->second==0 && n.getKind()==AND ) ||\r
( it->second==1 && n.getKind()==OR ) ){\r
- construct_def_entry( m, q, it->second );\r
+ construct_def_entry( m, q[0], it->second );\r
return true;\r
}\r
}\r
Trace("ambqi-check-debug2") << "Construct compose..." << std::endl;\r
std::vector< unsigned > entry;\r
std::vector< bool > entry_def;\r
- construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def, incomplete );\r
+ if( f ){\r
+ AbsDef unorm;\r
+ unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );\r
+ //normalize\r
+ std::vector< AbsDef* > defs;\r
+ defs.push_back( &unorm );\r
+ construct_normalize( m, q, defs );\r
+ }else{\r
+ construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );\r
+ }\r
return true;\r
}else if( varChCount==1 && n.getKind()==EQUAL ){\r
Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;\r
//expand the variable based on its finite domain\r
AbsDef a;\r
- a.construct_var( m, q, vchildren.begin()->second, -1 );\r
+ a.construct_var( m, q, vchildren.begin()->second, val_none );\r
children[vchildren.begin()->first] = &a;\r
vchildren.clear();\r
std::vector< unsigned > entry;\r
std::vector< bool > entry_def;\r
Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl;\r
- construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def, incomplete );\r
+ construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );\r
return true;\r
}else if( varChCount==2 && n.getKind()==EQUAL ){\r
Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl;\r
//efficient expansion of the equality\r
- construct_var_eq( m, q, vchildren[0], vchildren[1], -1, -1 );\r
+ construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none );\r
return true;\r
}else{\r
return false;\r
if( depth==vars.size() ){\r
TypeNode tn = op.getType();\r
if( tn.getNumChildren()>0 ){\r
- tn = tn[tn.getNumChildren()-1];\r
+ tn = tn[tn.getNumChildren() - 1];\r
}\r
if( d_value>=0 ){\r
Assert( d_value<(int)m->d_rep_set.d_type_reps[tn].size() );\r
}\r
}\r
\r
-unsigned AbsDef::getId( unsigned n ) {\r
+bool AbsDef::isSimple( unsigned n ) {\r
+ return (n & (n - 1))==0;\r
+}\r
+\r
+unsigned AbsDef::getId( unsigned n, unsigned start ) {\r
Assert( n!=0 );\r
- unsigned index = 0;\r
- while( (n & ( 1 << index )) == 0 ){\r
- index++;\r
+ while( (n & ( 1 << start )) == 0 ){\r
+ start++;\r
+ if( start==32 ){\r
+ return start;\r
+ }\r
}\r
- return index;\r
+ return start;\r
}\r
\r
Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) {\r
}\r
\r
Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< unsigned >& iargs, unsigned depth ) {\r
- if( d_value!=-1 ){\r
- Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() );\r
- return m->d_rep_set.d_type_reps[retTyp][d_value];\r
+ if( d_value!=val_none ){\r
+ if( d_value==val_unk ){\r
+ return Node::null();\r
+ }else{\r
+ Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() );\r
+ return m->d_rep_set.d_type_reps[retTyp][d_value];\r
+ }\r
}else{\r
std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] );\r
if( it==d_def.end() ){\r
Node f = it->first;\r
Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;\r
//reset the model\r
+ it->second->clear();\r
//get all (non-redundant) f-applications\r
std::vector< TNode > fapps;\r
Trace("ambqi-model-debug") << "Initial terms: " << std::endl;\r
it->second->construct_func( fm, fapps );\r
Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;\r
it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );\r
-\r
- it->second->simplify( fm, Node::null() );\r
+ Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;\r
+ it->second->simplify( fm, fapps[0] );\r
Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;\r
it->second->debugPrint("ambqi-model", fm, fapps[0] );\r
\r
AbsDef ad;\r
doCheck( fma, q, ad, q[1] );\r
//now process entries\r
+ Trace("ambqi-inst-debug") << "...Current : " << d_addedLemmas << std::endl;\r
Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;\r
- ad.debugPrint( "ambqi-inst", fma, q );\r
+ ad.debugPrint( "ambqi-inst", fma, q[0] );\r
Trace("ambqi-inst") << std::endl;\r
- int lem = ad.addInstantiations( fma, d_qe, q );\r
+ int lem = 0;\r
+ quantValid = ad.addInstantiations( fma, d_qe, q, lem );\r
Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;\r
+ if( lem>0 ){\r
+ //if we were incomplete but added at least one lemma, we are ok\r
+ quantValid = true;\r
+ }\r
d_addedLemmas += lem;\r
+ Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl;\r
}\r
return quantValid;\r
}\r
std::map< unsigned, AbsDef > children;\r
std::map< unsigned, int > bchildren;\r
std::map< unsigned, int > vchildren;\r
- bool incomplete = false;\r
int varChCount = 0;\r
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
if( n[i].getKind()==FORALL ){\r
- bchildren[i] = -1;\r
- incomplete = true;\r
+ bchildren[i] = AbsDef::val_unk;\r
}else if( n[i].getKind() == BOUND_VARIABLE ){\r
varChCount++;\r
vchildren[i] = m->getVariableId( q, n[i] );\r
bchildren[i] = m->getRepresentativeId( n[i] );\r
}else{\r
if( !doCheck( m, q, children[i], n[i] ) ){\r
- bchildren[i] = -1;\r
- incomplete = true;\r
+ bchildren[i] = AbsDef::val_unk;\r
+ children.erase( i );\r
}\r
}\r
}\r
}\r
//uninterpreted compose\r
if( m->d_models_valid[op] ){\r
- ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount, incomplete );\r
+ ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount );\r
}else{\r
Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl;\r
return false;\r
}\r
- }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount, incomplete ) ){\r
+ }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){\r
Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl;\r
return false;\r
}\r
- Trace("ambqi-check-debug2") << "Interpretation for " << n << " is : " << std::endl;\r
- ad.debugPrint("ambqi-check-debug2", m, q[0] );\r
- ad.simplify( m, q );\r
+ Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;\r
+ ad.debugPrint("ambqi-check-try", m, q[0] );\r
+ ad.simplify( m, q[0] );\r
Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;\r
ad.debugPrint("ambqi-check-debug", m, q[0] );\r
Trace("ambqi-check-debug") << std::endl;\r
projects / cvc5.git / commitdiff