Skip to content

Commit

Permalink
adding stubs to find fixed variables
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Apr 27, 2023
1 parent ef94334 commit c48dc69
Show file tree
Hide file tree
Showing 3 changed files with 112 additions and 58 deletions.
55 changes: 53 additions & 2 deletions src/math/lp/lar_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
1 change: 1 addition & 0 deletions src/math/lp/lar_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)); }
Expand Down
114 changes: 58 additions & 56 deletions src/smt/theory_lra.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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())
Expand All @@ -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())
Expand All @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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: {
Expand All @@ -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)
Expand All @@ -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";);
Expand All @@ -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;
Expand Down Expand Up @@ -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();
}

Expand Down

0 comments on commit c48dc69

Please sign in to comment.