From 9b4f3a7075e8dd3d9bc3ce248753be0459a11731 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Dec 2021 06:16:57 -1000 Subject: [PATCH] start using lar_solver::is_feasible() (#5697) Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5c2f5bf1b97..9f116cf2801 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1529,7 +1529,7 @@ class theory_lra::imp { IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); lbool is_sat = l_true; SASSERT(lp().ax_is_correct()); - if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) { + if (!lp().is_feasible() || lp().has_changed_columns()) { is_sat = make_feasible(); } final_check_status st = FC_DONE; @@ -3083,21 +3083,14 @@ class theory_lra::imp { TRACE("pcs", tout << lp().constraints();); auto status = lp().find_feasible_solution(); TRACE("arith_verbose", display(tout);); - switch (status) { - case lp::lp_status::INFEASIBLE: - return l_false; - case lp::lp_status::FEASIBLE: - case lp::lp_status::OPTIMAL: - // SASSERT(lp().all_constraints_hold()); + if (lp().is_feasible()) return l_true; - case lp::lp_status::TIME_EXHAUSTED: - - default: - TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";); + if (status == lp::lp_status::INFEASIBLE) + return l_false; + TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";); // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, // FLOATING_POINT_ERROR, TIME_EXAUSTED, EMPTY, UNSTABLE - return l_undef; - } + return l_undef; } lp::explanation m_explanation; @@ -3467,7 +3460,7 @@ class theory_lra::imp { st = lp::lp_status::UNBOUNDED; } else { - if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) + if (!lp().is_feasible() || lp().has_changed_columns()) make_feasible(); vi = get_lpvar(v);