mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dc1783aafa
commit
6beec7b642
2 changed files with 3 additions and 2 deletions
|
@ -53,6 +53,7 @@ namespace euf {
|
|||
|
||||
bool is_external() const { return m_kind == external_t; }
|
||||
bool is_congruence() const { return m_kind == congruence_t; }
|
||||
bool is_commutative() const { return m_comm; }
|
||||
template <typename T>
|
||||
T* ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); }
|
||||
};
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue