From: Andrew Reynolds Date: Wed, 7 May 2014 18:36:58 +0000 (-0500) Subject: Fixes to ambqi, now solution-sound. X-Git-Tag: cvc5-1.0.0~6927 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e5586535df361348f003d41e4a3f27716f087f5;p=cvc5.git Fixes to ambqi, now solution-sound. --- diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 7a296c934..7813f2cc1 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -28,10 +28,14 @@ void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps d_def.clear(); Assert( !fapps.empty() ); if( depth==fapps[0].getNumChildren() ){ + //if( fapps.size()>1 ){ + // for( unsigned i=0; i " << m->getRepresentativeId( fapps[i] ) << std::endl; + // } + //} //get representative in model for this term - Assert( fapps.size()==1 ); d_value = m->getRepresentativeId( fapps[0] ); - Assert( d_value!=-1 ); + Assert( d_value!=val_none ); }else{ TypeNode tn = fapps[0][depth].getType(); std::map< unsigned, std::vector< TNode > > fapp_child; @@ -69,20 +73,22 @@ void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps } } -void AbsDef::simplify( FirstOrderModelAbs * m, Node q, unsigned depth ) { - if( d_value==-1 ){ +void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) { + if( d_value==val_none && !d_def.empty() ){ //process the default std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default ); + Assert( defd!=d_def.end() ); unsigned newDef = d_default; std::vector< unsigned > to_erase; - defd->second.simplify( m, q, depth+1 ); - bool isConstant = ( defd->second.d_value!=-1 ); + defd->second.simplify( m, n, depth+1 ); + int defVal = defd->second.d_value; + bool isConstant = ( defVal!=val_none ); //process each child for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ if( it->first!=d_default ){ - it->second.simplify( m, q, depth+1 ); - if( it->second.d_value==defd->second.d_value && it->second.d_value!=-1 ){ - newDef = d_default | it->first; + it->second.simplify( m, n, depth+1 ); + if( it->second.d_value==defVal && it->second.d_value!=val_none ){ + newDef = newDef | it->first; to_erase.push_back( it->first ); }else{ isConstant = false; @@ -95,7 +101,7 @@ void AbsDef::simplify( FirstOrderModelAbs * m, Node q, unsigned depth ) { d_def.erase( d_default ); //set new default d_default = newDef; - d_def[d_default].construct_def_entry( m, q, defVal, depth+1 ); + d_def[d_default].construct_def_entry( m, n, defVal, depth+1 ); //erase redundant entries for( unsigned i=0; isecond.d_value; + d_value = defVal; + }else{ + d_value = val_none; } } } -void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) { +void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{ for( unsigned i=0; id_rep_set.d_type_reps[tn].size(); + unsigned dSize = m->d_rep_set.getNumRepresentatives( tn ); Assert( dSize<32 ); - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ + for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){ for( unsigned i=0; ifirst ); if( it->first==d_default ){ Trace(c) << "*"; } - if( it->second.d_value!=-1 ){ + if( it->second.d_value!=val_none ){ Trace(c) << " -> V[" << it->second.d_value << "]"; } Trace(c) << std::endl; @@ -139,25 +147,49 @@ void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, Node f, unsigne } } -int AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, std::vector< Node >& terms, unsigned depth ) { - if( depth==q[0].getNumChildren() ){ - if( d_value!=1 ){ +bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) { + if( d_value==1 ){ + //instantiations are all true : ignore this + return true; + }else{ + if( depth==q[0].getNumChildren() ){ if( qe->addInstantiation( q, terms ) ){ - return 1; + Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl; + inst++; + return true; + }else{ + Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl; + //we are incomplete + return false; } + }else{ + bool osuccess = true; + TypeNode tn = q[0][depth].getType(); + for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ + //get witness term + unsigned index = 0; + bool success; + do { + success = false; + index = getId( it->first, index ); + if( index<32 ){ + Assert( indexd_rep_set.d_type_reps[tn].size() ); + terms.push_back( m->d_rep_set.d_type_reps[tn][index] ); + if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){ + //if we are incomplete, and have not yet added an instantiation, keep trying + index++; + Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl; + }else{ + success = true; + } + terms.pop_back(); + } + }while( !success && index<32 ); + //mark if we are incomplete + osuccess = osuccess && success; + } + return osuccess; } - return 0; - }else{ - int sum = 0; - TypeNode tn = q[0][depth].getType(); - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - //get witness term - int index = getId( it->first ); - terms.push_back( m->d_rep_set.d_type_reps[tn][index] ); - sum += it->second.addInstantiations( m, qe, q, terms, depth+1 ); - terms.pop_back(); - } - return sum; } } @@ -172,24 +204,82 @@ void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool } } -void AbsDef::construct_def_entry( FirstOrderModelAbs * m, Node q, int v, unsigned depth ) { +void AbsDef::get_defs( unsigned u, std::vector< AbsDef * >& defs ) { + for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ + if( ( u & it->first )!=0 ){ + Assert( (u & it->first)==u ); + defs.push_back( &it->second ); + } + } +} + +void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth ) { if( depth==q[0].getNumChildren() ){ - d_value = v; + Assert( defs.size()==1 ); + d_value = defs[0]->d_value; }else{ - unsigned dom = m->d_domain[q[0][depth].getType()]; - d_def[dom].construct_def_entry( m, q, v, depth+1 ); + TypeNode tn = q[0][depth].getType(); + unsigned def = m->d_domain[tn]; + for( unsigned i=0; i::iterator itd = defs[i]->d_def.begin(); itd != defs[i]->d_def.end(); ++itd ){ + if( isSimple( itd->first ) && ( def & itd->first )!=0 ){ + def &= ~( itd->first ); + //process this value + std::vector< AbsDef * > cdefs; + for( unsigned j=0; jget_defs( itd->first, cdefs ); + } + d_def[itd->first].construct_normalize( m, q, cdefs, depth+1 ); + if( def==0 ){ + d_default = itd->first; + break; + } + } + } + if( def==0 ){ + break; + } + } + if( def!=0 ){ + d_default = def; + //process the default + std::vector< AbsDef * > cdefs; + for( unsigned j=0; jget_defs( d_default, cdefs ); + } + d_def[d_default].construct_normalize( m, q, cdefs, depth+1 ); + } + } +} + +void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth ) { + d_value = v; + if( depthd_domain[n[depth].getType()]; + d_def[dom].construct_def_entry( m, n, v, depth+1 ); d_default = dom; } } -void AbsDef::apply_ucompose( std::vector< unsigned >& entry, std::vector< bool >& entry_def, +void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q, + std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms, std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth ) { if( depth==terms.size() ){ + if( Trace.isOn("ambqi-check-debug2") ){ + Trace("ambqi-check-debug2") << "Add entry ( "; + for( unsigned i=0; id_rep_set.d_type_reps[q[0][i].getType()].size(); + debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] ); + Trace("ambqi-check-debug2") << " "; + } + Trace("ambqi-check-debug2") << ")" << std::endl; + } a->construct_entry( entry, entry_def, d_value ); }else{ unsigned id; - if( terms[depth]==-1 ){ + if( terms[depth]==val_none ){ //a variable std::map< unsigned, int >::iterator itv = vchildren.find( depth ); Assert( itv!=vchildren.end() ); @@ -199,7 +289,7 @@ void AbsDef::apply_ucompose( std::vector< unsigned >& entry, std::vector< bool > entry[itv->second] = it->first & prev_v; entry_def[itv->second] = ( it->first==d_default ) && prev_vd; if( entry[itv->second]!=0 ){ - it->second.apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 ); + it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); } } entry[itv->second] = prev_v; @@ -210,28 +300,28 @@ void AbsDef::apply_ucompose( std::vector< unsigned >& entry, std::vector< bool > unsigned fid = 1 << id; std::map< unsigned, AbsDef >::iterator it = d_def.find( fid ); if( it!=d_def.end() ){ - it->second.apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 ); + it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); }else{ - d_def[d_default].apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 ); + d_def[d_default].apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); } } } } -void AbsDef::construct_var_eq( FirstOrderModelAbs * m, Node q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) { +void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) { if( depth==q[0].getNumChildren() ){ - Assert( currv!=-1 ); + Assert( currv!=val_none ); d_value = currv; }else{ TypeNode tn = q[0][depth].getType(); unsigned dom = m->d_domain[tn]; - int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : -1 ); - if( vindex==-1 ){ + int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none ); + if( vindex==val_none ){ d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 ); d_default = dom; }else{ - Assert( currv==-1 ); - if( curr==-1 ){ + Assert( currv==val_none ); + if( curr==val_none ){ unsigned numReps = m->d_rep_set.d_type_reps[tn].size(); Assert( numReps < 32 ); for( unsigned i=0; id_domain[tn]; d_def[dom].construct_var( m, q, v, currv, depth+1 ); @@ -270,60 +360,87 @@ void AbsDef::construct_var( FirstOrderModelAbs * m, Node q, unsigned v, int curr } } -void AbsDef::construct_compose( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f, +void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, std::map< unsigned, AbsDef * >& children, std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - std::vector< unsigned >& entry, std::vector< bool >& entry_def, - bool incomplete ) { - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i& entry, std::vector< bool >& entry_def ) { if( n.getKind()==OR || n.getKind()==AND ){ // short circuiting for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ if( ( it->second->d_value==0 && n.getKind()==AND ) || ( it->second->d_value==1 && n.getKind()==OR ) ){ + //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl; + unsigned count = q[0].getNumChildren() - entry.size(); + for( unsigned i=0; id_domain[q[0][entry.size()].getType()] ); + entry_def.push_back( true ); + } construct_entry( entry, entry_def, it->second->d_value ); + for( unsigned i=0; i values; - values.resize( n.getNumChildren(), -1 ); - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - values[it->first] = it->second->d_value; - } - for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ - values[it->first] = it->second; - } - //look up value(s) - f->apply_ucompose( entry, entry_def, values, vchildren, this ); - }else{ - //we are composing with an interpreted function - std::vector< TNode > values; - values.resize( n.getNumChildren(), TNode::null() ); - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - Assert( it->second->d_value>=0 && it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ); + } + //we are composing with an uninterpreted function + std::vector< int > values; + values.resize( n.getNumChildren(), val_none ); + for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ + values[it->first] = it->second->d_value; + } + for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ + values[it->first] = it->second; + } + //look up value(s) + f->apply_ucompose( m, q, entry, entry_def, values, vchildren, this ); + }else{ + bool incomplete = false; + //we are composing with an interpreted function + std::vector< TNode > values; + values.resize( n.getNumChildren(), TNode::null() ); + for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ + Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value; + if( it->second->d_value>=0 ){ + if( it->second->d_value>=(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ){ + 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; + } + Assert( it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ); values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second->d_value]; - Trace("ambqi-check-debug2") << it->first << " : " << it->second->d_value << " ->> " << values[it->first] << std::endl; + }else{ + incomplete = true; } - for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ - Assert( it->second>=0 && it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ); + Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl; + } + for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ + Trace("ambqi-check-debug2") << " basic : " << it->first << " : " << it->second; + if( it->second>=0 ){ + Assert( it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ); values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second]; - Trace("ambqi-check-debug2") << it->first << " : " << it->second << " ->> " << values[it->first] << std::endl; + }else{ + incomplete = true; } - Assert( vchildren.empty() ); + Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl; + } + Assert( vchildren.empty() ); + if( incomplete ){ + Trace("ajr-temp") << "Construct incomplete entry." << std::endl; + + //if a child is unknown, we must return unknown + construct_entry( entry, entry_def, val_unk ); + }else{ if( Trace.isOn("ambqi-check-debug2") ){ + for( unsigned i=0; iisValidType( tn ) ); unsigned def = m->d_domain[tn]; - Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl; + if( Trace.isOn("ambqi-check-debug2") ){ + for( unsigned i=0; i::iterator it = children.begin(); it != children.end(); ++it ){ + Assert( it->second!=NULL ); //process each child for( std::map< unsigned, AbsDef >::iterator itd = it->second->d_def.begin(); itd != it->second->d_def.end(); ++itd ){ if( itd->first!=it->second->d_default && ( def & itd->first )!=0 ){ @@ -348,22 +470,24 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, Node q, Node n, AbsDef * //process this value std::map< unsigned, AbsDef * > cchildren; for( std::map< unsigned, AbsDef * >::iterator it2 = children.begin(); it2 != children.end(); ++it2 ){ - std::map< unsigned, AbsDef >::iterator itdf = it->second->d_def.find( itd->first ); - if( itdf!=it->second->d_def.end() ){ - cchildren[it->first] = &itdf->second; + Assert( it2->second!=NULL ); + std::map< unsigned, AbsDef >::iterator itdf = it2->second->d_def.find( itd->first ); + if( itdf!=it2->second->d_def.end() ){ + cchildren[it2->first] = &itdf->second; }else{ - cchildren[it->first] = it2->second->getDefault(); + Assert( it2->second->getDefault()!=NULL ); + cchildren[it2->first] = it2->second->getDefault(); } } if( Trace.isOn("ambqi-check-debug2") ){ for( unsigned i=0; id_rep_set.d_type_reps[tn].size(), itd->first ); - Trace("ambqi-check-debug2") << std::endl; + Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl; } entry.push_back( itd->first ); entry_def.push_back( def==0 ); - construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def, incomplete ); + construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def ); entry_def.pop_back(); entry.pop_back(); if( def==0 ){ @@ -376,36 +500,59 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, Node q, Node n, AbsDef * } } if( def!=0 ){ + if( Trace.isOn("ambqi-check-debug2") ){ + for( unsigned i=0; i cdchildren; for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ + Assert( it->second->getDefault()!=NULL ); cdchildren[it->first] = it->second->getDefault(); } if( Trace.isOn("ambqi-check-debug2") ){ for( unsigned i=0; id_rep_set.d_type_reps[tn].size(), def ); - Trace("ambqi-check-debug2") << std::endl; + debugPrintUInt("ambqi-check-debug2", m->d_rep_set.getNumRepresentatives( tn ), def ); + Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl; } entry.push_back( def ); entry_def.push_back( true ); - construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def, incomplete ); + construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def ); entry_def.pop_back(); entry.pop_back(); } } } -bool AbsDef::construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f, +bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, std::map< unsigned, AbsDef * >& children, std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - int varChCount, bool incomplete ) { + int varChCount ) { + if( Trace.isOn("ambqi-check-debug3") ){ + for( unsigned i=0; i::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){ if( ( it->second==0 && n.getKind()==AND ) || ( it->second==1 && n.getKind()==OR ) ){ - construct_def_entry( m, q, it->second ); + construct_def_entry( m, q[0], it->second ); return true; } } @@ -413,24 +560,33 @@ bool AbsDef::construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f, Trace("ambqi-check-debug2") << "Construct compose..." << std::endl; std::vector< unsigned > entry; std::vector< bool > entry_def; - construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def, incomplete ); + if( f ){ + AbsDef unorm; + unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); + //normalize + std::vector< AbsDef* > defs; + defs.push_back( &unorm ); + construct_normalize( m, q, defs ); + }else{ + construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); + } return true; }else if( varChCount==1 && n.getKind()==EQUAL ){ Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl; //expand the variable based on its finite domain AbsDef a; - a.construct_var( m, q, vchildren.begin()->second, -1 ); + a.construct_var( m, q, vchildren.begin()->second, val_none ); children[vchildren.begin()->first] = &a; vchildren.clear(); std::vector< unsigned > entry; std::vector< bool > entry_def; Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl; - construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def, incomplete ); + construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); return true; }else if( varChCount==2 && n.getKind()==EQUAL ){ Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl; //efficient expansion of the equality - construct_var_eq( m, q, vchildren[0], vchildren[1], -1, -1 ); + construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none ); return true; }else{ return false; @@ -441,7 +597,7 @@ Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< No if( depth==vars.size() ){ TypeNode tn = op.getType(); if( tn.getNumChildren()>0 ){ - tn = tn[tn.getNumChildren()-1]; + tn = tn[tn.getNumChildren() - 1]; } if( d_value>=0 ){ Assert( d_value<(int)m->d_rep_set.d_type_reps[tn].size() ); @@ -474,13 +630,19 @@ Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< No } } -unsigned AbsDef::getId( unsigned n ) { +bool AbsDef::isSimple( unsigned n ) { + return (n & (n - 1))==0; +} + +unsigned AbsDef::getId( unsigned n, unsigned start ) { Assert( n!=0 ); - unsigned index = 0; - while( (n & ( 1 << index )) == 0 ){ - index++; + while( (n & ( 1 << start )) == 0 ){ + start++; + if( start==32 ){ + return start; + } } - return index; + return start; } Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) { @@ -493,9 +655,13 @@ Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Nod } Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< unsigned >& iargs, unsigned depth ) { - if( d_value!=-1 ){ - Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() ); - return m->d_rep_set.d_type_reps[retTyp][d_value]; + if( d_value!=val_none ){ + if( d_value==val_unk ){ + return Node::null(); + }else{ + Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() ); + return m->d_rep_set.d_type_reps[retTyp][d_value]; + } }else{ std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] ); if( it==d_def.end() ){ @@ -575,6 +741,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { Node f = it->first; Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; //reset the model + it->second->clear(); //get all (non-redundant) f-applications std::vector< TNode > fapps; Trace("ambqi-model-debug") << "Initial terms: " << std::endl; @@ -606,8 +773,8 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { it->second->construct_func( fm, fapps ); Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl; it->second->debugPrint("ambqi-model-debug", fm, fapps[0] ); - - it->second->simplify( fm, Node::null() ); + Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl; + it->second->simplify( fm, fapps[0] ); Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl; it->second->debugPrint("ambqi-model", fm, fapps[0] ); @@ -645,12 +812,19 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in AbsDef ad; doCheck( fma, q, ad, q[1] ); //now process entries + Trace("ambqi-inst-debug") << "...Current : " << d_addedLemmas << std::endl; Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl; - ad.debugPrint( "ambqi-inst", fma, q ); + ad.debugPrint( "ambqi-inst", fma, q[0] ); Trace("ambqi-inst") << std::endl; - int lem = ad.addInstantiations( fma, d_qe, q ); + int lem = 0; + quantValid = ad.addInstantiations( fma, d_qe, q, lem ); Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl; + if( lem>0 ){ + //if we were incomplete but added at least one lemma, we are ok + quantValid = true; + } d_addedLemmas += lem; + Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl; } return quantValid; } @@ -662,12 +836,10 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod std::map< unsigned, AbsDef > children; std::map< unsigned, int > bchildren; std::map< unsigned, int > vchildren; - bool incomplete = false; int varChCount = 0; for( unsigned i=0; igetVariableId( q, n[i] ); @@ -675,8 +847,8 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod bchildren[i] = m->getRepresentativeId( n[i] ); }else{ if( !doCheck( m, q, children[i], n[i] ) ){ - bchildren[i] = -1; - incomplete = true; + bchildren[i] = AbsDef::val_unk; + children.erase( i ); } } } @@ -696,18 +868,18 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod } //uninterpreted compose if( m->d_models_valid[op] ){ - ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount, incomplete ); + ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount ); }else{ Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl; return false; } - }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount, incomplete ) ){ + }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){ Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl; return false; } - Trace("ambqi-check-debug2") << "Interpretation for " << n << " is : " << std::endl; - ad.debugPrint("ambqi-check-debug2", m, q[0] ); - ad.simplify( m, q ); + Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl; + ad.debugPrint("ambqi-check-try", m, q[0] ); + ad.simplify( m, q[0] ); Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl; ad.debugPrint("ambqi-check-debug", m, q[0] ); Trace("ambqi-check-debug") << std::endl; diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index d0818a784..29cee448b 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -30,40 +30,48 @@ class FirstOrderModelAbs; class AbsDef { private: - int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, std::vector< Node >& terms, unsigned depth ); - void construct_compose( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f, + bool addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ); + void construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, std::map< unsigned, AbsDef * >& children, std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - std::vector< unsigned >& entry, std::vector< bool >& entry_def, - bool incomplete ); + std::vector< unsigned >& entry, std::vector< bool >& entry_def ); void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 ); - void construct_def_entry( FirstOrderModelAbs * m, Node q, int v, unsigned depth = 0 ); - void apply_ucompose( std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms, + void construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth = 0 ); + void apply_ucompose( FirstOrderModelAbs * m, TNode q, + std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms, std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 ); - void construct_var_eq( FirstOrderModelAbs * m, Node q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 ); - void construct_var( FirstOrderModelAbs * m, Node q, unsigned v, int currv, unsigned depth = 0 ); + void construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 ); + void construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth = 0 ); + void get_defs( unsigned u, std::vector< AbsDef * >& defs ); + void construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth = 0 ); public: - AbsDef() : d_value( -1 ){} + enum { + val_none = -1, + val_unk = -2, + }; + AbsDef() : d_default( 0 ), d_value( -1 ){} std::map< unsigned, AbsDef > d_def; unsigned d_default; int d_value; + void clear() { d_def.clear(); d_default = 0; d_value = -1; } AbsDef * getDefault() { return &d_def[d_default]; } void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 ); - void debugPrintUInt( const char * c, unsigned dSize, unsigned u ); - void debugPrint( const char * c, FirstOrderModelAbs * m, Node f, unsigned depth = 0 ); - void simplify( FirstOrderModelAbs * m, Node q, unsigned depth = 0 ); - int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q ){ + void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const; + void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const; + void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 ); + int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){ std::vector< Node > terms; - return addInstantiations( m, qe, q, terms, 0 ); + return addInstantiations( m, qe, q, terms, inst, 0 ); } - bool construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f, + bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, std::map< unsigned, AbsDef * >& children, std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - int varChCount, bool incomplete ); + int varChCount ); Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 ); - static unsigned getId( unsigned n ); + static bool isSimple( unsigned n ); + static unsigned getId( unsigned n, unsigned start=0 ); Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args ); Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 ); };