diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2020-12-10 19:53:00 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-10 10:53:00 -0800 |
commit | e4fd524b02054a3ac9724f184e55a983cb6cb6b9 (patch) | |
tree | b67af610d902a293423ef313f5510985372beaf5 /src/theory/uf/equality_engine.h | |
parent | a20e8855be20f2cb4a8f43e03df35ff7caf31f96 (diff) |
Refactor KindMap (#5646)
The KindMap class is only used in the EqualityEngine and implements way more than necessary.
This PR removes all the functionality that is never used.
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 70d5389c1..92665b358 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -683,22 +683,22 @@ private: /** * Returns true if this kind is used for congruence closure. */ - bool isFunctionKind(Kind fun) const { - return d_congruenceKinds.tst(fun); - } + bool isFunctionKind(Kind fun) const { return d_congruenceKinds.test(fun); } /** * Returns true if this kind is used for congruence closure + evaluation of constants. */ - bool isInterpretedFunctionKind(Kind fun) const { - return d_congruenceKindsInterpreted.tst(fun); + bool isInterpretedFunctionKind(Kind fun) const + { + return d_congruenceKindsInterpreted.test(fun); } /** * Returns true if this kind has an operator that is considered external (e.g. not internal). */ - bool isExternalOperatorKind(Kind fun) const { - return d_congruenceKindsExtOperators.tst(fun); + bool isExternalOperatorKind(Kind fun) const + { + return d_congruenceKindsExtOperators.test(fun); } /** |