From 06b0f44a375a74780f91efd4cbf6afc127acd8be Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 26 Apr 2022 17:06:45 -0500 Subject: [PATCH] Move rep set iterator to its own file (#8647) --- src/CMakeLists.txt | 2 + .../quantifiers/fmf/bounded_integers.cpp | 3 +- src/theory/quantifiers/fmf/bounded_integers.h | 2 +- .../quantifiers/fmf/full_model_check.cpp | 3 +- .../quantifiers/quant_bound_inference.cpp | 2 +- .../quantifiers/quant_bound_inference.h | 2 +- .../quantifiers/quant_rep_bound_ext.cpp | 6 +- src/theory/quantifiers/quant_rep_bound_ext.h | 10 +- src/theory/rep_set.cpp | 274 --------------- src/theory/rep_set.h | 211 +---------- src/theory/rep_set_iterator.cpp | 331 ++++++++++++++++++ src/theory/rep_set_iterator.h | 240 +++++++++++++ 12 files changed, 589 insertions(+), 497 deletions(-) create mode 100644 src/theory/rep_set_iterator.cpp create mode 100644 src/theory/rep_set_iterator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ea10d8fcf..6facce4e8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -998,6 +998,8 @@ libcvc5_add_sources( theory/relevance_manager.h theory/rep_set.cpp theory/rep_set.h + theory/rep_set_iterator.cpp + theory/rep_set_iterator.h theory/rewriter.cpp theory/rewriter.h theory/rewriter_attributes.h diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index ee2804d97..ef47b2fb3 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -28,6 +28,7 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" +#include "theory/rep_set_iterator.h" #include "theory/rewriter.h" #include "util/rational.h" @@ -560,7 +561,7 @@ BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const } void BoundedIntegers::getBoundVarIndices(Node q, - std::vector& indices) const + std::vector& indices) const { std::map >::const_iterator it = d_set.find(q); if (it != d_set.end()) diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index fee80ded4..08bad9f56 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -193,7 +193,7 @@ private: * bound, z has a finite bound assuming x has a finite bound, and y does not * have a finite bound. */ - void getBoundVarIndices(Node q, std::vector& indices) const; + void getBoundVarIndices(Node q, std::vector& indices) const; /** * Get bound elements * diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index c21ed4393..4c6eac6eb 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -29,6 +29,7 @@ #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/rep_set_iterator.h" #include "theory/rewriter.h" using namespace cvc5::internal::kind; @@ -834,7 +835,7 @@ class RepBoundFmcEntry : public QRepBoundExt ~RepBoundFmcEntry() {} /** set bound */ virtual RsiEnumType setBound(Node owner, - unsigned i, + size_t i, std::vector& elements) override { if (!d_fm->isStar(d_entry[i])) diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index d6e3f61b1..3e521c57e 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -94,7 +94,7 @@ BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v) } void QuantifiersBoundInference::getBoundVarIndices( - Node q, std::vector& indices) const + Node q, std::vector& indices) const { Assert(indices.empty()); // we take the bounded variables first diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h index c507fcf6d..a3afe6f66 100644 --- a/src/theory/quantifiers/quant_bound_inference.h +++ b/src/theory/quantifiers/quant_bound_inference.h @@ -93,7 +93,7 @@ class QuantifiersBoundInference * * For details, see BoundedIntegers::getBoundVarIndices. */ - void getBoundVarIndices(Node q, std::vector& indices) const; + void getBoundVarIndices(Node q, std::vector& indices) const; /** * Get bound elements * diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp index b83b4a207..79cd4c3d4 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.cpp +++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp @@ -30,7 +30,7 @@ QRepBoundExt::QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m) } RsiEnumType QRepBoundExt::setBound(Node owner, - unsigned i, + size_t i, std::vector& elements) { // builtin: check if it is bound by bounded integer module @@ -51,7 +51,7 @@ RsiEnumType QRepBoundExt::setBound(Node owner, bool QRepBoundExt::resetIndex(RepSetIterator* rsi, Node owner, - unsigned i, + size_t i, bool initial, std::vector& elements) { @@ -73,7 +73,7 @@ bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn) return d_model->initializeRepresentativesForType(tn); } -bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) +bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) { // must set a variable index order based on bounded integers if (owner.getKind() != FORALL) diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h index b74a663fc..9f950a888 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.h +++ b/src/theory/quantifiers/quant_rep_bound_ext.h @@ -21,7 +21,7 @@ #include #include "expr/node.h" -#include "theory/rep_set.h" +#include "theory/rep_set_iterator.h" #include "theory/theory_model.h" namespace cvc5::internal { @@ -44,18 +44,18 @@ class QRepBoundExt : public RepBoundExt virtual ~QRepBoundExt() {} /** set bound */ RsiEnumType setBound(Node owner, - unsigned i, + size_t i, std::vector& elements) override; /** reset index */ bool resetIndex(RepSetIterator* rsi, Node owner, - unsigned i, + size_t i, bool initial, std::vector& elements) override; /** initialize representative set for type */ bool initializeRepresentativesForType(TypeNode tn) override; /** get variable order */ - bool getVariableOrder(Node owner, std::vector& varOrder) override; + bool getVariableOrder(Node owner, std::vector& varOrder) override; private: /** Reference to the quantifiers bound inference */ @@ -63,7 +63,7 @@ class QRepBoundExt : public RepBoundExt /** Pointer to the quantifiers model */ FirstOrderModel* d_model; /** indices that are bound integer enumeration */ - std::map d_bound_int; + std::map d_bound_int; }; } // namespace quantifiers diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 251d00ad1..fb421a997 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -191,279 +191,5 @@ void RepSet::toStream(std::ostream& out){ } } -RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext) - : d_rs(rs), d_rext(rext), d_incomplete(false) -{ -} - -unsigned RepSetIterator::domainSize(unsigned i) -{ - unsigned v = d_var_order[i]; - return d_domain_elements[v].size(); -} - -TypeNode RepSetIterator::getTypeOf(unsigned i) const { return d_types[i]; } - -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 < q[0].getNumChildren(); i++) - { - d_types.push_back(q[0][i].getType()); - } - d_owner = q; - return initialize(); -} - -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() ); - TypeNode tn = d_types[v]; - Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl; - bool inc = true; - bool setEnum = false; - //check if it is externally bound - 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 (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 (!setEnum) - { - if (d_rs->hasType(tn)) - { - d_enum_type.push_back( ENUM_DEFAULT ); - if (const auto* type_reps = d_rs->getTypeRepsOrNull(tn)) - { - std::vector& v_domain_elements = d_domain_elements[v]; - v_domain_elements.insert(v_domain_elements.end(), - type_reps->begin(), type_reps->end()); - } - }else{ - Assert(d_incomplete); - return false; - } - } - } - - if (d_rext) - { - std::vector varOrder; - if (d_rext->getVariableOrder(d_owner, varOrder)) - { - if (TraceIsOn("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 (TraceIsOn("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); - } - } - //now reset the indices - do_reset_increment( -1, true ); - return true; -} - -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 - for( unsigned i=0; i=0){ - Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; - } - while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){ - i--; - if( i>=0){ - Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; - } - } - if( i==-1 ){ - Trace("rsi-debug") << "increment failed" << std::endl; - d_index.clear(); - return -1; - }else{ - Trace("rsi-debug") << "increment " << i << std::endl; - d_index[i]++; - return do_reset_increment( i ); - } -} - -int RepSetIterator::do_reset_increment( int i, bool initial ) { - Trace("rsi-debug") << "RepSetIterator::do_reset_increment: " << i - << ", initial=" << initial << std::endl; - for( unsigned ii=(i+1); ii 0) - { - // increment at the previous index - return incrementAtIndex(ii - 1); - } - else - { - // this is the first index, we are done - d_index.clear(); - return -1; - } - } - } - Trace("rsi-debug") << "Finished, return " << i << std::endl; - return i; -} - -int RepSetIterator::increment(){ - if( !isFinished() ){ - return incrementAtIndex(d_index.size() - 1); - }else{ - return -1; - } -} - -bool RepSetIterator::isFinished() const { return d_index.empty(); } - -Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const -{ - unsigned ii = d_index_order[i]; - unsigned curr = d_index[ii]; - Trace("rsi-debug") << "rsi : get term " << i - << ", index order = " << d_index_order[i] << std::endl; - Trace("rsi-debug") << "rsi : curr = " << curr << " / " - << d_domain_elements[i].size() << std::endl; - Assert(0 <= curr && curr < d_domain_elements[i].size()); - Node t = d_domain_elements[i][curr]; - Trace("rsi-debug") << "rsi : term = " << t << std::endl; - if (valTerm) - { - Node tt = d_rs->getTermForRepresentative(t); - if (!tt.isNull()) - { - Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl; - return tt; - } - } - Trace("rsi-debug") << "rsi : return" << std::endl; - return t; -} - -void RepSetIterator::getCurrentTerms(std::vector& terms) const -{ - for (unsigned i = 0, size = d_index_order.size(); i < size; i++) - { - terms.push_back(getCurrentTerm(i)); - } -} - -void RepSetIterator::debugPrint( const char* c ){ - for( unsigned v=0; v d_values_to_terms; };/* class RepSet */ -//representative domain -typedef std::vector< int > RepDomain; - -class RepBoundExt; - -/** - * Representative set iterator enumeration type, which indicates how the - * bound on a variable was determined. - */ -enum RsiEnumType -{ - // the bound on the variable is invalid - ENUM_INVALID = 0, - // the bound on the variable was determined in the default way, i.e. based - // on an enumeration of terms in the model. - ENUM_DEFAULT, - // The bound on the variable was determined in a custom way, i.e. via a - // quantifiers module like the BoundedIntegers module. - ENUM_CUSTOM, -}; - -/** 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: - RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr); - ~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 type of terms in the i^th field of this iterator */ - TypeNode getTypeOf(unsigned i) const; - /** - * Get the value for the i^th field in the tuple we are currently considering. - * If valTerm is true, we return a term instead of a value by calling - * RepSet::getTermForRepresentative on the value. - */ - Node getCurrentTerm(unsigned i, bool valTerm = false) const; - /** get the number of terms in the tuple we are considering */ - unsigned getNumTerms() const { return d_index_order.size(); } - /** get current terms */ - void getCurrentTerms(std::vector& terms) const; - /** 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 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; - } -}; } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/rep_set_iterator.cpp b/src/theory/rep_set_iterator.cpp new file mode 100644 index 000000000..52fa0c876 --- /dev/null +++ b/src/theory/rep_set_iterator.cpp @@ -0,0 +1,331 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of representative set utilities. + */ + +#include "theory/rep_set_iterator.h" + +#include + +#include "theory/type_enumerator.h" + +using namespace std; +using namespace cvc5::internal::kind; + +namespace cvc5::internal { +namespace theory { + +RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext) + : d_rs(rs), d_rext(rext), d_incomplete(false) +{ +} + +size_t RepSetIterator::domainSize(size_t i) const +{ + size_t v = d_var_order[i]; + return d_domain_elements[v].size(); +} + +TypeNode RepSetIterator::getTypeOf(size_t i) const { return d_types[i]; } + +bool RepSetIterator::setQuantifier(Node q) +{ + Trace("rsi") << "Make rsi for quantified formula " << q << std::endl; + Assert(d_types.empty()); + // store indicies + for (const Node& v : q[0]) + { + d_types.push_back(v.getType()); + } + d_owner = q; + return initialize(); +} + +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(); +} + +bool RepSetIterator::initialize() +{ + Trace("rsi") << "Initialize rep set iterator..." << std::endl; + size_t ntypes = d_types.size(); + d_var_order.resize(ntypes); + for (size_t v = 0; v < ntypes; v++) + { + d_index.push_back(0); + // store default index order + d_index_order.push_back(v); + d_var_order[v] = v; + // store default domain + // d_domain.push_back( RepDomain() ); + d_domain_elements.push_back(std::vector()); + TypeNode tn = d_types[v]; + Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl; + bool inc = true; + bool setEnum = false; + // check if it is externally bound + 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 (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 (!setEnum) + { + if (d_rs->hasType(tn)) + { + d_enum_type.push_back(ENUM_DEFAULT); + if (const auto* type_reps = d_rs->getTypeRepsOrNull(tn)) + { + std::vector& v_domain_elements = d_domain_elements[v]; + v_domain_elements.insert( + v_domain_elements.end(), type_reps->begin(), type_reps->end()); + } + } + else + { + Assert(d_incomplete); + return false; + } + } + } + + if (d_rext) + { + std::vector varOrder; + if (d_rext->getVariableOrder(d_owner, varOrder)) + { + if (TraceIsOn("bound-int-rsi")) + { + Trace("bound-int-rsi") << "Variable order : "; + for (size_t v : varOrder) + { + Trace("bound-int-rsi") << v << " "; + } + Trace("bound-int-rsi") << std::endl; + } + size_t nvars = varOrder.size(); + std::vector indexOrder; + indexOrder.resize(nvars); + for (size_t i = 0; i < nvars; i++) + { + Assert(varOrder[i] < indexOrder.size()); + indexOrder[varOrder[i]] = i; + } + if (TraceIsOn("bound-int-rsi")) + { + Trace("bound-int-rsi") << "Will use index order : "; + for (size_t i = 0, isize = indexOrder.size(); i < isize; i++) + { + Trace("bound-int-rsi") << indexOrder[i] << " "; + } + Trace("bound-int-rsi") << std::endl; + } + setIndexOrder(indexOrder); + } + } + // now reset the indices + doResetIncrement(-1, true); + return true; +} + +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 + for (size_t i = 0, isize = d_index_order.size(); i < isize; i++) + { + d_var_order[d_index_order[i]] = i; + } +} + +int RepSetIterator::resetIndex(size_t i, bool initial) +{ + d_index[i] = 0; + size_t v = d_var_order[i]; + Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v + << ", initial = " << initial << std::endl; + 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::incrementAtIndex(int i) +{ + Assert(!isFinished()); + Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i << std::endl; + // increment d_index + if (i >= 0) + { + Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) + << std::endl; + } + while (i >= 0 && d_index[i] >= (int)(domainSize(i) - 1)) + { + i--; + if (i >= 0) + { + Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) + << std::endl; + } + } + if (i == -1) + { + Trace("rsi-debug") << "increment failed" << std::endl; + d_index.clear(); + return -1; + } + else + { + Trace("rsi-debug") << "increment " << i << std::endl; + d_index[i]++; + return doResetIncrement(i); + } +} + +int RepSetIterator::doResetIncrement(int i, bool initial) +{ + Trace("rsi-debug") << "RepSetIterator::doResetIncrement: " << i + << ", initial=" << initial << std::endl; + for (size_t ii = (i + 1); ii < d_index.size(); ii++) + { + bool emptyDomain = false; + int ri_res = resetIndex(ii, initial); + if (ri_res == -1) + { + // failed + d_index.clear(); + d_incomplete = true; + break; + } + else if (ri_res == 0) + { + emptyDomain = true; + } + // force next iteration if currently an empty domain + if (emptyDomain) + { + Trace("rsi-debug") << "This is an empty domain (index " << ii << ")." + << std::endl; + if (ii > 0) + { + // increment at the previous index + return incrementAtIndex(ii - 1); + } + else + { + // this is the first index, we are done + d_index.clear(); + return -1; + } + } + } + Trace("rsi-debug") << "Finished, return " << i << std::endl; + return i; +} + +int RepSetIterator::increment() +{ + if (!isFinished()) + { + return incrementAtIndex(d_index.size() - 1); + } + else + { + return -1; + } +} + +bool RepSetIterator::isFinished() const { return d_index.empty(); } + +Node RepSetIterator::getCurrentTerm(size_t i, bool valTerm) const +{ + size_t ii = d_index_order[i]; + size_t curr = d_index[ii]; + Trace("rsi-debug") << "rsi : get term " << i + << ", index order = " << d_index_order[i] << std::endl; + Trace("rsi-debug") << "rsi : curr = " << curr << " / " + << d_domain_elements[i].size() << std::endl; + Assert(0 <= curr && curr < d_domain_elements[i].size()); + Node t = d_domain_elements[i][curr]; + Trace("rsi-debug") << "rsi : term = " << t << std::endl; + if (valTerm) + { + Node tt = d_rs->getTermForRepresentative(t); + if (!tt.isNull()) + { + Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl; + return tt; + } + } + Trace("rsi-debug") << "rsi : return" << std::endl; + return t; +} + +void RepSetIterator::getCurrentTerms(std::vector& terms) const +{ + for (size_t i = 0, size = d_index_order.size(); i < size; i++) + { + terms.push_back(getCurrentTerm(i)); + } +} + +void RepSetIterator::debugPrint(const char* c) +{ + for (size_t v = 0, isize = d_index.size(); v < isize; v++) + { + Trace(c) << v << " : " << getCurrentTerm(v) << std::endl; + } +} + +void RepSetIterator::debugPrintSmall(const char* c) +{ + Trace(c) << "RI: "; + for (size_t v = 0, isize = d_index.size(); v < isize; v++) + { + Trace(c) << v << ": " << getCurrentTerm(v) << " "; + } + Trace(c) << std::endl; +} + +} // namespace theory +} // namespace cvc5::internal diff --git a/src/theory/rep_set_iterator.h b/src/theory/rep_set_iterator.h new file mode 100644 index 000000000..0fd994d9c --- /dev/null +++ b/src/theory/rep_set_iterator.h @@ -0,0 +1,240 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Representative set utilities. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__REP_SET_ITERATOR_H +#define CVC5__THEORY__REP_SET_ITERATOR_H + +#include +#include + +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/rep_set.h" + +namespace cvc5::internal { +namespace theory { + +// representative domain +typedef std::vector RepDomain; + +class RepBoundExt; + +/** + * Representative set iterator enumeration type, which indicates how the + * bound on a variable was determined. + */ +enum RsiEnumType +{ + // the bound on the variable is invalid + ENUM_INVALID = 0, + // the bound on the variable was determined in the default way, i.e. based + // on an enumeration of terms in the model. + ENUM_DEFAULT, + // The bound on the variable was determined in a custom way, i.e. via a + // quantifiers module like the BoundedIntegers module. + ENUM_CUSTOM, +}; + +/** 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 + */ +class RepSetIterator +{ + public: + RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr); + ~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 */ + size_t domainSize(size_t i) const; + /** Get the type of terms in the i^th field of this iterator */ + TypeNode getTypeOf(size_t i) const; + /** + * Get the value for the i^th field in the tuple we are currently considering. + * If valTerm is true, we return a term instead of a value by calling + * RepSet::getTermForRepresentative on the value. + */ + Node getCurrentTerm(size_t i, bool valTerm = false) const; + /** get the number of terms in the tuple we are considering */ + size_t getNumTerms() const { return d_index_order.size(); } + /** get current terms */ + void getCurrentTerms(std::vector& terms) const; + /** get index order, returns var # */ + size_t getIndexOrder(size_t v) const { return d_index_order[v]; } + /** get variable order, returns index # */ + size_t getVariableOrder(size_t i) const { 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); + /** 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(size_t i, bool initial = false); + /** set index order (see below) */ + void setIndexOrder(std::vector& indexOrder); + /** do reset increment the iterator at index=counter */ + int doResetIncrement(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::vector 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 RsiEnumType setBound(Node owner, + size_t 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, + size_t 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; + } +}; + +} // namespace theory +} // namespace cvc5::internal + +#endif /* CVC5__THEORY__REP_SET_H */ -- 2.30.2