diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 1016c972b2e..0eb65e1973b 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1382,11 +1382,62 @@ namespace lp {
// the lower/upper bound is not strict.
// the LP obtained by making the bound strict is infeasible
// -> the column has to be fixed
- bool is_fixed_at_bound(column_index const& j) {
- NOT_IMPLEMENTED_YET();
+ bool lar_solver::is_fixed_at_bound(column_index const& j) {
+ if (column_is_fixed(j))
+ return false;
+ mpq val;
+ if (!has_value(j, val))
+ return false;
+ lp::lconstraint_kind k;
+ if (column_has_upper_bound(j) &&
+ get_upper_bound(j).x == val) {
+ verbose_stream() << "check upper " << j << "\n";
+ push();
+ if (column_is_int(j))
+ k = LE, val -= 1;
+ else
+ k = LT;
+ auto ci = mk_var_bound(j, k, val);
+ update_column_type_and_bound(j, k, val, ci);
+ auto st = find_feasible_solution();
+ pop(1);
+ return st == lp_status::INFEASIBLE;
+ }
+ if (column_has_lower_bound(j) &&
+ get_lower_bound(j).x == val) {
+ verbose_stream() << "check lower " << j << "\n";
+ push();
+ if (column_is_int(j))
+ k = GE, val += 1;
+ else
+ k = GT;
+ auto ci = mk_var_bound(j, k, val);
+ update_column_type_and_bound(j, k, val, ci);
+ auto st = find_feasible_solution();
+ pop(1);
+ return st == lp_status::INFEASIBLE;
+ }
+
return false;
}
+ bool lar_solver::has_fixed_at_bound() {
+ verbose_stream() << "has-fixed-at-bound\n";
+ unsigned num_fixed = 0;
+ for (unsigned j = 0; j < A_r().m_columns.size(); ++j) {
+ auto ci = column_index(j);
+ if (is_fixed_at_bound(ci)) {
+ ++num_fixed;
+ verbose_stream() << "fixed " << j << "\n";
+ }
+ }
+ verbose_stream() << "num fixed " << num_fixed << "\n";
+ if (num_fixed > 0)
+ find_feasible_solution();
+ return num_fixed > 0;
+ }
+
+
// below is the initialization functionality of lar_solver
bool lar_solver::strategy_is_undecided() const {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 76d8528a0aa..182ef0be3bf 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -367,6 +367,7 @@ class lar_solver : public column_namer {
}
bool is_fixed_at_bound(column_index const& j);
+ bool has_fixed_at_bound();
bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f5a10f94215..a5a31709b26 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -45,6 +45,7 @@
#include "ast/ast_ll_pp.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
+#include "util/distribution.h"
typedef lp::var_index lpvar;
@@ -1646,6 +1647,7 @@ class theory_lra::imp {
}
unsigned m_final_check_idx = 0;
+ distribution m_dist { 0 };
final_check_status final_check_eh() {
if (propagate_core())
@@ -1657,34 +1659,53 @@ class theory_lra::imp {
if (!lp().is_feasible() || lp().has_changed_columns()) {
is_sat = make_feasible();
}
- final_check_status st = FC_DONE, result = FC_DONE;
- m_final_check_idx = 0; // remove to experiment.
+ bool giveup = false;
+ final_check_status st = FC_DONE;
+ // m_final_check_idx = 0; // remove to experiment.
unsigned old_idx = m_final_check_idx;
-
switch (is_sat) {
case l_true:
TRACE("arith", display(tout));
-#if 0
- distribution dist(++m_final_check_idx);
+ // if (lp().has_fixed_at_bound()) // explain and propagate.
- dist.add(0, 2);
- dist.add(1, 1);
- dist.add(1, 1);
+#if 0
+ m_dist.reset();
+ m_dist.push(0, 1);
+ m_dist.push(1, 1);
+ m_dist.push(2, 1);
- for (auto idx : dist) {
+ for (auto idx : m_dist) {
if (!m.inc())
return FC_GIVEUP;
switch (idx) {
case 0:
+ if (assume_eqs())
+ st = FC_CONTINUE;
+ break;
case 1:
+ st = check_nla();
+ break;
case 2:
+ st = check_lia();
+ break;
default:
-
+ UNREACHABLE();
+ break;
+ }
+ switch (st) {
+ case FC_DONE:
+ break;
+ case FC_CONTINUE:
+ return st;
+ case FC_GIVEUP:
+ giveup = true;
+ break;
}
}
-#endif
+
+#else
do {
if (!m.inc())
@@ -1696,22 +1717,10 @@ class theory_lra::imp {
break;
case 1:
if (assume_eqs())
- st = FC_CONTINUE;
-
+ st = FC_CONTINUE;
break;
case 2:
- switch (check_nla()) {
- case l_true:
- st = FC_DONE;
- break;
- case l_false:
- st = FC_CONTINUE;
- break;
- case l_undef:
- TRACE("arith", tout << "check-nra giveup\n";);
- st = FC_GIVEUP;
- break;
- }
+ st = check_nla();
break;
}
m_final_check_idx = (m_final_check_idx + 1) % 3;
@@ -1721,14 +1730,15 @@ class theory_lra::imp {
case FC_CONTINUE:
return st;
case FC_GIVEUP:
- result = st;
+ giveup = true;
break;
}
}
while (old_idx != m_final_check_idx);
+#endif
- if (result == FC_GIVEUP)
- return result;
+ if (giveup)
+ return FC_GIVEUP;
for (expr* e : m_not_handled) {
if (!ctx().is_relevant(e))
continue;
@@ -1963,14 +1973,12 @@ class theory_lra::imp {
TRACE("arith", tout << "canceled\n";);
return FC_CONTINUE;
}
- final_check_status lia_check = FC_GIVEUP;
auto cr = m_lia->check(&m_explanation);
if (cr != lp::lia_move::sat && ctx().get_fparams().m_arith_ignore_int)
return FC_GIVEUP;
switch (cr) {
case lp::lia_move::sat:
- lia_check = FC_DONE;
break;
case lp::lia_move::branch: {
@@ -1993,9 +2001,8 @@ class theory_lra::imp {
// TBD: ctx().force_phase(ctx().get_literal(b));
// at this point we have a new unassigned atom that the
// SAT core assigns a value to
- lia_check = FC_CONTINUE;
++m_stats.m_branch;
- break;
+ return FC_CONTINUE;
}
case lp::lia_move::cut: {
if (ctx().get_fparams().m_arith_ignore_int)
@@ -2021,8 +2028,7 @@ class theory_lra::imp {
ctx().display_lemma_as_smt_problem(tout << "new cut:\n", m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
display(tout););
assign(lit, m_core, m_eqs, m_params);
- lia_check = FC_CONTINUE;
- break;
+ return FC_CONTINUE;
}
case lp::lia_move::conflict:
TRACE("arith", tout << "conflict\n";);
@@ -2031,18 +2037,19 @@ class theory_lra::imp {
return FC_CONTINUE;
case lp::lia_move::undef:
TRACE("arith", tout << "lia undef\n";);
- lia_check = FC_CONTINUE;
- break;
+ return FC_CONTINUE;
case lp::lia_move::continue_with_check:
- lia_check = FC_CONTINUE;
- break;
+ return FC_CONTINUE;
default:
UNREACHABLE();
}
- if (lia_check != l_false && !check_idiv_bounds())
+ if (!check_idiv_bounds())
return FC_CONTINUE;
- return lia_check;
+ if (assume_eqs())
+ return FC_CONTINUE;
+
+ return FC_DONE;
}
nla::lemma m_lemma;
@@ -2079,36 +2086,31 @@ class theory_lra::imp {
set_conflict_or_lemma(core, false);
}
- lbool check_nla_continue() {
+ final_check_status check_nla_continue() {
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_lemma_vector);
switch (r) {
- case l_false: {
+ case l_false:
for (const nla::lemma & l : m_nla_lemma_vector)
- false_case_of_check_nla(l);
- break;
- }
+ false_case_of_check_nla(l);
+ return FC_CONTINUE;
case l_true:
- if (assume_eqs()) {
- return l_false;
- }
- break;
- case l_undef:
- break;
+ return assume_eqs()? FC_CONTINUE: FC_DONE;
+ default:
+ return FC_GIVEUP;
}
- return r;
}
- lbool check_nla() {
+ final_check_status check_nla() {
if (!m.inc()) {
TRACE("arith", tout << "canceled\n";);
- return l_undef;
+ return FC_GIVEUP;
}
CTRACE("arith",!m_nla, tout << "no nla\n";);
if (!m_nla)
- return l_true;
+ return FC_DONE;
if (!m_nla->need_check())
- return l_true;
+ return FC_DONE;
return check_nla_continue();
}