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

sat.euf add missing function

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-22 19:17:17 -07:00
parent 800fef6653
commit 32beb91efa
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -129,7 +129,7 @@ namespace euf {
return n; return n;
} }
egraph::egraph(ast_manager& m) : m(m), m_table(m), m_exprs(m) { egraph::egraph(ast_manager& m) : m(m), m_table(m), m_tmp_app(2), m_exprs(m) {
m_tmp_eq = enode::mk_tmp(m_region, 2); m_tmp_eq = enode::mk_tmp(m_region, 2);
} }
@ -418,12 +418,10 @@ namespace euf {
std::swap(n1, n2); std::swap(n1, n2);
} }
if (m.is_false(r2->get_expr()) && r1->value() == l_true) { if (m.is_false(r2->get_expr()) && r1->value() == l_true) {
std::cout << "value assign conflict\n";
set_conflict(n1, n2, j); set_conflict(n1, n2, j);
return; return;
} }
if (m.is_true(r2->get_expr()) && r1->value() == l_false) { if (m.is_true(r2->get_expr()) && r1->value() == l_false) {
std::cout << "value assign conflict\n";
set_conflict(n1, n2, j); set_conflict(n1, n2, j);
return; return;
} }
@ -604,6 +602,12 @@ namespace euf {
return false; return false;
} }
enode* egraph::get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args) {
m_tmp_app.set_decl(f);
m_tmp_app.set_num_args(num_args);
return find(m_tmp_app.get_app(), num_args, args);
}
/** /**
\brief generate an explanation for a congruence. \brief generate an explanation for a congruence.
Each pair of children under a congruence have the same roots Each pair of children under a congruence have the same roots

3
src/ast/euf/euf_egraph.h
View file

@ -159,6 +159,7 @@ namespace euf {
enode* m_tmp_eq = nullptr; enode* m_tmp_eq = nullptr;
enode* m_tmp_node = nullptr; enode* m_tmp_node = nullptr;
unsigned m_tmp_node_capacity = 0; unsigned m_tmp_node_capacity = 0;
tmp_app m_tmp_app;
enode_vector m_nodes; enode_vector m_nodes;
expr_ref_vector m_exprs; expr_ref_vector m_exprs;
vector<enode_vector> m_decl2enodes; vector<enode_vector> m_decl2enodes;
@ -261,7 +262,7 @@ namespace euf {
*/ */
bool are_diseq(enode* a, enode* b) const; bool are_diseq(enode* a, enode* b) const;
enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) { UNREACHABLE(); return nullptr; } enode* get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args);
/** /**
\brief Maintain and update cursor into propagated consequences. \brief Maintain and update cursor into propagated consequences.