From 6480823e5620b316b4c319453f45f6d7d452e2b1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 3 Jun 2014 14:01:01 +0200 Subject: Support E-matching/QCF for Set operators. --- src/theory/quantifiers/trigger.cpp | 11 +++++++++-- 1 file changed, 9 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 3de12b9c9..77a4efff5 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -323,9 +323,16 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ } bool Trigger::isAtomicTrigger( Node n ){ - return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; + Kind k = n.getKind(); + 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==SET_SINGLETON; +} + bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ -- cgit v1.2.3