diff options
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 228 |
1 files changed, 112 insertions, 116 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 5c02b631c..bff5e36cd 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -14,18 +14,14 @@ #include <unordered_set> -#include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers/term_util.h" #include "theory/rep_set.h" #include "theory/type_enumerator.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; + +namespace CVC4 { +namespace theory { void RepSet::clear(){ d_type_reps.clear(); @@ -64,6 +60,14 @@ Node RepSet::getRepresentative(TypeNode tn, unsigned i) const return it->second[i]; } +void RepSet::getRepresentatives(TypeNode tn, std::vector<Node>& reps) const +{ + std::map<TypeNode, std::vector<Node> >::const_iterator it = + d_type_reps.find(tn); + Assert(it != d_type_reps.end()); + reps.insert(reps.end(), it->second.begin(), it->second.end()); +} + bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache) { if( std::find( cache.begin(), cache.end(), n )==cache.end() ){ @@ -184,43 +188,44 @@ void RepSet::toStream(std::ostream& out){ } } - -RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){ - d_incomplete = false; +RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext) + : d_rs(rs), d_rext(rext), d_incomplete(false) +{ } -int RepSetIterator::domainSize( int i ) { - Assert(i>=0); - int v = d_var_order[i]; +unsigned RepSetIterator::domainSize(unsigned i) +{ + unsigned v = d_var_order[i]; return d_domain_elements[v].size(); } -bool RepSetIterator::setQuantifier( Node f, RepBoundExt* rext ){ - Trace("rsi") << "Make rsi for " << f << std::endl; +bool RepSetIterator::setQuantifier(Node q) +{ + Trace("rsi") << "Make rsi for quantified formula " << q << std::endl; Assert( d_types.empty() ); //store indicies - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - d_types.push_back( f[0][i].getType() ); + for (size_t i = 0; i < q[0].getNumChildren(); i++) + { + d_types.push_back(q[0][i].getType()); } - d_owner = f; - return initialize( rext ); + d_owner = q; + return initialize(); } -bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){ - Trace("rsi") << "Make rsi for " << op << std::endl; +bool RepSetIterator::setFunctionDomain(Node op) +{ + Trace("rsi") << "Make rsi for function " << op << std::endl; Assert( d_types.empty() ); TypeNode tn = op.getType(); for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ d_types.push_back( tn[i] ); } d_owner = op; - return initialize( rext ); + return initialize(); } -// TODO : as part of #1199, the portions of this -// function which modify d_rep_set should be -// moved to TheoryModel. -bool RepSetIterator::initialize( RepBoundExt* rext ){ +bool RepSetIterator::initialize() +{ Trace("rsi") << "Initialize rep set iterator..." << std::endl; for( unsigned v=0; v<d_types.size(); v++ ){ d_index.push_back( 0 ); @@ -232,103 +237,81 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){ d_domain_elements.push_back( std::vector< Node >() ); TypeNode tn = d_types[v]; Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl; - if( tn.isSort() ){ - //must ensure uninterpreted type is non-empty. - if( !d_rep_set->hasType( tn ) ){ - //FIXME: - // terms in rep_set are now constants which mapped to terms through TheoryModel - // thus, should introduce a constant and a term. for now, just a term. - - //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 ); - Node var = d_qe->getModel()->getSomeDomainElement( tn ); - Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; - d_rep_set->add( tn, var ); - } - } bool inc = true; + bool setEnum = false; //check if it is externally bound - if( rext && rext->setBound( d_owner, v, tn, d_domain_elements[v] ) ){ - d_enum_type.push_back( ENUM_DEFAULT ); - inc = false; - //builtin: check if it is bound by bounded integer module - }else if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ - if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){ - unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] ); - if( bvt!=quantifiers::BoundedIntegers::BOUND_FINITE ){ - d_enum_type.push_back( ENUM_BOUND_INT ); - inc = false; - }else{ - //will treat in default way - } + if (d_rext) + { + inc = !d_rext->initializeRepresentativesForType(tn); + RsiEnumType rsiet = d_rext->setBound(d_owner, v, d_domain_elements[v]); + if (rsiet != ENUM_INVALID) + { + d_enum_type.push_back(rsiet); + inc = false; + setEnum = true; } } - if( !tn.isSort() ){ - if( inc ){ - if (d_qe->getTermEnumeration()->mayComplete(tn)) - { - Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; - d_rep_set->complete( tn ); - //must have succeeded - Assert( d_rep_set->hasType( tn ) ); - }else{ - Trace("rsi") << " variable cannot be bounded." << std::endl; - Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; - d_incomplete = true; - } - } + if (inc) + { + Trace("fmf-incomplete") << "Incomplete because of quantification of type " + << tn << std::endl; + d_incomplete = true; } //if we have yet to determine the type of enumeration - if( d_enum_type.size()<=v ){ - if( d_rep_set->hasType( tn ) ){ + if (!setEnum) + { + if (d_rs->hasType(tn)) + { d_enum_type.push_back( ENUM_DEFAULT ); - for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){ - //d_domain[v].push_back( j ); - d_domain_elements[v].push_back( d_rep_set->d_type_reps[tn][j] ); - } + d_rs->getRepresentatives(tn, d_domain_elements[v]); }else{ Assert( d_incomplete ); return false; } } } - //must set a variable index order based on bounded integers - if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ - Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; - std::vector< int > varOrder; - for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){ - Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i ); - Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl; - varOrder.push_back( d_qe->getTermUtil()->getVariableNum( d_owner, v ) ); - } - for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) { - if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { - varOrder.push_back(i); + + if (d_rext) + { + std::vector<unsigned> varOrder; + if (d_rext->getVariableOrder(d_owner, varOrder)) + { + if (Trace.isOn("bound-int-rsi")) + { + Trace("bound-int-rsi") << "Variable order : "; + for (unsigned i = 0; i < varOrder.size(); i++) + { + Trace("bound-int-rsi") << varOrder[i] << " "; + } + Trace("bound-int-rsi") << std::endl; } + std::vector<unsigned> indexOrder; + indexOrder.resize(varOrder.size()); + for (unsigned i = 0; i < varOrder.size(); i++) + { + Assert(varOrder[i] < indexOrder.size()); + indexOrder[varOrder[i]] = i; + } + if (Trace.isOn("bound-int-rsi")) + { + Trace("bound-int-rsi") << "Will use index order : "; + for (unsigned i = 0; i < indexOrder.size(); i++) + { + Trace("bound-int-rsi") << indexOrder[i] << " "; + } + Trace("bound-int-rsi") << std::endl; + } + setIndexOrder(indexOrder); } - Trace("bound-int-rsi") << "Variable order : "; - for( unsigned i=0; i<varOrder.size(); i++) { - Trace("bound-int-rsi") << varOrder[i] << " "; - } - Trace("bound-int-rsi") << std::endl; - std::vector< int > indexOrder; - indexOrder.resize(varOrder.size()); - for( unsigned i=0; i<varOrder.size(); i++){ - indexOrder[varOrder[i]] = i; - } - Trace("bound-int-rsi") << "Will use index order : "; - for( unsigned i=0; i<indexOrder.size(); i++) { - Trace("bound-int-rsi") << indexOrder[i] << " "; - } - Trace("bound-int-rsi") << std::endl; - setIndexOrder( indexOrder ); } //now reset the indices do_reset_increment( -1, true ); return true; } -void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ +void RepSetIterator::setIndexOrder(std::vector<unsigned>& indexOrder) +{ d_index_order.clear(); d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() ); //make the d_var_order mapping @@ -337,20 +320,23 @@ void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ } } -int RepSetIterator::resetIndex( int i, bool initial ) { +int RepSetIterator::resetIndex(unsigned i, bool initial) +{ d_index[i] = 0; - int v = d_var_order[i]; + unsigned v = d_var_order[i]; Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl; - if( d_enum_type[v]==ENUM_BOUND_INT ){ - Assert( d_owner.getKind()==FORALL ); - if( !d_qe->getBoundedIntegers()->getBoundElements( this, initial, d_owner, d_owner[0][v], d_domain_elements[v] ) ){ + if (d_rext) + { + if (!d_rext->resetIndex(this, d_owner, v, initial, d_domain_elements[v])) + { return -1; } } return d_domain_elements[v].empty() ? 0 : 1; } -int RepSetIterator::increment2( int i ){ +int RepSetIterator::incrementAtIndex(int i) +{ Assert( !isFinished() ); #ifdef DISABLE_EVAL_SKIP_MULTIPLE i = (int)d_index.size()-1; @@ -402,23 +388,31 @@ int RepSetIterator::do_reset_increment( int i, bool initial ) { int RepSetIterator::increment(){ if( !isFinished() ){ - return increment2( (int)d_index.size()-1 ); + return incrementAtIndex(d_index.size() - 1); }else{ return -1; } } -bool RepSetIterator::isFinished(){ - return d_index.empty(); -} +bool RepSetIterator::isFinished() const { return d_index.empty(); } -Node RepSetIterator::getCurrentTerm( int v ){ - int ii = d_index_order[v]; - int curr = d_index[ii]; +Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm) +{ + unsigned ii = d_index_order[v]; + unsigned curr = d_index[ii]; Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl; Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl; - Assert( 0<=curr && curr<(int)d_domain_elements[v].size() ); - return d_domain_elements[v][curr]; + Assert(0 <= curr && curr < d_domain_elements[v].size()); + Node t = d_domain_elements[v][curr]; + if (valTerm) + { + Node tt = d_rs->getTermForRepresentative(t); + if (!tt.isNull()) + { + return tt; + } + } + return t; } void RepSetIterator::debugPrint( const char* c ){ @@ -435,3 +429,5 @@ void RepSetIterator::debugPrintSmall( const char* c ){ Debug( c ) << std::endl; } +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ |