mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-18 17:15:43 +01:00
parent 948a1e600e
commit 9fef51553c
1 changed files with 195 additions and 195 deletions
Download patch file Download diff file Expand all files Collapse all files

390
src/smt/theory_arith_nl.h
View file

@ -23,9 +23,9 @@ Revision History:
namespace smt { namespace smt {
template<typename Ext> template<typename Ext>
expr * theory_arith<Ext>::mk_nary_mul(unsigned sz, expr * const * args, bool is_int) { expr * theory_arith<Ext>::mk_nary_mul(unsigned sz, expr * const * args, bool is_int) {
if (sz == 0) if (sz == 0)
return m_util.mk_numeral(rational(1), is_int); return m_util.mk_numeral(rational(1), is_int);
if (sz == 1) if (sz == 1)
return args[0]; return args[0];
@ -36,21 +36,21 @@ namespace smt {
return m_util.mk_mul(sz, args); return m_util.mk_mul(sz, args);
} }
template<typename Ext> template<typename Ext>
expr * theory_arith<Ext>::mk_nary_add(unsigned sz, expr * const * args, bool is_int) { expr * theory_arith<Ext>::mk_nary_add(unsigned sz, expr * const * args, bool is_int) {
if (sz == 0) if (sz == 0)
return m_util.mk_numeral(rational(0), is_int); return m_util.mk_numeral(rational(0), is_int);
if (sz == 1) if (sz == 1)
return args[0]; return args[0];
return m_util.mk_add(sz, args); return m_util.mk_add(sz, args);
} }
template<typename Ext> template<typename Ext>
expr * theory_arith<Ext>::mk_nary_add(unsigned sz, expr * const * args) { expr * theory_arith<Ext>::mk_nary_add(unsigned sz, expr * const * args) {
SASSERT(sz != 0); SASSERT(sz != 0);
return mk_nary_add(sz, args, false); return mk_nary_add(sz, args, false);
} }
/** /**
\brief Insert v into vars and already_found if v is not already in already_found. \brief Insert v into vars and already_found if v is not already in already_found.
*/ */
@ -92,21 +92,21 @@ namespace smt {
theory_var s = r.get_base_var(); theory_var s = r.get_base_var();
// ignore quasi base vars... actually they should not be used if the problem is non linear... // ignore quasi base vars... actually they should not be used if the problem is non linear...
if (is_quasi_base(s)) if (is_quasi_base(s))
continue; continue;
// If s is a base variable different from v and it is free, then this row can be ignored. // If s is a base variable different from v and it is free, then this row can be ignored.
// It doesn't need to be part of the non linear cluster. For all purposes, this variable // It doesn't need to be part of the non linear cluster. For all purposes, this variable
// was eliminated by substitution. // was eliminated by substitution.
if (is_free(s) && s != v) if (is_free(s) && s != v)
continue; continue;
typename vector<row_entry>::const_iterator it2 = r.begin_entries(); typename vector<row_entry>::const_iterator it2 = r.begin_entries();
typename vector<row_entry>::const_iterator end2 = r.end_entries(); typename vector<row_entry>::const_iterator end2 = r.end_entries();
for (; it2 != end2; ++it2) { for (; it2 != end2; ++it2) {
if (!it2->is_dead() && !is_fixed(it2->m_var)) if (!it2->is_dead() && !is_fixed(it2->m_var))
mark_var(it2->m_var, vars, already_found); mark_var(it2->m_var, vars, already_found);
} }
} }
} }
/** /**
\brief Store in vars the variables that are in the non linear cluster of constraints, \brief Store in vars the variables that are in the non linear cluster of constraints,
and are not satisfied by the current assignment. and are not satisfied by the current assignment.
@ -123,7 +123,7 @@ namespace smt {
for (; it != end; ++it) { for (; it != end; ++it) {
theory_var v = *it; theory_var v = *it;
expr * n = var2expr(v); expr * n = var2expr(v);
if (ctx.is_relevant(n)) if (ctx.is_relevant(n))
mark_var(v, vars, already_found); mark_var(v, vars, already_found);
} }
for (unsigned idx = 0; idx < vars.size(); idx++) { for (unsigned idx = 0; idx < vars.size(); idx++) {
@ -134,7 +134,7 @@ namespace smt {
svector<theory_var>::const_iterator it = vars.begin(); svector<theory_var>::const_iterator it = vars.begin();
svector<theory_var>::const_iterator end = vars.end(); svector<theory_var>::const_iterator end = vars.end();
for (; it != end; ++it) tout << "v" << *it << " "; for (; it != end; ++it) tout << "v" << *it << " ";
tout << "\n";); tout << "\n";);
} }
/** /**
@ -148,7 +148,7 @@ namespace smt {
\remark if a variables has an even number of occurrences, then \remark if a variables has an even number of occurrences, then
I consider that it has a bound associated with it. I consider that it has a bound associated with it.
Examples: Examples:
1) Assume x1, x4 have bounds: 1) Assume x1, x4 have bounds:
analyze_monomial(x1 * x2 * x2 * x3 * x3 * x3 * x4) analyze_monomial(x1 * x2 * x2 * x3 * x3 * x3 * x4)
@ -168,24 +168,24 @@ namespace smt {
int idx = 0; int idx = 0;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
if (var == 0) { if (var == 0) {
var = arg; var = arg;
power = 1; power = 1;
} }
else if (arg == var) { else if (arg == var) {
power++; power++;
} }
else { else {
if (power % 2 == 1 && is_free(var)) { if (power % 2 == 1 && is_free(var)) {
c++; c++;
free_var_idx = idx; free_var_idx = idx;
if (c > 1) if (c > 1)
return std::make_pair(2, free_var_idx); return std::make_pair(2, free_var_idx);
} }
var = arg; var = arg;
power = 1; power = 1;
idx++; idx++;
} }
} }
if (power % 2 == 1 && is_free(var)) { if (power % 2 == 1 && is_free(var)) {
c++; c++;
@ -257,17 +257,17 @@ namespace smt {
unsigned j; unsigned j;
for (j = 0; j < to_app(m)->get_num_args(); j++) { for (j = 0; j < to_app(m)->get_num_args(); j++) {
expr * arg = to_app(m)->get_arg(j); expr * arg = to_app(m)->get_arg(j);
if (var == 0) { if (var == 0) {
var = arg; var = arg;
power = 1; power = 1;
} }
else if (var == arg) { else if (var == arg) {
power++; power++;
} }
else { else {
if (curr_idx == i) if (curr_idx == i)
return var_power_pair(var, power); return var_power_pair(var, power);
curr_idx++; curr_idx++;
var = arg; var = arg;
power = 1; power = 1;
} }
@ -289,24 +289,24 @@ namespace smt {
bound * l = lower(v); bound * l = lower(v);
bound * u = upper(v); bound * u = upper(v);
if (l && u) { if (l && u) {
return interval(m_dep_manager, return interval(m_dep_manager,
l->get_value().get_rational().to_rational(), l->get_value().get_rational().to_rational(),
!l->get_value().get_infinitesimal().to_rational().is_zero(), !l->get_value().get_infinitesimal().to_rational().is_zero(),
m_dep_manager.mk_leaf(l), m_dep_manager.mk_leaf(l),
u->get_value().get_rational().to_rational(), u->get_value().get_rational().to_rational(),
!u->get_value().get_infinitesimal().to_rational().is_zero(), !u->get_value().get_infinitesimal().to_rational().is_zero(),
m_dep_manager.mk_leaf(u)); m_dep_manager.mk_leaf(u));
} }
else if (l) { else if (l) {
return interval(m_dep_manager, return interval(m_dep_manager,
l->get_value().get_rational().to_rational(), l->get_value().get_rational().to_rational(),
!l->get_value().get_infinitesimal().to_rational().is_zero(), !l->get_value().get_infinitesimal().to_rational().is_zero(),
true, true,
m_dep_manager.mk_leaf(l)); m_dep_manager.mk_leaf(l));
} }
else if (u) { else if (u) {
return interval(m_dep_manager, return interval(m_dep_manager,
u->get_value().get_rational().to_rational(), u->get_value().get_rational().to_rational(),
!u->get_value().get_infinitesimal().to_rational().is_zero(), !u->get_value().get_infinitesimal().to_rational().is_zero(),
false, false,
m_dep_manager.mk_leaf(u)); m_dep_manager.mk_leaf(u));
@ -333,12 +333,12 @@ namespace smt {
void theory_arith<Ext>::mul_bound_of(expr * var, unsigned power, interval & target) { void theory_arith<Ext>::mul_bound_of(expr * var, unsigned power, interval & target) {
theory_var v = expr2var(var); theory_var v = expr2var(var);
interval i = mk_interval_for(v); interval i = mk_interval_for(v);
TRACE("non_linear", TRACE("non_linear",
display_interval(tout << "bound: ",i); tout << i << "\n"; display_interval(tout << "bound: ",i); tout << i << "\n";
tout << mk_pp(var, get_manager()) << "\n"; tout << mk_pp(var, get_manager()) << "\n";
tout << "power " << power << ": " << expt(i, power) << "\n"; tout << "power " << power << ": " << expt(i, power) << "\n";
display_interval(tout << "target before: ", target); tout << "\n";); display_interval(tout << "target before: ", target); tout << "\n";);
i.expt(power); i.expt(power);
target *= i; target *= i;
TRACE("non_linear", display_interval(tout << "target after: ", target); tout << "\n";); TRACE("non_linear", display_interval(tout << "target after: ", target); tout << "\n";);
@ -348,7 +348,7 @@ namespace smt {
\brief Evaluate the given expression using interval arithmetic. \brief Evaluate the given expression using interval arithmetic.
- If a subexpression is internalized, then mk_interval_for is used to - If a subexpression is internalized, then mk_interval_for is used to
compute its interval. compute its interval.
- Only +, *, and numerals are handled. - Only +, *, and numerals are handled.
*/ */
@ -382,7 +382,7 @@ namespace smt {
interval it = evaluate_as_interval(var); interval it = evaluate_as_interval(var);
it.expt(power); it.expt(power);
r *= it; r *= it;
} }
TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
return r; return r;
} }
@ -424,7 +424,7 @@ namespace smt {
ptr_vector<void>::const_iterator end = bounds.end(); ptr_vector<void>::const_iterator end = bounds.end();
for (; it != end; ++it) { for (; it != end; ++it) {
bound * b = static_cast<bound*>(*it); bound * b = static_cast<bound*>(*it);
accumulate_justification(*b, new_bound, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set); accumulate_justification(*b, new_bound, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
} }
} }
@ -476,7 +476,7 @@ namespace smt {
} }
return r; return r;
} }
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::update_bounds_using_interval(expr * n, interval const & i) { bool theory_arith<Ext>::update_bounds_using_interval(expr * n, interval const & i) {
SASSERT(expr2var(n) != null_theory_var); SASSERT(expr2var(n) != null_theory_var);
@ -510,7 +510,7 @@ namespace smt {
} }
/** /**
\brief Propagate a bound to the i-th variable of the given monomial \brief Propagate a bound to the i-th variable of the given monomial
using the bounds of m and other variables in m. using the bounds of m and other variables in m.
\remark We do not support roots in interval... so, if the i-th var has power != 1 \remark We do not support roots in interval... so, if the i-th var has power != 1
@ -523,7 +523,7 @@ namespace smt {
var_power_pair p = get_var_and_degree(m, i); var_power_pair p = get_var_and_degree(m, i);
expr * v = p.first; expr * v = p.first;
unsigned power = p.second; unsigned power = p.second;
TRACE("propagate_nl_downward", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) << TRACE("propagate_nl_downward", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
"\npower: " << power << "\n";); "\npower: " << power << "\n";);
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.
@ -556,7 +556,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::propagate_nl_bound(expr * m, int i) { 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";); TRACE("propagate_nl_bound", tout << "propagate using i: " << i << "\n"; display_monomial(tout, m); tout << "\n";);
if (i == -1) if (i == -1)
return propagate_nl_upward(m); return propagate_nl_upward(m);
else else
return propagate_nl_downward(m, i); return propagate_nl_downward(m, i);
@ -657,13 +657,13 @@ namespace smt {
rational val(1); rational val(1);
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
theory_var curr = expr2var(arg); theory_var curr = expr2var(arg);
SASSERT(curr != null_theory_var); SASSERT(curr != null_theory_var);
val *= get_value(curr, computed_epsilon); val *= get_value(curr, computed_epsilon);
} }
return get_value(v, computed_epsilon) == val; return get_value(v, computed_epsilon) == val;
} }
/** /**
\brief Return true if for every monomial x_1 * ... * x_n, \brief Return true if for every monomial x_1 * ... * x_n,
@ -691,11 +691,11 @@ namespace smt {
/** /**
\brief Try to find an integer variable for performing branching \brief Try to find an integer variable for performing branching
in the non linear cluster. in the non linear cluster.
The idea is select a variable in a monomial with an invalid The idea is select a variable in a monomial with an invalid
assignment. I give preference to variables with small ranges. assignment. I give preference to variables with small ranges.
If no variable is bounded, then select a random one. If no variable is bounded, then select a random one.
Free variables are not considered. Free variables are not considered.
*/ */
template<typename Ext> template<typename Ext>
@ -705,44 +705,44 @@ namespace smt {
theory_var target = null_theory_var; theory_var target = null_theory_var;
bool bounded = false; bool bounded = false;
unsigned n = 0; unsigned n = 0;
numeral range; numeral range;
svector<theory_var>::const_iterator it = m_nl_monomials.begin(); svector<theory_var>::const_iterator it = m_nl_monomials.begin();
svector<theory_var>::const_iterator end = m_nl_monomials.end(); svector<theory_var>::const_iterator end = m_nl_monomials.end();
for (; it != end; ++it) { for (; it != end; ++it) {
theory_var v = *it; theory_var v = *it;
if (is_real(v)) if (is_real(v))
continue; continue;
bool computed_epsilon = false; bool computed_epsilon = false;
bool r = check_monomial_assignment(v, computed_epsilon); bool r = check_monomial_assignment(v, computed_epsilon);
SASSERT(!computed_epsilon); // integer variables do not use epsilon SASSERT(!computed_epsilon); // integer variables do not use epsilon
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 (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); 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)) {
if (is_bounded(curr)) { if (is_bounded(curr)) {
numeral new_range; numeral new_range;
new_range = upper_bound(curr).get_rational(); new_range = upper_bound(curr).get_rational();
new_range -= lower_bound(curr).get_rational(); new_range -= lower_bound(curr).get_rational();
if (!bounded || new_range < range) { if (!bounded || new_range < range) {
target = curr; target = curr;
range = new_range; range = new_range;
bounded = true; bounded = true;
} }
} }
else if (!bounded) { else if (!bounded) {
n++; n++;
TRACE("nl_branching", tout << "n: " << n << "\n";); TRACE("nl_branching", tout << "n: " << n << "\n";);
if (m_random()%n == 0) if (m_random()%n == 0)
target = curr; target = curr;
SASSERT(target != null_theory_var); SASSERT(target != null_theory_var);
} }
SASSERT(target != null_theory_var); SASSERT(target != null_theory_var);
} }
TRACE("nl_branching", tout << "after target: v" << target << "\n";); TRACE("nl_branching", tout << "after target: v" << target << "\n";);
} }
} }
} }
@ -762,7 +762,7 @@ namespace smt {
m_stats.m_nl_branching++; m_stats.m_nl_branching++;
SASSERT(is_int(v)); SASSERT(is_int(v));
expr * bound = 0; expr * bound = 0;
if (lower(v)) if (lower(v))
bound = m_util.mk_le(var2expr(v), m_util.mk_numeral(lower_bound(v).get_rational().to_rational(), true)); bound = m_util.mk_le(var2expr(v), m_util.mk_numeral(lower_bound(v).get_rational().to_rational(), true));
else if (upper(v)) else if (upper(v))
bound = m_util.mk_ge(var2expr(v), m_util.mk_numeral(upper_bound(v).get_rational().to_rational(), true)); bound = m_util.mk_ge(var2expr(v), m_util.mk_numeral(upper_bound(v).get_rational().to_rational(), true));
@ -787,14 +787,14 @@ namespace smt {
unsigned num_nl_vars = 0; unsigned num_nl_vars = 0;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg); theory_var _var = expr2var(arg);
if (!is_fixed(_var)) { if (!is_fixed(_var)) {
num_nl_vars++; num_nl_vars++;
} }
else { else {
if (lower_bound(_var).is_zero()) if (lower_bound(_var).is_zero())
return true; return true;
} }
} }
return num_nl_vars <= 1; return num_nl_vars <= 1;
} }
@ -809,9 +809,9 @@ namespace smt {
numeral r(1); numeral r(1);
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg); theory_var _var = expr2var(arg);
if (is_fixed(_var)) if (is_fixed(_var))
r *= lower_bound(_var).get_rational(); r *= lower_bound(_var).get_rational();
} }
return r; return r;
} }
@ -825,9 +825,9 @@ namespace smt {
SASSERT(is_pure_monomial(m)); SASSERT(is_pure_monomial(m));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg); theory_var _var = expr2var(arg);
if (!is_fixed(_var)) if (!is_fixed(_var))
return arg; return arg;
} }
return 0; return 0;
} }
@ -886,7 +886,7 @@ namespace smt {
} }
else { else {
// One of the x_i variables is zero, // One of the x_i variables is zero,
// or all of them are assigned. // or all of them are assigned.
// Assert the equality // Assert the equality
// (= (* x_1 ... x_n) k) // (= (* x_1 ... x_n) k)
@ -908,45 +908,45 @@ namespace smt {
SASSERT(is_pure_monomial(m)); SASSERT(is_pure_monomial(m));
bool found_zero = false; bool found_zero = false;
for (unsigned i = 0; !found_zero && i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; !found_zero && i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg); theory_var _var = expr2var(arg);
if (is_fixed(_var)) { if (is_fixed(_var)) {
bound * l = lower(_var); bound * l = lower(_var);
bound * u = upper(_var); bound * u = upper(_var);
if (l->get_value().is_zero()) { if (l->get_value().is_zero()) {
/* if zero was found, then it is the explanation */ /* if zero was found, then it is the explanation */
SASSERT(k.is_zero()); SASSERT(k.is_zero());
found_zero = true; found_zero = true;
m_tmp_lit_set.reset(); m_tmp_lit_set.reset();
m_tmp_eq_set.reset(); m_tmp_eq_set.reset();
new_lower->m_lits.reset(); new_lower->m_lits.reset();
new_lower->m_eqs.reset(); new_lower->m_eqs.reset();
} }
accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set); accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear", TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) { for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]); ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " "; tout << " ";
} }
tout << "\n";); tout << "\n";);
accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set); accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear", TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) { for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]); ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " "; tout << " ";
} }
tout << "\n";); tout << "\n";);
} }
} }
new_upper->m_lits.append(new_lower->m_lits); new_upper->m_lits.append(new_lower->m_lits);
new_upper->m_eqs.append(new_lower->m_eqs); new_upper->m_eqs.append(new_lower->m_eqs);
TRACE("non_linear", TRACE("non_linear",
tout << "lower: " << new_lower << " upper: " << new_upper << "\n"; tout << "lower: " << new_lower << " upper: " << new_upper << "\n";
for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) { for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_upper->m_lits[j]); ctx.display_detailed_literal(tout, new_upper->m_lits[j]);
@ -979,9 +979,9 @@ namespace smt {
/* /*
Interval arithmetic does not satisfy distributivity. Interval arithmetic does not satisfy distributivity.
Actually, it satisfies the sub-distributivity property: Actually, it satisfies the sub-distributivity property:
x*(y + z) \subseteq x*y + x*z x*(y + z) \subseteq x*y + x*z
The sub-distributivity property only holds if condensation The sub-distributivity property only holds if condensation
is not used. For example: is not used. For example:
@ -995,11 +995,11 @@ namespace smt {
x*(x^3+1) = [-7, 14] x*(x^3+1) = [-7, 14]
x^4 + x = [-2, 17] x^4 + x = [-2, 17]
This weakness of AI is known as the "dependency problem", This weakness of AI is known as the "dependency problem",
which comes from the decorrelation of the multiple occurrences which comes from the decorrelation of the multiple occurrences
of one variable during interval evaluation. of one variable during interval evaluation.
Given a polynomial: Given a polynomial:
p(x) = a_0 + a_1 * x + ... + a_n * x^n p(x) = a_0 + a_1 * x + ... + a_n * x^n
The horner extension is: The horner extension is:
@ -1009,13 +1009,13 @@ namespace smt {
h_p(x) = x(2 + x^3(1 + x)) h_p(x) = x(2 + x^3(1 + x))
The horner extension evaluates tighter intervals when The horner extension evaluates tighter intervals when
condensation is not used. condensation is not used.
Remark: there is no guarantee that horner extension will Remark: there is no guarantee that horner extension will
provide a tighter interval than a sum of monomials when provide a tighter interval than a sum of monomials when
condensation is used. condensation is used.
For multivariate polynomials nested (or cross nested) forms For multivariate polynomials nested (or cross nested) forms
are used. The idea is to select one variable, and pretend the are used. The idea is to select one variable, and pretend the
other are parameters. The horner form is computed for the selected other are parameters. The horner form is computed for the selected
variable, and the computation continues for the polynomials on the variable, and the computation continues for the polynomials on the
@ -1027,13 +1027,13 @@ namespace smt {
p(x) = a*x^n + b*x^{n+m} for n >= m p(x) = a*x^n + b*x^{n+m} for n >= m
is equivalent to is equivalent to
b*x^{n-m}*[(x^{m} + a/(2b))^2 - (a/2b)^2] b*x^{n-m}*[(x^{m} + a/(2b))^2 - (a/2b)^2]
This polynomial provides tight bound when n and m have the same parity and: This polynomial provides tight bound when n and m have the same parity and:
1) a*b > 0 and (lower(x) >= 0 or upper(x)^m <= -a/b) 1) a*b > 0 and (lower(x) >= 0 or upper(x)^m <= -a/b)
2) a*b < 0 and (upper(x) <= 0 or lower(x)^m >= a/b) 2) a*b < 0 and (upper(x) <= 0 or lower(x)^m >= a/b)
This polynomial also provides tight bounds when n = m, This polynomial also provides tight bounds when n = m,
and the polynomial is simplified to, and n and m may have arbitrary parities: and the polynomial is simplified to, and n and m may have arbitrary parities:
@ -1047,7 +1047,7 @@ namespace smt {
If we compute the bounds for x^2 - x we obtain If we compute the bounds for x^2 - x we obtain
(-oo, oo). (-oo, oo).
On the other hand, if we compute the bounds for On the other hand, if we compute the bounds for
(x - 1/2)^2 - 1/4 (x - 1/2)^2 - 1/4
we obtain the bounds (0, oo), and the inconsistency we obtain the bounds (0, oo), and the inconsistency
is detected. is detected.
@ -1055,8 +1055,8 @@ namespace smt {
Remark: In Z3, I condensate multiple occurrences of a variable Remark: In Z3, I condensate multiple occurrences of a variable
when evaluating monomials. So, the interval for a monomial is when evaluating monomials. So, the interval for a monomial is
always tight. always tight.
Remark: M1*(M2 + M3) is more precise than M1 * M2 + M1 * M3, Remark: M1*(M2 + M3) is more precise than M1 * M2 + M1 * M3,
if intersection(Vars(M1), union(Vars(M2), Vars(M3))) = empty-set, if intersection(Vars(M1), union(Vars(M2), Vars(M3))) = empty-set,
Remark: A trivial consequence of Moore's theorem for interval Remark: A trivial consequence of Moore's theorem for interval
@ -1066,7 +1066,7 @@ namespace smt {
/** /**
\brief Check whether the same variable occurs in two different monomials. \brief Check whether the same variable occurs in two different monomials.
\remark Fixed variables are ignored. \remark Fixed variables are ignored.
\remark A trivial consequence of Moore's theorem for interval \remark A trivial consequence of Moore's theorem for interval
@ -1208,7 +1208,7 @@ namespace smt {
UNREACHABLE(); UNREACHABLE();
} }
} }
// Update the number of occurrences in the result vector. // Update the number of occurrences in the result vector.
typename var2num_occs::iterator it2 = m_var2num_occs.begin(); typename var2num_occs::iterator it2 = m_var2num_occs.begin();
typename var2num_occs::iterator end2 = m_var2num_occs.end(); typename var2num_occs::iterator end2 = m_var2num_occs.end();
@ -1263,14 +1263,14 @@ namespace smt {
m_nl_new_exprs.push_back(r); m_nl_new_exprs.push_back(r);
return r; return r;
} }
/** /**
\brief Return true if var only occurs in two monovariate monomials, \brief Return true if var only occurs in two monovariate monomials,
and return its power and coefficients and these monomials. and return its power and coefficients and these monomials.
The arguments i1 and i2 contain the position in p of the two monomials. The arguments i1 and i2 contain the position in p of the two monomials.
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::in_monovariate_monomials(sbuffer<coeff_expr> & p, expr * var, bool theory_arith<Ext>::in_monovariate_monomials(sbuffer<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) { \ #define SET_RESULT(POWER) { \
@ -1289,7 +1289,7 @@ namespace smt {
else \ else \
return false; \ return false; \
} }
typename sbuffer<coeff_expr>::const_iterator it = p.begin(); typename sbuffer<coeff_expr>::const_iterator it = p.begin();
typename sbuffer<coeff_expr>::const_iterator end = p.end(); typename sbuffer<coeff_expr>::const_iterator end = p.end();
for (unsigned i = 0; it != end; ++it, ++i) { for (unsigned i = 0; it != end; ++it, ++i) {
@ -1396,7 +1396,7 @@ namespace smt {
SASSERT(d != UINT_MAX); SASSERT(d != UINT_MAX);
return d; return d;
} }
/** /**
\brief Divide m by var^d. \brief Divide m by var^d.
*/ */
@ -1416,19 +1416,19 @@ namespace smt {
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
if (arg == var) { if (arg == var) {
if (idx < d) if (idx < d)
idx++; idx++;
else else
new_args.push_back(arg); new_args.push_back(arg);
} }
else { else {
new_args.push_back(arg); new_args.push_back(arg);
} }
} }
SASSERT(idx == d); SASSERT(idx == d);
TRACE("factor_bug", tout << "new_args:\n"; for(unsigned i = 0; i < new_args.size(); i++) tout << mk_pp(new_args[i], get_manager()) << "\n";); TRACE("factor_bug", tout << "new_args:\n"; for(unsigned i = 0; i < new_args.size(); i++) tout << mk_pp(new_args[i], get_manager()) << "\n";);
expr * result = mk_nary_mul(new_args.size(), new_args.c_ptr(), m_util.is_int(var)); expr * result = mk_nary_mul(new_args.size(), new_args.c_ptr(), m_util.is_int(var));
m_nl_new_exprs.push_back(result); m_nl_new_exprs.push_back(result);
TRACE("factor", tout << "result: " << mk_pp(result, get_manager()) << "\n";); TRACE("factor", tout << "result: " << mk_pp(result, get_manager()) << "\n";);
return result; return result;
@ -1442,7 +1442,7 @@ namespace smt {
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);
TRACE("horner_bug", tout << "poly:\n"; TRACE("horner_bug", tout << "poly:\n";
for (unsigned i = 0; i < p.size(); i++) { if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager()); } tout << "\n"; for (unsigned i = 0; i < p.size(); i++) { if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager()); } tout << "\n";
tout << "var: " << mk_pp(var, get_manager()) << "\n"; tout << "var: " << mk_pp(var, get_manager()) << "\n";
tout << "min_degree: " << d << "\n";); tout << "min_degree: " << d << "\n";);
@ -1467,7 +1467,7 @@ namespace smt {
// TODO: improve here // TODO: improve here
s = m_util.mk_add(q, s); s = m_util.mk_add(q, s);
} }
expr * result = s; expr * result = s;
if (d != 0) { if (d != 0) {
expr * xd = power(var, d); expr * xd = power(var, d);
@ -1513,9 +1513,9 @@ namespace smt {
unsigned nm = UINT_MAX; unsigned nm = UINT_MAX;
if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) { if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) {
CTRACE("in_monovariate_monomials", n == nm, CTRACE("in_monovariate_monomials", n == nm,
for (unsigned i = 0; i < p.size(); i++) { for (unsigned i = 0; i < p.size(); i++) {
if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager()); if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager());
} }
tout << "\n"; tout << "\n";
tout << "var: " << mk_pp(var, get_manager()) << "\n"; tout << "var: " << mk_pp(var, get_manager()) << "\n";
tout << "i1: " << i1 << "\n"; tout << "i1: " << i1 << "\n";
@ -1556,7 +1556,7 @@ namespace smt {
sbuffer<coeff_expr> rest; sbuffer<coeff_expr> rest;
unsigned sz = p.size(); unsigned sz = p.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
if (i != i1 && i != i2) if (i != i1 && i != i2)
rest.push_back(p[i]); rest.push_back(p[i]);
} }
if (rest.empty()) if (rest.empty())
@ -1620,7 +1620,7 @@ namespace smt {
/** /**
\brief Check whether the polynomial represented by the current row is \brief Check whether the polynomial represented by the current row is
consistent with respect to the known bound when converted into a consistent with respect to the known bound when converted into a
equivalent cross nested form. equivalent cross nested form.
*/ */
template<typename Ext> template<typename Ext>
@ -1630,17 +1630,17 @@ namespace smt {
return true; return true;
TRACE("cross_nested", tout << "problematic...\n";); TRACE("cross_nested", tout << "problematic...\n";);
/* /*
The method is_cross_nested converts rows back to expressions. The method is_cross_nested converts rows back to expressions.
The conversion back to expressions may create sort incorrect expressions. The conversion back to expressions may create sort incorrect expressions.
This is in some sense ok, since these expressions are temporary, but This is in some sense ok, since these expressions are temporary, but
the sort incorrect expressions may generate assertion violations. the sort incorrect expressions may generate assertion violations.
Sort incorrect expressions may be created in the following cases: Sort incorrect expressions may be created in the following cases:
1) mixed real int rows. 1) mixed real int rows.
2) int rows that contain non integer coefficients. 2) int rows that contain non integer coefficients.
3) int rows that when converted to cross nested form use non integer coefficients. 3) int rows that when converted to cross nested form use non integer coefficients.
@ -1654,10 +1654,10 @@ namespace smt {
c) Disable the assertions temporally. This sounds like a big HACK. c) Disable the assertions temporally. This sounds like a big HACK.
d) Use a different data-structure to represent polynomials in cross-nested form. Disadvantage: code duplication, the data-structure d) Use a different data-structure to represent polynomials in cross-nested form. Disadvantage: code duplication, the data-structure
is essentially identical to the ASTs we are using right now. is essentially identical to the ASTs we are using right now.
e) Disable the test when we cannot create a well-sorted expression. e) Disable the test when we cannot create a well-sorted expression.
I'm temporally using this solution. I'm temporally using this solution.
I implemented the following logic: I implemented the following logic:
1) (mixed real int) Disable the test. Most benchmarks do not contain mixed int real variables. 1) (mixed real int) Disable the test. Most benchmarks do not contain mixed int real variables.
2) (int coeffs) I multiply the row by a constant to force it to have only integer coefficients. 2) (int coeffs) I multiply the row by a constant to force it to have only integer coefficients.
@ -1696,7 +1696,7 @@ namespace smt {
svector<theory_var>::const_iterator end = nl_cluster.end(); svector<theory_var>::const_iterator end = nl_cluster.end();
for (; it != end; ++it) { for (; it != end; ++it) {
theory_var v = *it; theory_var v = *it;
if (!is_base(v)) if (!is_base(v))
continue; continue;
m_stats.m_nl_cross_nested++; m_stats.m_nl_cross_nested++;
row const & r = m_rows[get_var_row(v)]; row const & r = m_rows[get_var_row(v)];
@ -1719,8 +1719,8 @@ namespace smt {
/** /**
\brief Initialize variable order for grobner basis computation. \brief Initialize variable order for grobner basis computation.
Make: Make:
"quoted free vars" > "free vars" > "quoted variables with lower or upper bounds" > "quoted free vars" > "free vars" > "quoted variables with lower or upper bounds" >
"variables with lower or upper bounds" > "quoted bounded variables" > "variables with lower or upper bounds" > "quoted bounded variables" >
"bounded variables" > "quoted fixed variables" > "fixed variables" "bounded variables" > "quoted fixed variables" > "fixed variables"
*/ */
template<typename Ext> template<typename Ext>
@ -1801,7 +1801,7 @@ namespace smt {
} }
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
return 0; return 0;
} }
@ -1918,7 +1918,7 @@ namespace smt {
derived_bound b(null_theory_var, inf_numeral(0), B_LOWER); derived_bound b(null_theory_var, inf_numeral(0), B_LOWER);
dependency2new_bound(d, b); dependency2new_bound(d, b);
set_conflict(b, ante, "arith_nl"); set_conflict(b, ante, "arith_nl");
TRACE("non_linear", TRACE("non_linear",
for (unsigned i = 0; i < b.m_lits.size(); ++i) { for (unsigned i = 0; i < b.m_lits.size(); ++i) {
tout << b.m_lits[i] << " "; tout << b.m_lits[i] << " ";
}); });
@ -2027,7 +2027,7 @@ namespace smt {
unsigned num1 = m1_sq->get_degree(); unsigned num1 = m1_sq->get_degree();
unsigned num2 = m2_sq->get_degree(); unsigned num2 = m2_sq->get_degree();
unsigned num12 = m1m2->get_degree(); unsigned num12 = m1m2->get_degree();
if (num1 + num2 != num12 * 2) if (num1 + num2 != num12 * 2)
return false; return false;
unsigned i1, i2, i12; unsigned i1, i2, i12;
i1 = i2 = i12 = 0; i1 = i2 = i12 = 0;
@ -2072,8 +2072,8 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::is_inconsistent2(grobner::equation const * eq, grobner & gb) { bool theory_arith<Ext>::is_inconsistent2(grobner::equation const * eq, grobner & gb) {
// TODO: a possible improvement: create a quotation for (M1 - M2)^2 // TODO: a possible improvement: create a quotation for (M1 - M2)^2
// instead of trying to find it in a specific equation. // instead of trying to find it in a specific equation.
// This approach is more precise, but more expensive // This approach is more precise, but more expensive
// since a new row must be created. // since a new row must be created.
buffer<interval> intervals; buffer<interval> intervals;
@ -2117,7 +2117,7 @@ namespace smt {
continue; continue;
// m1, m2, and m1m2 form a perfect square. // m1, m2, and m1m2 form a perfect square.
// check if [0, oo) provides a better lowerbound than adding the intervals of m1, m2 and m1m2; // check if [0, oo) provides a better lowerbound than adding the intervals of m1, m2 and m1m2;
TRACE("non_linear", tout << "found perfect square (M1-M2)^2:\n"; TRACE("non_linear", tout << "found perfect square (M1-M2)^2:\n";
gb.display_monomial(tout, *m1); tout << "\n"; gb.display_monomial(tout, *m1); tout << "\n";
gb.display_monomial(tout, *m2); tout << "\n"; gb.display_monomial(tout, *m2); tout << "\n";
gb.display_monomial(tout, *m1m2); tout << "\n";); gb.display_monomial(tout, *m1m2); tout << "\n";);
@ -2131,7 +2131,7 @@ namespace smt {
deleted[i] = true; deleted[i] = true;
deleted[j] = true; deleted[j] = true;
deleted[k] = true; deleted[k] = true;
break; break;
} }
} }
if (k < num) if (k < num)
@ -2184,7 +2184,7 @@ namespace smt {
grobner::monomial const * m = eq->get_monomial(i); grobner::monomial const * m = eq->get_monomial(i);
if (m->get_degree() == 0) if (m->get_degree() == 0)
k -= m->get_coeff(); k -= m->get_coeff();
else else
args.push_back(monomial2expr(eq->get_monomial(i), is_int)); args.push_back(monomial2expr(eq->get_monomial(i), is_int));
} }
context & ctx = get_context(); context & ctx = get_context();
@ -2213,7 +2213,7 @@ namespace smt {
TRACE("non_linear", tout << "inserted new equation into the tableau\n"; display_var(tout, v);); TRACE("non_linear", tout << "inserted new equation into the tableau\n"; display_var(tout, v););
return true; return true;
} }
/** /**
\brief Compute Grobner basis, return true if a conflict or new fixed variables were detected. \brief Compute Grobner basis, return true if a conflict or new fixed variables were detected.
*/ */
@ -2227,7 +2227,7 @@ namespace smt {
bool warn = false; bool warn = false;
unsigned next_weight = MAX_DEFAULT_WEIGHT + 1; // next weight using during perturbation phase. unsigned next_weight = MAX_DEFAULT_WEIGHT + 1; // next weight using during perturbation phase.
ptr_vector<grobner::equation> eqs; ptr_vector<grobner::equation> eqs;
while (true) { while (true) {
TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout);); TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
bool r = false; bool r = false;
@ -2267,7 +2267,7 @@ namespace smt {
if (is_inconsistent2(eq, gb)) if (is_inconsistent2(eq, gb))
return GB_PROGRESS; return GB_PROGRESS;
} }
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed, // Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue // then assert bounds for x, and continue
gb_result result = GB_FAIL; gb_result result = GB_FAIL;
if (m_params.m_nl_arith_gb_eqs) { if (m_params.m_nl_arith_gb_eqs) {
@ -2277,7 +2277,7 @@ namespace smt {
if (!eq->is_linear_combination()) { if (!eq->is_linear_combination()) {
TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq);); TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
TRACE("non_linear_bug", tout << "processing new equality:\n"; gb.display_equation(tout, *eq);); TRACE("non_linear_bug", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
if (internalize_gb_eq(eq)) if (internalize_gb_eq(eq))
result = GB_NEW_EQ; result = GB_NEW_EQ;
} }
} }
@ -2372,10 +2372,10 @@ namespace smt {
IF_VERBOSE(3, verbose_stream() << "Max. non linear arithmetic rounds. Increase threshold using NL_ARITH_ROUNDS=<limit>\n";); IF_VERBOSE(3, verbose_stream() << "Max. non linear arithmetic rounds. Increase threshold using NL_ARITH_ROUNDS=<limit>\n";);
return FC_GIVEUP; return FC_GIVEUP;
} }
get_context().push_trail(value_trail<context, unsigned>(m_nl_rounds)); get_context().push_trail(value_trail<context, unsigned>(m_nl_rounds));
m_nl_rounds++; m_nl_rounds++;
elim_quasi_base_rows(); elim_quasi_base_rows();
move_non_base_vars_to_bounds(); move_non_base_vars_to_bounds();
TRACE("non_linear", tout << "processing non linear constraints...\n"; get_context().display(tout);); TRACE("non_linear", tout << "processing non linear constraints...\n"; get_context().display(tout););
@ -2384,8 +2384,8 @@ namespace smt {
failed(); failed();
return FC_CONTINUE; return FC_CONTINUE;
} }
if (!max_min_nl_vars()) if (!max_min_nl_vars())
return FC_CONTINUE; return FC_CONTINUE;
if (check_monomial_assignments()) { if (check_monomial_assignments()) {
@ -2409,20 +2409,20 @@ namespace smt {
} }
break; break;
case 1: case 1:
if (!is_cross_nested_consistent(vars)) if (!is_cross_nested_consistent(vars))
progress = true; progress = true;
break; break;
case 2: case 2:
if (m_params.m_nl_arith_gb) { if (m_params.m_nl_arith_gb) {
switch(compute_grobner(vars)) { switch(compute_grobner(vars)) {
case GB_PROGRESS: case GB_PROGRESS:
progress = true; progress = true;
break; break;
case GB_NEW_EQ: case GB_NEW_EQ:
progress = true; progress = true;
propagate_core(); propagate_core();
break; break;
case GB_FAIL: case GB_FAIL:
break; break;
} }
} }