diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 10:43:57 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 10:44:11 +0100 |
| commit | 0e761324a33a993ae9a268bc2d2ed46f7e86b42d (patch) | |
| tree | d27052ba5aa4520436d8cb6ce059229f2df76ec2 /src/theory/quantifiers/conjecture_generator.cpp | |
| parent | 270a5577f9a34c92ee991bff1d047d78a8f6d5ab (diff) | |
More preparation for filtering relevant terms in TermDb.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 871d4ddc6..06552196d 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -416,8 +416,10 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee );
while( !ieqc_i.isFinished() ){
TNode n = (*ieqc_i);
- if( isHandledTerm( n ) ){
- d_op_arg_index[r].addTerm( this, n );
+ if( getTermDatabase()->hasTermCurrent( n ) ){
+ if( isHandledTerm( n ) ){
+ d_op_arg_index[r].addTerm( this, n );
+ }
}
++ieqc_i;
}
@@ -472,7 +474,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
- if( !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){
+ if( getTermDatabase()->hasTermCurrent( n ) && !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){
if( firstTime ){
Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
firstTime = false;
|