mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

get-theory-id

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-13 12:22:11 -08:00
parent 1f23ffb23c
commit 0ca94b9c2f
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_egraph.cpp
View file

@ -805,8 +805,8 @@ namespace euf {
} }
else if (j.is_equality()) else if (j.is_equality())
explain_eq(justifications, cc, j.lhs(), j.rhs()); explain_eq(justifications, cc, j.lhs(), j.rhs());
else if (j.is_axiom() && j.theory_id() != null_theory_id) { else if (j.is_axiom() && j.get_theory_id() != null_theory_id) {
IF_VERBOSE(0, verbose_stream() << "TODO add theory axiom to justification"); IF_VERBOSE(20, verbose_stream() << "TODO add theory axiom to justification\n");
} }
if (cc && j.is_congruence()) if (cc && j.is_congruence())
cc->push_back(std::tuple(a->get_app(), b->get_app(), j.timestamp(), j.is_commutative())); cc->push_back(std::tuple(a->get_app(), b->get_app(), j.timestamp(), j.is_commutative()));

2
src/ast/euf/euf_justification.h
View file

@ -112,7 +112,7 @@ namespace euf {
enode* lhs() const { SASSERT(is_equality()); return m_n1; } enode* lhs() const { SASSERT(is_equality()); return m_n1; }
enode* rhs() const { SASSERT(is_equality()); return m_n2; } enode* rhs() const { SASSERT(is_equality()); return m_n2; }
uint64_t timestamp() const { SASSERT(is_congruence()); return m_timestamp; } uint64_t timestamp() const { SASSERT(is_congruence()); return m_timestamp; }
theory_id theory_id() const { SASSERT(is_axiom()); return m_theory_id; } theory_id get_theory_id() const { SASSERT(is_axiom()); return m_theory_id; }
template <typename T> template <typename T>
T* ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); } T* ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); }