mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix a bug in Horner heuristic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
8f297666fe
commit
8921ed56b5
|
@ -48,8 +48,12 @@ bool horner::row_is_interesting(const T& row) const {
|
|||
c().clear_active_var_set();
|
||||
for (const auto& p : row) {
|
||||
lpvar j = p.var();
|
||||
if (!c().is_monic_var(j))
|
||||
if (!c().is_monic_var(j)) {
|
||||
if (c().active_var_set_contains(j))
|
||||
return true;
|
||||
c().insert_to_active_var_set(j);
|
||||
continue;
|
||||
}
|
||||
auto & m = c().emons()[j];
|
||||
|
||||
for (lpvar k : m.vars()) {
|
||||
|
|
|
@ -314,13 +314,6 @@ void lar_solver::fill_explanation_from_crossed_bounds_column(explanation & evide
|
|||
|
||||
unsigned lar_solver::get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); }
|
||||
|
||||
vector<unsigned> lar_solver::get_list_of_all_var_indices() const {
|
||||
vector<unsigned> ret;
|
||||
for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_heading.size(); j++)
|
||||
ret.push_back(j);
|
||||
return ret;
|
||||
}
|
||||
|
||||
void lar_solver::push() {
|
||||
m_simplex_strategy = m_settings.simplex_strategy();
|
||||
m_simplex_strategy.push();
|
||||
|
|
|
@ -269,7 +269,6 @@ class lar_solver : public column_namer {
|
|||
m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
|
||||
}
|
||||
public:
|
||||
vector<unsigned> get_list_of_all_var_indices() const;
|
||||
inline void set_column_value_test(unsigned j, const impq& v) {
|
||||
set_column_value(j, v);
|
||||
}
|
||||
|
|
|
@ -133,9 +133,6 @@ template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init
|
|||
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::A_mult_x_is_off_on_index(vector<unsigned int> const&) const;
|
||||
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::find_x_by_solving();
|
||||
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_x(unsigned int, lp::numeric_pair<lp::mpq> const&);
|
||||
template bool lp::lp_core_solver_base<double, double>::pivot_for_tableau_on_basis();
|
||||
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivot_for_tableau_on_basis();
|
||||
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::pivot_for_tableau_on_basis();
|
||||
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::pivot_column_tableau(unsigned int, unsigned int);
|
||||
template bool lp::lp_core_solver_base<double, double>::pivot_column_tableau(unsigned int, unsigned int);
|
||||
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivot_column_tableau(unsigned int, unsigned int);
|
||||
|
|
|
@ -453,8 +453,6 @@ public:
|
|||
void pivot_fixed_vars_from_basis();
|
||||
bool remove_from_basis(unsigned j);
|
||||
bool pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w);
|
||||
bool pivot_for_tableau_on_basis();
|
||||
bool pivot_row_for_tableau_on_basis(unsigned row);
|
||||
void init_basic_part_of_basis_heading() {
|
||||
unsigned m = m_basis.size();
|
||||
for (unsigned i = 0; i < m; i++) {
|
||||
|
|
|
@ -85,16 +85,6 @@ init() {
|
|||
init_factorization(m_factorization, m_A, m_basis, m_settings);
|
||||
}
|
||||
|
||||
template <typename T, typename X> bool lp_core_solver_base<T, X>::
|
||||
pivot_for_tableau_on_basis() {
|
||||
m_d = m_costs; // we will be pivoting to m_d as well
|
||||
unsigned m = m_A.row_count();
|
||||
for (unsigned i = 0; i < m; i++)
|
||||
if (!pivot_column_tableau(m_basis[i], i))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
// i is the pivot row, and j is the pivot column
|
||||
template <typename T, typename X> void lp_core_solver_base<T, X>::
|
||||
pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
|
||||
|
|
|
@ -91,7 +91,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_si
|
|||
TRACE("nla_solver_bl", tout << "zero product sign: " << pp_mon(_(), m)<< "\n"; );
|
||||
generate_zero_lemmas(m);
|
||||
} else {
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
for(lpvar j: m.vars()) {
|
||||
negate_strict_sign(j);
|
||||
}
|
||||
|
@ -158,7 +158,7 @@ bool basics::basic_sign_lemma(bool derived) {
|
|||
// the value of the i-th monic has to be equal to the value of the k-th monic modulo sign
|
||||
// but it is not the case in the model
|
||||
void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) {
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
TRACE("nla_solver",
|
||||
tout << "m = " << pp_mon_with_vars(_(), m);
|
||||
tout << "n = " << pp_mon_with_vars(_(), n);
|
||||
|
@ -186,7 +186,7 @@ lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) cons
|
|||
return zero_j;
|
||||
}
|
||||
void basics::add_trival_zero_lemma(lpvar zero_j, const monic& m) {
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
c().mk_ineq(zero_j, llc::NE);
|
||||
c().mk_ineq(m.var(), llc::EQ);
|
||||
TRACE("nla_solver", c().print_lemma(tout););
|
||||
|
@ -194,7 +194,7 @@ void basics::add_trival_zero_lemma(lpvar zero_j, const monic& m) {
|
|||
void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) {
|
||||
TRACE("nla_solver_bl", tout << "sign_of_zj = " << sign_of_zj << "\n";);
|
||||
// we know all the signs
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT));
|
||||
for (unsigned j : m.vars()){
|
||||
if (j != zero_j) {
|
||||
|
@ -205,7 +205,7 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in
|
|||
TRACE("nla_solver", c().print_lemma(tout););
|
||||
}
|
||||
void basics::add_fixed_zero_lemma(const monic& m, lpvar j) {
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
c().explain_fixed_var(j);
|
||||
c().mk_ineq(m.var(), llc::EQ);
|
||||
TRACE("nla_solver", c().print_lemma(tout););
|
||||
|
@ -234,7 +234,7 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) {
|
|||
return true;
|
||||
#if 0
|
||||
TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
c().explain_fixed_var(var(rm));
|
||||
std::unordered_set<lpvar> processed;
|
||||
for (auto j : f) {
|
||||
|
@ -315,7 +315,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori
|
|||
if (zero_j == -1) {
|
||||
return false;
|
||||
}
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
c().explain_fixed_var(zero_j);
|
||||
c().explain_var_separated_from_zero(var(rm));
|
||||
explain(rm);
|
||||
|
@ -364,7 +364,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm
|
|||
return false;
|
||||
}
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
// mon_var = 0
|
||||
if (mon_var_is_sep_from_zero)
|
||||
c().explain_var_separated_from_zero(mon_var);
|
||||
|
@ -426,7 +426,7 @@ bool basics::proportion_lemma_derived(const monic& rm, const factorization& fact
|
|||
}
|
||||
// if there are no zero factors then |m| >= |m[factor_index]|
|
||||
void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) {
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
unsigned mon_var = m.var();
|
||||
rational mv = val(mon_var);
|
||||
rational sm = rational(nla::rat_sign(mv));
|
||||
|
@ -457,7 +457,7 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind
|
|||
generate_pl_on_mon(m, factor_index);
|
||||
return;
|
||||
}
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
int fi = 0;
|
||||
rational mv = var_val(m);
|
||||
rational sm = rational(nla::rat_sign(mv));
|
||||
|
@ -506,7 +506,7 @@ bool basics::factorization_has_real(const factorization& f) const {
|
|||
void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {
|
||||
TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
|
||||
SASSERT(var_val(rm).is_zero()&& ! c().rm_check(rm));
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
if (!is_separated_from_zero(f)) {
|
||||
c().mk_ineq(var(rm), llc::NE);
|
||||
for (auto j : f) {
|
||||
|
@ -577,7 +577,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
|
|||
return false;
|
||||
}
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
// mon_var = 0
|
||||
c().mk_ineq(mon_var, llc::EQ);
|
||||
|
||||
|
@ -625,7 +625,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co
|
|||
}
|
||||
}
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
for (auto j : m.vars()){
|
||||
if (not_one == j) continue;
|
||||
c().mk_ineq(j, llc::NE, val(j));
|
||||
|
@ -678,7 +678,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic
|
|||
return false;
|
||||
}
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
// mon_var = 0
|
||||
c().mk_ineq(mon_var, llc::EQ);
|
||||
|
||||
|
@ -753,7 +753,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const
|
|||
|
||||
TRACE("nla_solver_bl", tout << "not_one = " << not_one << "\n";);
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
|
||||
for (auto j : f){
|
||||
lpvar var_j = var(j);
|
||||
|
@ -788,7 +788,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
|
|||
}
|
||||
|
||||
if (zero_j == -1) { return; }
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
c().mk_ineq(zero_j, llc::NE);
|
||||
c().mk_ineq(f.mon().var(), llc::EQ);
|
||||
TRACE("nla_solver", c().print_lemma(tout););
|
||||
|
|
|
@ -41,7 +41,7 @@ rational common::mul_val(monic const& m) const { return c().mul_val(m); }
|
|||
template <typename T> lpvar common::var(T const& t) const { return c().var(t); }
|
||||
template lpvar common::var<factor>(factor const& t) const;
|
||||
template lpvar common::var<monic>(monic const& t) const;
|
||||
void common::add_empty_lemma() { c().add_empty_lemma(); }
|
||||
void common::add_lemma() { c().add_lemma(); }
|
||||
template <typename T> bool common::canonize_sign(const T& t) const {
|
||||
return c().canonize_sign(t);
|
||||
}
|
||||
|
|
|
@ -63,7 +63,7 @@ struct common {
|
|||
bool done() const;
|
||||
template <typename T> void explain(const T&);
|
||||
void explain(lpvar);
|
||||
void add_empty_lemma();
|
||||
void add_lemma();
|
||||
template <typename T> bool canonize_sign(const T&) const;
|
||||
void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs);
|
||||
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs);
|
||||
|
|
|
@ -1243,7 +1243,7 @@ rational core::val(const factorization& f) const {
|
|||
return r;
|
||||
}
|
||||
|
||||
void core::add_empty_lemma() {
|
||||
void core::add_lemma() {
|
||||
m_lemma_vec->push_back(lemma());
|
||||
}
|
||||
|
||||
|
@ -1656,7 +1656,7 @@ bool core::check_pdd_eq(const dd::solver::equation* e) {
|
|||
return false;
|
||||
eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd);
|
||||
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
current_expl().add(e);
|
||||
};
|
||||
if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
|
||||
|
|
|
@ -161,7 +161,7 @@ public:
|
|||
svector<lpvar> sorted_rvars(const factor& f) const;
|
||||
bool done() const;
|
||||
|
||||
void add_empty_lemma();
|
||||
void add_lemma();
|
||||
// the value of the factor is equal to the value of the variable multiplied
|
||||
// by the canonize_sign
|
||||
bool canonize_sign(const factor& f) const;
|
||||
|
|
|
@ -84,7 +84,7 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
|
|||
m_core->lp_settings().stats().m_cross_nested_forms++;
|
||||
scoped_dep_interval i(get_dep_intervals());
|
||||
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
|
||||
m_core->add_empty_lemma();
|
||||
m_core->add_lemma();
|
||||
m_core->current_expl().add(e);
|
||||
};
|
||||
if (!interval_of_expr<e_with_deps::without_deps>(n, 1, i, f)) {
|
||||
|
|
|
@ -48,7 +48,7 @@ void monotone::monotonicity_lemma(monic const& m) {
|
|||
void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) {
|
||||
TRACE("nla_solver", tout << "prod_val = " << prod_val << "\n";
|
||||
tout << "m = "; c().print_monic_with_vars(m, tout););
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
for (lpvar j : m.vars()) {
|
||||
c().add_abs_bound(j, llc::GT);
|
||||
}
|
||||
|
@ -64,7 +64,7 @@ void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) {
|
|||
\/_i |m[i]| < |val(m[i])} or |m| >= |product_i val(m[i])|
|
||||
*/
|
||||
void monotone::monotonicity_lemma_lt(const monic& m, const rational& prod_val) {
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
for (lpvar j : m.vars()) {
|
||||
c().add_abs_bound(j, llc::LT);
|
||||
}
|
||||
|
|
|
@ -92,7 +92,7 @@ void order::order_lemma_on_binomial(const monic& ac) {
|
|||
void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
|
||||
SASSERT(!_().mon_has_zero(xy.vars()));
|
||||
int sy = rat_sign(val(y));
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy
|
||||
mk_ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x));
|
||||
mk_ineq(xy.var(), - val(x), y, sign == 1 ? llc::LE : llc::GE);
|
||||
|
@ -175,7 +175,7 @@ void order::generate_mon_ol(const monic& ac,
|
|||
SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign));
|
||||
SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign));
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
mk_ineq(c_sign, c, llc::LE);
|
||||
explain(c); // this explains c == +- d
|
||||
mk_ineq(c_sign, a, -d_sign * b.rat_sign(), b.var(), negate(ab_cmp));
|
||||
|
@ -261,7 +261,7 @@ void order::generate_ol_eq(const monic& ac,
|
|||
const monic& bc,
|
||||
const factor& b) {
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
#if 0
|
||||
IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
|
||||
<< " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
|
||||
|
@ -287,7 +287,7 @@ void order::generate_ol(const monic& ac,
|
|||
const monic& bc,
|
||||
const factor& b) {
|
||||
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
#if 0
|
||||
IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
|
||||
<< " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
|
||||
|
@ -339,7 +339,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
|
|||
*/
|
||||
void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b) {
|
||||
SASSERT(sign * var_val(m) > val(a) * val(b));
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
if (val(a).is_pos()) {
|
||||
TRACE("nla_solver", tout << "a is pos\n";);
|
||||
//negate a > 0
|
||||
|
@ -369,7 +369,7 @@ void order::order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a,
|
|||
TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) <<
|
||||
", b = "; c().print_var(b, tout) << "\n";);
|
||||
SASSERT(sign * var_val(m) < val(a) * val(b));
|
||||
add_empty_lemma();
|
||||
add_lemma();
|
||||
if (val(a).is_pos()) {
|
||||
//negate a > 0
|
||||
mk_ineq(a, llc::LE);
|
||||
|
|
|
@ -75,7 +75,7 @@ struct imp {
|
|||
|
||||
|
||||
void generate_tang_plane(const point & pl) {
|
||||
c().add_empty_lemma();
|
||||
c().add_lemma();
|
||||
c().negate_relation(m_jx, m_x.rat_sign()*pl.x);
|
||||
c().negate_relation(m_jy, m_y.rat_sign()*pl.y);
|
||||
#if Z3DEBUG
|
||||
|
@ -95,12 +95,12 @@ struct imp {
|
|||
}
|
||||
|
||||
void generate_two_tang_lines() {
|
||||
m_tang.add_empty_lemma();
|
||||
m_tang.add_lemma();
|
||||
// Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var())
|
||||
c().mk_ineq(m_jx, llc::NE, c().val(m_jx));
|
||||
c().mk_ineq(m_j, - m_y.rat_sign() * m_xy.x, m_jy, llc::EQ);
|
||||
|
||||
m_tang.add_empty_lemma();
|
||||
m_tang.add_lemma();
|
||||
c().mk_ineq(m_jy, llc::NE, c().val(m_jy));
|
||||
c().mk_ineq(m_j, - m_x.rat_sign() * m_xy.y, m_jx, llc::EQ);
|
||||
}
|
||||
|
|
|
@ -2683,7 +2683,10 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
|
|||
return;
|
||||
}
|
||||
std::cout << "checking randomize" << std::endl;
|
||||
vector<var_index> all_vars = solver->get_list_of_all_var_indices();
|
||||
vector<var_index> all_vars;
|
||||
for (unsigned j = 0; j < solver->number_of_vars(); j++)
|
||||
all_vars.push_back(j);
|
||||
|
||||
unsigned m = all_vars.size();
|
||||
if (m > 100)
|
||||
m = 100;
|
||||
|
|
Loading…
Reference in a new issue