mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

address #3886 and #3891 by revamping nl_arith decoupling of monomial analysis and access

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-10 01:33:46 -07:00
parent addbe55823
commit ee9c797822
3 changed files with 182 additions and 293 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context_pp.cpp
View file

@ -454,7 +454,6 @@ namespace smt {
display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic); display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic);
TRACE("non_linear", display_lemma_as_smt_problem(tout, num_antecedents, antecedents, consequent, logic);); TRACE("non_linear", display_lemma_as_smt_problem(tout, num_antecedents, antecedents, consequent, logic););
out.close(); out.close();
// SASSERT(m_lemma_id != 2);
return m_lemma_id; return m_lemma_id;
} }
@ -495,10 +494,9 @@ namespace smt {
std::ofstream out(strm.str()); std::ofstream out(strm.str());
TRACE("lemma", tout << strm.str() << "\n"; TRACE("lemma", tout << strm.str() << "\n";
display_lemma_as_smt_problem(tout, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); display_lemma_as_smt_problem(tout, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
); );
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close(); out.close();
//SASSERT(m_lemma_id != 2);
return m_lemma_id; return m_lemma_id;
} }

20
src/smt/theory_arith.h
View file

@ -978,15 +978,16 @@ namespace smt {
void mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found); void mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found);
void mark_dependents(theory_var v, svector<theory_var> & vars, var_set & already_found, row_set & already_visited_rows); void mark_dependents(theory_var v, svector<theory_var> & vars, var_set & already_found, row_set & already_visited_rows);
void get_non_linear_cluster(svector<theory_var> & vars); void get_non_linear_cluster(svector<theory_var> & vars);
std::pair<unsigned, int> analyze_monomial(expr * m) const;
expr * get_monomial_body(expr * m) const;
rational get_monomial_coeff(expr * m) const;
unsigned get_num_vars_in_monomial(expr * m) const;
typedef std::pair<expr *, unsigned> var_power_pair; typedef std::pair<expr *, unsigned> var_power_pair;
var_power_pair get_var_and_degree(expr * m, unsigned i) const; typedef std::pair<unsigned, var_power_pair> n_var_power_pair;
n_var_power_pair analyze_monomial(expr * m) const;
rational decompose_monomial(expr* m, buffer<var_power_pair>& vp) const;
void display_monomial(std::ostream & out, expr * m) const; void display_monomial(std::ostream & out, expr * m) const;
bool propagate_nl_upward(expr * m); bool propagate_nl_upward(expr * m);
bool propagate_nl_downward(expr * m, unsigned i); bool propagate_nl_downward(expr * m, var_power_pair const& p);
interval mk_interval_for(theory_var v); interval mk_interval_for(theory_var v);
interval mk_interval_for(expr * n); interval mk_interval_for(expr * n);
void mul_bound_of(expr * var, unsigned power, interval & target); void mul_bound_of(expr * var, unsigned power, interval & target);
@ -996,14 +997,13 @@ namespace smt {
bool update_bounds_using_interval(theory_var v, interval const & i); bool update_bounds_using_interval(theory_var v, interval const & i);
bool update_bounds_using_interval(expr * n, interval const & i); bool update_bounds_using_interval(expr * n, interval const & i);
bool propagate_nl_bounds(expr * m); bool propagate_nl_bounds(expr * m);
bool propagate_nl_bound(expr * m, int i);
bool propagate_nl_bounds(); bool propagate_nl_bounds();
bool is_problematic_non_linear_row(row const & r); bool is_problematic_non_linear_row(row const & r);
bool is_mixed_real_integer(row const & r) const; bool is_mixed_real_integer(row const & r) const;
bool is_integer(row const & r) const; bool is_integer(row const & r) const;
typedef std::pair<rational, expr *> coeff_expr; typedef std::pair<rational, expr *> coeff_expr;
bool get_polynomial_info(buffer<coeff_expr> const & p, sbuffer<var_num_occs> & vars); bool get_polynomial_info(buffer<coeff_expr> const & p, sbuffer<var_num_occs> & vars);
expr * p2expr(buffer<coeff_expr> & p); expr_ref p2expr(buffer<coeff_expr> & p);
expr * power(expr * var, unsigned power); expr * power(expr * var, unsigned power);
expr * mk_nary_mul(unsigned sz, expr * const * args, bool is_int); expr * mk_nary_mul(unsigned sz, expr * const * args, bool is_int);
expr * mk_nary_add(unsigned sz, expr * const * args, bool is_int); expr * mk_nary_add(unsigned sz, expr * const * args, bool is_int);
@ -1013,8 +1013,8 @@ namespace smt {
unsigned get_min_degree(buffer<coeff_expr> & p, expr * var); unsigned get_min_degree(buffer<coeff_expr> & p, expr * var);
expr * factor(expr * m, expr * var, unsigned d); expr * factor(expr * m, expr * var, unsigned d);
bool in_monovariate_monomials(buffer<coeff_expr> & p, expr * var, unsigned & i1, rational & c1, unsigned & n1, unsigned & i2, rational & c2, unsigned & n2); bool in_monovariate_monomials(buffer<coeff_expr> & p, expr * var, unsigned & i1, rational & c1, unsigned & n1, unsigned & i2, rational & c2, unsigned & n2);
expr * horner(unsigned depth, buffer<coeff_expr> & p, expr * var); expr_ref horner(unsigned depth, buffer<coeff_expr> & p, expr * var);
expr * cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var); expr_ref cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var);
bool is_cross_nested_consistent(buffer<coeff_expr> & p); bool is_cross_nested_consistent(buffer<coeff_expr> & p);
bool is_cross_nested_consistent(row const & r); bool is_cross_nested_consistent(row const & r);
bool is_cross_nested_consistent(svector<theory_var> const & nl_cluster); bool is_cross_nested_consistent(svector<theory_var> const & nl_cluster);

451
src/smt/theory_arith_nl.h
View file

@ -137,6 +137,7 @@ void theory_arith<Ext>::get_non_linear_cluster(svector<theory_var> & vars) {
tout << "\n";); tout << "\n";);
} }
/** /**
\brief Return the number of variables that \brief Return the number of variables that
do not have bounds associated with it. do not have bounds associated with it.
@ -158,134 +159,49 @@ void theory_arith<Ext>::get_non_linear_cluster(svector<theory_var> & vars) {
So x2*x2 has bound [0, oo). So, there is one variable without bounds x3. So x2*x2 has bound [0, oo). So, there is one variable without bounds x3.
It is the third variable in the monomial, then its idx is 2. It is the third variable in the monomial, then its idx is 2.
*/ */
template<typename Ext> template<typename Ext>
std::pair<unsigned, int> theory_arith<Ext>::analyze_monomial(expr * m) const { typename theory_arith<Ext>::n_var_power_pair theory_arith<Ext>::analyze_monomial(expr * m) const {
SASSERT(is_pure_monomial(m));
expr * var = nullptr; buffer<var_power_pair> vp;
unsigned power = 0; decompose_monomial(m, vp);
unsigned c = 0; unsigned c = 0;
int free_var_idx = -1; var_power_pair q(nullptr, 0);
int idx = 0; for (auto const& p : vp) {
for (expr * arg : *to_app(m)) { if (p.second % 2 == 1 && is_free(p.first)) {
if (m_util.is_numeral(arg)) c++;
continue; q = p;
if (var == nullptr) { if (c > 1)
var = arg; break;
power = 1;
}
else if (arg == var) {
power++;
}
else {
if (power % 2 == 1 && is_free(var)) {
c++;
free_var_idx = idx;
if (c > 1)
return std::make_pair(2, free_var_idx);
}
var = arg;
power = 1;
idx++;
} }
} }
if (power % 2 == 1 && is_free(var)) { return std::make_pair(c, q);
c++;
free_var_idx = idx;
}
return std::make_pair(c, free_var_idx);
} }
/**
\brief Given a monomial c*M, return M
*/
template<typename Ext> template<typename Ext>
expr * theory_arith<Ext>::get_monomial_body(expr * m) const { rational theory_arith<Ext>::decompose_monomial(expr* m, buffer<var_power_pair>& vp) const {
SASSERT(m_util.is_mul(m)); rational coeff(1);
if (to_app(m)->get_num_args() == 2 && m_util.is_numeral(to_app(m)->get_arg(0))) vp.reset();
return to_app(m)->get_arg(1); auto insert = [&](expr* arg) {
return m; rational r;
} if (m_util.is_numeral(arg, r))
coeff *= r;
/** else if (!vp.empty() && vp.back().first == arg)
\brief Given a monomial c*M, return c vp.back().second += 1;
*/ else
template<typename Ext> vp.push_back(var_power_pair(arg, 1));
rational theory_arith<Ext>::get_monomial_coeff(expr * m) const { };
SASSERT(m_util.is_mul(m)); while (m_util.is_mul(m)) {
rational result(1), r; unsigned sz = to_app(m)->get_num_args();
for (expr* arg : *to_app(m)) { for (unsigned i = 0; i + 1 < sz; ++i) {
if (m_util.is_numeral(arg, r)) insert(to_app(m)->get_arg(i));
result *= r;
}
return result;
}
/**
\brief Return the number of distinct variables in the given monomial.
*/
template<typename Ext>
unsigned theory_arith<Ext>::get_num_vars_in_monomial(expr * m) const {
SASSERT(m_util.is_mul(m));
m = get_monomial_body(m);
if (m_util.is_numeral(m))
return 0;
if (m_util.is_mul(m)) {
unsigned num_vars = 0;
expr * var = nullptr;
for (expr * curr : *to_app(m)) {
if (m_util.is_numeral(curr))
continue;
if (var != curr) {
num_vars++;
var = curr;
}
} }
return num_vars; m = to_app(m)->get_arg(sz - 1);
}
else {
return 1;
} }
insert(m);
return coeff;
} }
/**
\brief Return the i-th var of m and its power.
*/
template<typename Ext>
typename theory_arith<Ext>::var_power_pair theory_arith<Ext>::get_var_and_degree(expr * m, unsigned i) const {
SASSERT(m_util.is_mul(m));
SASSERT(i < get_num_vars_in_monomial(m));
m = get_monomial_body(m);
if (m_util.is_mul(m)) {
unsigned curr_idx = 0;
expr * var = nullptr;
unsigned power = 0;
for (expr * arg : *to_app(m)) {
if (m_util.is_numeral(arg)) {
continue;
}
else if (var == nullptr) {
var = arg;
power = 1;
}
else if (var == arg) {
power++;
}
else {
if (curr_idx == i)
return var_power_pair(var, power);
curr_idx++;
var = arg;
power = 1;
}
}
SASSERT(curr_idx == i);
return var_power_pair(var, power);
}
else {
SASSERT(i == 0);
return var_power_pair(m, 1);
}
}
/** /**
\brief Return an interval using the bounds for v. \brief Return an interval using the bounds for v.
@ -367,43 +283,43 @@ template<typename Ext>
interval theory_arith<Ext>::evaluate_as_interval(expr * n) { interval theory_arith<Ext>::evaluate_as_interval(expr * n) {
expr* arg; expr* arg;
rational val; rational val;
TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";); #define TR() TRACE("nl_evaluate", tout << "eval: " << mk_bounded_pp(n, get_manager(), 10) << "\n";\
display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
if (has_var(n)) { if (has_var(n)) {
TRACE("nl_evaluate", tout << "n has a variable associated with it\n";); interval r = mk_interval_for(n);
TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << mk_interval_for(n) << "\n"; TR();
display_var(tout, expr2var(n));); return r;
return mk_interval_for(n);
} }
else if (m_util.is_add(n)) { else if (m_util.is_add(n)) {
TRACE("nl_evaluate", tout << "is add\n";);
interval r(m_dep_manager, rational(0)); interval r(m_dep_manager, rational(0));
for (expr* arg : *to_app(n)) { for (expr* arg : *to_app(n)) {
r += evaluate_as_interval(arg); r += evaluate_as_interval(arg);
} }
TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); TR();
return r; return r;
} }
else if (m_util.is_mul(n)) { else if (m_util.is_mul(n)) {
TRACE("nl_evaluate", tout << "is mul\n";); buffer<var_power_pair> vp;
interval r(m_dep_manager, get_monomial_coeff(n)); rational coeff = decompose_monomial(n, vp);
unsigned num_vars = get_num_vars_in_monomial(n); interval r(m_dep_manager, coeff);
for (unsigned i = 0; i < num_vars; i++) { for (var_power_pair const& p : vp) {
var_power_pair p = get_var_and_degree(n, i);
expr * var = p.first; expr * var = p.first;
unsigned power = p.second; unsigned power = p.second;
interval it = evaluate_as_interval(var); interval it = evaluate_as_interval(var);
it.expt(power); it.expt(power);
r *= it; r *= it;
} }
TRACE("nl_evaluate", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); TR();
return r; return r;
} }
else if (m_util.is_to_real(n, arg)) { else if (m_util.is_to_real(n, arg)) {
return evaluate_as_interval(arg); return evaluate_as_interval(arg);
} }
else if (m_util.is_numeral(n, val)) { else if (m_util.is_numeral(n, val)) {
TRACE("nl_evaluate", tout << "is numeral\n";); interval r = interval(m_dep_manager, val);
return interval(m_dep_manager, val); TR();
return r;
} }
else { else {
TRACE("nl_evaluate", tout << "is unknown\n";); TRACE("nl_evaluate", tout << "is unknown\n";);
@ -414,9 +330,13 @@ interval theory_arith<Ext>::evaluate_as_interval(expr * n) {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::display_monomial(std::ostream & out, expr * n) const { void theory_arith<Ext>::display_monomial(std::ostream & out, expr * n) const {
bool first = true; bool first = true;
unsigned num_vars = get_num_vars_in_monomial(n); buffer<var_power_pair> vp;
for (unsigned i = 0; i < num_vars; i++) { rational coeff = decompose_monomial(n, vp);
var_power_pair p = get_var_and_degree(n, i); if (!coeff.is_one()) {
out << coeff;
first = false;
}
for (auto const& p : vp) {
SASSERT(p.first != 0); SASSERT(p.first != 0);
if (first) first = false; else out << " * "; if (first) first = false; else out << " * ";
out << mk_bounded_pp(p.first, get_manager()) << "^" << p.second; out << mk_bounded_pp(p.first, get_manager()) << "^" << p.second;
@ -519,19 +439,18 @@ bool theory_arith<Ext>::update_bounds_using_interval(expr * n, interval const &
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::propagate_nl_upward(expr * m) { bool theory_arith<Ext>::propagate_nl_upward(expr * m) {
SASSERT(is_pure_monomial(m)); SASSERT(is_pure_monomial(m));
unsigned num_vars = get_num_vars_in_monomial(m);
interval new_bounds(m_dep_manager, rational(1));
// TODO: the following code can be improved it is quadratic on the degree of the monomial.
TRACE("nl_arith_bug", tout << "processing upward:\n" << mk_pp(m, get_manager()) << "\n";); TRACE("nl_arith_bug", tout << "processing upward:\n" << mk_pp(m, get_manager()) << "\n";);
for (unsigned i = 0; i < num_vars; i++) { buffer<var_power_pair> vp;
var_power_pair p = get_var_and_degree(m, i); rational coeff = decompose_monomial(m, vp);
interval new_bounds(m_dep_manager, coeff);
for (var_power_pair const& p : vp) {
expr * var = p.first; expr * var = p.first;
unsigned power = p.second; unsigned power = p.second;
TRACE("nl_arith_bug", tout << "interval before: " << new_bounds << "\n"; TRACE("nl_arith_bug", tout << "interval before: " << new_bounds << "\n";
theory_var v = expr2var(var); theory_var v = expr2var(var);
interval i = mk_interval_for(v); interval i = mk_interval_for(v);
display_var(tout, v); display_var(tout, v);
tout << "interval for var: " << i << "\n" << mk_pp(var, get_manager()) << "\npower: " << power << " " << expt(i, power) << "\n";); tout << "interval for v" << i << " " << mk_pp(var, get_manager()) << "\npower: " << power << " " << expt(i, power) << "\n";);
mul_bound_of(var, power, new_bounds); mul_bound_of(var, power, new_bounds);
TRACE("nl_arith_bug", tout << "interval after: " << new_bounds << "\n";); TRACE("nl_arith_bug", tout << "interval after: " << new_bounds << "\n";);
} }
@ -546,19 +465,19 @@ bool theory_arith<Ext>::propagate_nl_upward(expr * m) {
the method returns without doing anything. the method returns without doing anything.
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::propagate_nl_downward(expr * n, unsigned i) { bool theory_arith<Ext>::propagate_nl_downward(expr * n, var_power_pair const& p) {
SASSERT(is_pure_monomial(n)); SASSERT(is_pure_monomial(n));
SASSERT(i < get_num_vars_in_monomial(n));
var_power_pair p = get_var_and_degree(n, i);
expr * v = p.first; expr * v = p.first;
unsigned power = p.second; unsigned power = p.second;
if (power != 1) if (power != 1)
return false; // TODO: remove, when the n-th root is implemented in interval. return false; // TODO: remove, when the n-th root is implemented in interval.
unsigned num_vars = get_num_vars_in_monomial(n);
interval other_bounds(m_dep_manager, rational(1)); buffer<var_power_pair> vp;
rational coeff = decompose_monomial(n, vp);
interval other_bounds(m_dep_manager, coeff);
// TODO: the following code can be improved it is quadratic on the degree of the monomial. // TODO: the following code can be improved it is quadratic on the degree of the monomial.
for (unsigned i = 0; i < num_vars; i++) { for (var_power_pair const& p : vp) {
var_power_pair p = get_var_and_degree(n, i);
if (p.first == v) if (p.first == v)
continue; continue;
expr * var = p.first; expr * var = p.first;
@ -570,7 +489,6 @@ bool theory_arith<Ext>::propagate_nl_downward(expr * n, unsigned i) {
interval r = mk_interval_for(n); interval r = mk_interval_for(n);
TRACE("nl_arith_bug", tout << "m: " << mk_ismt2_pp(n, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) << TRACE("nl_arith_bug", tout << "m: " << mk_ismt2_pp(n, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
"\npower: " << power << "\n"; "\npower: " << power << "\n";
tout << "num_vars: " << num_vars << "\n";
display_interval(tout << "monomial bounds\n", r); display_interval(tout << "monomial bounds\n", r);
display_interval(tout << "other bounds\n", other_bounds); display_interval(tout << "other bounds\n", other_bounds);
); );
@ -578,22 +496,6 @@ bool theory_arith<Ext>::propagate_nl_downward(expr * n, unsigned i) {
return update_bounds_using_interval(v, r); return update_bounds_using_interval(v, r);
} }
/**
\brief Try to propagate a bound using the given non linear
monomial.
Return true if some bound was propagated.
If i == -1, then use the bound of the variables to propagate a bound for
the monomial m.
If i != -1, then it is the index of the variable that I will compute bounds for.
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_nl_bound(expr * m, int i) {
TRACE("propagate_nl_bound", tout << "propagate using i: " << i << "\n"; display_monomial(tout, m); tout << "\n";);
if (i == -1)
return propagate_nl_upward(m);
else
return propagate_nl_downward(m, i);
}
/** /**
\brief The given monomial and its elements have bounds. \brief The given monomial and its elements have bounds.
@ -604,12 +506,14 @@ template<typename Ext>
bool theory_arith<Ext>::propagate_nl_bounds(expr * m) { bool theory_arith<Ext>::propagate_nl_bounds(expr * m) {
TRACE("non_linear", tout << "propagate several bounds using:\n"; display_monomial(tout, m); tout << "\n";); TRACE("non_linear", tout << "propagate several bounds using:\n"; display_monomial(tout, m); tout << "\n";);
bool result = propagate_nl_upward(m); bool result = propagate_nl_upward(m);
unsigned num_vars = get_num_vars_in_monomial(m); buffer<var_power_pair> vp;
for (unsigned i = 0; i < num_vars; i++) rational coeff = decompose_monomial(m, vp);
if (propagate_nl_downward(m, i)) { for (auto const& p : vp) {
if (propagate_nl_downward(m, p)) {
m_stats.m_nl_bounds++; m_stats.m_nl_bounds++;
result = true; result = true;
} }
}
return result; return result;
} }
@ -627,11 +531,11 @@ bool theory_arith<Ext>::propagate_nl_bounds() {
expr * m = var2expr(v); expr * m = var2expr(v);
if (!ctx.is_relevant(m)) if (!ctx.is_relevant(m))
continue; continue;
std::pair<unsigned, int> p = analyze_monomial(m); auto p = analyze_monomial(m);
TRACE("propagate_nl_bound", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\n" << "p: " << p.first << " " << p.second << "\n";); TRACE("propagate_nl_bound", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\n" << "p: " << p.first << "\n";);
unsigned num_bad_vars = p.first; unsigned num_bad_vars = p.first;
int free_var_idx = p.second; var_power_pair q = p.second;
SASSERT(num_bad_vars != 1 || free_var_idx != -1); SASSERT(num_bad_vars != 1 || q.first != nullptr);
if (num_bad_vars >= 2) if (num_bad_vars >= 2)
continue; continue;
bool is_free_m = is_free(m); bool is_free_m = is_free(m);
@ -644,7 +548,7 @@ bool theory_arith<Ext>::propagate_nl_bounds() {
propagated = true; propagated = true;
} }
else { else {
if (propagate_nl_bound(m, -1)) { if (propagate_nl_upward(m)) {
m_stats.m_nl_bounds++; m_stats.m_nl_bounds++;
propagated = true; propagated = true;
} }
@ -652,7 +556,7 @@ bool theory_arith<Ext>::propagate_nl_bounds() {
} }
else { else {
SASSERT (!is_free_m); SASSERT (!is_free_m);
if (propagate_nl_bound(m, free_var_idx)) { if (propagate_nl_downward(m, q)) {
m_stats.m_nl_bounds++; m_stats.m_nl_bounds++;
propagated = true; propagated = true;
} }
@ -709,16 +613,13 @@ template<typename Ext>
bool theory_arith<Ext>::check_monomial_assignments() { bool theory_arith<Ext>::check_monomial_assignments() {
bool computed_epsilon = false; bool computed_epsilon = false;
context & ctx = get_context(); context & ctx = get_context();
svector<theory_var>::const_iterator it = m_nl_monomials.begin(); for (theory_var v : m_nl_monomials) {
svector<theory_var>::const_iterator end = m_nl_monomials.end(); TRACE("non_linear", tout << "v" << v << " is relevant: " << ctx.is_relevant(get_enode(v)) << "\n";
for (; it != end; ++it) { tout << "check_monomial_assignments result: " << check_monomial_assignment(v, computed_epsilon) << "\n";
TRACE("non_linear", tout << "v" << *it << " is relevant: " << ctx.is_relevant(get_enode(*it)) << "\n";
tout << "check_monomial_assignments result: " << check_monomial_assignment(*it, computed_epsilon) << "\n";
tout << "computed_epsilon: " << computed_epsilon << "\n";); tout << "computed_epsilon: " << computed_epsilon << "\n";);
if (ctx.is_relevant(get_enode(*it)) && !check_monomial_assignment(*it, computed_epsilon)) { if (ctx.is_relevant(get_enode(v)) && !check_monomial_assignment(v, computed_epsilon)) {
TRACE("non_linear_failed", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(*it), get_manager()) << "\n"; TRACE("non_linear_failed", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(v), get_manager()) << "\n";
display_var(tout, *it);); display_var(tout, v););
return false; return false;
} }
} }
@ -752,8 +653,7 @@ theory_var theory_arith<Ext>::find_nl_var_for_branching() {
if (!r) { if (!r) {
expr * m = get_enode(v)->get_owner(); expr * m = get_enode(v)->get_owner();
SASSERT(is_pure_monomial(m)); SASSERT(is_pure_monomial(m));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (expr * arg : *to_app(m)) {
expr * arg = to_app(m)->get_arg(i);
theory_var curr = ctx.get_enode(arg)->get_th_var(get_id()); theory_var curr = ctx.get_enode(arg)->get_th_var(get_id());
TRACE("nl_branching", tout << "target: v" << target << ", curr: v" << curr << "\n";); TRACE("nl_branching", tout << "target: v" << target << ", curr: v" << curr << "\n";);
if (!is_fixed(curr) && is_int(curr)) { if (!is_fixed(curr) && is_int(curr)) {
@ -1195,14 +1095,13 @@ bool theory_arith<Ext>::is_integer(row const & r) const {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::display_coeff_exprs(std::ostream & out, buffer<coeff_expr> const & p) const { void theory_arith<Ext>::display_coeff_exprs(std::ostream & out, buffer<coeff_expr> const & p) const {
typename buffer<coeff_expr>::const_iterator it = p.begin(); bool first = true;
typename buffer<coeff_expr>::const_iterator end = p.end(); for (coeff_expr const& ce : p) {
for (bool first = true; it != end; ++it) {
if (first) if (first)
first = false; first = false;
else else
out << "+\n"; out << "+\n";
out << it->first << " * " << mk_pp(it->second, get_manager()) << "\n"; out << ce.first << " * " << mk_pp(ce.second, get_manager()) << "\n";
} }
} }
@ -1234,9 +1133,9 @@ bool theory_arith<Ext>::get_polynomial_info(buffer<coeff_expr> const & p, sbuffe
ADD_OCC(m); ADD_OCC(m);
} }
else { else {
unsigned num_vars = get_num_vars_in_monomial(m); buffer<var_power_pair> vp;
for (unsigned i = 0; i < num_vars; i++) { decompose_monomial(m, vp);
var_power_pair p = get_var_and_degree(m, i); for (auto const& p : vp) {
ADD_OCC(p.first); ADD_OCC(p.first);
} }
} }
@ -1254,7 +1153,7 @@ bool theory_arith<Ext>::get_polynomial_info(buffer<coeff_expr> const & p, sbuffe
\brief Convert p into an expression. \brief Convert p into an expression.
*/ */
template<typename Ext> template<typename Ext>
expr * theory_arith<Ext>::p2expr(buffer<coeff_expr> & p) { expr_ref theory_arith<Ext>::p2expr(buffer<coeff_expr> & p) {
SASSERT(!p.empty()); SASSERT(!p.empty());
TRACE("p2expr_bug", display_coeff_exprs(tout, p);); TRACE("p2expr_bug", display_coeff_exprs(tout, p););
ptr_buffer<expr> args; ptr_buffer<expr> args;
@ -1276,7 +1175,7 @@ expr * theory_arith<Ext>::p2expr(buffer<coeff_expr> & p) {
} }
} }
SASSERT(!args.empty()); SASSERT(!args.empty());
expr * r = mk_nary_add(args.size(), args.c_ptr()); expr_ref r(mk_nary_add(args.size(), args.c_ptr()), get_manager());
m_nl_new_exprs.push_back(r); m_nl_new_exprs.push_back(r);
return r; return r;
} }
@ -1303,40 +1202,41 @@ template<typename Ext>
bool theory_arith<Ext>::in_monovariate_monomials(buffer<coeff_expr> & p, expr * var, bool theory_arith<Ext>::in_monovariate_monomials(buffer<coeff_expr> & p, expr * var,
unsigned & i1, rational & c1, unsigned & n1, unsigned & i2, rational & c2, unsigned & n2) { unsigned & i1, rational & c1, unsigned & n1, unsigned & i2, rational & c2, unsigned & n2) {
int idx = 0; int idx = 0;
#define SET_RESULT(POWER) { \
if (idx == 0) { \
c1 = it->first; \
n1 = POWER; \
idx = 1; \
i1 = i; \
} \
else if (idx == 1) { \
c2 = it->first; \
n2 = POWER; \
idx = 2; \
i2 = i; \
} \
else \
return false; \
}
typename buffer<coeff_expr>::const_iterator it = p.begin(); auto set_result = [&](unsigned i, unsigned power, coeff_expr const& ce) {
typename buffer<coeff_expr>::const_iterator end = p.end(); if (idx == 0) {
for (unsigned i = 0; it != end; ++it, ++i) { c1 = ce.first;
expr * m = it->second; n1 = power;
idx = 1;
i1 = i;
}
else if (idx == 1) {
c2 = ce.first;
n2 = power;
idx = 2;
i2 = i;
}
else {
idx = 3;
}
};
for (unsigned i = 0; i < p.size() && idx != 3; ++i) {
auto const& ce = p[i];
expr * m = ce.second;
if (is_pure_monomial(m)) { if (is_pure_monomial(m)) {
unsigned num_vars = get_num_vars_in_monomial(m); buffer<var_power_pair> vp;
for (unsigned j = 0; j < num_vars; j++) { decompose_monomial(m, vp);
var_power_pair p = get_var_and_degree(m, j); for (auto const& p : vp) {
if (p.first == var) { if (p.first == var) {
if (num_vars > 1) if (vp.size() > 1)
return false; return false;
SET_RESULT(p.second); set_result(i, p.second, ce); }
}
} }
} }
else if (m == var) { else if (m == var) {
SET_RESULT(1); set_result(i, 1, ce);
} }
} }
if (idx != 2) if (idx != 2)
@ -1344,6 +1244,7 @@ bool theory_arith<Ext>::in_monovariate_monomials(buffer<coeff_expr> & p, expr *
return true; return true;
} }
/** /**
\brief Display a nested form expression \brief Display a nested form expression
*/ */
@ -1362,16 +1263,15 @@ void theory_arith<Ext>::display_nested_form(std::ostream & out, expr * p) {
out << ")"; out << ")";
} }
else if (m_util.is_mul(p)) { else if (m_util.is_mul(p)) {
rational c = get_monomial_coeff(p); buffer<var_power_pair> vp;
rational c = decompose_monomial(p, vp);
bool first = true; bool first = true;
if (!c.is_one()) { if (!c.is_one()) {
out << c; out << c;
first = false; first = false;
} }
unsigned num_vars = get_num_vars_in_monomial(p); for (auto const& pair : vp) {
for (unsigned i = 0; i < num_vars; i++) {
if (first) first = false; else out << "*"; if (first) first = false; else out << "*";
var_power_pair pair = get_var_and_degree(p, i);
expr * var = pair.first; expr * var = pair.first;
unsigned power = pair.second; unsigned power = pair.second;
display_nested_form(out, var); display_nested_form(out, var);
@ -1396,9 +1296,9 @@ unsigned theory_arith<Ext>::get_degree_of(expr * m, expr * var) {
if (m == var) if (m == var)
return 1; return 1;
if (is_pure_monomial(m)) { if (is_pure_monomial(m)) {
unsigned num_vars = get_num_vars_in_monomial(m); buffer<var_power_pair> vp;
for (unsigned i = 0; i < num_vars; i++) { decompose_monomial(m, vp);
var_power_pair p = get_var_and_degree(m, i); for (auto const& p : vp) {
if (p.first == var) if (p.first == var)
return p.second; return p.second;
} }
@ -1415,10 +1315,8 @@ unsigned theory_arith<Ext>::get_min_degree(buffer<coeff_expr> & p, expr * var) {
SASSERT(var != 0); SASSERT(var != 0);
// get monomial where the degree of var is min. // get monomial where the degree of var is min.
unsigned d = UINT_MAX; // min. degree of var unsigned d = UINT_MAX; // min. degree of var
buffer<coeff_expr>::const_iterator it = p.begin(); for (coeff_expr const& ce : p) {
buffer<coeff_expr>::const_iterator end = p.end(); expr * m = ce.second;
for (; it != end; ++it) {
expr * m = it->second;
d = std::min(d, get_degree_of(m, var)); d = std::min(d, get_degree_of(m, var));
if (d == 0) if (d == 0)
return d; return d;
@ -1467,7 +1365,7 @@ expr * theory_arith<Ext>::factor(expr * m, expr * var, unsigned d) {
\brief Return the horner extension of p with respect to var. \brief Return the horner extension of p with respect to var.
*/ */
template<typename Ext> template<typename Ext>
expr * theory_arith<Ext>::horner(unsigned depth, buffer<coeff_expr> & p, expr * var) { expr_ref theory_arith<Ext>::horner(unsigned depth, buffer<coeff_expr> & p, expr * var) {
SASSERT(!p.empty()); SASSERT(!p.empty());
SASSERT(var != 0); SASSERT(var != 0);
unsigned d = get_min_degree(p, var); unsigned d = get_min_degree(p, var);
@ -1488,14 +1386,14 @@ expr * theory_arith<Ext>::horner(unsigned depth, buffer<coeff_expr> & p, expr *
r.push_back(coeff_expr(kv.first, f)); r.push_back(coeff_expr(kv.first, f));
} }
} }
expr * s = cross_nested(depth + 1, e, nullptr); expr_ref s = cross_nested(depth + 1, e, nullptr);
if (!r.empty()) { if (!r.empty()) {
expr * q = horner(depth + 1, r, var); expr_ref q = horner(depth + 1, r, var);
// TODO: improve here // TODO: improve here
s = m_util.mk_add(q, s); s = m_util.mk_add(q, s);
} }
expr * result = s; expr_ref result = s;
if (d != 0) { if (d != 0) {
expr * xd = power(var, d); expr * xd = power(var, d);
result = m_util.mk_mul(xd, s); result = m_util.mk_mul(xd, s);
@ -1504,6 +1402,7 @@ expr * theory_arith<Ext>::horner(unsigned depth, buffer<coeff_expr> & p, expr *
return result; return result;
} }
/** /**
\brief Convert the polynomial p into an equivalent cross nested \brief Convert the polynomial p into an equivalent cross nested
expression. The idea is to obtain an expression e where expression. The idea is to obtain an expression e where
@ -1513,7 +1412,7 @@ expr * theory_arith<Ext>::horner(unsigned depth, buffer<coeff_expr> & p, expr *
If var != 0, then it is used for performing the horner extension If var != 0, then it is used for performing the horner extension
*/ */
template<typename Ext> template<typename Ext>
expr * theory_arith<Ext>::cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var) { expr_ref theory_arith<Ext>::cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var) {
TRACE("non_linear", tout << "p.size: " << p.size() << "\n";); TRACE("non_linear", tout << "p.size: " << p.size() << "\n";);
if (var == nullptr) { if (var == nullptr) {
sbuffer<var_num_occs> varinfo; sbuffer<var_num_occs> varinfo;
@ -1587,12 +1486,12 @@ template<typename Ext>
rest.push_back(p[i]); rest.push_back(p[i]);
} }
if (rest.empty()) if (rest.empty())
return new_expr; return expr_ref(new_expr, get_manager());
TRACE("non_linear", tout << "rest size: " << rest.size() << ", i1: " << i1 << ", i2: " << i2 << "\n";); TRACE("non_linear", tout << "rest size: " << rest.size() << ", i1: " << i1 << ", i2: " << i2 << "\n";);
expr * h = cross_nested(depth + 1, rest, nullptr); expr_ref h = cross_nested(depth + 1, rest, nullptr);
expr * r = m_util.mk_add(new_expr, h); expr * r = m_util.mk_add(new_expr, h);
m_nl_new_exprs.push_back(r); m_nl_new_exprs.push_back(r);
return r; return expr_ref(r, get_manager());
} }
} }
} }
@ -1618,7 +1517,7 @@ bool theory_arith<Ext>::is_cross_nested_consistent(buffer<coeff_expr> & p) {
for (auto const& kv : varinfo) { for (auto const& kv : varinfo) {
m_nl_new_exprs.reset(); m_nl_new_exprs.reset();
expr * var = kv.first; expr * var = kv.first;
expr * cn = cross_nested(0, p, var); expr_ref cn = cross_nested(0, p, var);
// Remark: cn may not be well-sorted because, since a row may contain mixed integer/real monomials. // Remark: cn may not be well-sorted because, since a row may contain mixed integer/real monomials.
// This is not really a problem, since evaluate_as_interval will work even if cn is not well-sorted. // This is not really a problem, since evaluate_as_interval will work even if cn is not well-sorted.
if (!cn) if (!cn)
@ -1725,7 +1624,7 @@ bool theory_arith<Ext>::is_cross_nested_consistent(svector<theory_var> const & n
} }
return true; return true;
} }
#define FIXED 0 #define FIXED 0
#define QUOTED_FIXED 1 #define QUOTED_FIXED 1
#define BOUNDED 2 #define BOUNDED 2
@ -1765,6 +1664,7 @@ void theory_arith<Ext>::init_grobner_var_order(svector<theory_var> const & nl_cl
} }
} }
/** /**
\brief Create a new monomial using the given coeff and m. Fixed \brief Create a new monomial using the given coeff and m. Fixed
variables in m are substituted by their values. The arg dep is variables in m are substituted by their values. The arg dep is
@ -1779,43 +1679,33 @@ grobner::monomial * theory_arith<Ext>::mk_gb_monomial(rational const & _coeff, e
ptr_buffer<expr> vars; ptr_buffer<expr> vars;
rational coeff = _coeff; rational coeff = _coeff;
rational r; rational r;
#undef PROC_VAR auto proc_var = [&](expr* v) {
#define PROC_VAR(VAR) { \ if (m_util.is_numeral(v, r)) {
if (m_util.is_numeral(VAR, r)) { \ coeff *= r;
coeff *= r; \ return;
} \ }
else { \ theory_var _var = expr2var(v);
theory_var _var = expr2var(VAR); \ if (is_fixed(_var)) {
if (is_fixed(_var)) { \ if (!already_found.contains(_var)) {
if (!already_found.contains(_var)) { \ already_found.insert(_var);
already_found.insert(_var); \ dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lower(_var)), m_dep_manager.mk_leaf(upper(_var))));
dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lower(_var)), m_dep_manager.mk_leaf(upper(_var)))); \ }
} \ coeff *= lower_bound(_var).get_rational().to_rational();
coeff *= lower_bound(_var).get_rational().to_rational(); \ }
} \ else {
else { \ vars.push_back(v);
vars.push_back(VAR); \ }
} \ };
} \
}
if (m_util.is_mul(m)) { while (m_util.is_mul(m)) {
coeff *= get_monomial_coeff(m); unsigned sz = to_app(m)->get_num_args();
m = get_monomial_body(m); for (unsigned i = 0; i + 1 < sz; ++i) {
if (m_util.is_mul(m)) { proc_var(to_app(m)->get_arg(i));
if (!is_pure_monomial(m))
return nullptr;
for (expr* arg : *to_app(m)) {
PROC_VAR(arg);
}
}
else {
PROC_VAR(m);
} }
m = to_app(m)->get_arg(sz-1);
} }
else { proc_var(m);
PROC_VAR(m);
}
if (!coeff.is_zero()) if (!coeff.is_zero())
return gb.mk_monomial(coeff, vars.size(), vars.c_ptr()); return gb.mk_monomial(coeff, vars.size(), vars.c_ptr());
else else
@ -2311,7 +2201,7 @@ bool theory_arith<Ext>::scan_for_linear(ptr_vector<grobner::equation>& eqs, grob
} }
return result; return result;
} }
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::compute_basis_loop(grobner & gb) { bool theory_arith<Ext>::compute_basis_loop(grobner & gb) {
@ -2486,10 +2376,11 @@ final_check_status theory_arith<Ext>::process_non_linear() {
} }
TRACE("non_linear", display(tout);); TRACE("non_linear", display(tout););
return FC_GIVEUP; return FC_GIVEUP;
} }
}; };