diff options
Diffstat (limited to 'src/theory/uf/equality_engine.h')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 25092f37f..a26947ed1 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -165,12 +165,12 @@ public: /** * Initialize the equality engine, given the notification class. */ - EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name); + EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool constantsAreTriggers); /** * Initialize the equality engine with no notification class. */ - EqualityEngine(context::Context* context, std::string name); + EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers); /** * Just a destructor. @@ -554,6 +554,9 @@ private: } };/* struct EqualityEngine::TriggerTermSet */ + /** Are the constants triggers */ + bool d_constantsAreTriggers; + /** The information about trigger terms is stored in this easily maintained memory. */ char* d_triggerDatabase; |