theory/quantifiers/quant_epr.h
theory/quantifiers/quant_relevance.cpp
theory/quantifiers/quant_relevance.h
+ theory/quantifiers/quant_rep_bound_ext.cpp
+ theory/quantifiers/quant_rep_bound_ext.h
theory/quantifiers/quant_split.cpp
theory/quantifiers/quant_split.h
theory/quantifiers/quant_util.cpp
namespace theory {
namespace quantifiers {
-RepSetIterator::RsiEnumType QRepBoundExt::setBound(Node owner,
- unsigned i,
- std::vector<Node>& 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<Node>& 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<unsigned>& 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)
struct IsStarAttributeId {};
typedef expr::Attribute<IsStarAttributeId, bool> 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 */
- RepSetIterator::RsiEnumType setBound(Node owner,
- unsigned i,
- std::vector<Node>& elements) override;
- /** reset index */
- bool resetIndex(RepSetIterator* rsi,
- Node owner,
- unsigned 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;
-
- private:
- /** quantifiers engine associated with this bound */
- QuantifiersEngine* d_qe;
- /** indices that are bound integer enumeration */
- std::map<unsigned, bool> d_bound_int;
-};
-
// TODO (#1301) : document and refactor this class
class FirstOrderModel : public TheoryModel
{
d_bnd_it.clear();
}
-bool BoundedIntegers::isBound( Node f, Node v ) {
- return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
-}
-
bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) {
if( visited.find( b )==visited.end() ){
visited[b] = true;
}
Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl;
}
-void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
+void BoundedIntegers::setBoundedVar(Node q, Node v, BoundVarType bound_type)
+{
d_bound_type[q][v] = bound_type;
d_set_nums[q][v] = d_set[q].size();
d_set[q].push_back( v );
- Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl;
+ Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v
+ << std::endl;
}
void BoundedIntegers::checkOwnership(Node f)
}
}
-unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) {
- std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v );
- if( it==d_bound_type[q].end() ){
+bool BoundedIntegers::isBound(Node q, Node v) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator its = d_set.find(q);
+ if (its == d_set.end())
+ {
+ return false;
+ }
+ return std::find(its->second.begin(), its->second.end(), v)
+ != its->second.end();
+}
+
+BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const
+{
+ std::map<Node, std::map<Node, BoundVarType> >::const_iterator itb =
+ d_bound_type.find(q);
+ if (itb == d_bound_type.end())
+ {
return BOUND_NONE;
- }else{
- return it->second;
+ }
+ std::map<Node, BoundVarType>::const_iterator it = itb->second.find(v);
+ if (it == itb->second.end())
+ {
+ return BOUND_NONE;
+ }
+ return it->second;
+}
+
+void BoundedIntegers::getBoundVarIndices(Node q,
+ std::vector<unsigned>& indices) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator it = d_set.find(q);
+ if (it != d_set.end())
+ {
+ for (const Node& v : it->second)
+ {
+ indices.push_back(d_quantEngine->getTermUtil()->getVariableNum(q, v));
+ }
}
}
bool BoundedIntegers::isGroundRange(Node q, Node v)
{
- if (isBoundVar(q, v))
+ if (isBound(q, v))
{
if (d_bound_type[q][v] == BOUND_INT_RANGE)
{
bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
if( initial || !isGroundRange( q, v ) ){
elements.clear();
- unsigned bvt = getBoundVarType( q, v );
+ BoundVarType bvt = getBoundVarType(q, v);
if( bvt==BOUND_INT_RANGE ){
Node l, u;
getBoundValues( q, v, rsi, l, u );
namespace quantifiers {
-
class BoundedIntegers : public QuantifiersModule
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
typedef context::CDHashMap<int, bool> IntBoolMap;
-public:
- enum {
- BOUND_FINITE,
- BOUND_INT_RANGE,
- BOUND_SET_MEMBER,
- BOUND_FIXED_SET,
- BOUND_NONE
- };
private:
//for determining bounds
- bool isBound( Node f, Node v );
bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited );
bool hasNonBoundVar( Node f, Node b );
- //bound type
- std::map< Node, std::map< Node, unsigned > > d_bound_type;
+ /** The bound type for each quantified formula, variable pair */
+ std::map<Node, std::map<Node, BoundVarType>> d_bound_type;
+ /**
+ * The ordered list of variables that are finitely bound, for each quantified
+ * formulas. Variables that occur later in this list may depend on having
+ * finite bounds for variables earlier in this list.
+ */
std::map< Node, std::vector< Node > > d_set;
std::map< Node, std::map< Node, int > > d_set_nums;
std::map< Node, std::map< Node, Node > > d_range;
}
};
std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
-private:
-
- void setBoundedVar( Node f, Node v, unsigned bound_type );
public:
BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
virtual ~BoundedIntegers();
bool needsCheck(Theory::Effort e) override;
void check(Theory::Effort e, QEffort quant_e) override;
void checkOwnership(Node q) override;
- bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
- unsigned getBoundVarType( Node q, Node v );
- unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
- Node getBoundVar( Node q, int i ) { return d_set[q][i]; }
-private:
+ /**
+ * Is v a variable of quantified formula q that this class has inferred to
+ * have a finite bound?
+ */
+ bool isBound(Node q, Node v) const;
+ /**
+ * Get the type of bound that was inferred for variable v of quantified
+ * formula q, or BOUND_NONE if no bound was inferred.
+ */
+ BoundVarType getBoundVarType(Node q, Node v) const;
+ /**
+ * Get the indices of bound variables, in the order they should be processed
+ * in a RepSetIterator. For example, for q:
+ * forall xyz. 0 <= x < 5 ^ 0 <= z <= x+7 => P(x,y,z)
+ * this would add {1,3} to the vector indices, indicating that x has a finite
+ * 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;
+ /**
+ * Get bound elements
+ *
+ * This gets the (finite) enumeration of the range of variable v of quantified
+ * formula q and adds it into the vector elements in the context of the
+ * iteration being performed by rsi. It returns true if it could successfully
+ * determine this range.
+ *
+ * This method determines the range of a variable depending on the current
+ * state of the iterator rsi and flag initial (which is true when rsi is
+ * being initialized). For example, if q is:
+ * forall xy. 0 <= x < 5 ^ 0 <= y <= x+7 => P(x,y)
+ * v is y, and rsi currently maps x to 4, then we add the elements 0...11 to
+ * the vector elements.
+ */
+ bool getBoundElements(RepSetIterator* rsi,
+ bool initial,
+ Node q,
+ Node v,
+ std::vector<Node>& elements);
+ /** Identify this module */
+ std::string identify() const override { return "BoundedIntegers"; }
+
+ private:
+ /**
+ * Set that variable v of quantified formula q has a finite bound, where
+ * bound_type indicates how that bound was inferred.
+ */
+ void setBoundedVar(Node f, Node v, BoundVarType bound_type);
//for integer range
Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; }
Node matchBoundVar( Node v, Node t, Node e );
bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
-public:
- bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements );
-
- /** Identify this module */
- std::string identify() const override { return "BoundedIntegers"; }
};
}
#include "options/uf_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
}
~RepBoundFmcEntry() {}
/** set bound */
- virtual RepSetIterator::RsiEnumType setBound(
- Node owner, unsigned i, std::vector<Node>& elements) override
+ virtual RsiEnumType setBound(Node owner,
+ unsigned i,
+ std::vector<Node>& elements) override
{
if (!d_fm->isStar(d_entry[i]))
{
// only need to consider the single point
elements.push_back(d_entry[i]);
- return RepSetIterator::ENUM_DEFAULT;
+ return ENUM_DEFAULT;
}
return QRepBoundExt::setBound(owner, i, elements);
}
int index = riter.increment();
Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
if( !riter.isFinished() ){
- if (index>=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;
+ if (index >= 0 && riter.d_index[index] > 0 && addedLemmas > 0
+ && riter.d_enum_type[index] == ENUM_CUSTOM)
+ {
+ Trace("fmc-exh-debug")
+ << "Since this is a custom enumeration, skip to the next..."
+ << std::endl;
riter.incrementAtIndex(index - 1);
}
}
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/full_model_check.h"
#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
--- /dev/null
+/********************* */
+/*! \file quant_rep_bound_ext.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Implementation of quantifiers representative bound utility
+ **/
+
+#include "theory/quantifiers/quant_rep_bound_ext.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QRepBoundExt::QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
+
+RsiEnumType QRepBoundExt::setBound(Node owner,
+ unsigned i,
+ std::vector<Node>& elements)
+{
+ // builtin: check if it is bound by bounded integer module
+ if (owner.getKind() == FORALL)
+ {
+ BoundVarType bvt = d_qe->getBoundVarType(owner, owner[0][i]);
+ if (bvt != BOUND_FINITE)
+ {
+ d_bound_int[i] = true;
+ return ENUM_CUSTOM;
+ }
+ // indicates the variable is finitely bound due to
+ // the (small) cardinality of its type,
+ // will treat in default way
+ }
+ return ENUM_INVALID;
+}
+
+bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
+ Node owner,
+ unsigned i,
+ bool initial,
+ std::vector<Node>& elements)
+{
+ if (d_bound_int.find(i) == d_bound_int.end())
+ {
+ // not bound
+ return true;
+ }
+ Assert(owner.getKind() == FORALL);
+ if (!d_qe->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<unsigned>& varOrder)
+{
+ // must set a variable index order based on bounded integers
+ if (owner.getKind() != FORALL)
+ {
+ return false;
+ }
+ Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
+ d_qe->getBoundVarIndices(owner, varOrder);
+ return true;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file quant_rep_bound_ext.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Quantifiers representative bound utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+#define CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/rep_set.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+
+/** 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)
+ * based on modules from the quantifiers engine.
+ */
+class QRepBoundExt : public RepBoundExt
+{
+ public:
+ QRepBoundExt(QuantifiersEngine* qe);
+ virtual ~QRepBoundExt() {}
+ /** set bound */
+ RsiEnumType setBound(Node owner,
+ unsigned i,
+ std::vector<Node>& elements) override;
+ /** reset index */
+ bool resetIndex(RepSetIterator* rsi,
+ Node owner,
+ unsigned 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;
+
+ private:
+ /** Quantifiers engine associated with this bound */
+ QuantifiersEngine* d_qe;
+ /** indices that are bound integer enumeration */
+ std::map<unsigned, bool> d_bound_int;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__FIRST_ORDER_MODEL_H */
virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
};/* class EqualityQuery */
+/** Types of bounds that can be inferred for quantified formulas */
+enum BoundVarType
+{
+ // a variable has a finite bound because it has finite cardinality
+ BOUND_FINITE,
+ // a variable has a finite bound because it is in an integer range, e.g.
+ // forall x. u <= x <= l => P(x)
+ BOUND_INT_RANGE,
+ // a variable has a finite bound because it is a member of a set, e.g.
+ // forall x. x in S => P(x)
+ BOUND_SET_MEMBER,
+ // a variable has a finite bound because only a fixed set of terms are
+ // relevant for it in the domain of the quantified formula, e.g.
+ // forall x. ( x = t1 OR ... OR x = tn ) => P(x)
+ BOUND_FIXED_SET,
+ // a bound has not been inferred for the variable
+ BOUND_NONE
+};
}
}
#include "theory/quantifiers/anti_skolem.h"
#include "theory/quantifiers/conjecture_generator.h"
#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/fmf/full_model_check.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/inst_propagator.h"
return d_tr_trie.get();
}
-quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const
-{
- return d_private->d_bint.get();
-}
quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const
{
return d_private->d_synth_e.get();
return mo==m || mo==NULL;
}
-bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
- if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){
+bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
+{
+ quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ if (bi && bi->isBound(q, v))
+ {
return true;
- }else{
- TypeNode tn = v.getType();
- if( tn.isSort() && options::finiteModelFind() ){
- return true;
- }
- else if (d_term_enum->mayComplete(tn))
+ }
+ TypeNode tn = v.getType();
+ if (tn.isSort() && options::finiteModelFind())
+ {
+ return true;
+ }
+ else if (d_term_enum->mayComplete(tn))
+ {
+ return true;
+ }
+ return false;
+}
+
+BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
+{
+ quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ if (bi)
+ {
+ return bi->getBoundVarType(q, v);
+ }
+ return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
+}
+
+void QuantifiersEngine::getBoundVarIndices(Node q,
+ std::vector<unsigned>& indices) const
+{
+ Assert(indices.empty());
+ // we take the bounded variables first
+ quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ if (bi)
+ {
+ bi->getBoundVarIndices(q, indices);
+ }
+ // then get the remaining ones
+ for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+ {
+ if (std::find(indices.begin(), indices.end(), i) == indices.end())
{
- return true;
+ indices.push_back(i);
}
}
+}
+
+bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
+ bool initial,
+ Node q,
+ Node v,
+ std::vector<Node>& elements) const
+{
+ quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+ if (bi)
+ {
+ return bi->getBoundElements(rsi, initial, q, v, elements);
+ }
return false;
}
#include "theory/quantifiers/equality_infer.h"
#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_epr.h"
quantifiers::RelevantDomain* getRelevantDomain() const;
//---------------------- end utilities
//---------------------- modules (TODO remove these #1163)
- /** get bounded integers utility */
- quantifiers::BoundedIntegers* getBoundedIntegers() const;
/** ceg instantiation */
quantifiers::SynthEngine* getSynthEngine() const;
//---------------------- end modules
void setOwner(Node q, quantifiers::QAttributes& qa);
/** considers */
bool hasOwnership( Node q, QuantifiersModule * m = NULL );
- /** is finite bound */
- bool isFiniteBound( Node q, Node v );
-public:
+ /** does variable v of quantified formula q have a finite bound? */
+ bool isFiniteBound(Node q, Node v) const;
+ /** get bound var type
+ *
+ * This returns the type of bound that was inferred for variable v of
+ * quantified formula q.
+ */
+ BoundVarType getBoundVarType(Node q, Node v) const;
+ /**
+ * Get the indices of bound variables, in the order they should be processed
+ * in a RepSetIterator.
+ *
+ * For details, see BoundedIntegers::getBoundVarIndices.
+ */
+ void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
+ /**
+ * Get bound elements
+ *
+ * This gets the (finite) enumeration of the range of variable v of quantified
+ * formula q and adds it into the vector elements in the context of the
+ * iteration being performed by rsi. It returns true if it could successfully
+ * determine this range.
+ *
+ * For details, see BoundedIntegers::getBoundElements.
+ */
+ bool getBoundElements(RepSetIterator* rsi,
+ bool initial,
+ Node q,
+ Node v,
+ std::vector<Node>& elements) const;
+
+ public:
/** presolve */
void presolve();
/** notify preprocessed assertion */
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
* TODO (#1199): this class needs further documentation.
*/
class RepSetIterator {
-public:
- enum RsiEnumType
- {
- ENUM_INVALID = 0,
- ENUM_DEFAULT,
- ENUM_BOUND_INT,
- };
-
public:
RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
~RepSetIterator() {}
* iterating over domain elements of the type
* of its i^th bound variable.
*/
- virtual RepSetIterator::RsiEnumType setBound(Node owner,
- unsigned i,
- std::vector<Node>& elements) = 0;
+ virtual RsiEnumType setBound(Node owner,
+ unsigned i,
+ std::vector<Node>& elements) = 0;
/** reset index
*
* This method initializes iteration for the i^th
projects / cvc5.git / commitdiff