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

#5223

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-02 10:30:35 -07:00
parent 323e0e6270
commit 0810720267
3 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lp_api.h
View file

@ -66,7 +66,7 @@ namespace lp_api {
lp::constraint_index get_constraint(bool b) const { return m_constraints[b]; } lp::constraint_index get_constraint(bool b) const { return m_constraints[b]; }
inf_rational get_value(bool is_true) const { inf_rational get_value(bool is_true) const {
if (is_true) if (is_true == !get_lit().sign())
return inf_rational(m_value); // v >= value or v <= value return inf_rational(m_value); // v >= value or v <= value
if (m_is_int) { if (m_is_int) {
SASSERT(m_value.is_int()); SASSERT(m_value.is_int());

5
src/sat/smt/arith_internalize.cpp
View file

@ -382,7 +382,7 @@ namespace arith {
updt_unassigned_bounds(v, +1); updt_unassigned_bounds(v, +1);
m_bounds_trail.push_back(v); m_bounds_trail.push_back(v);
m_bool_var2bound.insert(bv, b); m_bool_var2bound.insert(bv, b);
TRACE("arith_verbose", tout << "Internalized " << bv << ": " << mk_pp(atom, m) << "\n";); TRACE("arith_verbose", tout << "Internalized " << lit << ": " << mk_pp(atom, m) << " " << *b << "\n";);
m_new_bounds.push_back(b); m_new_bounds.push_back(b);
//add_use_lists(b); //add_use_lists(b);
return true; return true;
@ -583,11 +583,10 @@ namespace arith {
if (e->is_attached_to(get_id())) if (e->is_attached_to(get_id()))
return e->get_th_var(get_id()); return e->get_th_var(get_id());
theory_var v = mk_var(e); theory_var v = mk_var(e);
TRACE("arith", tout << "fresh var: v" << v << " " << mk_pp(n, m) << "\n";); TRACE("arith_verbose", tout << "v" << v << " " << mk_pp(n, m) << "\n";);
SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty()); SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty());
reserve_bounds(v); reserve_bounds(v);
ctx.attach_th_var(e, this, v); ctx.attach_th_var(e, this, v);
TRACE("arith", tout << mk_pp(n, m) << " " << v << "\n";);
SASSERT(euf::null_theory_var != v); SASSERT(euf::null_theory_var != v);
return v; return v;
} }

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

@ -145,7 +145,7 @@ namespace arith {
bool v_is_int = b.is_int(); bool v_is_int = b.is_int();
literal lit2 = sat::null_literal; literal lit2 = sat::null_literal;
bool find_glb = (is_true == (k == lp_api::lower_t)); bool find_glb = (is_true == (k == lp_api::lower_t));
TRACE("arith", tout << "v" << v << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";); TRACE("arith", tout << lit1 << " v" << v << " val " << val << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
if (find_glb) { if (find_glb) {
rational glb; rational glb;
api_bound* lb = nullptr; api_bound* lb = nullptr;
@ -187,6 +187,7 @@ namespace arith {
m_params.push_back(parameter(m_farkas)); m_params.push_back(parameter(m_farkas));
m_params.push_back(parameter(rational(1))); m_params.push_back(parameter(rational(1)));
m_params.push_back(parameter(rational(1))); m_params.push_back(parameter(rational(1)));
TRACE("arith", tout << lit2 << " <- " << m_core << "\n";);
assign(lit2, m_core, m_eqs, m_params); assign(lit2, m_core, m_eqs, m_params);
++m_stats.m_bounds_propagations; ++m_stats.m_bounds_propagations;
} }