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/trigger.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/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 4a99852d1..11ec0210d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -210,15 +210,6 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); } -bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ - for( int i=0; i<(int)nodes.size(); i++ ){ - if( !isUsableTrigger( nodes[i], f ) ){ - return false; - } - } - return true; -} - bool Trigger::isUsable( Node n, Node f ){ if( quantifiers::TermDb::getInstConstAttr(n)==f ){ if( isAtomicTrigger( n ) ){ @@ -234,7 +225,7 @@ bool Trigger::isUsable( Node n, Node f ){ std::map< Node, Node > coeffs; if( isBooleanTermTrigger( n ) ){ return true; - } + } } return false; }else{ |