diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-05 15:32:48 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-05 15:32:48 +0100 |
| commit | 36a5437abbddd484b8bdb18c024cc7573240054f (patch) | |
| tree | 587994c441c49995624029c9094c5caeed9cf7d1 /src/theory/quantifiers/trigger.h | |
| parent | a84864da338f74958c6754696d98cd6355e798a8 (diff) | |
More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
| -rw-r--r-- | src/theory/quantifiers/trigger.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 75ada4f83..482701a82 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -95,6 +95,8 @@ private: static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); + /** is local theory extensions term */ + static bool isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ); public: //different strategies for choosing trigger terms enum { @@ -111,6 +113,7 @@ public: static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); + static bool isLocalTheoryExt( Node n, std::vector< Node >& patTerms ); /** return data structure for producing matches for this trigger. */ static InstMatchGenerator* getInstMatchGenerator( Node n ); static Node getInversionVariable( Node n ); |