mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

adding stubs to find fixed variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-04-26 19:39:42 -07:00
parent ef943347ee
commit c48dc69050
3 changed files with 112 additions and 58 deletions
Download patch file Download diff file Expand all files Collapse all files

55
src/math/lp/lar_solver.cpp
View file

@ -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 {

1
src/math/lp/lar_solver.h
View file

@ -367,6 +367,7 @@ public:
}
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)); }

114
src/smt/theory_lra.cpp
View file

@ -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 @@ public:
}
unsigned m_final_check_idx = 0;
distribution m_dist { 0 };
final_check_status final_check_eh() {
if (propagate_core())
@ -1657,34 +1659,53 @@ public:
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 (lp().has_fixed_at_bound()) // explain and propagate.
#if 0
distribution dist(++m_final_check_idx);
m_dist.reset();
m_dist.push(0, 1);
m_dist.push(1, 1);
m_dist.push(2, 1);
dist.add(0, 2);
dist.add(1, 1);
dist.add(1, 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 @@ public:
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 @@ public:
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 @@ public:
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 @@ public:
// 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 @@ public:
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 @@ public:
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 @@ public:
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();
}