Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/rep_set.cpp	Lines:	189	254	74.4 %
Date:	2021-09-18	Branches:	290	818	35.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 */

#include <unordered_set>

#include "theory/rep_set.h"
#include "theory/type_enumerator.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {

void RepSet::clear(){
  d_type_reps.clear();
  d_type_complete.clear();
  d_tmap.clear();
  d_values_to_terms.clear();
}

bool RepSet::hasRep(TypeNode tn, Node n) const
{
  std::map<TypeNode, std::vector<Node> >::const_iterator it =
      d_type_reps.find(tn);
  if( it==d_type_reps.end() ){
    return false;
  }else{
    return std::find( it->second.begin(), it->second.end(), n )!=it->second.end();
  }
}

size_t RepSet::getNumRepresentatives(TypeNode tn) const
{
  const std::vector<Node>* reps = getTypeRepsOrNull(tn);
  return (reps != nullptr) ? reps->size() : 0;
}

Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
{
  std::map<TypeNode, std::vector<Node> >::const_iterator it =
      d_type_reps.find(tn);
  Assert(it != d_type_reps.end());
  Assert(i < it->second.size());
  return it->second[i];
}

const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const
{
  auto it = d_type_reps.find(tn);
  if (it == d_type_reps.end())
  {
    return nullptr;
  }
  return &(it->second);
}

namespace {

bool containsStoreAll(Node n, std::unordered_set<Node>& cache)
{
  if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
    cache.insert(n);
    if( n.getKind()==STORE_ALL ){
      return true;
    }else{
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
        if( containsStoreAll( n[i], cache ) ){
          return true;
        }
      }
    }
  }
  return false;
}

}  // namespace

void RepSet::add( TypeNode tn, Node n ){
  //for now, do not add array constants FIXME
  if( tn.isArray() ){
    std::unordered_set<Node> cache;
    if( containsStoreAll( n, cache ) ){
      return;
    }
  }
  Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
  Assert(n.getType().isSubtypeOf(tn));
  d_tmap[ n ] = (int)d_type_reps[tn].size();
  d_type_reps[tn].push_back( n );
}

int RepSet::getIndexFor( Node n ) const {
  std::map< Node, int >::const_iterator it = d_tmap.find( n );
  if( it!=d_tmap.end() ){
    return it->second;
  }else{
    return -1;
  }
}

bool RepSet::complete( TypeNode t ){
  std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
  if( it==d_type_complete.end() ){
    //remove all previous
    for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
      d_tmap.erase( d_type_reps[t][i] );
    }
    d_type_reps[t].clear();
    //now complete the type
    d_type_complete[t] = true;
    TypeEnumerator te(t);
    while( !te.isFinished() ){
      Node n = *te;
      if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
        add( t, n );
      }
      ++te;
    }
    for( size_t i=0; i<d_type_reps[t].size(); i++ ){
      Trace("reps-complete") << d_type_reps[t][i] << " ";
    }
    Trace("reps-complete") << std::endl;
    return true;
  }else{
    return it->second;
  }
}

Node RepSet::getTermForRepresentative(Node n) const
{
  std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n);
  if (it != d_values_to_terms.end())
  {
    return it->second;
  }
  else
  {
    return Node::null();
  }
}

void RepSet::setTermForRepresentative(Node n, Node t)
{
  d_values_to_terms[n] = t;
}

Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const
{
  std::map<TypeNode, std::vector<Node> >::const_iterator it =
      d_type_reps.find(tn);
  if (it != d_type_reps.end())
  {
    // try to find a pre-existing arbitrary element
    for (size_t i = 0; i < it->second.size(); i++)
    {
      if (std::find(exclude.begin(), exclude.end(), it->second[i])
          == exclude.end())
      {
        return it->second[i];
      }
    }
  }
  return Node::null();
}

void RepSet::toStream(std::ostream& out){
  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
    if( !it->first.isFunction() && !it->first.isPredicate() ){
      out << "(" << it->first << " " << it->second.size();
      out << " (";
      for( unsigned i=0; i<it->second.size(); i++ ){
        if( i>0 ){ out << " "; }
        out << it->second[i];
      }
      out << ")";
      out << ")" << std::endl;
    }
  }
}

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 (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);
    }
  }
  //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++ ){
    Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
  }
}

void RepSetIterator::debugPrintSmall( const char* c ){
  Debug( c ) << "RI: ";
  for( unsigned v=0; v<d_index.size(); v++ ){
    Debug( c ) << v << ": " << getCurrentTerm( v ) << " ";
  }
  Debug( c ) << std::endl;
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King, Morgan Deters
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of representative set.
14		*/
15
16		#include <unordered_set>
17
18		#include "theory/rep_set.h"
19		#include "theory/type_enumerator.h"
20
21		using namespace std;
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26
27	20988	void RepSet::clear(){
28	20988	d_type_reps.clear();
29	20988	d_type_complete.clear();
30	20988	d_tmap.clear();
31	20988	d_values_to_terms.clear();
32	20988	}
33
34		bool RepSet::hasRep(TypeNode tn, Node n) const
35		{
36		std::map<TypeNode, std::vector<Node> >::const_iterator it =
37		d_type_reps.find(tn);
38		if( it==d_type_reps.end() ){
39		return false;
40		}else{
41		return std::find( it->second.begin(), it->second.end(), n )!=it->second.end();
42		}
43		}
44
45	162336	size_t RepSet::getNumRepresentatives(TypeNode tn) const
46		{
47	162336	const std::vector<Node>* reps = getTypeRepsOrNull(tn);
48	162336	return (reps != nullptr) ? reps->size() : 0;
49		}
50
51	4140	Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
52		{
53		std::map<TypeNode, std::vector<Node> >::const_iterator it =
54	4140	d_type_reps.find(tn);
55	4140	Assert(it != d_type_reps.end());
56	4140	Assert(i < it->second.size());
57	4140	return it->second[i];
58		}
59
60	165940	const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const
61		{
62	165940	auto it = d_type_reps.find(tn);
63	165940	if (it == d_type_reps.end())
64		{
65	4	return nullptr;
66		}
67	165936	return &(it->second);
68		}
69
70		namespace {
71
72	2289	bool containsStoreAll(Node n, std::unordered_set<Node>& cache)
73		{
74	2289	if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
75	2289	cache.insert(n);
76	2289	if( n.getKind()==STORE_ALL ){
77	1003	return true;
78		}else{
79	1286	for( unsigned i=0; i<n.getNumChildren(); i++ ){
80	1282	if( containsStoreAll( n[i], cache ) ){
81	1282	return true;
82		}
83		}
84		}
85		}
86	4	return false;
87		}
88
89		} // namespace
90
91	587965	void RepSet::add( TypeNode tn, Node n ){
92		//for now, do not add array constants FIXME
93	587965	if( tn.isArray() ){
94	1011	std::unordered_set<Node> cache;
95	1007	if( containsStoreAll( n, cache ) ){
96	1003	return;
97		}
98		}
99	586962	Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
100	586962	Assert(n.getType().isSubtypeOf(tn));
101	586962	d_tmap[ n ] = (int)d_type_reps[tn].size();
102	586962	d_type_reps[tn].push_back( n );
103		}
104
105		int RepSet::getIndexFor( Node n ) const {
106		std::map< Node, int >::const_iterator it = d_tmap.find( n );
107		if( it!=d_tmap.end() ){
108		return it->second;
109		}else{
110		return -1;
111		}
112		}
113
114	2132	bool RepSet::complete( TypeNode t ){
115	2132	std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
116	2132	if( it==d_type_complete.end() ){
117		//remove all previous
118	774	for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
119	579	d_tmap.erase( d_type_reps[t][i] );
120		}
121	195	d_type_reps[t].clear();
122		//now complete the type
123	195	d_type_complete[t] = true;
124	390	TypeEnumerator te(t);
125	1431	while( !te.isFinished() ){
126	1236	Node n = *te;
127	618	if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
128	618	add( t, n );
129		}
130	618	++te;
131		}
132	813	for( size_t i=0; i<d_type_reps[t].size(); i++ ){
133	618	Trace("reps-complete") << d_type_reps[t][i] << " ";
134		}
135	195	Trace("reps-complete") << std::endl;
136	195	return true;
137		}else{
138	1937	return it->second;
139		}
140		}
141
142	41631	Node RepSet::getTermForRepresentative(Node n) const
143		{
144	41631	std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n);
145	41631	if (it != d_values_to_terms.end())
146		{
147	41256	return it->second;
148		}
149		else
150		{
151	375	return Node::null();
152		}
153		}
154
155	586074	void RepSet::setTermForRepresentative(Node n, Node t)
156		{
157	586074	d_values_to_terms[n] = t;
158	586074	}
159
160		Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const
161		{
162		std::map<TypeNode, std::vector<Node> >::const_iterator it =
163		d_type_reps.find(tn);
164		if (it != d_type_reps.end())
165		{
166		// try to find a pre-existing arbitrary element
167		for (size_t i = 0; i < it->second.size(); i++)
168		{
169		if (std::find(exclude.begin(), exclude.end(), it->second[i])
170		== exclude.end())
171		{
172		return it->second[i];
173		}
174		}
175		}
176		return Node::null();
177		}
178
179		void RepSet::toStream(std::ostream& out){
180		for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
181		if( !it->first.isFunction() && !it->first.isPredicate() ){
182		out << "(" << it->first << " " << it->second.size();
183		out << " (";
184		for( unsigned i=0; i<it->second.size(); i++ ){
185		if( i>0 ){ out << " "; }
186		out << it->second[i];
187		}
188		out << ")";
189		out << ")" << std::endl;
190		}
191		}
192		}
193
194	5439	RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext)
195	5439	: d_rs(rs), d_rext(rext), d_incomplete(false)
196		{
197	5439	}
198
199	80386	unsigned RepSetIterator::domainSize(unsigned i)
200		{
201	80386	unsigned v = d_var_order[i];
202	80386	return d_domain_elements[v].size();
203		}
204
205	75773	TypeNode RepSetIterator::getTypeOf(unsigned i) const { return d_types[i]; }
206
207	5439	bool RepSetIterator::setQuantifier(Node q)
208		{
209	5439	Trace("rsi") << "Make rsi for quantified formula " << q << std::endl;
210	5439	Assert(d_types.empty());
211		//store indicies
212	12929	for (size_t i = 0; i < q[0].getNumChildren(); i++)
213		{
214	7490	d_types.push_back(q[0][i].getType());
215		}
216	5439	d_owner = q;
217	5439	return initialize();
218		}
219
220		bool RepSetIterator::setFunctionDomain(Node op)
221		{
222		Trace("rsi") << "Make rsi for function " << op << std::endl;
223		Assert(d_types.empty());
224		TypeNode tn = op.getType();
225		for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
226		d_types.push_back( tn[i] );
227		}
228		d_owner = op;
229		return initialize();
230		}
231
232	5439	bool RepSetIterator::initialize()
233		{
234	5439	Trace("rsi") << "Initialize rep set iterator..." << std::endl;
235	12929	for( unsigned v=0; v<d_types.size(); v++ ){
236	7490	d_index.push_back( 0 );
237		//store default index order
238	7490	d_index_order.push_back( v );
239	7490	d_var_order[v] = v;
240		//store default domain
241		//d_domain.push_back( RepDomain() );
242	7490	d_domain_elements.push_back( std::vector< Node >() );
243	14980	TypeNode tn = d_types[v];
244	7490	Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
245	7490	bool inc = true;
246	7490	bool setEnum = false;
247		//check if it is externally bound
248	7490	if (d_rext)
249		{
250	7490	inc = !d_rext->initializeRepresentativesForType(tn);
251	7490	RsiEnumType rsiet = d_rext->setBound(d_owner, v, d_domain_elements[v]);
252	7490	if (rsiet != ENUM_INVALID)
253		{
254	3900	d_enum_type.push_back(rsiet);
255	3900	inc = false;
256	3900	setEnum = true;
257		}
258		}
259	7490	if (inc)
260		{
261		Trace("fmf-incomplete") << "Incomplete because of quantification of type "
262		<< tn << std::endl;
263		d_incomplete = true;
264		}
265
266		//if we have yet to determine the type of enumeration
267	7490	if (!setEnum)
268		{
269	3590	if (d_rs->hasType(tn))
270		{
271	3590	d_enum_type.push_back( ENUM_DEFAULT );
272	3590	if (const auto* type_reps = d_rs->getTypeRepsOrNull(tn))
273		{
274	3590	std::vector<Node>& v_domain_elements = d_domain_elements[v];
275	10770	v_domain_elements.insert(v_domain_elements.end(),
276	10770	type_reps->begin(), type_reps->end());
277		}
278		}else{
279		Assert(d_incomplete);
280		return false;
281		}
282		}
283		}
284
285	5439	if (d_rext)
286		{
287	10878	std::vector<unsigned> varOrder;
288	5439	if (d_rext->getVariableOrder(d_owner, varOrder))
289		{
290	5439	if (Trace.isOn("bound-int-rsi"))
291		{
292		Trace("bound-int-rsi") << "Variable order : ";
293		for (unsigned i = 0; i < varOrder.size(); i++)
294		{
295		Trace("bound-int-rsi") << varOrder[i] << " ";
296		}
297		Trace("bound-int-rsi") << std::endl;
298		}
299	10878	std::vector<unsigned> indexOrder;
300	5439	indexOrder.resize(varOrder.size());
301	12929	for (unsigned i = 0; i < varOrder.size(); i++)
302		{
303	7490	Assert(varOrder[i] < indexOrder.size());
304	7490	indexOrder[varOrder[i]] = i;
305		}
306	5439	if (Trace.isOn("bound-int-rsi"))
307		{
308		Trace("bound-int-rsi") << "Will use index order : ";
309		for (unsigned i = 0; i < indexOrder.size(); i++)
310		{
311		Trace("bound-int-rsi") << indexOrder[i] << " ";
312		}
313		Trace("bound-int-rsi") << std::endl;
314		}
315	5439	setIndexOrder(indexOrder);
316		}
317		}
318		//now reset the indices
319	5439	do_reset_increment( -1, true );
320	5439	return true;
321		}
322
323	5439	void RepSetIterator::setIndexOrder(std::vector<unsigned>& indexOrder)
324		{
325	5439	d_index_order.clear();
326	5439	d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
327		//make the d_var_order mapping
328	12929	for( unsigned i=0; i<d_index_order.size(); i++ ){
329	7490	d_var_order[d_index_order[i]] = i;
330		}
331	5439	}
332
333	14585	int RepSetIterator::resetIndex(unsigned i, bool initial)
334		{
335	14585	d_index[i] = 0;
336	14585	unsigned v = d_var_order[i];
337	14585	Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
338	14585	if (d_rext)
339		{
340	14585	if (!d_rext->resetIndex(this, d_owner, v, initial, d_domain_elements[v]))
341		{
342	103	return -1;
343		}
344		}
345	14482	return d_domain_elements[v].empty() ? 0 : 1;
346		}
347
348	32609	int RepSetIterator::incrementAtIndex(int i)
349		{
350	32609	Assert(!isFinished());
351		#ifdef DISABLE_EVAL_SKIP_MULTIPLE
352		i = (int)d_index.size()-1;
353		#endif
354	32609	Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i << std::endl;
355		//increment d_index
356	32609	if( i>=0){
357	32186	Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
358		}
359	58063	while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){
360	12727	i--;
361	12727	if( i>=0){
362	8007	Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
363		}
364		}
365	32609	if( i==-1 ){
366	5143	Trace("rsi-debug") << "increment failed" << std::endl;
367	5143	d_index.clear();
368	5143	return -1;
369		}else{
370	27466	Trace("rsi-debug") << "increment " << i << std::endl;
371	27466	d_index[i]++;
372	27466	return do_reset_increment( i );
373		}
374		}
375
376	32905	int RepSetIterator::do_reset_increment( int i, bool initial ) {
377	65810	Trace("rsi-debug") << "RepSetIterator::do_reset_increment: " << i
378	32905	<< ", initial=" << initial << std::endl;
379	47152	for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){
380	14585	bool emptyDomain = false;
381	14585	int ri_res = resetIndex( ii, initial );
382	14585	if( ri_res==-1 ){
383		//failed
384	103	d_index.clear();
385	103	d_incomplete = true;
386	103	break;
387	14482	}else if( ri_res==0 ){
388	235	emptyDomain = true;
389		}
390		//force next iteration if currently an empty domain
391	14482	if (emptyDomain)
392		{
393	470	Trace("rsi-debug") << "This is an empty domain (index " << ii << ")."
394	235	<< std::endl;
395	235	if (ii > 0)
396		{
397		// increment at the previous index
398	277	return incrementAtIndex(ii - 1);
399		}
400		else
401		{
402		// this is the first index, we are done
403	193	d_index.clear();
404	193	return -1;
405		}
406		}
407		}
408	65340	Trace("rsi-debug") << "Finished, return " << i << std::endl;
409	32670	return i;
410		}
411
412	31182	int RepSetIterator::increment(){
413	31182	if( !isFinished() ){
414	31182	return incrementAtIndex(d_index.size() - 1);
415		}else{
416		return -1;
417		}
418		}
419
420	130917	bool RepSetIterator::isFinished() const { return d_index.empty(); }
421
422	78828	Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const
423		{
424	78828	unsigned ii = d_index_order[i];
425	78828	unsigned curr = d_index[ii];
426	157656	Trace("rsi-debug") << "rsi : get term " << i
427	78828	<< ", index order = " << d_index_order[i] << std::endl;
428	157656	Trace("rsi-debug") << "rsi : curr = " << curr << " / "
429	78828	<< d_domain_elements[i].size() << std::endl;
430	78828	Assert(0 <= curr && curr < d_domain_elements[i].size());
431	157656	Node t = d_domain_elements[i][curr];
432	78828	Trace("rsi-debug") << "rsi : term = " << t << std::endl;
433	78828	if (valTerm)
434		{
435	36644	Node tt = d_rs->getTermForRepresentative(t);
436	36269	if (!tt.isNull())
437		{
438	35894	Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl;
439	35894	return tt;
440		}
441		}
442	42934	Trace("rsi-debug") << "rsi : return" << std::endl;
443	42934	return t;
444		}
445
446		void RepSetIterator::getCurrentTerms(std::vector<Node>& terms) const
447		{
448		for (unsigned i = 0, size = d_index_order.size(); i < size; i++)
449		{
450		terms.push_back(getCurrentTerm(i));
451		}
452		}
453
454		void RepSetIterator::debugPrint( const char* c ){
455		for( unsigned v=0; v<d_index.size(); v++ ){
456		Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
457		}
458		}
459
460		void RepSetIterator::debugPrintSmall( const char* c ){
461		Debug( c ) << "RI: ";
462		for( unsigned v=0; v<d_index.size(); v++ ){
463		Debug( c ) << v << ": " << getCurrentTerm( v ) << " ";
464		}
465		Debug( c ) << std::endl;
466		}
467
468		} // namespace theory
469	29574	} // namespace cvc5