From 7497856dedd21c185e94caaf11f68be0bd847ae9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 May 2022 15:14:22 -0700 Subject: [PATCH] add ignore int to new arithmetic solvers Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_solver.cpp | 9 ++++++++- src/smt/theory_lra.cpp | 10 +++++++++- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 14ed76738..68c25c110 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1014,6 +1014,9 @@ namespace arith { return sat::check_result::CR_CONTINUE; case l_undef: 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; break; } @@ -1127,7 +1130,11 @@ namespace arith { if (!check_idiv_bounds()) 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: lia_check = l_true; break; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index cf1d73892..94702a32b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1539,6 +1539,8 @@ public: return FC_CONTINUE; case l_undef: TRACE("arith", tout << "check-lia giveup\n";); + if (ctx().get_fparams().m_arith_ignore_int) + return FC_GIVEUP; st = FC_CONTINUE; break; } @@ -1866,7 +1868,11 @@ public: return 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: lia_check = l_true; break; @@ -1896,6 +1902,8 @@ public: break; } case lp::lia_move::cut: { + if (ctx().get_fparams().m_arith_ignore_int) + return l_undef; TRACE("arith", tout << "cut\n";); ++m_stats.m_gomory_cuts; // m_explanation implies term <= k