mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

instrument for align solver=2, 6

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-05-22 16:09:22 +01:00
parent fca9939371
commit 8a996dc2ac
9 changed files with 700 additions and 660 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/rewriter/seq_rewriter.cpp
View file

@ -5024,12 +5024,14 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
* (re.range c_1 c_n)
*/
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
zstring s;
zstring slo, shi;
unsigned len = 0;
bool is_empty = false;
if (str().is_string(lo, s) && s.length() != 1)
if (str().is_string(lo, slo) && slo.length() != 1)
is_empty = true;
if (str().is_string(hi, s) && s.length() != 1)
if (str().is_string(hi, shi) && shi.length() != 1)
is_empty = true;
if (slo.length() == 1 && shi.length() == 1 && slo[0] > shi[0])
is_empty = true;
len = min_length(lo).second;
if (len > 1)
@ -5246,7 +5248,17 @@ br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) {
else if (re().is_range(r, r1, r2) &&
str().is_string(r1, s1) && str().is_string(r2, s2) &&
s1.length() == 1 && s2.length() == 1) {
result = m().mk_bool_val(s1[0] <= s2[0]);
result = m().mk_bool_val(s1[0] > s2[0]);
return BR_DONE;
}
else if (re().is_range(r, r1, r2) &&
str().is_string(r1, s1) && s1.length() != 1) {
result = m().mk_true();
return BR_DONE;
}
else if (re().is_range(r, r1, r2) &&
str().is_string(r2, s2) && s2.length() != 1) {
result = m().mk_true();
return BR_DONE;
}
else if ((re().is_loop(r, r1, lo) ||
@ -5307,6 +5319,7 @@ br_status seq_rewriter::mk_le_core(expr * l, expr * r, expr_ref & result) {
}
br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
TRACE("seq", tout << mk_pp(l, m()) << " == " << mk_pp(r, m()) << "\n");
expr_ref_vector res(m());
expr_ref_pair_vector new_eqs(m());
if (m_util.is_re(l)) {

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

@ -14,34 +14,51 @@
namespace lp {
int_solver::patcher::patcher(int_solver& lia):
int_solver::patcher::patcher(int_solver& lia):
lia(lia),
lra(lia.lra),
lrac(lia.lrac)
{}
{}
void int_solver::patcher::remove_fixed_vars_from_base() {
unsigned num = lra.A_r().column_count();
for (unsigned v = 0; v < num; v++) {
if (!lia.is_base(v) || !lia.is_fixed(v))
continue;
auto const & r = lra.basic2row(v);
for (auto const& c : r) {
if (c.var() != v && !lia.is_fixed(c.var())) {
lra.pivot(c.var(), v);
break;
}
}
}
}
lia_move int_solver::patcher::patch_nbasic_columns() {
lia_move int_solver::patcher::patch_nbasic_columns() {
remove_fixed_vars_from_base();
lia.settings().stats().m_patches++;
lp_assert(lia.is_feasible());
m_patch_success = 0;
m_patch_fail = 0;
m_num_ones = 0;
m_num_divides = 0;
unsigned num = lra.A_r().column_count();
for (unsigned v = 0; v < num; v++) {
if (lia.is_base(v))
continue;
patch_nbasic_column(v);
}
// for (unsigned j : lia.lrac.m_r_nbasis)
// patch_nbasic_column(j);
lp_assert(lia.is_feasible());
verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << "\n";
verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << "\n";
//lra.display(verbose_stream());
//exit(0);
if (!lia.has_inf_int()) {
lia.settings().stats().m_patches_success++;
return lia_move::sat;
}
return lia_move::undef;
}
}
void int_solver::patcher::patch_nbasic_column(unsigned j) {
impq & val = lrac.m_r_x[j];
@ -54,8 +71,24 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
bool m_is_one = m.is_one();
bool val_is_int = lia.value_is_int(j);
const auto & A = lra.A_r();
if (!m_is_one) {
verbose_stream() << "divisor: " << m << "\n";
lia.display_column(verbose_stream(), j);
for (auto c : A.column(j)) {
unsigned row_index = c.var();
lia.display_row(verbose_stream(), A.m_rows[row_index]);
verbose_stream() << "\n";
}
}
// check whether value of j is already a multiple of m.
if (val_is_int && (m_is_one || (val.x / m).is_int())) {
if (m_is_one)
++m_num_ones;
else
++m_num_divides;
return;
}
@ -77,12 +110,14 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
}
#endif
#if 0
verbose_stream() << "TARGET v" << j << " -> [";
if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x);
verbose_stream() << ", ";
if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x);
verbose_stream() << "]";
verbose_stream() << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";
#endif
if (!inf_l) {
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
@ -472,14 +507,11 @@ bool int_solver::at_upper(unsigned j) const {
}
std::ostream & int_solver::display_row(std::ostream & out, lp::row_strip<rational> const & row) const {
bool first = true;
bool first = true;
auto & rslv = lrac.m_r_solver;
for (const auto &c : row)
{
if (is_fixed(c.var()))
{
if (!get_value(c.var()).is_zero())
{
for (const auto &c : row) {
if (is_fixed(c.var())) {
if (!get_value(c.var()).is_zero()) {
impq val = get_value(c.var()) * c.coeff();
if (!first && val.is_pos())
out << "+";
@ -498,17 +530,11 @@ for (const auto &c : row)
}
else if (c.coeff().is_minus_one())
out << "-";
else
{
if (c.coeff().is_pos())
{
if (!first)
else {
if (c.coeff().is_pos() && !first)
out << "+";
}
if (c.coeff().is_big())
{
out << " b*";
}
else
out << c.coeff();
}
@ -516,8 +542,7 @@ for (const auto &c : row)
first = false;
}
out << "\n";
for (const auto &c : row)
{
for (const auto &c : row) {
if (is_fixed(c.var()))
continue;
rslv.print_column_info(c.var(), out);
@ -526,14 +551,13 @@ for (const auto &c : row)
}
return out;
}
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
auto & rslv = lrac.m_r_solver;
auto const& row = rslv.m_A.m_rows[row_index];
return display_row(out, row);
}
bool int_solver::shift_var(unsigned j, unsigned range) {
if (is_fixed(j) || is_base(j))
return false;

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

@ -46,12 +46,15 @@ class int_solver {
lar_core_solver& lrac;
unsigned m_patch_success = 0;
unsigned m_patch_fail = 0;
unsigned m_num_ones = 0;
unsigned m_num_divides = 0;
public:
patcher(int_solver& lia);
bool should_apply() const { return true; }
lia_move operator()() { return patch_nbasic_columns(); }
void patch_nbasic_column(unsigned j);
private:
void remove_fixed_vars_from_base();
lia_move patch_nbasic_columns();
};

2
src/math/lp/lar_core_solver.h
View file

@ -93,6 +93,8 @@ public:
void solve();
void pivot(int entering, int leaving) { m_r_solver.pivot(entering, leaving); }
bool lower_bounds_are_set() const { return true; }
const indexed_vector<mpq> & get_pivot_row() const {

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

@ -393,9 +393,15 @@ public:
void clear_inf_set() {
m_mpq_lar_core_solver.m_r_solver.inf_set().clear();
}
inline void remove_column_from_inf_set(unsigned j) {
m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j);
}
void pivot(int entering, int leaving) {
m_mpq_lar_core_solver.pivot(entering, leaving);
}
template <typename ChangeReport>
void change_basic_columns_dependend_on_a_given_nb_column_report(unsigned j,
const numeric_pair<mpq> & delta,
@ -403,14 +409,13 @@ public:
for (const auto & c : A_r().m_columns[j]) {
unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()];
if (tableau_with_costs()) {
if (tableau_with_costs())
m_basic_columns_with_changed_cost.insert(bj);
}
m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, - A_r().get_val(c) * delta);
after(bj);
TRACE("change_x_del",
tout << "changed basis column " << bj << ", it is " <<
( m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj)? "feas":"inf") << std::endl;);
( m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj)?"feas":"inf") << std::endl;);
}
}

2
src/math/lp/lp_core_solver_base_def.h
View file

@ -324,7 +324,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
return false;
}
if (m_pivoted_rows!= nullptr)
if (m_pivoted_rows != nullptr)
m_pivoted_rows->insert(c.var());
}

88
src/math/lp/lp_primal_core_solver.h
View file

@ -35,12 +35,12 @@ Revision History:
#include <unordered_map>
namespace lp {
// This core solver solves (Ax=b, lower_bound_values \leq x \leq
// upper_bound_values, maximize costs*x ) The right side b is given implicitly
// by x and the basis
template <typename T, typename X>
class lp_primal_core_solver : public lp_core_solver_base<T, X> {
public:
// This core solver solves (Ax=b, lower_bound_values \leq x \leq
// upper_bound_values, maximize costs*x ) The right side b is given implicitly
// by x and the basis
template <typename T, typename X>
class lp_primal_core_solver : public lp_core_solver_base<T, X> {
public:
int m_sign_of_entering_delta;
vector<T> m_costs_backup;
unsigned m_inf_row_index_for_tableau;
@ -96,22 +96,12 @@ public:
case column_type::fixed:
return false;
case column_type::lower_bound:
if (is_pos(rc.coeff())) {
return this->x_above_lower_bound(j);
}
return true;
return !is_pos(rc.coeff()) || this->x_above_lower_bound(j);
case column_type::upper_bound:
if (is_pos(rc.coeff())) {
return true;
}
return this->x_below_upper_bound(j);
return is_pos(rc.coeff()) || this->x_below_upper_bound(j);
case column_type::boxed:
if (is_pos(rc.coeff())) {
if (is_pos(rc.coeff()))
return this->x_above_lower_bound(j);
}
return this->x_below_upper_bound(j);
default:
return false;
@ -129,22 +119,16 @@ public:
case column_type::fixed:
return false;
case column_type::lower_bound:
if (is_neg(rc.coeff())) {
if (is_neg(rc.coeff()))
return this->x_above_lower_bound(j);
}
return true;
case column_type::upper_bound:
if (is_neg(rc.coeff())) {
if (is_neg(rc.coeff()))
return true;
}
return this->x_below_upper_bound(j);
case column_type::boxed:
if (is_neg(rc.coeff())) {
if (is_neg(rc.coeff()))
return this->x_above_lower_bound(j);
}
return this->x_below_upper_bound(j);
default:
return false;
@ -153,8 +137,8 @@ public:
return false;
}
unsigned get_number_of_basic_vars_that_might_become_inf(
unsigned j) const { // consider looking at the signs here: todo
unsigned get_number_of_basic_vars_that_might_become_inf(unsigned j) const {
// consider looking at the signs here: todo
unsigned r = 0;
for (const auto &cc : this->m_A.m_columns[j]) {
unsigned k = this->m_basis[cc.var()];
@ -174,7 +158,8 @@ public:
if (bj_needs_to_grow) {
if (!monoid_can_decrease(rc))
continue;
} else {
}
else {
if (!monoid_can_increase(rc))
continue;
}
@ -183,10 +168,8 @@ public:
a_ent = rc.coeff();
}
}
if (j == -1) {
if (j == -1)
m_inf_row_index_for_tableau = i;
}
return j;
}
@ -219,7 +202,8 @@ public:
len = this->m_A.m_columns[j].size();
choice = k;
nchoices = 1;
} else if (damage == num_of_non_free_basics &&
}
else if (damage == num_of_non_free_basics &&
this->m_A.m_columns[j].size() <= len &&
(this->m_settings.random_next() % (++nchoices))) {
choice = k;
@ -236,46 +220,43 @@ public:
return rc.var();
}
bool try_jump_to_another_bound_on_entering(unsigned entering, const X &theta,
X &t, bool &unlimited);
bool try_jump_to_another_bound_on_entering(unsigned entering, const X &theta, X &t, bool &unlimited);
bool try_jump_to_another_bound_on_entering_unlimited(unsigned entering, X &t);
int find_leaving_and_t_tableau(unsigned entering, X &t);
void limit_theta(const X &lim, X &theta, bool &unlimited) {
if (unlimited) {
theta = lim;
unlimited = false;
} else {
theta = std::min(lim, theta);
}
else
theta = std::min(lim, theta);
}
void limit_theta_on_basis_column_for_inf_case_m_neg_upper_bound(
unsigned j, const T &m, X &theta, bool &unlimited) {
lp_assert(m < 0 && this->m_column_types[j] == column_type::upper_bound);
limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bounds[j],
theta, unlimited);
limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited);
}
void limit_theta_on_basis_column_for_inf_case_m_neg_lower_bound(
unsigned j, const T &m, X &theta, bool &unlimited) {
lp_assert(m < 0 && this->m_column_types[j] == column_type::lower_bound);
limit_inf_on_bound_m_neg(m, this->m_x[j], this->m_lower_bounds[j], theta,
unlimited);
limit_inf_on_bound_m_neg(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited);
}
void limit_theta_on_basis_column_for_inf_case_m_pos_lower_bound(
unsigned j, const T &m, X &theta, bool &unlimited) {
lp_assert(m > 0 && this->m_column_types[j] == column_type::lower_bound);
limit_inf_on_lower_bound_m_pos(m, this->m_x[j], this->m_lower_bounds[j],
theta, unlimited);
limit_inf_on_lower_bound_m_pos(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited);
}
void limit_theta_on_basis_column_for_inf_case_m_pos_upper_bound(
unsigned j, const T &m, X &theta, bool &unlimited) {
lp_assert(m > 0 && this->m_column_types[j] == column_type::upper_bound);
limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta,
unlimited);
limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited);
};
void get_bound_on_variable_and_update_leaving_precisely(
@ -305,6 +286,11 @@ public:
void advance_on_entering_and_leaving_tableau(int entering, int leaving, X &t);
void advance_on_entering_equal_leaving_tableau(int entering, X &t);
void pivot(int entering, int leaving) {
this->pivot_column_tableau(entering, this->m_basis_heading[leaving]);
this->change_basis(entering, leaving);
}
bool need_to_switch_costs() const {
if (this->m_settings.simplex_strategy() ==
simplex_strategy_enum::tableau_rows)
@ -334,13 +320,11 @@ public:
void update_x_tableau_rows(unsigned entering, unsigned leaving,
const X &delta) {
this->add_delta_to_x(entering, delta);
for (const auto &c : this->m_A.m_columns[entering]) {
if (leaving != this->m_basis[c.var()]) {
for (const auto &c : this->m_A.m_columns[entering])
if (leaving != this->m_basis[c.var()])
this->add_delta_to_x_and_track_feasibility(
this->m_basis[c.var()], -delta * this->m_A.get_val(c));
}
}
}
void update_basis_and_x_tableau_rows(int entering, int leaving, X const &tt) {
lp_assert(entering != leaving);
@ -670,5 +654,5 @@ public:
}
friend core_solver_pretty_printer<T, X>;
};
};
} // namespace lp

5
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -162,13 +162,14 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
return;
}
if (!is_zero(t)) {
if (this->current_x_is_feasible() ) {
if (this->current_x_is_feasible()) {
if (m_sign_of_entering_delta == -1)
t = -t;
}
this->update_basis_and_x_tableau(entering, leaving, t);
this->iters_with_no_cost_growing() = 0;
} else {
}
else {
this->pivot_column_tableau(entering, this->m_basis_heading[leaving]);
this->change_basis(entering, leaving);
}

16
src/smt/theory_arith_int.h
View file

@ -908,15 +908,20 @@ namespace smt {
inf_numeral l, u;
numeral m;
unsigned num_patched = 0, num_not_patched = 0;
unsigned num_one = 0, num_divides = 0;
for (theory_var v = 0; v < num; v++) {
if (!is_non_base(v))
continue;
get_freedom_interval(v, inf_l, l, inf_u, u, m);
if (m.is_one() && get_value(v).is_int())
if (m.is_one() && get_value(v).is_int()) {
num_one++;
continue;
}
// check whether value of v is already a multiple of m.
if ((get_value(v).get_rational() / m).is_int())
if ((get_value(v).get_rational() / m).is_int()) {
num_divides++;
continue;
}
TRACE("patch_int",
tout << "TARGET v" << v << " -> [";
@ -927,13 +932,14 @@ namespace smt {
tout << ", m: " << m << ", val: " << get_value(v) << ", is_int: " << is_int(v) << "\n";);
#if 0
verbose_stream() << "TARGET v" << v << " -> [";
if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l);
verbose_stream() << ", ";
if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u);
verbose_stream() << "]";
verbose_stream() << ", m: " << m << ", val: " << get_value(v) << ", is_int: " << is_int(v) << "\n";
#endif
if (!inf_l)
l = ceil(l);
if (!inf_u)
@ -957,7 +963,9 @@ namespace smt {
set_value(v, inf_numeral(0));
}
SASSERT(m_to_patch.empty());
verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << "\n";
verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << "\n";
//display(verbose_stream());
//exit(0);
}
/**