mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

add branch / cut selection heuristic from solver=2

Browse source 
disabled for testing.
This commit is contained in:
Nikolaj Bjorner 2023-04-10 22:14:03 -07:00
parent bb44b91e45
commit 368d60f553
6 changed files with 114 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/ast/rewriter/arith_rewriter.cpp
View file

@ -16,6 +16,7 @@ Author:
Notes:
--*/
#include "params/arith_rewriter_params.hpp"
#include "ast/rewriter/arith_rewriter.h"
#include "ast/rewriter/poly_rewriter_def.h"
@ -1046,19 +1047,21 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
set_curr_sort(arg1->get_sort());
numeral v1, v2;
bool is_int;
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
bool is_num1 = m_util.is_numeral(arg1, v1, is_int);
bool is_num2 = m_util.is_numeral(arg2, v2, is_int);
if (is_num1 && is_num2 && !v2.is_zero()) {
result = m_util.mk_numeral(div(v1, v2), is_int);
return BR_DONE;
}
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
if (is_num2 && v2.is_one()) {
result = arg1;
return BR_DONE;
}
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_minus_one()) {
if (is_num2 && v2.is_minus_one()) {
result = m_util.mk_mul(m_util.mk_int(-1), arg1);
return BR_REWRITE1;
}
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
if (is_num2 && v2.is_zero()) {
return BR_FAILED;
}
if (arg1 == arg2) {
@ -1066,7 +1069,7 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
result = m.mk_ite(m.mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1));
return BR_REWRITE3;
}
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_pos() && m_util.is_add(arg1)) {
if (is_num2 && v2.is_pos() && m_util.is_add(arg1)) {
expr_ref_buffer args(m);
bool change = false;
rational add(0);
@ -1092,7 +1095,14 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
expr_ref zero(m_util.mk_int(0), m);
result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result);
return BR_REWRITE_FULL;
}
}
#if 0
expr* x = nullptr, *y = nullptr, *z = nullptr;
if (is_num2 && m_util.is_idiv(arg1, x, y) && m_util.is_numeral(y, v1) && v1 > 0 && v2 > 0) {
result = m_util.mk_idiv(x, m_util.mk_numeral(v1*v2, is_int));
return BR_DONE;
}
#endif
return BR_FAILED;
}

15
src/math/lp/gomory.cpp
View file

@ -377,10 +377,20 @@ bool gomory::is_gomory_cut_target(const row_strip<mpq>& row) {
}
int gomory::find_basic_var() {
int result = -1;
unsigned n = 0;
int result = -1;
unsigned min_row_size = UINT_MAX;
// Prefer smaller row size
#if 0
result = lia.select_int_infeasible_var();
if (result == -1)
return result;
const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(result));
if (is_gomory_cut_target(row))
return result;
#endif
for (unsigned j : lra.r_basis()) {
if (!lia.column_is_int_inf(j))
@ -389,6 +399,7 @@ int gomory::find_basic_var() {
if (!is_gomory_cut_target(row))
continue;
IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j)));
// Prefer smaller row size
if (min_row_size == UINT_MAX ||
2*row.size() < min_row_size ||
(4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) {

11
src/math/lp/int_branch.cpp
View file

@ -52,16 +52,22 @@ lia_move int_branch::create_branch_on_column(int j) {
int int_branch::find_inf_int_base_column() {
#if 0
return lia.select_int_infeasible_var();
#endif
int result = -1;
mpq range;
mpq new_range;
mpq small_range_thresold(1024);
mpq small_value(1024);
unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
unsigned prev_usage = 0; // to quiet down the compile
unsigned k = 0;
unsigned usage;
unsigned j;
// this loop looks for a column with the most usages, but breaks when
// a column with a small span of bounds is found
for (; k < lra.r_basis().size(); k++) {
@ -69,12 +75,13 @@ int int_branch::find_inf_int_base_column() {
if (!lia.column_is_int_inf(j))
continue;
usage = lra.usage_in_terms(j);
if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_range_thresold) {
if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
result = j;
k++;
n = 1;
break;
}
if (n == 0 || usage > prev_usage) {
result = j;
prev_usage = usage;

69
src/math/lp/int_solver.cpp
View file

@ -632,4 +632,73 @@ bool int_solver::non_basic_columns_are_at_bounds() const {
return true;
}
int int_solver::select_int_infeasible_var() {
int result = -1;
mpq range;
mpq new_range;
mpq small_value(1024);
unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
unsigned prev_usage = 0; // to quiet down the compile
unsigned k = 0;
unsigned usage;
unsigned j;
enum state { small_box, is_small_value, any_value, not_found };
state st = not_found;
// 1. small box
// 2. small value
// 3. any value
for (; k < lra.r_basis().size(); k++) {
j = lra.r_basis()[k];
if (!column_is_int_inf(j))
continue;
usage = lra.usage_in_terms(j);
if (is_boxed(j) && (new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
SASSERT(!is_fixed(j));
if (st != small_box) {
n = 0;
st = small_box;
}
if (n == 0 || new_range < range) {
result = j;
range = new_range;
n = 1;
}
else if (new_range == range && (random() % (++n) == 0)) {
result = j;
}
continue;
}
if (st == small_box)
continue;
impq const& value = get_value(j);
if (abs(value.x) < small_value ||
(has_upper(j) && small_value > upper_bound(j).x - value.x) ||
(has_lower(j) && small_value > value.x - lower_bound(j).x)) {
if (st != is_small_value) {
n = 0;
st = is_small_value;
}
if (random() % (++n) == 0)
result = j;
}
if (st == is_small_value)
continue;
SASSERT(st == not_found || st == any_value);
st = any_value;
if (n == 0 /*|| usage > prev_usage*/) {
result = j;
prev_usage = usage;
n = 1;
}
else if (usage > 0 && /*usage == prev_usage && */ (random() % (++n) == 0))
result = j;
}
return result;
}
}

3
src/math/lp/int_solver.h
View file

@ -129,5 +129,8 @@ public:
void find_feasible_solution();
lia_move hnf_cut();
void patch_nbasic_column(unsigned j) { m_patcher.patch_nbasic_column(j); }
int select_int_infeasible_var();
};
}

6
src/smt/theory_arith_int.h
View file

@ -514,9 +514,11 @@ namespace smt {
// SASSERT(m_value[x_i].is_rational()); // infinitesimals are not used for integer variables
SASSERT(!m_value[x_i].is_int()); // the base variable is not assigned to an integer value.
if (constrain_free_vars(r) || !is_gomory_cut_target(r)) {
bool cfv = constrain_free_vars(r);
if (cfv || !is_gomory_cut_target(r)) {
TRACE("gomory_cut", tout << "failed to apply gomory cut:\n";
tout << "constrain_free_vars(r): " << constrain_free_vars(r) << "\n";);
tout << "constrain_free_vars(r): " << cfv << "\n";);
return false;
}