mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-04 10:17:53 -07:00
parent 73118012c5
commit c194441824
2 changed files with 20 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -138,26 +138,31 @@ namespace arith {
lp_api::bound_kind k = b.get_bound_kind(); lp_api::bound_kind k = b.get_bound_kind();
theory_var v = b.get_var(); theory_var v = b.get_var();
inf_rational val = b.get_value(is_true); inf_rational val = b.get_value(is_true);
bool same_polarity = b.get_lit().sign() == lit1.sign();
lp_bounds const& bounds = m_bounds[v]; lp_bounds const& bounds = m_bounds[v];
SASSERT(!bounds.empty()); SASSERT(!bounds.empty());
if (bounds.size() == 1) return; if (bounds.size() == 1) return;
if (m_unassigned_bounds[v] == 0) return; if (m_unassigned_bounds[v] == 0) return;
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 = (same_polarity == (k == lp_api::lower_t));
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";); 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;
for (api_bound* b2 : bounds) { for (api_bound* b2 : bounds) {
if (b2 == &b) continue; if (b2 == &b)
continue;
rational const& val2 = b2->get_value(); rational const& val2 = b2->get_value();
if (((is_true || v_is_int) ? val2 < val : val2 <= val) && (!lb || glb < val2)) { if (lb && glb >= val2)
continue;
if (((same_polarity || v_is_int) ? val2 < val : val2 <= val)) {
lb = b2; lb = b2;
glb = val2; glb = val2;
} }
} }
if (!lb) return; if (!lb)
return;
bool sign = lb->get_bound_kind() != lp_api::lower_t; bool sign = lb->get_bound_kind() != lp_api::lower_t;
lit2 = lb->get_lit(); lit2 = lb->get_lit();
if (sign) if (sign)
@ -167,14 +172,18 @@ namespace arith {
rational lub; rational lub;
api_bound* ub = nullptr; api_bound* ub = nullptr;
for (api_bound* b2 : bounds) { for (api_bound* b2 : bounds) {
if (b2 == &b) continue; if (b2 == &b)
continue;
rational const& val2 = b2->get_value(); rational const& val2 = b2->get_value();
if (((is_true || v_is_int) ? val < val2 : val <= val2) && (!ub || val2 < lub)) { if (ub && val2 >= lub)
continue;
if (((same_polarity || v_is_int) ? val < val2 : val <= val2)) {
ub = b2; ub = b2;
lub = val2; lub = val2;
} }
} }
if (!ub) return; if (!ub)
return;
bool sign = ub->get_bound_kind() != lp_api::upper_t; bool sign = ub->get_bound_kind() != lp_api::upper_t;
lit2 = ub->get_lit(); lit2 = ub->get_lit();
if (sign) if (sign)

6
src/sat/smt/euf_model.cpp
View file

@ -209,8 +209,10 @@ namespace euf {
mdl->register_decl(f, fi); mdl->register_decl(f, fi);
} }
args.reset(); args.reset();
for (enode* arg : enode_args(n)) for (expr* arg : *a) {
args.push_back(m_values.get(arg->get_root_id())); enode* earg = get_enode(arg);
args.push_back(m_values.get(earg->get_root_id()));
}
DEBUG_CODE(for (expr* arg : args) VERIFY(arg);); DEBUG_CODE(for (expr* arg : args) VERIFY(arg););
SASSERT(args.size() == arity); SASSERT(args.size() == arity);
if (!fi->get_entry(args.data())) if (!fi->get_entry(args.data()))