diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 13:05:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-18 13:05:04 -0500 |
| commit | 944cb8e5381c47ccc49955a19609921399bb9437 (patch) | |
| tree | 788411c7f26ceedc7f75e2eb9d591ebb6860b5fd /src/theory/theory_engine.h | |
| parent | ab9742939d7706e10ea3d70c73275e97a5235f03 (diff) | |
Quantifiers engine stores a pointer to the master equality engine (#4908)
This is work towards a configurable approach to theory combination.
Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index aa23aa29b..bedd54130 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -738,8 +738,6 @@ public: SharedTermsDatabase* getSharedTermsDatabase(); - theory::eq::EqualityEngine* getMasterEqualityEngine(); - SortInference* getSortInference() { return &d_sortInfer; } /** Prints the assertions to the debug stream */ |