From c9404d8ecdfbc6da4fd125cefede7a21a5499e4d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 6 May 2014 08:19:04 -0500 Subject: [PATCH] First draft of ambqi_builder (new implementation of MBQI based on disjoint sets). --- src/Makefile.am | 2 + src/theory/quantifiers/ambqi_builder.cpp | 715 +++++++++++++++++++ src/theory/quantifiers/ambqi_builder.h | 90 +++ src/theory/quantifiers/first_order_model.cpp | 99 +++ src/theory/quantifiers/first_order_model.h | 23 + src/theory/quantifiers/model_engine.cpp | 4 + src/theory/quantifiers/modes.cpp | 3 + src/theory/quantifiers/modes.h | 2 + src/theory/quantifiers/options_handlers.h | 5 + src/theory/quantifiers_engine.cpp | 2 + 10 files changed, 945 insertions(+) create mode 100755 src/theory/quantifiers/ambqi_builder.cpp create mode 100755 src/theory/quantifiers/ambqi_builder.h diff --git a/src/Makefile.am b/src/Makefile.am index e7cc9628e..573181ccf 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -306,6 +306,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/symmetry_breaking.cpp \ theory/quantifiers/qinterval_builder.h \ theory/quantifiers/qinterval_builder.cpp \ + theory/quantifiers/ambqi_builder.h \ + theory/quantifiers/ambqi_builder.cpp \ theory/quantifiers/quant_conflict_find.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/options_handlers.h \ diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp new file mode 100755 index 000000000..7a296c934 --- /dev/null +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -0,0 +1,715 @@ +/********************* */ +/*! \file ambqi_builder.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of abstract MBQI builder + **/ + + +#include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/term_database.h" + + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) { + d_def.clear(); + Assert( !fapps.empty() ); + if( depth==fapps[0].getNumChildren() ){ + //get representative in model for this term + Assert( fapps.size()==1 ); + d_value = m->getRepresentativeId( fapps[0] ); + Assert( d_value!=-1 ); + }else{ + TypeNode tn = fapps[0][depth].getType(); + std::map< unsigned, std::vector< TNode > > fapp_child; + + //partition based on evaluations of fapps[1][depth]....fapps[n][depth] + for( unsigned i=0; igetRepresentativeId( fapps[i][depth] ); + Assert( r < 32 ); + fapp_child[r].push_back( fapps[i] ); + } + + //do completion + std::map< unsigned, unsigned > fapp_child_index; + unsigned def = m->d_domain[ tn ]; + unsigned minSize = fapp_child.begin()->second.size(); + unsigned minSizeIndex = fapp_child.begin()->first; + for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){ + fapp_child_index[it->first] = ( 1 << it->first ); + def = def & ~( 1 << it->first ); + if( it->second.size()second.size(); + minSizeIndex = it->first; + } + } + fapp_child_index[minSizeIndex] |= def; + d_default = fapp_child_index[minSizeIndex]; + + //construct children + for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){ + Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : "; + debugPrintUInt( "abs-model-debug", m->d_rep_set.d_type_reps[tn].size(), fapp_child_index[it->first] ); + Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl; + d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 ); + } + } +} + +void AbsDef::simplify( FirstOrderModelAbs * m, Node q, unsigned depth ) { + if( d_value==-1 ){ + //process the default + std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default ); + unsigned newDef = d_default; + std::vector< unsigned > to_erase; + defd->second.simplify( m, q, depth+1 ); + bool isConstant = ( defd->second.d_value!=-1 ); + //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; + to_erase.push_back( it->first ); + }else{ + isConstant = false; + } + } + } + if( !to_erase.empty() ){ + //erase old default + int defVal = defd->second.d_value; + d_def.erase( d_default ); + //set new default + d_default = newDef; + d_def[d_default].construct_def_entry( m, q, defVal, depth+1 ); + //erase redundant entries + for( unsigned i=0; isecond.d_value; + } + } +} + +void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) { + for( unsigned i=0; id_rep_set.d_type_reps[tn].size(); + Assert( dSize<32 ); + for( std::map< unsigned, AbsDef >::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 ){ + Trace(c) << " -> V[" << it->second.d_value << "]"; + } + Trace(c) << std::endl; + it->second.debugPrint( c, m, f, depth+1 ); + } + } + } +} + +int AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, std::vector< Node >& terms, unsigned depth ) { + if( depth==q[0].getNumChildren() ){ + if( d_value!=1 ){ + if( qe->addInstantiation( q, terms ) ){ + return 1; + } + } + 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; + } +} + +void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth ) { + if( depth==entry.size() ){ + d_value = v; + }else{ + d_def[entry[depth]].construct_entry( entry, entry_def, v, depth+1 ); + if( entry_def[depth] ){ + d_default = entry[depth]; + } + } +} + +void AbsDef::construct_def_entry( FirstOrderModelAbs * m, Node q, int v, unsigned depth ) { + if( depth==q[0].getNumChildren() ){ + d_value = v; + }else{ + unsigned dom = m->d_domain[q[0][depth].getType()]; + d_def[dom].construct_def_entry( m, q, v, depth+1 ); + d_default = dom; + } +} + +void AbsDef::apply_ucompose( 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() ){ + a->construct_entry( entry, entry_def, d_value ); + }else{ + unsigned id; + if( terms[depth]==-1 ){ + //a variable + std::map< unsigned, int >::iterator itv = vchildren.find( depth ); + Assert( itv!=vchildren.end() ); + unsigned prev_v = entry[itv->second]; + bool prev_vd = entry_def[itv->second]; + for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ + 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 ); + } + } + entry[itv->second] = prev_v; + entry_def[itv->second] = prev_vd; + }else{ + id = (unsigned)terms[depth]; + Assert( id<32 ); + 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 ); + }else{ + d_def[d_default].apply_ucompose( 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 ) { + if( depth==q[0].getNumChildren() ){ + Assert( currv!=-1 ); + 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 ){ + d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 ); + d_default = dom; + }else{ + Assert( currv==-1 ); + if( curr==-1 ){ + unsigned numReps = m->d_rep_set.d_type_reps[tn].size(); + Assert( numReps < 32 ); + for( unsigned i=0; id_rep_set.d_type_reps[tn].size(); + Assert( numReps>0 && numReps < 32 ); + for( unsigned i=0; id_domain[tn]; + d_def[dom].construct_var( m, q, v, currv, depth+1 ); + d_default = dom; + } + } +} + +void AbsDef::construct_compose( FirstOrderModelAbs * m, Node q, Node 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::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 ) ){ + construct_entry( entry, entry_def, it->second->d_value ); + return; + } + } + } + if( entry.size()==q[0].getNumChildren() ){ + if( incomplete ){ + //if a child is unknown, we must return unknown + construct_entry( entry, entry_def, -1 ); + }else{ + if( f ){ + Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl; + //we are composing with an uninterpreted function + std::vector< int > 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() ); + 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; + } + 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() ); + 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; + } + Assert( vchildren.empty() ); + if( Trace.isOn("ambqi-check-debug2") ){ + Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( "; + for( unsigned i=0; imkNode( n.getKind(), values ); + vv = Rewriter::rewrite( vv ); + int v = m->getRepresentativeId( vv ); + construct_entry( entry, entry_def, v ); + } + } + }else{ + //take product of arguments + TypeNode tn = q[0][entry.size()].getType(); + unsigned def = m->d_domain[tn]; + Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl; + for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ + //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 ){ + def &= ~( itd->first ); + //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; + }else{ + cchildren[it->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; + } + entry.push_back( itd->first ); + entry_def.push_back( def==0 ); + construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def, incomplete ); + entry_def.pop_back(); + entry.pop_back(); + if( def==0 ){ + break; + } + } + } + if( def==0 ){ + break; + } + } + if( def!=0 ){ + std::map< unsigned, AbsDef * > cdchildren; + for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ + 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; + } + entry.push_back( def ); + entry_def.push_back( true ); + construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def, incomplete ); + entry_def.pop_back(); + entry.pop_back(); + } + } +} + +bool AbsDef::construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f, + std::map< unsigned, AbsDef * >& children, + std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, + int varChCount, bool incomplete ) { + if( varChCount==0 || f ){ + //short-circuit + if( n.getKind()==AND || n.getKind()==OR ){ + for( std::map< unsigned, int >::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 ); + return true; + } + } + } + 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 ); + 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 ); + 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 ); + 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 ); + return true; + }else{ + return false; + } +} + +Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) { + if( depth==vars.size() ){ + TypeNode tn = op.getType(); + if( tn.getNumChildren()>0 ){ + tn = tn[tn.getNumChildren()-1]; + } + if( d_value>=0 ){ + Assert( d_value<(int)m->d_rep_set.d_type_reps[tn].size() ); + if( tn.isBoolean() ){ + return NodeManager::currentNM()->mkConst( d_value==1 ); + }else{ + return m->d_rep_set.d_type_reps[tn][d_value]; + } + }else{ + return Node::null(); + } + }else{ + TypeNode tn = vars[depth].getType(); + Node curr; + curr = d_def[d_default].getFunctionValue( m, op, vars, depth+1 ); + for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ + if( it->first!=d_default ){ + unsigned id = getId( it->first ); + Assert( idd_rep_set.d_type_reps[tn].size() ); + TNode n = m->d_rep_set.d_type_reps[tn][id]; + Node fv = it->second.getFunctionValue( m, op, vars, depth+1 ); + if( !curr.isNull() && !fv.isNull() ){ + curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr ); + }else{ + curr = Node::null(); + } + } + } + return curr; + } +} + +unsigned AbsDef::getId( unsigned n ) { + Assert( n!=0 ); + unsigned index = 0; + while( (n & ( 1 << index )) == 0 ){ + index++; + } + return index; +} + +Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) { + std::vector< unsigned > iargs; + for( unsigned i=0; igetRepresentativeId( args[i] ); + iargs.push_back( v ); + } + return evaluate( m, retTyp, iargs, 0 ); +} + +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]; + }else{ + std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] ); + if( it==d_def.end() ){ + return d_def[d_default].evaluate( m, retTyp, iargs, depth+1 ); + }else{ + return it->second.evaluate( m, retTyp, iargs, depth+1 ); + } + } +} + +AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) : +QModelBuilder( c, qe ){ + d_true = NodeManager::currentNM()->mkConst( true ); + d_false = NodeManager::currentNM()->mkConst( false ); +} + + +//------------------------model construction---------------------------- + +void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { + Trace("ambqi-debug") << "process build model " << fullModel << std::endl; + FirstOrderModel* f = (FirstOrderModel*)m; + FirstOrderModelAbs* fm = f->asFirstOrderModelAbs(); + if( fullModel ){ + Trace("ambqi-model") << "Construct model representation..." << std::endl; + //make function values + for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + if( it->first.getType().getNumChildren()>1 ){ + Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; + m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" ); + } + } + TheoryEngineModelBuilder::processBuildModel( m, fullModel ); + //mark that the model has been set + fm->markModelSet(); + //debug the model + debugModel( fm ); + }else{ + fm->initialize( d_considerAxioms ); + //process representatives + fm->d_rep_id.clear(); + fm->d_domain.clear(); + + //initialize boolean sort + TypeNode b = d_true.getType(); + fm->d_rep_set.d_type_reps[b].clear(); + fm->d_rep_set.d_type_reps[b].push_back( d_false ); + fm->d_rep_set.d_type_reps[b].push_back( d_true ); + fm->d_rep_id[d_false] = 0; + fm->d_rep_id[d_true] = 1; + + //initialize unintpreted sorts + Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl; + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); + it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Assert( !it->second.empty() ); + //set the domain + fm->d_domain[it->first] = 0; + Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl; + for( unsigned i=0; isecond.size(); i++ ){ + if( i<32 ){ + fm->d_domain[it->first] |= ( 1 << i ); + } + Trace("ambqi-model") << i << " : " << it->second[i] << std::endl; + fm->d_rep_id[it->second[i]] = i; + } + if( it->second.size()>=32 ){ + fm->d_domain.erase( it->first ); + } + } + } + + Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl; + //construct the models for functions + for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node f = it->first; + Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; + //reset the model + //get all (non-redundant) f-applications + std::vector< TNode > fapps; + Trace("ambqi-model-debug") << "Initial terms: " << std::endl; + for( size_t i=0; id_uf_terms[f].size(); i++ ){ + Node n = fm->d_uf_terms[f][i]; + if( !n.getAttribute(NoMatchAttribute()) ){ + Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; + fapps.push_back( n ); + } + } + if( fapps.empty() ){ + //choose arbitrary value + Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); + Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; + fapps.push_back( mbt ); + } + bool fValid = true; + for( unsigned i=0; id_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){ + Trace("ambqi-model") << "Interpretation of " << f << " is not valid."; + Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl; + fValid = false; + break; + } + } + fm->d_models_valid[f] = fValid; + if( fValid ){ + //construct the ambqi model + 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") << "(Simplified) interpretation of " << f << " : " << std::endl; + it->second->debugPrint("ambqi-model", fm, fapps[0] ); + +/* + if( Debug.isOn("ambqi-model-debug") ){ + for( size_t i=0; id_uf_terms[f].size(); i++ ){ + Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); + Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; + Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); + } + } +*/ + } + } + } +} + + +//--------------------model checking--------------------------------------- + +//do exhaustive instantiation +bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { + Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl; + if (effort==0) { + FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs(); + bool quantValid = true; + for( unsigned i=0; iisValidType( q[0][i].getType() ) ){ + quantValid = false; + Trace("ambqi-inst") << "Interpretation of " << q << " is not valid because of type " << q[0][i].getType() << std::endl; + break; + } + } + if( quantValid ){ + AbsDef ad; + doCheck( fma, q, ad, q[1] ); + //now process entries + Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl; + ad.debugPrint( "ambqi-inst", fma, q ); + Trace("ambqi-inst") << std::endl; + int lem = ad.addInstantiations( fma, d_qe, q ); + Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl; + d_addedLemmas += lem; + } + return quantValid; + } + return true; +} + +bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) { + Assert( n.getKind()!=FORALL ); + 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] ); + }else if( m->hasTerm( n[i] ) ){ + bchildren[i] = m->getRepresentativeId( n[i] ); + }else{ + if( !doCheck( m, q, children[i], n[i] ) ){ + bchildren[i] = -1; + incomplete = true; + } + } + } + //convert to pointers + std::map< unsigned, AbsDef * > pchildren; + for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){ + pchildren[it->first] = &it->second; + } + //construct the interpretation + Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl; + if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){ + Node op; + if( n.getKind() == APPLY_UF ){ + op = n.getOperator(); + }else{ + op = n; + } + //uninterpreted compose + if( m->d_models_valid[op] ){ + ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount, incomplete ); + }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 ) ){ + 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-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl; + ad.debugPrint("ambqi-check-debug", m, q[0] ); + Trace("ambqi-check-debug") << std::endl; + return true; +} diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h new file mode 100755 index 000000000..d0818a784 --- /dev/null +++ b/src/theory/quantifiers/ambqi_builder.h @@ -0,0 +1,90 @@ +/********************* */ +/*! \file ambqi_builder.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Abstract MBQI model builder class + **/ + +#include "cvc4_private.h" + +#ifndef ABSTRACT_MBQI_BUILDER +#define ABSTRACT_MBQI_BUILDER + +#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class FirstOrderModelAbs; + +//representiation of function and term interpretations +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, + 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 ); + 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, + 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 ); +public: + AbsDef() : d_value( -1 ){} + std::map< unsigned, AbsDef > d_def; + unsigned d_default; + int d_value; + + 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 ){ + std::vector< Node > terms; + return addInstantiations( m, qe, q, terms, 0 ); + } + bool construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f, + std::map< unsigned, AbsDef * >& children, + std::map< unsigned, int >& bchildren, + std::map< unsigned, int >& vchildren, + int varChCount, bool incomplete ); + Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 ); + static unsigned getId( unsigned n ); + Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args ); + Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 ); +}; + +class AbsMbqiBuilder : public QModelBuilder +{ + friend class AbsDef; +private: + Node d_true; + Node d_false; + bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ); +public: + AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ); + //process build model + void processBuildModel(TheoryModel* m, bool fullModel); + //do exhaustive instantiation + bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 509c00bb6..0b2fae5d4 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/qinterval_builder.h" +#include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/options.h" #define USE_INDEX_ORDERING @@ -882,3 +883,101 @@ bool FirstOrderModelQInt::doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, //return lr==ur || lr.isNull() || isLessThan( lr, ur ); return lr.isNull() || isLessThan( lr, ur ); } + + + + +FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(qe, c, name) { + +} + +void FirstOrderModelAbs::processInitialize( bool ispre ) { + if( !ispre ){ + Trace("ambqi-debug") << "Process initialize" << std::endl; + for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + Trace("ambqi-debug") << " Init " << op << " " << tno << std::endl; + for( unsigned i=0; i::iterator it = d_rep_id.find( r ); + if( it!=d_rep_id.end() ){ + return it->second; + }else{ + return 0; + } +} + +TNode FirstOrderModelAbs::getUsedRepresentative( TNode n ) { + if( hasTerm( n ) ){ + if( n.getType().isBoolean() ){ + return areEqual(n, d_true) ? d_true : d_false; + }else{ + return getRepresentative( n ); + } + }else{ + Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl; + Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() ); + return d_rep_set.d_type_reps[n.getType()][0]; + } +} + +Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) { + if( d_models_valid[op] ){ + Trace("ambqi-debug") << "Get function value for " << op << std::endl; + TypeNode type = op.getType(); + std::vector< Node > vars; + for( size_t i=0; imkBoundVar( ss.str(), type[i] ); + vars.push_back( b ); + } + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); + Node curr = d_models[op]->getFunctionValue( this, op, vars ); + Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); + Trace("ambqi-debug") << "Return " << fv << std::endl; + return fv; + }else{ + + } + return Node::null(); +} + +Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { + Debug("qint-debug") << "get curr uf value " << n << std::endl; + if( d_models_valid[n] ){ + TypeNode tn = n.getType(); + if( tn.getNumChildren()>0 ){ + tn = tn[tn.getNumChildren()-1]; + } + return d_models[n]->evaluate( this, tn, args ); + }else{ + return Node::null(); + } +} + +void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) { + if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ + Node op = n.getKind()==APPLY_UF ? n.getOperator() : n; + if( d_models.find(op)==d_models.end()) { + Trace("abmqi-debug") << "init model for " << op << std::endl; + d_models[op] = new AbsDef; + d_models_valid[op] = false; + } + } +} diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 63d8ffcce..d799cfad3 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -37,6 +37,7 @@ namespace fmcheck { }/* CVC4::theory::quantifiers::fmcheck namespace */ class FirstOrderModelQInt; +class FirstOrderModelAbs; struct IsStarAttributeId {}; typedef expr::Attribute IsStarAttribute; @@ -75,6 +76,7 @@ public: virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; } virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; } virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; } + virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; } // initialize the model void initialize( bool considerAxioms = true ); virtual void processInitialize( bool ispre ) = 0; @@ -220,6 +222,27 @@ public: int getOrderedVarNumToVarNum( Node q, int i ); };/* class FirstOrderModelQInt */ +class AbsDef; + +class FirstOrderModelAbs : public FirstOrderModel +{ +public: + std::map< Node, AbsDef * > d_models; + std::map< Node, bool > d_models_valid; + std::map< TNode, unsigned > d_rep_id; + std::map< TypeNode, unsigned > d_domain; + /** get current model value */ + Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); + void processInitializeModelForTerm(Node n); +public: + FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); + FirstOrderModelAbs * asFirstOrderModelAbs() { return this; } + void processInitialize( bool ispre ); + unsigned getRepresentativeId( TNode n ); + TNode getUsedRepresentative( TNode n ); + bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); } + Node getFunctionValue(Node op, const char* argPrefix ); +}; }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 3a4879b42..dfbc01414 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/qinterval_builder.h" +#include "theory/quantifiers/ambqi_builder.h" using namespace std; using namespace CVC4; @@ -44,6 +45,9 @@ QuantifiersModule( qe ){ }else if( options::mbqiMode()==MBQI_INTERVAL ){ Trace("model-engine-debug") << "...make interval builder." << std::endl; d_builder = new QIntervalBuilder( c, qe ); + }else if( options::mbqiMode()==MBQI_ABS ){ + Trace("model-engine-debug") << "...make abs mbqi builder." << std::endl; + d_builder = new AbsMbqiBuilder( c, qe ); }else if( options::mbqiMode()==MBQI_INST_GEN ){ Trace("model-engine-debug") << "...make inst-gen builder." << std::endl; d_builder = new QModelBuilderInstGen( c, qe ); diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index 8bd97a8a7..b24721170 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -94,6 +94,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) case theory::quantifiers::MBQI_INTERVAL: out << "MBQI_INTERVAL"; break; + case theory::quantifiers::MBQI_ABS: + out << "MBQI_ABS"; + break; case theory::quantifiers::MBQI_TRUST: out << "MBQI_TRUST"; break; diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 80534c8b0..230495f1f 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -70,6 +70,8 @@ typedef enum { MBQI_FMC_INTERVAL, /** mbqi with interval abstraction of uninterpreted sorts */ MBQI_INTERVAL, + /** abstract mbqi algorithm */ + MBQI_ABS, /** mbqi trust (produce no instantiations) */ MBQI_TRUST, } MbqiMode; diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index b7e624a66..c0b76bcec 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -101,6 +101,9 @@ fmc-interval \n\ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ \n\ +abs \n\ ++ Use abstract MBQI algorithm (uses disjoint sets). \n\ +\n\ "; static const std::string qcfWhenModeHelp = "\ Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ @@ -226,6 +229,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi return MBQI_FMC_INTERVAL; } else if(optarg == "interval") { return MBQI_INTERVAL; + } else if(optarg == "abs") { + return MBQI_ABS; } else if(optarg == "trust") { return MBQI_TRUST; } else if(optarg == "help") { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index b79c0da69..929a638d7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -60,6 +60,8 @@ d_lemmas_produced_c(u){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" ); + }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ + d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" ); }else{ d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); } -- 2.30.2