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
#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"
}
void BoundedIntegers::getBoundVarIndices(Node q,
- std::vector<unsigned>& indices) const
+ std::vector<size_t>& indices) const
{
std::map<Node, std::vector<Node> >::const_iterator it = d_set.find(q);
if (it != d_set.end())
* 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<unsigned>& indices) const;
+ void getBoundVarIndices(Node q, std::vector<size_t>& indices) const;
/**
* Get bound elements
*
#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;
~RepBoundFmcEntry() {}
/** set bound */
virtual RsiEnumType setBound(Node owner,
- unsigned i,
+ size_t i,
std::vector<Node>& elements) override
{
if (!d_fm->isStar(d_entry[i]))
}
void QuantifiersBoundInference::getBoundVarIndices(
- Node q, std::vector<unsigned>& indices) const
+ Node q, std::vector<size_t>& indices) const
{
Assert(indices.empty());
// we take the bounded variables first
*
* For details, see BoundedIntegers::getBoundVarIndices.
*/
- void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
+ void getBoundVarIndices(Node q, std::vector<size_t>& indices) const;
/**
* Get bound elements
*
}
RsiEnumType QRepBoundExt::setBound(Node owner,
- unsigned i,
+ size_t i,
std::vector<Node>& elements)
{
// builtin: check if it is bound by bounded integer module
bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
Node owner,
- unsigned i,
+ size_t i,
bool initial,
std::vector<Node>& elements)
{
return d_model->initializeRepresentativesForType(tn);
}
-bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
+bool QRepBoundExt::getVariableOrder(Node owner, std::vector<size_t>& varOrder)
{
// must set a variable index order based on bounded integers
if (owner.getKind() != FORALL)
#include <map>
#include "expr/node.h"
-#include "theory/rep_set.h"
+#include "theory/rep_set_iterator.h"
#include "theory/theory_model.h"
namespace cvc5::internal {
virtual ~QRepBoundExt() {}
/** set bound */
RsiEnumType setBound(Node owner,
- unsigned i,
+ size_t i,
std::vector<Node>& elements) override;
/** reset index */
bool resetIndex(RepSetIterator* rsi,
Node owner,
- unsigned i,
+ size_t i,
bool initial,
std::vector<Node>& elements) override;
/** initialize representative set for type */
bool initializeRepresentativesForType(TypeNode tn) override;
/** get variable order */
- bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
+ bool getVariableOrder(Node owner, std::vector<size_t>& varOrder) override;
private:
/** Reference to the quantifiers bound inference */
/** Pointer to the quantifiers model */
FirstOrderModel* d_model;
/** indices that are bound integer enumeration */
- std::map<unsigned, bool> d_bound_int;
+ std::map<size_t, bool> d_bound_int;
};
} // namespace quantifiers
}
}
-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<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;
- for( unsigned v=0; v<d_types.size(); 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< Node >() );
- 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<Node>& 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<unsigned> 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<unsigned> 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<unsigned>& 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<d_index_order.size(); i++ ){
- d_var_order[d_index_order[i]] = i;
- }
-}
-
-int RepSetIterator::resetIndex(unsigned i, bool initial)
-{
- d_index[i] = 0;
- unsigned 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());
-#ifdef DISABLE_EVAL_SKIP_MULTIPLE
- i = (int)d_index.size()-1;
-#endif
- 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 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<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(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<Node>& 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_index.size(); v++ ){
- Trace( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
- }
-}
-
-void RepSetIterator::debugPrintSmall( const char* c ){
- Trace( c ) << "RI: ";
- for( unsigned v=0; v<d_index.size(); v++ ){
- Trace( c ) << v << ": " << getCurrentTerm( v ) << " ";
- }
- Trace( c ) << std::endl;
-}
-
} // namespace theory
} // namespace cvc5::internal
* directory for licensing information.
* ****************************************************************************
*
- * Representative set class and utilities.
+ * Representative set class.
*/
#include "cvc5_private.h"
namespace cvc5::internal {
namespace theory {
-class QuantifiersEngine;
-
/** representative set
*
* This class contains finite lists of values for types, typically values and
std::map<Node, Node> 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<Node>& 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<RsiEnumType> d_enum_type;
- /** the current tuple we are considering */
- std::vector<int> 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<TypeNode> d_types;
- /** for each argument, the domain we are iterating over */
- std::vector<std::vector<Node> > 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<unsigned>& 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<unsigned> 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<unsigned, unsigned> 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<Node>& 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<Node>& 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<unsigned>& varOrder)
- {
- return false;
- }
-};
} // namespace theory
} // namespace cvc5::internal
--- /dev/null
+/******************************************************************************
+ * 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 <unordered_set>
+
+#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<Node>());
+ 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<Node>& 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<size_t> 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<size_t> 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<size_t>& 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<Node>& 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
--- /dev/null
+/******************************************************************************
+ * 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 <map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/rep_set.h"
+
+namespace cvc5::internal {
+namespace theory {
+
+// 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
+ */
+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<Node>& 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<RsiEnumType> d_enum_type;
+ /** the current tuple we are considering */
+ std::vector<int> 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<TypeNode> d_types;
+ /** for each argument, the domain we are iterating over */
+ std::vector<std::vector<Node> > 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<size_t>& 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<size_t> 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<size_t> 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<Node>& 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<Node>& 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<size_t>& varOrder)
+ {
+ return false;
+ }
+};
+
+} // namespace theory
+} // namespace cvc5::internal
+
+#endif /* CVC5__THEORY__REP_SET_H */
projects / cvc5.git / commitdiff