From 1a2547995acc5a98c8969e628ac5e1c45b0efe94 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 17 Jun 2016 15:55:56 -0500 Subject: Support for separation logic. Enable cbqi by default for pure BV. --- src/theory/quantifiers/trigger.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/trigger.cpp') diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 802acc089..ee091919d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -375,8 +375,13 @@ bool Trigger::isRelationalTriggerKind( Kind k ) { } bool Trigger::isCbqiKind( Kind k ) { - return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT || - k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER; + if( quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){ + return true; + }else{ + //CBQI typically works for satisfaction-complete theories + TheoryId t = kindToTheoryId( k ); + return t==THEORY_BV || t==THEORY_DATATYPES; + } } bool Trigger::isSimpleTrigger( Node n ){ -- cgit v1.2.3