diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-21 21:24:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-22 02:24:40 +0000 |
| commit | c7116b06892b5ff21fb04a3996880bfe48e44053 (patch) | |
| tree | 4ad855ab5d4514bb66eb38441ab0f388308cdb48 /src/theory/uf | |
| parent | 4f8927b6e56d55d8b69d525e57f407ff69bc1acd (diff) | |
Set up fine grained equality notifications (#6734)
This adds fields to equality engine setup information which will be used to hook up theories to the central equality engine.
This PR does not impact any behavior.
This is in preparation for the central equality engine.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 36b05b145..f1adde143 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -73,6 +73,14 @@ bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = d_instanceName + "theory::uf::ee"; + if (options::finiteModelFind() + && options::ufssMode() != options::UfssMode::NONE) + { + // need notifications about sorts + esi.d_notifyNewClass = true; + esi.d_notifyMerge = true; + esi.d_notifyDisequal = true; + } return true; } |