From 36f18a81d18fbfe063ec36cc101ff4ba1c069ea2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 13 Nov 2017 18:43:40 -0600 Subject: [PATCH] (Refactor) Decouple rep set iterator and quantifiers (#1339) * Refactoring rep set iterator, does not modify rep set externally. * Decouple quantifiers engine and rep set iterator. * Documentation * Clang format * Minor * Minor * More * Format * Address review. * Format * Minor --- src/theory/quantifiers/bounded_integers.cpp | 8 +- src/theory/quantifiers/first_order_model.cpp | 134 +++++++++- src/theory/quantifiers/first_order_model.h | 50 ++++ src/theory/quantifiers/full_model_check.cpp | 85 ++++-- src/theory/quantifiers/model_builder.cpp | 16 +- src/theory/quantifiers/model_engine.cpp | 7 +- src/theory/rep_set.cpp | 228 ++++++++-------- src/theory/rep_set.h | 266 +++++++++++++------ 8 files changed, 550 insertions(+), 244 deletions(-) diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index f3244937d..972b404de 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -739,14 +739,8 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl; int v = rsi->getVariableOrder( i ); Assert( q[0][v]==d_set[q][i] ); - Node t = rsi->getCurrentTerm( v ); + Node t = rsi->getCurrentTerm(v, true); Trace("bound-int-rsi") << "term : " << t << std::endl; - Node tt = rsi->d_rep_set->getTermForRepresentative(t); - if (!tt.isNull()) - { - t = tt; - Trace("bound-int-rsi") << "term (post-rep) : " << t << std::endl; - } vars.push_back( d_set[q][i] ); subs.push_back( t ); } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index f4cf1b32a..6749a8c0d 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -16,6 +16,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -26,13 +27,14 @@ #define USE_INDEX_ORDERING using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::quantifiers::fmcheck; +namespace CVC4 { +namespace theory { +namespace quantifiers { + struct sortQuantifierRelevance { FirstOrderModel * d_fm; bool operator() (Node i, Node j) { @@ -46,6 +48,83 @@ struct sortQuantifierRelevance { } }; +RepSetIterator::RsiEnumType QRepBoundExt::setBound(Node owner, + unsigned i, + std::vector& elements) +{ + // builtin: check if it is bound by bounded integer module + if (owner.getKind() == FORALL && d_qe->getBoundedIntegers()) + { + if (d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i])) + { + unsigned bvt = + d_qe->getBoundedIntegers()->getBoundVarType(owner, owner[0][i]); + if (bvt != BoundedIntegers::BOUND_FINITE) + { + d_bound_int[i] = true; + return RepSetIterator::ENUM_BOUND_INT; + } + else + { + // indicates the variable is finitely bound due to + // the (small) cardinality of its type, + // will treat in default way + } + } + } + return RepSetIterator::ENUM_INVALID; +} + +bool QRepBoundExt::resetIndex(RepSetIterator* rsi, + Node owner, + unsigned i, + bool initial, + std::vector& elements) +{ + if (d_bound_int.find(i) != d_bound_int.end()) + { + Assert(owner.getKind() == FORALL); + Assert(d_qe->getBoundedIntegers() != nullptr); + if (!d_qe->getBoundedIntegers()->getBoundElements( + rsi, initial, owner, owner[0][i], elements)) + { + return false; + } + } + return true; +} + +bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn) +{ + return d_qe->getModel()->initializeRepresentativesForType(tn); +} + +bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) +{ + // must set a variable index order based on bounded integers + if (owner.getKind() == FORALL && d_qe->getBoundedIntegers()) + { + Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; + for (unsigned i = 0; i < d_qe->getBoundedIntegers()->getNumBoundVars(owner); + i++) + { + Node v = d_qe->getBoundedIntegers()->getBoundVar(owner, i); + Trace("bound-int-rsi") << " bound var #" << i << " is " << v + << std::endl; + varOrder.push_back(d_qe->getTermUtil()->getVariableNum(owner, v)); + } + for (unsigned i = 0; i < owner[0].getNumChildren(); i++) + { + if (!d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i])) + { + varOrder.push_back(i); + } + } + return true; + } + return false; +} + FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) : TheoryModel( c, name, true ), d_qe( qe ), d_forall_asserts( c ){ @@ -104,18 +183,51 @@ void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& vi Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ //check if there is even any domain elements at all - if (!d_rep_set.hasType(tn)) { - Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; + if (!d_rep_set.hasType(tn) || d_rep_set.d_type_reps[tn].size() == 0) + { + Trace("fm-debug") << "Must create domain element for " << tn << "..." + << std::endl; Node mbt = getModelBasisTerm(tn); - Trace("fmc-model-debug") << "Add to representative set..." << std::endl; + Trace("fm-debug") << "Add to representative set..." << std::endl; d_rep_set.add(tn, mbt); - }else if( d_rep_set.d_type_reps[tn].size()==0 ){ - Message() << "empty reps" << std::endl; - exit(0); } return d_rep_set.d_type_reps[tn][0]; } +bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) +{ + if (tn.isSort()) + { + // must ensure uninterpreted type is non-empty. + if (!d_rep_set.hasType(tn)) + { + // terms in rep_set are now constants which mapped to terms through + // TheoryModel. Thus, should introduce a constant and a term. + // For now, we just add an arbitrary term. + Node var = d_qe->getModel()->getSomeDomainElement(tn); + Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn + << std::endl; + d_rep_set.add(tn, var); + } + return true; + } + else + { + // can we complete it? + if (d_qe->getTermEnumeration()->mayComplete(tn)) + { + Trace("fm-debug") << " do complete, since cardinality is small (" + << tn.getCardinality() << ")..." << std::endl; + d_rep_set.complete(tn); + // must have succeeded + Assert(d_rep_set.hasType(tn)); + return true; + } + Trace("fm-debug") << " variable cannot be bounded." << std::endl; + return false; + } +} + /** needs check */ bool FirstOrderModel::checkNeeded() { return d_forall_asserts.size()>0; @@ -1022,3 +1134,7 @@ void FirstOrderModelAbs::processInitializeQuantifier( Node q ) { Node FirstOrderModelAbs::getVariable( Node q, unsigned i ) { return q[0][d_var_order[q][i]]; } + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 6305a3807..57582a856 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -54,6 +54,40 @@ class FirstOrderModelAbs; struct IsStarAttributeId {}; typedef expr::Attribute IsStarAttribute; +/** Quantifiers representative bound + * + * This class is used for computing (finite) + * bounds for the domain of a quantifier + * in the context of a RepSetIterator + * (see theory/rep_set.h). + */ +class QRepBoundExt : public RepBoundExt +{ + public: + QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {} + virtual ~QRepBoundExt() {} + /** set bound */ + virtual RepSetIterator::RsiEnumType setBound( + Node owner, unsigned i, std::vector& elements) override; + /** reset index */ + virtual bool resetIndex(RepSetIterator* rsi, + Node owner, + unsigned i, + bool initial, + std::vector& elements) override; + /** initialize representative set for type */ + virtual bool initializeRepresentativesForType(TypeNode tn) override; + /** get variable order */ + virtual bool getVariableOrder(Node owner, + std::vector& varOrder) override; + + private: + /** quantifiers engine associated with this bound */ + QuantifiersEngine* d_qe; + /** indices that are bound integer enumeration */ + std::map d_bound_int; +}; + // TODO (#1301) : document and refactor this class class FirstOrderModel : public TheoryModel { @@ -109,6 +143,22 @@ class FirstOrderModel : public TheoryModel unsigned getModelBasisArg(Node n); /** get some domain element */ Node getSomeDomainElement(TypeNode tn); + /** initialize representative set for type + * + * This ensures that TheoryModel::d_rep_set + * is initialized for type tn. In particular: + * (1) If tn is an uninitialized (unconstrained) + * uninterpreted sort, then we interpret it + * as a set of size one, + * (2) If tn is a "small" enumerable finite type, + * then we ensure that all its values are in + * TheoryModel::d_rep_set. + * + * Returns true if the initialization was complete, + * in that the set for tn in TheoryModel::d_rep_set + * has all representatives of type tn. + */ + bool initializeRepresentativesForType(TypeNode tn); protected: /** quant engine */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 5847449cf..4277ab366 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -747,36 +747,76 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } } -class RepBoundFmcEntry : public RepBoundExt { -public: - Node d_entry; - FirstOrderModelFmc * d_fm; - bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) { - if( d_fm->isInterval(d_entry[i]) ){ - //explicitly add the interval TODO? - }else if( d_fm->isStar(d_entry[i]) ){ - //add the full range - return false; - }else{ - //only need to consider the single point - elements.push_back( d_entry[i] ); - return true; +/** Representative bound fmc entry + * + * This bound information corresponds to one + * entry in a term definition (see terminology in + * Chapter 5 of Finite Model Finding for + * Satisfiability Modulo Theories thesis). + * For example, a term definition for the body + * of a quantified formula: + * forall xyz. P( x, y, z ) + * may be: + * ( 0, 0, 0 ) -> false + * ( *, 1, 2 ) -> false + * ( *, *, * ) -> true + * Indicating that the quantified formula evaluates + * to false in the current model for x=0, y=0, z=0, + * or y=1, z=2 for any x, and evaluates to true + * otherwise. + * This class is used if we wish + * to iterate over all values corresponding to one + * of these entries. For example, for the second entry: + * (*, 1, 2 ) + * we iterate over all values of x, but only {1} + * for y and {2} for z. + */ +class RepBoundFmcEntry : public QRepBoundExt +{ + public: + RepBoundFmcEntry(QuantifiersEngine* qe, Node e, FirstOrderModelFmc* f) + : QRepBoundExt(qe), d_entry(e), d_fm(f) + { + } + ~RepBoundFmcEntry() {} + /** set bound */ + virtual RepSetIterator::RsiEnumType setBound( + Node owner, unsigned i, std::vector& elements) override + { + if (d_fm->isInterval(d_entry[i])) + { + // explicitly add the interval? } - return false; + else if (d_fm->isStar(d_entry[i])) + { + // must add the full range + } + else + { + // only need to consider the single point + elements.push_back(d_entry[i]); + return RepSetIterator::ENUM_DEFAULT; + } + return QRepBoundExt::setBound(owner, i, elements); } + + private: + /** the entry for this bound */ + Node d_entry; + /** the model builder associated with this bound */ + FirstOrderModelFmc* d_fm; }; bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) { - RepSetIterator riter( d_qe, &(fm->d_rep_set) ); Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " "; debugPrintCond("fmc-exh", c, true); Trace("fmc-exh")<< std::endl; - RepBoundFmcEntry rbfe; - rbfe.d_entry = c; - rbfe.d_fm = fm; + RepBoundFmcEntry rbfe(d_qe, c, fm); + RepSetIterator riter(d_qe->getModel()->getRepSet(), &rbfe); Trace("fmc-exh-debug") << "Set quantifier..." << std::endl; //initialize - if( riter.setQuantifier( f, &rbfe ) ){ + if (riter.setQuantifier(f)) + { Trace("fmc-exh-debug") << "Set element domains..." << std::endl; int addedLemmas = 0; //now do full iteration @@ -785,7 +825,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh-debug") << "Inst : "; std::vector< Node > ev_inst; std::vector< Node > inst; - for( int i=0; i=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_BOUND_INT ) { Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl; - riter.increment2( index-1 ); + riter.incrementAtIndex(index - 1); } } } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index a72293ea1..358838b11 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -108,12 +108,14 @@ void QModelBuilder::debugModel( TheoryModel* m ){ for( unsigned j=0; jgetRepSetPtr()); + QRepBoundExt qrbe(d_qe); + RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe); if( riter.setQuantifier( f ) ){ while( !riter.isFinished() ){ tests++; std::vector< Node > terms; - for( int k=0; kgetInstantiation( f, vars, terms ); @@ -419,7 +421,8 @@ QModelBuilderIG::Statistics::~Statistics(){ //do exhaustive instantiation int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { if( optUseModel() ){ - RepSetIterator riter(d_qe, d_qe->getModel()->getRepSetPtr()); + QRepBoundExt qrbe(d_qe); + RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe); if( riter.setQuantifier( f ) ){ FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel(); Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; @@ -452,11 +455,12 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in } if( eval==1 ){ //instantiation is already true -> skip - riter.increment2( depIndex ); + riter.incrementAtIndex(depIndex); }else{ //instantiation was not shown to be true, construct the match InstMatch m( f ); - for( int i=0; igetModel()->getRepSetPtr()); + QRepBoundExt qrbe(d_quantEngine); + RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe); if( riter.setQuantifier( f ) ){ Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; if( !riter.isIncomplete() ){ @@ -287,7 +287,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); - for( int i=0; i -#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& reps) const +{ + std::map >::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& 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() ); 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; jd_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; igetBoundedIntegers()->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; igetBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { - varOrder.push_back(i); + + if (d_rext) + { + std::vector 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 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 indexOrder; - indexOrder.resize(varOrder.size()); - for( unsigned i=0; i& indexOrder ){ +void RepSetIterator::setIndexOrder(std::vector& 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 */ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index a20e56184..5b75fa943 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -74,6 +74,8 @@ public: unsigned getNumRepresentatives(TypeNode tn) const; /** get representative at index */ Node getRepresentative(TypeNode tn, unsigned i) const; + /** get representatives of type tn, appends them to reps */ + void getRepresentatives(TypeNode tn, std::vector& reps) const; /** add representative n for type tn, where n has type tn */ void add( TypeNode tn, Node n ); /** returns index in d_type_reps for node n */ @@ -113,93 +115,195 @@ public: //representative domain typedef std::vector< int > RepDomain; +class RepBoundExt; -class RepBoundExt { - public: - virtual ~RepBoundExt() {} - virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0; -}; - -/** this class iterates over a RepSet */ +/** Rep set iterator. + * + * This class is used for iterating over (tuples of) terms + * in the domain(s) of a RepSet. + * + * To use it, first it must + * be initialized with a call to: + * - setQuantifier or setFunctionDomain + * which initializes the d_owner field and sets up + * initial information. + * + * Then, we increment over the tuples of terms in the + * domains of the owner of this iterator using: + * - increment and incrementAtIndex + * + * TODO (#1199): this class needs further documentation. + */ class RepSetIterator { public: - enum { - ENUM_DEFAULT, - ENUM_BOUND_INT, - }; -private: - QuantifiersEngine * d_qe; - //initialize function - bool initialize( RepBoundExt* rext = NULL ); - //for int ranges - std::map< int, Node > d_lower_bounds; - //for set ranges - std::map< int, std::vector< Node > > d_setm_bounds; - //domain size - int domainSize( int i ); - //node this is rep set iterator is for - Node d_owner; - //reset index, 1:success, 0:empty, -1:fail - int resetIndex( int i, bool initial = false ); - /** set index order */ - void setIndexOrder( std::vector< int >& indexOrder ); - /** do reset increment the iterator at index=counter */ - int do_reset_increment( int counter, bool initial = false ); - //ordering for variables we are indexing over - // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, - // then we consider instantiations in this order: - // a/x a/y a/z - // a/x b/y a/z - // b/x a/y a/z - // b/x b/y a/z - // ... - std::vector< int > d_index_order; - //variables to index they are considered at - // for example, if d_index_order = { 2, 0, 1 } - // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } - std::map< int, int > d_var_order; - //are we only considering a strict subset of the domain of the quantifier? - bool d_incomplete; -public: - RepSetIterator( QuantifiersEngine * qe, RepSet* rs ); - ~RepSetIterator(){} - //set that this iterator will be iterating over instantiations for a quantifier - bool setQuantifier( Node f, RepBoundExt* rext = NULL ); - //set that this iterator will be iterating over the domain of a function - bool setFunctionDomain( Node op, RepBoundExt* rext = NULL ); -public: - //pointer to model - RepSet* d_rep_set; - //enumeration type? - std::vector< int > d_enum_type; - //current tuple we are considering - std::vector< int > d_index; - //types we are considering - std::vector< TypeNode > d_types; - //domain we are considering - std::vector< std::vector< Node > > d_domain_elements; + enum RsiEnumType + { + ENUM_INVALID = 0, + ENUM_DEFAULT, + ENUM_BOUND_INT, + }; + public: - /** increment the iterator at index=counter */ - int increment2( int i ); - /** increment the iterator */ - int increment(); - /** is the iterator finished? */ - bool isFinished(); - /** get the i_th term we are considering */ - Node getCurrentTerm( int v ); - /** get the number of terms we are considering */ - int getNumTerms() { return (int)d_index_order.size(); } - /** debug print */ - void debugPrint( const char* c ); - void debugPrintSmall( const char* c ); - //get index order, returns var # - int getIndexOrder( int v ) { return d_index_order[v]; } - //get variable order, returns index # - int getVariableOrder( int i ) { return d_var_order[i]; } - //is incomplete - bool isIncomplete() { return d_incomplete; } + RepSetIterator(const RepSet* rs, RepBoundExt* rext); + ~RepSetIterator() {} + /** set that this iterator will be iterating over instantiations for a + * quantifier */ + bool setQuantifier(Node q); + /** set that this iterator will be iterating over the domain of a function */ + bool setFunctionDomain(Node op); + /** increment the iterator */ + int increment(); + /** increment the iterator at index + * This increments the i^th field of the + * iterator, for examples, see operator next_i + * in Figure 2 of Reynolds et al. CADE 2013. + */ + int incrementAtIndex(int i); + /** is the iterator finished? */ + bool isFinished() const; + /** get domain size of the i^th field of this iterator */ + unsigned domainSize(unsigned i); + /** get the i^th term in the tuple we are considering */ + Node getCurrentTerm(unsigned v, bool valTerm = false); + /** get the number of terms in the tuple we are considering */ + unsigned getNumTerms() { return d_index_order.size(); } + /** get index order, returns var # */ + unsigned getIndexOrder(unsigned v) { return d_index_order[v]; } + /** get variable order, returns index # */ + unsigned getVariableOrder(unsigned i) { return d_var_order[i]; } + /** is incomplete + * Returns true if we are iterating over a strict subset of + * the domain of the quantified formula or function. + */ + bool isIncomplete() { return d_incomplete; } + /** debug print methods */ + void debugPrint(const char* c); + void debugPrintSmall(const char* c); + // TODO (#1199): these should be private + /** enumeration type for each field */ + std::vector d_enum_type; + /** the current tuple we are considering */ + std::vector d_index; + +private: + /** rep set associated with this iterator */ + const RepSet* d_rs; + /** rep set external bound information for this iterator */ + RepBoundExt* d_rext; + /** types we are considering */ + std::vector d_types; + /** for each argument, the domain we are iterating over */ + std::vector > d_domain_elements; + /** initialize + * This is called when the owner of this iterator is set. + * It initializes the typing information for the types + * that are involved in this iterator, initializes the + * domain elements we are iterating over, and variable + * and index orderings we are considering. + */ + bool initialize(); + /** owner + * This is the term that we are iterating for, which may either be: + * (1) a quantified formula, or + * (2) a function. + */ + Node d_owner; + /** reset index, 1:success, 0:empty, -1:fail */ + int resetIndex(unsigned i, bool initial = false); + /** set index order (see below) */ + void setIndexOrder(std::vector& indexOrder); + /** do reset increment the iterator at index=counter */ + int do_reset_increment(int counter, bool initial = false); + /** ordering for variables we are iterating over + * For example, given reps = { a, b } and quantifier + * forall( x, y, z ) P( x, y, z ) + * with d_index_order = { 2, 0, 1 }, + * then we consider instantiations in this order: + * a/x a/y a/z + * a/x b/y a/z + * b/x a/y a/z + * b/x b/y a/z + * ... + */ + std::vector d_index_order; + /** Map from variables to the index they are considered at + * For example, if d_index_order = { 2, 0, 1 } + * then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } + */ + std::map d_var_order; + /** incomplete flag */ + bool d_incomplete; };/* class RepSetIterator */ +/** Representative bound external + * + * This class manages bound information + * for an instance of a RepSetIterator. + * Its main functionalities are to set + * bounds on the domain of the iterator + * over quantifiers and function arguments. + */ +class RepBoundExt +{ + public: + virtual ~RepBoundExt() {} + /** set bound + * + * This method initializes the vector "elements" + * with list of terms to iterate over for the i^th + * field of owner, where owner may be : + * (1) A function, in which case we are iterating + * over domain elements of its argument type, + * (2) A quantified formula, in which case we are + * iterating over domain elements of the type + * of its i^th bound variable. + */ + virtual RepSetIterator::RsiEnumType setBound(Node owner, + unsigned i, + std::vector& elements) = 0; + /** reset index + * + * This method initializes iteration for the i^th + * field of owner, based on the current state of + * the iterator rsi. It initializes the vector + * "elements" with all appropriate terms to + * iterate over in this context. + * initial is whether this is the first call + * to this function for this iterator. + * + * This method returns false if we were unable + * to establish (finite) bounds for the current + * field we are considering, which indicates that + * the iterator will terminate with a failure. + */ + virtual bool resetIndex(RepSetIterator* rsi, + Node owner, + unsigned i, + bool initial, + std::vector& elements) + { + return true; + } + /** initialize representative set for type + * + * Returns true if the representative set associated + * with this bound has been given a complete interpretation + * for type tn. + */ + virtual bool initializeRepresentativesForType(TypeNode tn) { return false; } + /** get variable order + * If this method returns true, then varOrder is the order + * in which we want to consider variables for the iterator. + * If this method returns false, then varOrder is unchanged + * and the RepSetIterator is free to choose a default + * variable order. + */ + virtual bool getVariableOrder(Node owner, std::vector& varOrder) + { + return false; + } +}; + }/* CVC4::theory namespace */ }/* CVC4 namespace */ -- 2.30.2