Adding an option to the equality engine constructor to treat all constants as

trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.

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;