diff options
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index a86984cca..8ddf809b6 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -27,6 +27,8 @@ namespace CVC4 { namespace theory { +class Theory; + /** * A LemmaStatus, returned from OutputChannel::lemma(), provides information * about the lemma added. In particular, it contains the T-rewritten lemma @@ -206,8 +208,14 @@ public: * long-running operations, they cannot rely on resource() to break * out of infinite or intractable computations. */ - virtual void spendResource() throw() { - } + virtual void spendResource() throw() {} + + /** Handle user attribute + * Associates theory t with the attribute attr. Theory t will be + * notifed whenever an attribute of name attr is set on a node. + * This can happen through, for example, the SMT LIB v2 language. + */ + virtual void handleUserAttribute( const char* attr, Theory* t ){} };/* class OutputChannel */ |