mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

start using lar_solver::is_feasible() (#5697)

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2021-12-06 06:16:57 -10:00 • committed by GitHub
parent 7758b519bc
commit 9b4f3a7075
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/smt/theory_lra.cpp
View file

@ -1529,7 +1529,7 @@ public:
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 @@ public:
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 @@ public:
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);