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

re-enable delayed literal propagation

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-29 14:00:17 -08:00
parent 4289cfac8d
commit 2f01b5b567
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -83,7 +83,7 @@ namespace euf {
void egraph::reinsert_equality(enode* p) { void egraph::reinsert_equality(enode* p) {
SASSERT(p->is_equality()); SASSERT(p->is_equality());
if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root())
add_literal(p, nullptr); queue_literal(p, nullptr);
} }
void egraph::queue_literal(enode* p, enode* ante) { void egraph::queue_literal(enode* p, enode* ante) {

1
src/sat/smt/euf_solver.cpp
View file

@ -1059,6 +1059,7 @@ namespace euf {
}; };
r->m_egraph.copy_from(m_egraph, copy_justification); r->m_egraph.copy_from(m_egraph, copy_justification);
r->set_solver(s); r->set_solver(s);
r->m_egraph.copy_from(m_egraph, copy_justification);
for (euf::enode* n : r->m_egraph.nodes()) { for (euf::enode* n : r->m_egraph.nodes()) {
auto b = n->bool_var(); auto b = n->bool_var();
if (b != sat::null_bool_var) { if (b != sat::null_bool_var) {