diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-12 16:46:51 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-12 16:46:51 +0000 |
| commit | 0ba075e240b2083163ab35a3580547cae6927b6c (patch) | |
| tree | 47be765d608aff213ee58749adab458f315fcf89 /src/theory/rep_set.cpp | |
| parent | 341794b1cbd5693010c78b9f5bfe232ee90404b0 (diff) | |
minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver
Diffstat (limited to 'src/theory/rep_set.cpp')
| -rw-r--r-- | src/theory/rep_set.cpp | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 2770a4e77..b50878e70 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -99,25 +99,25 @@ RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){ }
-void RepSetIterator::setQuantifier( Node f ){
+bool RepSetIterator::setQuantifier( Node f ){
Assert( d_types.empty() );
//store indicies
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
d_types.push_back( f[0][i].getType() );
}
- initialize();
+ return initialize();
}
-void RepSetIterator::setFunctionDomain( Node op ){
+bool RepSetIterator::setFunctionDomain( Node op ){
Assert( d_types.empty() );
TypeNode tn = op.getType();
for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
d_types.push_back( tn[i] );
}
- initialize();
+ return initialize();
}
-void RepSetIterator::initialize(){
+bool RepSetIterator::initialize(){
for( size_t i=0; i<d_types.size(); i++ ){
d_index.push_back( 0 );
//store default index order
@@ -146,7 +146,7 @@ void RepSetIterator::initialize(){ d_incomplete = true;
}
}else{
- Trace("fmf-incomplete") << "Incomplete because of type " << tn << std::endl;
+ Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
d_incomplete = true;
}
if( d_rep_set->hasType( tn ) ){
@@ -154,11 +154,10 @@ void RepSetIterator::initialize(){ d_domain[i].push_back( j );
}
}else{
- Trace("fmf-incomplete") << "Incomplete, unknown type " << tn << std::endl;
- d_incomplete = true;
- Unimplemented("Cannot create representative set iterator for unknown type quantifier");
+ return false;
}
}
+ return true;
}
void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
|