diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:07:46 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:07:46 +0000 |
| commit | 2a731b9164bb178f1232a9af0babc7dd84450cea (patch) | |
| tree | 57d14d55f1bae93737dbee34c737771858572fad /src/theory/arith/congruence_manager.h | |
| parent | 164163c9c8fd255947cf3e8d236a5b9da1a1fdab (diff) | |
Adding support for a master equality engine. Each theory gets the master equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().
Diffstat (limited to 'src/theory/arith/congruence_manager.h')
| -rw-r--r-- | src/theory/arith/congruence_manager.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 502ea5cf0..5e2c80a63 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -144,6 +144,8 @@ public: return d_explanationMap.find(n) != d_explanationMap.end(); } + void setMasterEqualityEngine(eq::EqualityEngine* eq); + private: Node externalToInternal(TNode n) const{ Assert(canExplain(n)); |