mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
5cfe273460
commit
5d49cb5519
|
@ -765,7 +765,6 @@ namespace euf {
|
|||
|
||||
void egraph::copy_from(egraph const& src, std::function<void*(void*)>& copy_justification) {
|
||||
SASSERT(m_scopes.empty());
|
||||
SASSERT(src.m_scopes.empty());
|
||||
SASSERT(m_nodes.empty());
|
||||
ptr_vector<enode> old_expr2new_enode, args;
|
||||
ast_translation tr(src.m, m);
|
||||
|
@ -793,6 +792,8 @@ namespace euf {
|
|||
merge(n2, n2t, n1->m_justification.copy(copy_justification));
|
||||
}
|
||||
propagate();
|
||||
for (unsigned i = 0; i < src.m_scopes.size(); ++i)
|
||||
push();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -68,7 +68,7 @@ namespace sat {
|
|||
symbol m_name;
|
||||
solver* m_solver { nullptr };
|
||||
public:
|
||||
extension(symbol const& name, int id): m_id(id), m_name(name) {}
|
||||
extension(symbol const& name, int id): m_id(id), m_name(name) { }
|
||||
virtual ~extension() {}
|
||||
int get_id() const { return m_id; }
|
||||
void set_solver(solver* s) { m_solver = s; }
|
||||
|
|
|
@ -661,6 +661,7 @@ namespace bv {
|
|||
result->m_bits[i].append(m_bits[i]);
|
||||
result->m_zero_one_bits[i].append(m_zero_one_bits[i]);
|
||||
}
|
||||
result->set_solver(&ctx.s());
|
||||
for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i)
|
||||
if (find(i) != i)
|
||||
result->m_find.merge(i, find(i));
|
||||
|
|
Loading…
Reference in a new issue