mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

debug min_max

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-18 09:14:10 +02:00
parent eb1b578bfb
commit 392b419367
2 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/optsmt.cpp
View file

@ -298,11 +298,11 @@ namespace opt {
inf_eps optsmt::get_lower(unsigned i) const { inf_eps optsmt::get_lower(unsigned i) const {
return m_is_max[i]?m_lower[i]:-m_lower[i]; return m_is_max[i]?m_lower[i]:-m_upper[i];
} }
inf_eps optsmt::get_upper(unsigned i) const { inf_eps optsmt::get_upper(unsigned i) const {
return m_is_max[i]?m_upper[i]:-m_upper[i]; return m_is_max[i]?m_upper[i]:-m_lower[i];
} }
void optsmt::get_model(model_ref& mdl) { void optsmt::get_model(model_ref& mdl) {

4
src/smt/theory_arith_aux.h
View file

@ -930,6 +930,9 @@ namespace smt {
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::is_safe_to_leave(theory_var x) { bool theory_arith<Ext>::is_safe_to_leave(theory_var x) {
if (get_context().is_shared(get_enode(x))) {
return false;
}
column & c = m_columns[x]; column & c = m_columns[x];
typename svector<col_entry>::iterator it = c.begin_entries(); typename svector<col_entry>::iterator it = c.begin_entries();
typename svector<col_entry>::iterator end = c.end_entries(); typename svector<col_entry>::iterator end = c.end_entries();
@ -939,6 +942,7 @@ namespace smt {
theory_var s = r.get_base_var(); theory_var s = r.get_base_var();
numeral const & coeff = r[it->m_row_idx].m_coeff; numeral const & coeff = r[it->m_row_idx].m_coeff;
bool is_unsafe = (s != null_theory_var && is_int(s) && !coeff.is_int()); bool is_unsafe = (s != null_theory_var && is_int(s) && !coeff.is_int());
is_unsafe = is_unsafe || (s != null_theory_var && get_context().is_shared(get_enode(s)));
TRACE("opt", tout << "is v" << x << " safe to leave for v" << s << "? " << (is_unsafe?"no":"yes") << "\n"; TRACE("opt", tout << "is v" << x << " safe to leave for v" << s << "? " << (is_unsafe?"no":"yes") << "\n";
display_row(tout, r, true);); display_row(tout, r, true););
if (is_unsafe) return false; if (is_unsafe) return false;