diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
commit | dc3f45d6e41bdd4e52e39b0c6fecae3148a2944c (patch) | |
tree | 7516d3d5d43f0dadb943bb186615e0903cbd9f7f /src/theory/quantifiers/trigger.cpp | |
parent | 74bf9ff63f5566fbe1b5db9124f9dc1fde65cb82 (diff) | |
parent | 6b355496aaf27d46d6a33402814753589b755842 (diff) |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rwxr-xr-x | src/theory/quantifiers/trigger.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index ee091919d..2faed3af0 100755 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -386,9 +386,9 @@ bool Trigger::isCbqiKind( Kind k ) { bool Trigger::isSimpleTrigger( Node n ){ Node t = n.getKind()==NOT ? n[0] : n; - if( n.getKind()==IFF || n.getKind()==EQUAL ){ - if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){ - t = n[0]; + if( t.getKind()==IFF || t.getKind()==EQUAL ){ + if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){ + t = t[0]; } } if( isAtomicTrigger( t ) ){ @@ -742,6 +742,10 @@ InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) { } } +int Trigger::getActiveScore() { + return d_mg->getActiveScore( d_quantEngine ); +} + Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ if( nodes.empty() ){ return d_tr.empty() ? NULL : d_tr[0]; |