diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-16 12:44:11 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-16 12:44:11 +0200 |
| commit | 7c798a5a2085754b26a0720d162b2ee45a705c4e (patch) | |
| tree | 1d9d8614b69389b11eb0737989f4db2299e59269 /src/theory/quantifiers/trigger.h | |
| parent | a582fa3ea1de3b6419797bbebdcb415ff4d0c0d0 (diff) | |
More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
| -rw-r--r-- | src/theory/quantifiers/trigger.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 60e268a4f..f601a02ab 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -94,7 +94,7 @@ private: static bool isUsable( Node n, Node f ); 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 ); + static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); public: //different strategies for choosing trigger terms enum { @@ -116,6 +116,8 @@ public: static InstMatchGenerator* getInstMatchGenerator( Node q, Node n ); static Node getInversionVariable( Node n ); static Node getInversion( Node n, Node x ); + /** get all variables that E-matching can possibly handle */ + static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ); inline void toStream(std::ostream& out) const { /* |