mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

add ignore int to new arithmetic solvers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-11 15:14:22 -07:00
parent b1aa6b260b
commit 7497856ded
2 changed files with 17 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1014,6 +1014,9 @@ namespace arith {
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
case l_undef: case l_undef:
TRACE("arith", tout << "check-lia giveup\n";); TRACE("arith", tout << "check-lia giveup\n";);
if (ctx.get_config().m_arith_ignore_int)
return sat::check_result::CR_GIVEUP;
st = sat::check_result::CR_CONTINUE; st = sat::check_result::CR_CONTINUE;
break; break;
} }
@ -1127,7 +1130,11 @@ namespace arith {
if (!check_idiv_bounds()) if (!check_idiv_bounds())
return l_false; return l_false;
switch (m_lia->check(&m_explanation)) { auto cr = m_lia->check(&m_explanation);
if (cr != lp::lia_move::sat && ctx.get_config().m_arith_ignore_int)
return l_undef;
switch (cr) {
case lp::lia_move::sat: case lp::lia_move::sat:
lia_check = l_true; lia_check = l_true;
break; break;

10
src/smt/theory_lra.cpp
View file

@ -1539,6 +1539,8 @@ public:
return FC_CONTINUE; return FC_CONTINUE;
case l_undef: case l_undef:
TRACE("arith", tout << "check-lia giveup\n";); TRACE("arith", tout << "check-lia giveup\n";);
if (ctx().get_fparams().m_arith_ignore_int)
return FC_GIVEUP;
st = FC_CONTINUE; st = FC_CONTINUE;
break; break;
} }
@ -1866,7 +1868,11 @@ public:
return l_undef; return l_undef;
} }
lbool lia_check = l_undef; lbool lia_check = l_undef;
switch (m_lia->check(&m_explanation)) { auto cr = m_lia->check(&m_explanation);
if (cr != lp::lia_move::sat && ctx().get_fparams().m_arith_ignore_int)
return l_undef;
switch (cr) {
case lp::lia_move::sat: case lp::lia_move::sat:
lia_check = l_true; lia_check = l_true;
break; break;
@ -1896,6 +1902,8 @@ public:
break; break;
} }
case lp::lia_move::cut: { case lp::lia_move::cut: {
if (ctx().get_fparams().m_arith_ignore_int)
return l_undef;
TRACE("arith", tout << "cut\n";); TRACE("arith", tout << "cut\n";);
++m_stats.m_gomory_cuts; ++m_stats.m_gomory_cuts;
// m_explanation implies term <= k // m_explanation implies term <= k