mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

add placeholder for tracking theory justifications in EUF

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-13 11:59:01 -08:00
parent 73b032ae4e
commit 1f23ffb23c
6 changed files with 29 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/euf_ac_plugin.cpp
View file

@ -109,7 +109,7 @@ namespace euf {
m_shared_nodes.setx(n->get_id(), true, false);
sort(monomial(m));
m_shared_todo.insert(m_shared.size());
m_shared.push_back({ n, m, justification::axiom() });
m_shared.push_back({ n, m, justification::axiom(get_id()) });
push_undo(is_register_shared);
}

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

@ -673,7 +673,7 @@ namespace euf {
SASSERT(n1->get_root()->reaches(n1));
SASSERT(n1->m_target);
n1->m_target = nullptr;
n1->m_justification = justification::axiom();
n1->m_justification = justification::axiom(null_theory_id);
n1->get_root()->reverse_justification();
// ---------------
// n1 -> ... -> r1
@ -804,7 +804,10 @@ namespace euf {
explain_eq(justifications, cc, a, b, j2);
}
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) {
IF_VERBOSE(0, verbose_stream() << "TODO add theory axiom to justification");
}
if (cc && j.is_congruence())
cc->push_back(std::tuple(a->get_app(), b->get_app(), j.timestamp(), j.is_commutative()));
}

2
src/ast/euf/euf_enode.cpp
View file

@ -135,7 +135,7 @@ namespace euf {
enode* prev = this;
justification js = m_justification;
prev->m_target = nullptr;
prev->m_justification = justification::axiom();
prev->m_justification = justification::axiom(null_theory_id);
while (curr != nullptr) {
enode* new_curr = curr->m_target;
justification new_js = curr->m_justification;

4
src/ast/euf/euf_enode.h
View file

@ -36,10 +36,6 @@ namespace euf {
typedef std::pair<enode*,bool> enode_bool_pair;
typedef svector<enode_bool_pair> enode_bool_pair_vector;
typedef id_var_list<> th_var_list;
typedef int theory_var;
typedef int theory_id;
const theory_var null_theory_var = -1;
const theory_id null_theory_id = -1;
class enode {
expr* m_expr = nullptr;

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

@ -28,6 +28,11 @@ namespace euf {
class enode;
typedef int theory_var;
typedef int theory_id;
const theory_var null_theory_var = -1;
const theory_id null_theory_id = -1;
class justification {
public:
typedef stacked_dependency_manager<justification> dependency_manager;
@ -42,6 +47,7 @@ namespace euf {
};
kind_t m_kind;
union {
int m_theory_id;
bool m_comm;
enode* m_n1;
};
@ -76,19 +82,27 @@ namespace euf {
m_n2(n2)
{}
public:
justification():
justification(int theory_id):
m_kind(kind_t::axiom_t),
m_comm(false),
m_theory_id(theory_id),
m_external(nullptr)
{}
static justification axiom() { return justification(); }
public:
justification():
m_kind(kind_t::axiom_t),
m_theory_id(null_theory_id),
m_external(nullptr)
{}
static justification axiom(int theory_id) { return justification(theory_id); }
static justification congruence(bool c, uint64_t ts) { return justification(c, ts); }
static justification external(void* ext) { return justification(ext); }
static justification dependent(dependency* d) { return justification(d, 1); }
static justification equality(enode* a, enode* b) { return justification(a, b); }
bool is_axiom() const { return m_kind == kind_t::axiom_t; }
bool is_external() const { return m_kind == kind_t::external_t; }
bool is_congruence() const { return m_kind == kind_t::congruence_t; }
bool is_commutative() const { return m_comm; }
@ -98,6 +112,7 @@ namespace euf {
enode* lhs() const { SASSERT(is_equality()); return m_n1; }
enode* rhs() const { SASSERT(is_equality()); return m_n2; }
uint64_t timestamp() const { SASSERT(is_congruence()); return m_timestamp; }
theory_id theory_id() const { SASSERT(is_axiom()); return m_theory_id; }
template <typename T>
T* ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); }
@ -106,7 +121,7 @@ namespace euf {
case kind_t::external_t:
return external(copy_justification(m_external));
case kind_t::axiom_t:
return axiom();
return axiom(m_theory_id);
case kind_t::congruence_t:
return congruence(m_comm, m_timestamp);
case kind_t::dependent_t:
@ -114,7 +129,7 @@ namespace euf {
return dependent(m_dependency);
default:
UNREACHABLE();
return axiom();
return axiom(-1);
}
}

2
src/ast/euf/euf_plugin.cpp
View file

@ -32,7 +32,7 @@ namespace euf {
void plugin::push_merge(enode* a, enode* b) {
TRACE("plugin", tout << g.bpp(a) << " == " << g.bpp(b) << "\n");
g.push_merge(a, b, justification::axiom());
g.push_merge(a, b, justification::axiom(get_id()));
}
enode* plugin::mk(expr* e, unsigned n, enode* const* args) {