diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
| commit | 433401b05664d9c8827b19455ef7b93fd27efd9d (patch) | |
| tree | 9be15c6804521434d4116b05eb571ecd78ac2767 /src/theory/quantifiers/conjecture_generator.cpp | |
| parent | fc573f3512b5345763755c9d7a061d430c46ae5f (diff) | |
Accept user-provided triggers with variable terms. Flush lemmas before quantifiers check. Minor fix for conjecture generation.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index c775bb558..0b8e0e462 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -700,7 +700,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { d_tg_alloc[0].reset( this, TypeNode::null() );
while( d_tg_alloc[0].getNextTerm( this, depth ) ){
Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );
- if( d_tg_alloc[0].getDepth( this )==depth ){
+ //if( d_tg_alloc[0].getDepth( this )==depth ){
+ if( (int)d_tg_gdepth==d_tg_gdepth_limit ){
//construct term
Node nn = d_tg_alloc[0].getTerm( this );
if( getUniversalRepresentative( nn )==nn ){
|