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

#7027

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-02 12:05:06 -08:00
parent 7eab26e3ef
commit 331507c4cd
2 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/sat/smt/arith_solver.cpp
View file

@ -53,17 +53,22 @@ namespace arith {
euf::th_solver* solver::clone(euf::solver& dst_ctx) { euf::th_solver* solver::clone(euf::solver& dst_ctx) {
arith::solver* result = alloc(arith::solver, dst_ctx, get_id()); arith::solver* result = alloc(arith::solver, dst_ctx, get_id());
unsigned_vector var2var;
for (unsigned i = 0; i < result->get_num_vars(); ++i)
var2var.push_back(i);
for (unsigned i = result->get_num_vars(); i < get_num_vars(); ++i) for (unsigned i = result->get_num_vars(); i < get_num_vars(); ++i)
result->mk_evar(ctx.copy(dst_ctx, var2enode(i))->get_expr()); var2var.push_back(result->mk_evar(ctx.copy(dst_ctx, var2enode(i))->get_expr()));
unsigned v = 0; unsigned v = 0;
result->m_bounds.resize(m_bounds.size()); result->m_bounds.resize(m_bounds.size());
for (auto const& bounds : m_bounds) { for (auto const& bounds : m_bounds) {
auto w = var2var[v];
for (auto* b : bounds) { for (auto* b : bounds) {
auto* b2 = result->mk_var_bound(b->get_lit(), v, b->get_bound_kind(), b->get_value()); auto* b2 = result->mk_var_bound(b->get_lit(), w, b->get_bound_kind(), b->get_value());
result->m_bounds[v].push_back(b2); result->m_bounds[w].push_back(b2);
result->m_bounds_trail.push_back(v); result->m_bounds_trail.push_back(w);
result->updt_unassigned_bounds(v, +1); result->updt_unassigned_bounds(w, +1);
result->m_bool_var2bound.insert(b->get_lit().var(), b2); result->m_bool_var2bound.insert(b->get_lit().var(), b2);
result->m_new_bounds.push_back(b2); result->m_new_bounds.push_back(b2);
} }

4
src/sat/smt/euf_internalize.cpp
View file

@ -425,7 +425,7 @@ namespace euf {
// not marked as shared. // not marked as shared.
for (auto const& p : euf::enode_th_vars(n)) for (auto const& p : euf::enode_th_vars(n))
if (fid2solver(p.get_id())->is_shared(p.get_var())) { if (fid2solver(p.get_id()) && fid2solver(p.get_id())->is_shared(p.get_var())) {
n->set_is_shared(l_true); n->set_is_shared(l_true);
return true; return true;
} }
@ -436,7 +436,7 @@ namespace euf {
bool solver::is_beta_redex(enode* p, enode* n) const { bool solver::is_beta_redex(enode* p, enode* n) const {
for (auto const& th : enode_th_vars(p)) for (auto const& th : enode_th_vars(p))
if (fid2solver(th.get_id())->is_beta_redex(p, n)) if (fid2solver(th.get_id()) && fid2solver(th.get_id())->is_beta_redex(p, n))
return true; return true;
return false; return false;
} }