diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
commit | a7a9ba359a2a8a26f20ac8fdf5292c4e0e27c76a (patch) | |
tree | a62e3c29bb702a2e890b234504bbc121c4da2619 /src/theory/quantifiers/trigger.cpp | |
parent | 7e133dbb7c1adf077102d377d1f7eecae1640ee1 (diff) |
Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 0085177cc..5706c789e 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -312,12 +312,18 @@ bool Trigger::isAtomicTrigger( Node n ){ return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || ( k!=APPLY_UF && isAtomicTriggerKind( k ) ); } + bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON; } +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; +} + bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ |