mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

debugging mbi

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-13 21:33:21 -07:00 • committed by Arie Gurfinkel
parent 49279d7047
commit 1902360361
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/simplex/model_based_opt.cpp
View file

@ -526,6 +526,7 @@ namespace opt {
rational distance = src_c * dst_val + dst_c * src_val + slack; rational distance = src_c * dst_val + dst_c * src_val + slack;
bool use_case1 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one(); bool use_case1 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one();
#if 0
if (distance.is_nonpos() && !abs_src_c.is_one() && !abs_dst_c.is_one()) { if (distance.is_nonpos() && !abs_src_c.is_one() && !abs_dst_c.is_one()) {
unsigned r = copy_row(row_src); unsigned r = copy_row(row_src);
mul_add(false, r, rational::one(), row_dst); mul_add(false, r, rational::one(), row_dst);
@ -534,12 +535,13 @@ namespace opt {
TRACE("qe", tout << m_rows[r];); TRACE("qe", tout << m_rows[r];);
SASSERT(!m_rows[r].m_value.is_pos()); SASSERT(!m_rows[r].m_value.is_pos());
} }
#endif
if (use_case1) { if (use_case1) {
TRACE("opt", tout << "slack: " << slack << " " << src_c << " " << dst_val << " " << dst_c << " " << src_val << "\n";); TRACE("opt", tout << "slack: " << slack << " " << src_c << " " << dst_val << " " << dst_c << " " << src_val << "\n";);
// dst <- abs_src_c*dst + abs_dst_c*src - slack // dst <- abs_src_c*dst + abs_dst_c*src + slack
mul(row_dst, abs_src_c); mul(row_dst, abs_src_c);
sub(row_dst, slack); add(row_dst, slack);
mul_add(false, row_dst, abs_dst_c, row_src); mul_add(false, row_dst, abs_dst_c, row_src);
return; return;
} }