--- /dev/null
+/********************* */\r
+/*! \file ambqi_builder.cpp\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of abstract MBQI builder\r
+ **/\r
+\r
+\r
+#include "theory/quantifiers/ambqi_builder.h"\r
+#include "theory/quantifiers/term_database.h"\r
+\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+\r
+void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) {\r
+ d_def.clear();\r
+ Assert( !fapps.empty() );\r
+ if( depth==fapps[0].getNumChildren() ){\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
+ }else{\r
+ TypeNode tn = fapps[0][depth].getType();\r
+ std::map< unsigned, std::vector< TNode > > fapp_child;\r
+\r
+ //partition based on evaluations of fapps[1][depth]....fapps[n][depth]\r
+ for( unsigned i=0; i<fapps.size(); i++ ){\r
+ unsigned r = m->getRepresentativeId( fapps[i][depth] );\r
+ Assert( r < 32 );\r
+ fapp_child[r].push_back( fapps[i] );\r
+ }\r
+\r
+ //do completion\r
+ std::map< unsigned, unsigned > fapp_child_index;\r
+ unsigned def = m->d_domain[ tn ];\r
+ unsigned minSize = fapp_child.begin()->second.size();\r
+ unsigned minSizeIndex = fapp_child.begin()->first;\r
+ for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){\r
+ fapp_child_index[it->first] = ( 1 << it->first );\r
+ def = def & ~( 1 << it->first );\r
+ if( it->second.size()<minSize ){\r
+ minSize = it->second.size();\r
+ minSizeIndex = it->first;\r
+ }\r
+ }\r
+ fapp_child_index[minSizeIndex] |= def;\r
+ d_default = fapp_child_index[minSizeIndex];\r
+\r
+ //construct children\r
+ for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){\r
+ Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : ";\r
+ debugPrintUInt( "abs-model-debug", m->d_rep_set.d_type_reps[tn].size(), fapp_child_index[it->first] );\r
+ Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl;\r
+ d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 );\r
+ }\r
+ }\r
+}\r
+\r
+void AbsDef::simplify( FirstOrderModelAbs * m, Node q, unsigned depth ) {\r
+ if( d_value==-1 ){\r
+ //process the default\r
+ std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );\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
+ //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
+ to_erase.push_back( it->first );\r
+ }else{\r
+ isConstant = false;\r
+ }\r
+ }\r
+ }\r
+ if( !to_erase.empty() ){\r
+ //erase old default\r
+ int defVal = defd->second.d_value;\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
+ //erase redundant entries\r
+ for( unsigned i=0; i<to_erase.size(); i++ ){\r
+ d_def.erase( to_erase[i] );\r
+ }\r
+ }\r
+ //if constant, propagate the value upwards\r
+ if( isConstant ){\r
+ d_value = defd->second.d_value;\r
+ }\r
+ }\r
+}\r
+\r
+void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) {\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
+ 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
+ Assert( dSize<32 );\r
+ for( std::map< unsigned, AbsDef >::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
+ Trace(c) << " -> V[" << it->second.d_value << "]";\r
+ }\r
+ Trace(c) << std::endl;\r
+ it->second.debugPrint( c, m, f, depth+1 );\r
+ }\r
+ }\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
+ if( qe->addInstantiation( q, terms ) ){\r
+ return 1;\r
+ }\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
+void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth ) {\r
+ if( depth==entry.size() ){\r
+ d_value = v;\r
+ }else{\r
+ d_def[entry[depth]].construct_entry( entry, entry_def, v, depth+1 );\r
+ if( entry_def[depth] ){\r
+ d_default = entry[depth];\r
+ }\r
+ }\r
+}\r
+\r
+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, Node q, int v, unsigned depth ) {\r
+ if( depth==q[0].getNumChildren() ){\r
+ d_value = v;\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
+ d_default = dom;\r
+ }\r
+}\r
+\r
+void AbsDef::apply_ucompose( 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
+ a->construct_entry( entry, entry_def, d_value );\r
+ }else{\r
+ unsigned id;\r
+ if( terms[depth]==-1 ){\r
+ //a variable\r
+ std::map< unsigned, int >::iterator itv = vchildren.find( depth );\r
+ Assert( itv!=vchildren.end() );\r
+ unsigned prev_v = entry[itv->second];\r
+ bool prev_vd = entry_def[itv->second];\r
+ for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\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
+ }\r
+ }\r
+ entry[itv->second] = prev_v;\r
+ entry_def[itv->second] = prev_vd;\r
+ }else{\r
+ id = (unsigned)terms[depth];\r
+ Assert( id<32 );\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
+ }else{\r
+ d_def[d_default].apply_ucompose( 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
+ if( depth==q[0].getNumChildren() ){\r
+ Assert( currv!=-1 );\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
+ 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
+ unsigned numReps = m->d_rep_set.d_type_reps[tn].size();\r
+ Assert( numReps < 32 );\r
+ for( unsigned i=0; i<numReps; i++ ){\r
+ curr = 1 << i;\r
+ d_def[curr].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );\r
+ }\r
+ d_default = curr;\r
+ }else{\r
+ d_def[curr].construct_var_eq( m, q, v1, v2, curr, 1, depth+1 );\r
+ dom = dom & ~curr;\r
+ d_def[dom].construct_var_eq( m, q, v1, v2, curr, 0, depth+1 );\r
+ d_default = dom;\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+void AbsDef::construct_var( FirstOrderModelAbs * m, Node q, unsigned v, int currv, unsigned depth ) {\r
+ if( depth==q[0].getNumChildren() ){\r
+ Assert( currv!=-1 );\r
+ d_value = currv;\r
+ }else{\r
+ TypeNode tn = q[0][depth].getType();\r
+ if( v==depth ){\r
+ unsigned numReps = m->d_rep_set.d_type_reps[tn].size();\r
+ Assert( numReps>0 && numReps < 32 );\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
+ }else{\r
+ unsigned dom = m->d_domain[tn];\r
+ d_def[dom].construct_var( m, q, v, currv, depth+1 );\r
+ d_default = dom;\r
+ }\r
+ }\r
+}\r
+\r
+void AbsDef::construct_compose( FirstOrderModelAbs * m, Node q, Node 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
+ 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
+ construct_entry( entry, entry_def, it->second->d_value );\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
+ 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
+ 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
+ }\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
+ 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
+ }\r
+ Assert( vchildren.empty() );\r
+ if( Trace.isOn("ambqi-check-debug2") ){\r
+ Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( ";\r
+ for( unsigned i=0; i<values.size(); i++ ){\r
+ Trace("ambqi-check-debug2") << values[i] << " ";\r
+ }\r
+ Trace("ambqi-check-debug2") << ")..." << std::endl;\r
+ }\r
+ //evaluate\r
+ Node vv = NodeManager::currentNM()->mkNode( n.getKind(), values );\r
+ vv = Rewriter::rewrite( vv );\r
+ int v = m->getRepresentativeId( vv );\r
+ construct_entry( entry, entry_def, v );\r
+ }\r
+ }\r
+ }else{\r
+ //take product of arguments\r
+ TypeNode tn = q[0][entry.size()].getType();\r
+ unsigned def = m->d_domain[tn];\r
+ Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl;\r
+ for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\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
+ def &= ~( itd->first );\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
+ }else{\r
+ cchildren[it->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
+ }\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
+ entry_def.pop_back();\r
+ entry.pop_back();\r
+ if( def==0 ){\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ if( def==0 ){\r
+ break;\r
+ }\r
+ }\r
+ if( def!=0 ){\r
+ std::map< unsigned, AbsDef * > cdchildren;\r
+ for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){\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
+ }\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
+ 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
+ std::map< unsigned, AbsDef * >& children,\r
+ std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,\r
+ int varChCount, bool incomplete ) {\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
+ return true;\r
+ }\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
+ 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
+ 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
+ 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
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) {\r
+ if( depth==vars.size() ){\r
+ TypeNode tn = op.getType();\r
+ if( tn.getNumChildren()>0 ){\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
+ if( tn.isBoolean() ){\r
+ return NodeManager::currentNM()->mkConst( d_value==1 );\r
+ }else{\r
+ return m->d_rep_set.d_type_reps[tn][d_value];\r
+ }\r
+ }else{\r
+ return Node::null();\r
+ }\r
+ }else{\r
+ TypeNode tn = vars[depth].getType();\r
+ Node curr;\r
+ curr = d_def[d_default].getFunctionValue( m, op, vars, depth+1 );\r
+ for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
+ if( it->first!=d_default ){\r
+ unsigned id = getId( it->first );\r
+ Assert( id<m->d_rep_set.d_type_reps[tn].size() );\r
+ TNode n = m->d_rep_set.d_type_reps[tn][id];\r
+ Node fv = it->second.getFunctionValue( m, op, vars, depth+1 );\r
+ if( !curr.isNull() && !fv.isNull() ){\r
+ curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr );\r
+ }else{\r
+ curr = Node::null();\r
+ }\r
+ }\r
+ }\r
+ return curr;\r
+ }\r
+}\r
+\r
+unsigned AbsDef::getId( unsigned n ) {\r
+ Assert( n!=0 );\r
+ unsigned index = 0;\r
+ while( (n & ( 1 << index )) == 0 ){\r
+ index++;\r
+ }\r
+ return index;\r
+}\r
+\r
+Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) {\r
+ std::vector< unsigned > iargs;\r
+ for( unsigned i=0; i<args.size(); i++ ){\r
+ unsigned v = 1 << m->getRepresentativeId( args[i] );\r
+ iargs.push_back( v );\r
+ }\r
+ return evaluate( m, retTyp, iargs, 0 );\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
+ }else{\r
+ std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] );\r
+ if( it==d_def.end() ){\r
+ return d_def[d_default].evaluate( m, retTyp, iargs, depth+1 );\r
+ }else{\r
+ return it->second.evaluate( m, retTyp, iargs, depth+1 );\r
+ }\r
+ }\r
+}\r
+\r
+AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) :\r
+QModelBuilder( c, qe ){\r
+ d_true = NodeManager::currentNM()->mkConst( true );\r
+ d_false = NodeManager::currentNM()->mkConst( false );\r
+}\r
+\r
+\r
+//------------------------model construction----------------------------\r
+\r
+void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {\r
+ Trace("ambqi-debug") << "process build model " << fullModel << std::endl;\r
+ FirstOrderModel* f = (FirstOrderModel*)m;\r
+ FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();\r
+ if( fullModel ){\r
+ Trace("ambqi-model") << "Construct model representation..." << std::endl;\r
+ //make function values\r
+ for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
+ if( it->first.getType().getNumChildren()>1 ){\r
+ Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;\r
+ m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );\r
+ }\r
+ }\r
+ TheoryEngineModelBuilder::processBuildModel( m, fullModel );\r
+ //mark that the model has been set\r
+ fm->markModelSet();\r
+ //debug the model\r
+ debugModel( fm );\r
+ }else{\r
+ fm->initialize( d_considerAxioms );\r
+ //process representatives\r
+ fm->d_rep_id.clear();\r
+ fm->d_domain.clear();\r
+\r
+ //initialize boolean sort\r
+ TypeNode b = d_true.getType();\r
+ fm->d_rep_set.d_type_reps[b].clear();\r
+ fm->d_rep_set.d_type_reps[b].push_back( d_false );\r
+ fm->d_rep_set.d_type_reps[b].push_back( d_true );\r
+ fm->d_rep_id[d_false] = 0;\r
+ fm->d_rep_id[d_true] = 1;\r
+\r
+ //initialize unintpreted sorts\r
+ Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;\r
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();\r
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){\r
+ if( it->first.isSort() ){\r
+ Assert( !it->second.empty() );\r
+ //set the domain\r
+ fm->d_domain[it->first] = 0;\r
+ Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;\r
+ for( unsigned i=0; i<it->second.size(); i++ ){\r
+ if( i<32 ){\r
+ fm->d_domain[it->first] |= ( 1 << i );\r
+ }\r
+ Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;\r
+ fm->d_rep_id[it->second[i]] = i;\r
+ }\r
+ if( it->second.size()>=32 ){\r
+ fm->d_domain.erase( it->first );\r
+ }\r
+ }\r
+ }\r
+\r
+ Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;\r
+ //construct the models for functions\r
+ for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
+ Node f = it->first;\r
+ Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;\r
+ //reset the model\r
+ //get all (non-redundant) f-applications\r
+ std::vector< TNode > fapps;\r
+ Trace("ambqi-model-debug") << "Initial terms: " << std::endl;\r
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){\r
+ Node n = fm->d_uf_terms[f][i];\r
+ if( !n.getAttribute(NoMatchAttribute()) ){\r
+ Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;\r
+ fapps.push_back( n );\r
+ }\r
+ }\r
+ if( fapps.empty() ){\r
+ //choose arbitrary value\r
+ Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);\r
+ Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;\r
+ fapps.push_back( mbt );\r
+ }\r
+ bool fValid = true;\r
+ for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){\r
+ if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){\r
+ Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";\r
+ Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;\r
+ fValid = false;\r
+ break;\r
+ }\r
+ }\r
+ fm->d_models_valid[f] = fValid;\r
+ if( fValid ){\r
+ //construct the ambqi model\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") << "(Simplified) interpretation of " << f << " : " << std::endl;\r
+ it->second->debugPrint("ambqi-model", fm, fapps[0] );\r
+\r
+/*\r
+ if( Debug.isOn("ambqi-model-debug") ){\r
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){\r
+ Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );\r
+ Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;\r
+ Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );\r
+ }\r
+ }\r
+*/\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+\r
+//--------------------model checking---------------------------------------\r
+\r
+//do exhaustive instantiation\r
+bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {\r
+ Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl;\r
+ if (effort==0) {\r
+ FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();\r
+ bool quantValid = true;\r
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+ if( !fma->isValidType( q[0][i].getType() ) ){\r
+ quantValid = false;\r
+ Trace("ambqi-inst") << "Interpretation of " << q << " is not valid because of type " << q[0][i].getType() << std::endl;\r
+ break;\r
+ }\r
+ }\r
+ if( quantValid ){\r
+ AbsDef ad;\r
+ doCheck( fma, q, ad, q[1] );\r
+ //now process entries\r
+ Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;\r
+ ad.debugPrint( "ambqi-inst", fma, q );\r
+ Trace("ambqi-inst") << std::endl;\r
+ int lem = ad.addInstantiations( fma, d_qe, q );\r
+ Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;\r
+ d_addedLemmas += lem;\r
+ }\r
+ return quantValid;\r
+ }\r
+ return true;\r
+}\r
+\r
+bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {\r
+ Assert( n.getKind()!=FORALL );\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
+ }else if( n[i].getKind() == BOUND_VARIABLE ){\r
+ varChCount++;\r
+ vchildren[i] = m->getVariableId( q, n[i] );\r
+ }else if( m->hasTerm( 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
+ }\r
+ }\r
+ }\r
+ //convert to pointers\r
+ std::map< unsigned, AbsDef * > pchildren;\r
+ for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){\r
+ pchildren[it->first] = &it->second;\r
+ }\r
+ //construct the interpretation\r
+ Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;\r
+ if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){\r
+ Node op;\r
+ if( n.getKind() == APPLY_UF ){\r
+ op = n.getOperator();\r
+ }else{\r
+ op = n;\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
+ }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
+ 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-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
+ return true;\r
+}\r
projects / cvc5.git / commitdiff