diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-14 15:44:21 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-14 15:44:36 -0600 |
| commit | eb5debabce433774a0dbfd46745efb8fcf38b8ab (patch) | |
| tree | 265975eab00a2919d53eb32c6bb993ed7490cbd4 /src/theory/quantifiers/trigger.h | |
| parent | 4c7f8d38445f067bb85f38cf3ea343cc92e41ef2 (diff) | |
Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
| -rw-r--r-- | src/theory/quantifiers/trigger.h | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 23cf5f5d0..74fc16764 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -48,7 +48,6 @@ public: public: std::vector< Node > d_nodes; public: - void debugPrint( const char* c ); IMGenerator* getGenerator() { return d_mg; } public: /** reset instantiation round (call this whenever equivalence classes have changed) */ @@ -123,6 +122,14 @@ public: out << " )"; */ } + void debugPrint( const char * c ) { + Trace(c) << "TRIGGER( "; + for( int i=0; i<(int)d_nodes.size(); i++ ){ + if( i>0 ){ Trace(c) << ", "; } + Trace(c) << d_nodes[i]; + } + Trace(c) << " )"; + } }; inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { |