diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2014-11-19 22:42:31 -0500 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2014-11-19 22:42:31 -0500 |
commit | 2984c25a1b2ab36f5e3c6298c6ba99c0701c7141 (patch) | |
tree | 153bf42ab5da4c709fbf1ece708eaa82f75d36da /src/theory/uf/equality_engine.h | |
parent | 363dc9881a3b249978eec76c7c2b77eb2ef459ea (diff) |
Making construction of trigger sets not use the global engine state.
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index bf7c765b8..25092f37f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -554,15 +554,6 @@ private: } };/* struct EqualityEngine::TriggerTermSet */ - /** Internal tags for creating a new set */ - Theory::Set d_newSetTags; - - /** Internal triggers for creating a new set */ - EqualityNodeId d_newSetTriggers[THEORY_LAST]; - - /** Size of the internal triggers array */ - unsigned d_newSetTriggersSize; - /** The information about trigger terms is stored in this easily maintained memory. */ char* d_triggerDatabase; @@ -576,7 +567,7 @@ private: static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1); /** Create new trigger term set based on the internally set information */ - TriggerTermSetRef newTriggerTermSet(); + TriggerTermSetRef newTriggerTermSet(Theory::Set newSetTags, EqualityNodeId* newSetTriggers, unsigned newSetTriggersSize); /** Get the trigger set give a reference */ TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) { |