diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-22 23:41:42 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-22 21:41:42 -0800 |
| commit | 6f379f2b83a28995aa77504da1931a598b54bcc0 (patch) | |
| tree | 4133e6a9100d2cf68f0b00e10c6492059207d8f0 /src/theory/strings/solver_state.h | |
| parent | b70c2eb3fe78f6985fda3086a52d0d74aecb78c2 (diff) | |
Minor refactoring of equality notifications (#3798)
Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.
Diffstat (limited to 'src/theory/strings/solver_state.h')
| -rw-r--r-- | src/theory/strings/solver_state.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 28dfbfd09..b295ba12d 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -121,6 +121,8 @@ class SolverState const context::CDList<Node>& getDisequalityList() const; //-------------------------------------- end equality information //-------------------------------------- notifications for equalities + /** called when a new equivalence class is created */ + void eqNotifyNewClass(TNode t); /** called when two equivalence classes will merge */ void eqNotifyPreMerge(TNode t1, TNode t2); /** called when two equivalence classes are made disequal */ |