* Refactoring rep set iterator, does not modify rep set externally.
* Decouple quantifiers engine and rep set iterator.
* Documentation
* Clang format
* Minor
* Minor
* More
* Format
* Address review.
* Format
* Minor
Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
int v = rsi->getVariableOrder( i );
Assert( q[0][v]==d_set[q][i] );
- Node t = rsi->getCurrentTerm( v );
+ Node t = rsi->getCurrentTerm(v, true);
Trace("bound-int-rsi") << "term : " << t << std::endl;
- Node tt = rsi->d_rep_set->getTermForRepresentative(t);
- if (!tt.isNull())
- {
- t = tt;
- Trace("bound-int-rsi") << "term (post-rep) : " << t << std::endl;
- }
vars.push_back( d_set[q][i] );
subs.push_back( t );
}
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/bounded_integers.h"
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#define USE_INDEX_ORDERING
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
using namespace CVC4::theory::quantifiers::fmcheck;
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
struct sortQuantifierRelevance {
FirstOrderModel * d_fm;
bool operator() (Node i, Node j) {
}
};
+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 ) :
TheoryModel( c, name, true ),
d_qe( qe ), d_forall_asserts( c ){
Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
//check if there is even any domain elements at all
- if (!d_rep_set.hasType(tn)) {
- Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
+ if (!d_rep_set.hasType(tn) || d_rep_set.d_type_reps[tn].size() == 0)
+ {
+ Trace("fm-debug") << "Must create domain element for " << tn << "..."
+ << std::endl;
Node mbt = getModelBasisTerm(tn);
- Trace("fmc-model-debug") << "Add to representative set..." << std::endl;
+ Trace("fm-debug") << "Add to representative set..." << std::endl;
d_rep_set.add(tn, mbt);
- }else if( d_rep_set.d_type_reps[tn].size()==0 ){
- Message() << "empty reps" << std::endl;
- exit(0);
}
return d_rep_set.d_type_reps[tn][0];
}
+bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
+{
+ if (tn.isSort())
+ {
+ // must ensure uninterpreted type is non-empty.
+ if (!d_rep_set.hasType(tn))
+ {
+ // terms in rep_set are now constants which mapped to terms through
+ // TheoryModel. Thus, should introduce a constant and a term.
+ // For now, we just add an arbitrary term.
+ Node var = d_qe->getModel()->getSomeDomainElement(tn);
+ Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
+ << std::endl;
+ d_rep_set.add(tn, var);
+ }
+ return true;
+ }
+ else
+ {
+ // can we complete it?
+ if (d_qe->getTermEnumeration()->mayComplete(tn))
+ {
+ Trace("fm-debug") << " do complete, since cardinality is small ("
+ << tn.getCardinality() << ")..." << std::endl;
+ d_rep_set.complete(tn);
+ // must have succeeded
+ Assert(d_rep_set.hasType(tn));
+ return true;
+ }
+ Trace("fm-debug") << " variable cannot be bounded." << std::endl;
+ return false;
+ }
+}
+
/** needs check */
bool FirstOrderModel::checkNeeded() {
return d_forall_asserts.size()>0;
Node FirstOrderModelAbs::getVariable( Node q, unsigned i ) {
return q[0][d_var_order[q][i]];
}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
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 */
+ virtual RepSetIterator::RsiEnumType setBound(
+ Node owner, unsigned i, std::vector<Node>& elements) override;
+ /** reset index */
+ virtual bool resetIndex(RepSetIterator* rsi,
+ Node owner,
+ unsigned i,
+ bool initial,
+ std::vector<Node>& elements) override;
+ /** initialize representative set for type */
+ virtual bool initializeRepresentativesForType(TypeNode tn) override;
+ /** get variable order */
+ virtual 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
{
unsigned getModelBasisArg(Node n);
/** get some domain element */
Node getSomeDomainElement(TypeNode tn);
+ /** initialize representative set for type
+ *
+ * This ensures that TheoryModel::d_rep_set
+ * is initialized for type tn. In particular:
+ * (1) If tn is an uninitialized (unconstrained)
+ * uninterpreted sort, then we interpret it
+ * as a set of size one,
+ * (2) If tn is a "small" enumerable finite type,
+ * then we ensure that all its values are in
+ * TheoryModel::d_rep_set.
+ *
+ * Returns true if the initialization was complete,
+ * in that the set for tn in TheoryModel::d_rep_set
+ * has all representatives of type tn.
+ */
+ bool initializeRepresentativesForType(TypeNode tn);
protected:
/** quant engine */
}
}
-class RepBoundFmcEntry : public RepBoundExt {
-public:
- Node d_entry;
- FirstOrderModelFmc * d_fm;
- bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) {
- if( d_fm->isInterval(d_entry[i]) ){
- //explicitly add the interval TODO?
- }else if( d_fm->isStar(d_entry[i]) ){
- //add the full range
- return false;
- }else{
- //only need to consider the single point
- elements.push_back( d_entry[i] );
- return true;
+/** Representative bound fmc entry
+ *
+ * This bound information corresponds to one
+ * entry in a term definition (see terminology in
+ * Chapter 5 of Finite Model Finding for
+ * Satisfiability Modulo Theories thesis).
+ * For example, a term definition for the body
+ * of a quantified formula:
+ * forall xyz. P( x, y, z )
+ * may be:
+ * ( 0, 0, 0 ) -> false
+ * ( *, 1, 2 ) -> false
+ * ( *, *, * ) -> true
+ * Indicating that the quantified formula evaluates
+ * to false in the current model for x=0, y=0, z=0,
+ * or y=1, z=2 for any x, and evaluates to true
+ * otherwise.
+ * This class is used if we wish
+ * to iterate over all values corresponding to one
+ * of these entries. For example, for the second entry:
+ * (*, 1, 2 )
+ * we iterate over all values of x, but only {1}
+ * for y and {2} for z.
+ */
+class RepBoundFmcEntry : public QRepBoundExt
+{
+ public:
+ RepBoundFmcEntry(QuantifiersEngine* qe, Node e, FirstOrderModelFmc* f)
+ : QRepBoundExt(qe), d_entry(e), d_fm(f)
+ {
+ }
+ ~RepBoundFmcEntry() {}
+ /** set bound */
+ virtual RepSetIterator::RsiEnumType setBound(
+ Node owner, unsigned i, std::vector<Node>& elements) override
+ {
+ if (d_fm->isInterval(d_entry[i]))
+ {
+ // explicitly add the interval?
}
- return false;
+ else if (d_fm->isStar(d_entry[i]))
+ {
+ // must add the full range
+ }
+ else
+ {
+ // only need to consider the single point
+ elements.push_back(d_entry[i]);
+ return RepSetIterator::ENUM_DEFAULT;
+ }
+ return QRepBoundExt::setBound(owner, i, elements);
}
+
+ private:
+ /** the entry for this bound */
+ Node d_entry;
+ /** the model builder associated with this bound */
+ FirstOrderModelFmc* d_fm;
};
bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
- RepSetIterator riter( d_qe, &(fm->d_rep_set) );
Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " ";
debugPrintCond("fmc-exh", c, true);
Trace("fmc-exh")<< std::endl;
- RepBoundFmcEntry rbfe;
- rbfe.d_entry = c;
- rbfe.d_fm = fm;
+ RepBoundFmcEntry rbfe(d_qe, c, fm);
+ RepSetIterator riter(d_qe->getModel()->getRepSet(), &rbfe);
Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
//initialize
- if( riter.setQuantifier( f, &rbfe ) ){
+ if (riter.setQuantifier(f))
+ {
Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
int addedLemmas = 0;
//now do full iteration
Trace("fmc-exh-debug") << "Inst : ";
std::vector< Node > ev_inst;
std::vector< Node > inst;
- for( int i=0; i<riter.getNumTerms(); i++ ){
+ for (unsigned i = 0; i < riter.getNumTerms(); i++)
+ {
Node rr = riter.getCurrentTerm( i );
Node r = rr;
//if( r.getType().isSort() ){
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;
- riter.increment2( index-1 );
+ riter.incrementAtIndex(index - 1);
}
}
}
for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
vars.push_back( f[0][j] );
}
- RepSetIterator riter(d_qe, fm->getRepSetPtr());
+ QRepBoundExt qrbe(d_qe);
+ RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
if( riter.setQuantifier( f ) ){
while( !riter.isFinished() ){
tests++;
std::vector< Node > terms;
- for( int k=0; k<riter.getNumTerms(); k++ ){
+ for (unsigned k = 0; k < riter.getNumTerms(); k++)
+ {
terms.push_back( riter.getCurrentTerm( k ) );
}
Node n = d_qe->getInstantiation( f, vars, terms );
//do exhaustive instantiation
int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
if( optUseModel() ){
- RepSetIterator riter(d_qe, d_qe->getModel()->getRepSetPtr());
+ QRepBoundExt qrbe(d_qe);
+ RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
if( riter.setQuantifier( f ) ){
FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
}
if( eval==1 ){
//instantiation is already true -> skip
- riter.increment2( depIndex );
+ riter.incrementAtIndex(depIndex);
}else{
//instantiation was not shown to be true, construct the match
InstMatch m( f );
- for( int i=0; i<riter.getNumTerms(); i++ ){
+ for (unsigned i = 0; i < riter.getNumTerms(); i++)
+ {
m.set( d_qe, i, riter.getCurrentTerm( i ) );
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
}
//if the instantiation is show to be false, and we wish to skip multiple instantiations at once
if( eval==-1 ){
- riter.increment2( depIndex );
+ riter.incrementAtIndex(depIndex);
}else{
riter.increment();
}
Trace("fmf-exh-inst-debug") << std::endl;
}
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
- RepSetIterator riter(d_quantEngine,
- d_quantEngine->getModel()->getRepSetPtr());
+ QRepBoundExt qrbe(d_quantEngine);
+ RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe);
if( riter.setQuantifier( f ) ){
Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
if( !riter.isIncomplete() ){
while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
//instantiation was not shown to be true, construct the match
InstMatch m( f );
- for( int i=0; i<riter.getNumTerms(); i++ ){
+ for (unsigned i = 0; i < riter.getNumTerms(); i++)
+ {
m.set( d_quantEngine, i, riter.getCurrentTerm( i ) );
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
#include <unordered_set>
-#include "theory/quantifiers/bounded_integers.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/rep_set.h"
#include "theory/type_enumerator.h"
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace theory {
void RepSet::clear(){
d_type_reps.clear();
return it->second[i];
}
+void RepSet::getRepresentatives(TypeNode tn, std::vector<Node>& reps) const
+{
+ std::map<TypeNode, std::vector<Node> >::const_iterator it =
+ d_type_reps.find(tn);
+ Assert(it != d_type_reps.end());
+ reps.insert(reps.end(), it->second.begin(), it->second.end());
+}
+
bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
{
if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
}
}
-
-RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
- d_incomplete = false;
+RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext)
+ : d_rs(rs), d_rext(rext), d_incomplete(false)
+{
}
-int RepSetIterator::domainSize( int i ) {
- Assert(i>=0);
- int v = d_var_order[i];
+unsigned RepSetIterator::domainSize(unsigned i)
+{
+ unsigned v = d_var_order[i];
return d_domain_elements[v].size();
}
-bool RepSetIterator::setQuantifier( Node f, RepBoundExt* rext ){
- Trace("rsi") << "Make rsi for " << f << std::endl;
+bool RepSetIterator::setQuantifier(Node q)
+{
+ Trace("rsi") << "Make rsi for quantified formula " << q << std::endl;
Assert( d_types.empty() );
//store indicies
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- d_types.push_back( f[0][i].getType() );
+ for (size_t i = 0; i < q[0].getNumChildren(); i++)
+ {
+ d_types.push_back(q[0][i].getType());
}
- d_owner = f;
- return initialize( rext );
+ d_owner = q;
+ return initialize();
}
-bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){
- Trace("rsi") << "Make rsi for " << op << std::endl;
+bool RepSetIterator::setFunctionDomain(Node op)
+{
+ Trace("rsi") << "Make rsi for function " << op << std::endl;
Assert( d_types.empty() );
TypeNode tn = op.getType();
for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
d_types.push_back( tn[i] );
}
d_owner = op;
- return initialize( rext );
+ return initialize();
}
-// TODO : as part of #1199, the portions of this
-// function which modify d_rep_set should be
-// moved to TheoryModel.
-bool RepSetIterator::initialize( RepBoundExt* rext ){
+bool RepSetIterator::initialize()
+{
Trace("rsi") << "Initialize rep set iterator..." << std::endl;
for( unsigned v=0; v<d_types.size(); v++ ){
d_index.push_back( 0 );
d_domain_elements.push_back( std::vector< Node >() );
TypeNode tn = d_types[v];
Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
- if( tn.isSort() ){
- //must ensure uninterpreted type is non-empty.
- if( !d_rep_set->hasType( tn ) ){
- //FIXME:
- // terms in rep_set are now constants which mapped to terms through TheoryModel
- // thus, should introduce a constant and a term. for now, just a term.
-
- //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 );
- Node var = d_qe->getModel()->getSomeDomainElement( tn );
- Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
- d_rep_set->add( tn, var );
- }
- }
bool inc = true;
+ bool setEnum = false;
//check if it is externally bound
- if( rext && rext->setBound( d_owner, v, tn, d_domain_elements[v] ) ){
- d_enum_type.push_back( ENUM_DEFAULT );
- inc = false;
- //builtin: check if it is bound by bounded integer module
- }else if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
- if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
- unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
- if( bvt!=quantifiers::BoundedIntegers::BOUND_FINITE ){
- d_enum_type.push_back( ENUM_BOUND_INT );
- inc = false;
- }else{
- //will treat in default way
- }
+ if (d_rext)
+ {
+ inc = !d_rext->initializeRepresentativesForType(tn);
+ RsiEnumType rsiet = d_rext->setBound(d_owner, v, d_domain_elements[v]);
+ if (rsiet != ENUM_INVALID)
+ {
+ d_enum_type.push_back(rsiet);
+ inc = false;
+ setEnum = true;
}
}
- if( !tn.isSort() ){
- if( inc ){
- if (d_qe->getTermEnumeration()->mayComplete(tn))
- {
- Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
- d_rep_set->complete( tn );
- //must have succeeded
- Assert( d_rep_set->hasType( tn ) );
- }else{
- Trace("rsi") << " variable cannot be bounded." << std::endl;
- Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
- d_incomplete = true;
- }
- }
+ if (inc)
+ {
+ Trace("fmf-incomplete") << "Incomplete because of quantification of type "
+ << tn << std::endl;
+ d_incomplete = true;
}
//if we have yet to determine the type of enumeration
- if( d_enum_type.size()<=v ){
- if( d_rep_set->hasType( tn ) ){
+ if (!setEnum)
+ {
+ if (d_rs->hasType(tn))
+ {
d_enum_type.push_back( ENUM_DEFAULT );
- for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
- //d_domain[v].push_back( j );
- d_domain_elements[v].push_back( d_rep_set->d_type_reps[tn][j] );
- }
+ d_rs->getRepresentatives(tn, d_domain_elements[v]);
}else{
Assert( d_incomplete );
return false;
}
}
}
- //must set a variable index order based on bounded integers
- if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
- Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
- std::vector< int > varOrder;
- for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){
- Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i );
- Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl;
- varOrder.push_back( d_qe->getTermUtil()->getVariableNum( d_owner, v ) );
- }
- for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
- if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
- varOrder.push_back(i);
+
+ if (d_rext)
+ {
+ std::vector<unsigned> varOrder;
+ if (d_rext->getVariableOrder(d_owner, varOrder))
+ {
+ if (Trace.isOn("bound-int-rsi"))
+ {
+ Trace("bound-int-rsi") << "Variable order : ";
+ for (unsigned i = 0; i < varOrder.size(); i++)
+ {
+ Trace("bound-int-rsi") << varOrder[i] << " ";
+ }
+ Trace("bound-int-rsi") << std::endl;
}
+ std::vector<unsigned> indexOrder;
+ indexOrder.resize(varOrder.size());
+ for (unsigned i = 0; i < varOrder.size(); i++)
+ {
+ Assert(varOrder[i] < indexOrder.size());
+ indexOrder[varOrder[i]] = i;
+ }
+ if (Trace.isOn("bound-int-rsi"))
+ {
+ Trace("bound-int-rsi") << "Will use index order : ";
+ for (unsigned i = 0; i < indexOrder.size(); i++)
+ {
+ Trace("bound-int-rsi") << indexOrder[i] << " ";
+ }
+ Trace("bound-int-rsi") << std::endl;
+ }
+ setIndexOrder(indexOrder);
}
- Trace("bound-int-rsi") << "Variable order : ";
- for( unsigned i=0; i<varOrder.size(); i++) {
- Trace("bound-int-rsi") << varOrder[i] << " ";
- }
- Trace("bound-int-rsi") << std::endl;
- std::vector< int > indexOrder;
- indexOrder.resize(varOrder.size());
- for( unsigned i=0; i<varOrder.size(); i++){
- indexOrder[varOrder[i]] = i;
- }
- Trace("bound-int-rsi") << "Will use index order : ";
- for( unsigned i=0; i<indexOrder.size(); i++) {
- Trace("bound-int-rsi") << indexOrder[i] << " ";
- }
- Trace("bound-int-rsi") << std::endl;
- setIndexOrder( indexOrder );
}
//now reset the indices
do_reset_increment( -1, true );
return true;
}
-void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
+void RepSetIterator::setIndexOrder(std::vector<unsigned>& indexOrder)
+{
d_index_order.clear();
d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
//make the d_var_order mapping
}
}
-int RepSetIterator::resetIndex( int i, bool initial ) {
+int RepSetIterator::resetIndex(unsigned i, bool initial)
+{
d_index[i] = 0;
- int v = d_var_order[i];
+ unsigned v = d_var_order[i];
Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
- if( d_enum_type[v]==ENUM_BOUND_INT ){
- Assert( d_owner.getKind()==FORALL );
- if( !d_qe->getBoundedIntegers()->getBoundElements( this, initial, d_owner, d_owner[0][v], d_domain_elements[v] ) ){
+ if (d_rext)
+ {
+ if (!d_rext->resetIndex(this, d_owner, v, initial, d_domain_elements[v]))
+ {
return -1;
}
}
return d_domain_elements[v].empty() ? 0 : 1;
}
-int RepSetIterator::increment2( int i ){
+int RepSetIterator::incrementAtIndex(int i)
+{
Assert( !isFinished() );
#ifdef DISABLE_EVAL_SKIP_MULTIPLE
i = (int)d_index.size()-1;
int RepSetIterator::increment(){
if( !isFinished() ){
- return increment2( (int)d_index.size()-1 );
+ return incrementAtIndex(d_index.size() - 1);
}else{
return -1;
}
}
-bool RepSetIterator::isFinished(){
- return d_index.empty();
-}
+bool RepSetIterator::isFinished() const { return d_index.empty(); }
-Node RepSetIterator::getCurrentTerm( int v ){
- int ii = d_index_order[v];
- int curr = d_index[ii];
+Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm)
+{
+ unsigned ii = d_index_order[v];
+ unsigned curr = d_index[ii];
Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl;
- Assert( 0<=curr && curr<(int)d_domain_elements[v].size() );
- return d_domain_elements[v][curr];
+ Assert(0 <= curr && curr < d_domain_elements[v].size());
+ Node t = d_domain_elements[v][curr];
+ if (valTerm)
+ {
+ Node tt = d_rs->getTermForRepresentative(t);
+ if (!tt.isNull())
+ {
+ return tt;
+ }
+ }
+ return t;
}
void RepSetIterator::debugPrint( const char* c ){
Debug( c ) << std::endl;
}
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
unsigned getNumRepresentatives(TypeNode tn) const;
/** get representative at index */
Node getRepresentative(TypeNode tn, unsigned i) const;
+ /** get representatives of type tn, appends them to reps */
+ void getRepresentatives(TypeNode tn, std::vector<Node>& reps) const;
/** add representative n for type tn, where n has type tn */
void add( TypeNode tn, Node n );
/** returns index in d_type_reps for node n */
//representative domain
typedef std::vector< int > RepDomain;
+class RepBoundExt;
-class RepBoundExt {
- public:
- virtual ~RepBoundExt() {}
- virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0;
-};
-
-/** this class iterates over a RepSet */
+/** Rep set iterator.
+ *
+ * This class is used for iterating over (tuples of) terms
+ * in the domain(s) of a RepSet.
+ *
+ * To use it, first it must
+ * be initialized with a call to:
+ * - setQuantifier or setFunctionDomain
+ * which initializes the d_owner field and sets up
+ * initial information.
+ *
+ * Then, we increment over the tuples of terms in the
+ * domains of the owner of this iterator using:
+ * - increment and incrementAtIndex
+ *
+ * TODO (#1199): this class needs further documentation.
+ */
class RepSetIterator {
public:
- enum {
- ENUM_DEFAULT,
- ENUM_BOUND_INT,
- };
-private:
- QuantifiersEngine * d_qe;
- //initialize function
- bool initialize( RepBoundExt* rext = NULL );
- //for int ranges
- std::map< int, Node > d_lower_bounds;
- //for set ranges
- std::map< int, std::vector< Node > > d_setm_bounds;
- //domain size
- int domainSize( int i );
- //node this is rep set iterator is for
- Node d_owner;
- //reset index, 1:success, 0:empty, -1:fail
- int resetIndex( int i, bool initial = false );
- /** set index order */
- void setIndexOrder( std::vector< int >& indexOrder );
- /** do reset increment the iterator at index=counter */
- int do_reset_increment( int counter, bool initial = false );
- //ordering for variables we are indexing over
- // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
- // then we consider instantiations in this order:
- // a/x a/y a/z
- // a/x b/y a/z
- // b/x a/y a/z
- // b/x b/y a/z
- // ...
- std::vector< int > d_index_order;
- //variables to index they are considered at
- // for example, if d_index_order = { 2, 0, 1 }
- // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
- std::map< int, int > d_var_order;
- //are we only considering a strict subset of the domain of the quantifier?
- bool d_incomplete;
-public:
- RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
- ~RepSetIterator(){}
- //set that this iterator will be iterating over instantiations for a quantifier
- bool setQuantifier( Node f, RepBoundExt* rext = NULL );
- //set that this iterator will be iterating over the domain of a function
- bool setFunctionDomain( Node op, RepBoundExt* rext = NULL );
-public:
- //pointer to model
- RepSet* d_rep_set;
- //enumeration type?
- std::vector< int > d_enum_type;
- //current tuple we are considering
- std::vector< int > d_index;
- //types we are considering
- std::vector< TypeNode > d_types;
- //domain we are considering
- std::vector< std::vector< Node > > d_domain_elements;
+ enum RsiEnumType
+ {
+ ENUM_INVALID = 0,
+ ENUM_DEFAULT,
+ ENUM_BOUND_INT,
+ };
+
public:
- /** increment the iterator at index=counter */
- int increment2( int i );
- /** increment the iterator */
- int increment();
- /** is the iterator finished? */
- bool isFinished();
- /** get the i_th term we are considering */
- Node getCurrentTerm( int v );
- /** get the number of terms we are considering */
- int getNumTerms() { return (int)d_index_order.size(); }
- /** debug print */
- void debugPrint( const char* c );
- void debugPrintSmall( const char* c );
- //get index order, returns var #
- int getIndexOrder( int v ) { return d_index_order[v]; }
- //get variable order, returns index #
- int getVariableOrder( int i ) { return d_var_order[i]; }
- //is incomplete
- bool isIncomplete() { return d_incomplete; }
+ RepSetIterator(const RepSet* rs, RepBoundExt* rext);
+ ~RepSetIterator() {}
+ /** set that this iterator will be iterating over instantiations for a
+ * quantifier */
+ bool setQuantifier(Node q);
+ /** set that this iterator will be iterating over the domain of a function */
+ bool setFunctionDomain(Node op);
+ /** increment the iterator */
+ int increment();
+ /** increment the iterator at index
+ * This increments the i^th field of the
+ * iterator, for examples, see operator next_i
+ * in Figure 2 of Reynolds et al. CADE 2013.
+ */
+ int incrementAtIndex(int i);
+ /** is the iterator finished? */
+ bool isFinished() const;
+ /** get domain size of the i^th field of this iterator */
+ unsigned domainSize(unsigned i);
+ /** get the i^th term in the tuple we are considering */
+ Node getCurrentTerm(unsigned v, bool valTerm = false);
+ /** get the number of terms in the tuple we are considering */
+ unsigned getNumTerms() { return d_index_order.size(); }
+ /** get index order, returns var # */
+ unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
+ /** get variable order, returns index # */
+ unsigned getVariableOrder(unsigned i) { return d_var_order[i]; }
+ /** is incomplete
+ * Returns true if we are iterating over a strict subset of
+ * the domain of the quantified formula or function.
+ */
+ bool isIncomplete() { return d_incomplete; }
+ /** debug print methods */
+ void debugPrint(const char* c);
+ void debugPrintSmall(const char* c);
+ // TODO (#1199): these should be private
+ /** enumeration type for each field */
+ std::vector<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 RepSetIterator::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;
+ }
+};
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff