mirror of
https://github.com/Z3Prover/z3
synced 2026-06-12 20:05:36 +00:00
refactoring
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
Nikolaj Bjorner
parent
c9add31da7
commit
7909e2498a
2 changed files with 134 additions and 182 deletions
|
|
@ -280,6 +280,110 @@ namespace nlsat {
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
|
struct cell_root_info {
|
||||||
|
polynomial_ref m_eq;
|
||||||
|
polynomial_ref m_lower;
|
||||||
|
polynomial_ref m_upper;
|
||||||
|
unsigned m_eq_idx;
|
||||||
|
unsigned m_lower_idx;
|
||||||
|
unsigned m_upper_idx;
|
||||||
|
bool m_has_eq;
|
||||||
|
bool m_has_lower;
|
||||||
|
bool m_has_upper;
|
||||||
|
cell_root_info(pmanager & pm): m_eq(pm), m_lower(pm), m_upper(pm) {
|
||||||
|
reset();
|
||||||
|
}
|
||||||
|
void reset() {
|
||||||
|
m_eq = nullptr;
|
||||||
|
m_lower = nullptr;
|
||||||
|
m_upper = nullptr;
|
||||||
|
m_eq_idx = m_lower_idx = m_upper_idx = UINT_MAX;
|
||||||
|
m_has_eq = m_has_lower = m_has_upper = false;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
void find_cell_roots(polynomial_ref_vector & ps, var y, cell_root_info & info) {
|
||||||
|
info.reset();
|
||||||
|
SASSERT(m_assignment.is_assigned(y));
|
||||||
|
bool lower_inf = true;
|
||||||
|
bool upper_inf = true;
|
||||||
|
scoped_anum_vector & roots = m_roots_tmp;
|
||||||
|
scoped_anum lower(m_am);
|
||||||
|
scoped_anum upper(m_am);
|
||||||
|
anum const & y_val = m_assignment.value(y);
|
||||||
|
TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, y); tout << " -> ";
|
||||||
|
m_am.display_decimal(tout, y_val); tout << "\n";);
|
||||||
|
polynomial_ref p(m_pm);
|
||||||
|
unsigned sz = ps.size();
|
||||||
|
for (unsigned k = 0; k < sz; k++) {
|
||||||
|
p = ps.get(k);
|
||||||
|
if (max_var(p) != y)
|
||||||
|
continue;
|
||||||
|
roots.reset();
|
||||||
|
// Variable y is assigned in m_assignment. We must temporarily unassign it.
|
||||||
|
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
|
||||||
|
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
|
||||||
|
unsigned num_roots = roots.size();
|
||||||
|
TRACE(nlsat_explain,
|
||||||
|
tout << "isolated roots for "; display_var(tout, y);
|
||||||
|
tout << " with polynomial: " << p << "\n";
|
||||||
|
for (unsigned ri = 0; ri < num_roots; ++ri) {
|
||||||
|
m_am.display_decimal(tout << " root[" << (ri+1) << "] = ", roots[ri]);
|
||||||
|
tout << "\n";
|
||||||
|
});
|
||||||
|
bool all_lt = true;
|
||||||
|
for (unsigned i = 0; i < num_roots; i++) {
|
||||||
|
int s = m_am.compare(y_val, roots[i]);
|
||||||
|
TRACE(nlsat_explain,
|
||||||
|
m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n";
|
||||||
|
m_am.display_decimal(tout << "with y_val:", y_val);
|
||||||
|
tout << "\nsign " << s << "\n";
|
||||||
|
tout << "poly: " << p << "\n";
|
||||||
|
);
|
||||||
|
if (s == 0) {
|
||||||
|
info.m_eq = p;
|
||||||
|
info.m_eq_idx = i + 1;
|
||||||
|
info.m_has_eq = true;
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
else if (s < 0) {
|
||||||
|
if (i > 0) {
|
||||||
|
int j = i - 1;
|
||||||
|
if (lower_inf || m_am.lt(lower, roots[j])) {
|
||||||
|
lower_inf = false;
|
||||||
|
m_am.set(lower, roots[j]);
|
||||||
|
info.m_lower = p;
|
||||||
|
info.m_lower_idx = j + 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (upper_inf || m_am.lt(roots[i], upper)) {
|
||||||
|
upper_inf = false;
|
||||||
|
m_am.set(upper, roots[i]);
|
||||||
|
info.m_upper = p;
|
||||||
|
info.m_upper_idx = i + 1;
|
||||||
|
}
|
||||||
|
all_lt = false;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (all_lt && num_roots > 0) {
|
||||||
|
int j = num_roots - 1;
|
||||||
|
if (lower_inf || m_am.lt(lower, roots[j])) {
|
||||||
|
lower_inf = false;
|
||||||
|
m_am.set(lower, roots[j]);
|
||||||
|
info.m_lower = p;
|
||||||
|
info.m_lower_idx = j + 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (!lower_inf) {
|
||||||
|
info.m_has_lower = true;
|
||||||
|
}
|
||||||
|
if (!upper_inf) {
|
||||||
|
info.m_has_upper = true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
void add_zero_assumption(polynomial_ref& p) {
|
void add_zero_assumption(polynomial_ref& p) {
|
||||||
// Build a square-free representative of p so that we can speak about
|
// Build a square-free representative of p so that we can speak about
|
||||||
// a specific root that coincides with the current assignment.
|
// a specific root that coincides with the current assignment.
|
||||||
|
|
@ -296,26 +400,17 @@ namespace nlsat {
|
||||||
return;
|
return;
|
||||||
SASSERT(m_assignment.is_assigned(maxx));
|
SASSERT(m_assignment.is_assigned(maxx));
|
||||||
|
|
||||||
undef_var_assignment partial(m_assignment, maxx);
|
polynomial_ref_vector singleton(m_pm);
|
||||||
scoped_anum_vector & roots = m_roots_tmp;
|
singleton.push_back(q);
|
||||||
roots.reset();
|
cell_root_info info(m_pm);
|
||||||
// Isolate the roots of providing the assignment with maxx unassigned.
|
find_cell_roots(singleton, maxx, info);
|
||||||
m_am.isolate_roots(q, partial, roots);
|
if (!info.m_has_eq)
|
||||||
|
|
||||||
anum const & maxx_val = m_assignment.value(maxx);
|
|
||||||
unsigned root_idx = 0;
|
|
||||||
for (unsigned i = 0; i < roots.size(); ++i)
|
|
||||||
if (m_am.compare(maxx_val, roots[i]) == 0) {
|
|
||||||
root_idx = i + 1; // roots are 1-based
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
if (root_idx == 0)
|
|
||||||
return; // there are no root functions and therefore no constraints are generated
|
return; // there are no root functions and therefore no constraints are generated
|
||||||
|
|
||||||
TRACE(nlsat_explain,
|
TRACE(nlsat_explain,
|
||||||
tout << "adding zero-assumption root literal for ";
|
tout << "adding zero-assumption root literal for ";
|
||||||
display_var(tout, maxx); tout << " using root[" << root_idx << "] of " << q << "\n";);
|
display_var(tout, maxx); tout << " using root[" << info.m_eq_idx << "] of " << q << "\n";);
|
||||||
add_root_literal(atom::ROOT_EQ, maxx, root_idx, q);
|
add_root_literal(atom::ROOT_EQ, maxx, info.m_eq_idx, info.m_eq);
|
||||||
}
|
}
|
||||||
|
|
||||||
void add_assumption(atom::kind k, poly * p, bool sign = false) {
|
void add_assumption(atom::kind k, poly * p, bool sign = false) {
|
||||||
|
|
@ -927,7 +1022,6 @@ namespace nlsat {
|
||||||
add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
|
add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
|
||||||
}
|
}
|
||||||
return s;
|
return s;
|
||||||
#endif
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
|
@ -958,100 +1052,26 @@ namespace nlsat {
|
||||||
}
|
}
|
||||||
add_assumption(k, p, lsign);
|
add_assumption(k, p, lsign);
|
||||||
}
|
}
|
||||||
|
|
||||||
void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) {
|
void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) {
|
||||||
res.reset();
|
res.reset();
|
||||||
SASSERT(m_assignment.is_assigned(y));
|
cell_root_info info(m_pm);
|
||||||
bool lower_inf = true;
|
find_cell_roots(ps, y, info);
|
||||||
bool upper_inf = true;
|
if (info.m_has_eq) {
|
||||||
scoped_anum_vector & roots = m_roots_tmp;
|
res.push_back(info.m_eq);
|
||||||
scoped_anum lower(m_am);
|
add_root_literal(atom::ROOT_EQ, y, info.m_eq_idx, info.m_eq);
|
||||||
scoped_anum upper(m_am);
|
return;
|
||||||
anum const & y_val = m_assignment.value(y);
|
|
||||||
TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, y); tout << " -> ";
|
|
||||||
m_am.display_decimal(tout, y_val); tout << "\n";);
|
|
||||||
polynomial_ref p_lower(m_pm);
|
|
||||||
unsigned i_lower = UINT_MAX;
|
|
||||||
polynomial_ref p_upper(m_pm);
|
|
||||||
unsigned i_upper = UINT_MAX;
|
|
||||||
polynomial_ref p(m_pm);
|
|
||||||
unsigned sz = ps.size();
|
|
||||||
for (unsigned k = 0; k < sz; k++) {
|
|
||||||
p = ps.get(k);
|
|
||||||
if (max_var(p) != y)
|
|
||||||
continue;
|
|
||||||
roots.reset();
|
|
||||||
// Variable y is assigned in m_assignment. We must temporarily unassign it.
|
|
||||||
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
|
|
||||||
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
|
|
||||||
unsigned num_roots = roots.size();
|
|
||||||
TRACE(nlsat_explain,
|
|
||||||
tout << "isolated roots for "; display_var(tout, y);
|
|
||||||
tout << " with polynomial: " << p << "\n";
|
|
||||||
for (unsigned ri = 0; ri < num_roots; ++ri) {
|
|
||||||
m_am.display_decimal(tout << " root[" << (ri+1) << "] = ", roots[ri]);
|
|
||||||
tout << "\n";
|
|
||||||
});
|
|
||||||
bool all_lt = true;
|
|
||||||
for (unsigned i = 0; i < num_roots; i++) {
|
|
||||||
int s = m_am.compare(y_val, roots[i]);
|
|
||||||
TRACE(nlsat_explain,
|
|
||||||
m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n";
|
|
||||||
m_am.display_decimal(tout << "with y_val:", y_val);
|
|
||||||
tout << "\nsign " << s << "\n";
|
|
||||||
tout << "poly: " << p << "\n";
|
|
||||||
);
|
|
||||||
if (s == 0) {
|
|
||||||
// y_val == roots[i]
|
|
||||||
// add literal
|
|
||||||
// ! (y = root_i(p))
|
|
||||||
add_root_literal(atom::ROOT_EQ, y, i+1, p);
|
|
||||||
res.push_back(p);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
else if (s < 0) {
|
|
||||||
// y_val < roots[i]
|
|
||||||
if (i > 0) {
|
|
||||||
// y_val > roots[j]
|
|
||||||
int j = i - 1;
|
|
||||||
if (lower_inf || m_am.lt(lower, roots[j])) {
|
|
||||||
lower_inf = false;
|
|
||||||
m_am.set(lower, roots[j]);
|
|
||||||
p_lower = p;
|
|
||||||
i_lower = j + 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (upper_inf || m_am.lt(roots[i], upper)) {
|
|
||||||
upper_inf = false;
|
|
||||||
m_am.set(upper, roots[i]);
|
|
||||||
p_upper = p;
|
|
||||||
i_upper = i + 1;
|
|
||||||
}
|
|
||||||
all_lt = false;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (all_lt && num_roots > 0) {
|
|
||||||
int j = num_roots - 1;
|
|
||||||
if (lower_inf || m_am.lt(lower, roots[j])) {
|
|
||||||
lower_inf = false;
|
|
||||||
m_am.set(lower, roots[j]);
|
|
||||||
p_lower = p;
|
|
||||||
i_lower = j + 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
if (info.m_has_lower) {
|
||||||
if (!lower_inf) {
|
res.push_back(info.m_lower);
|
||||||
res.push_back(p_lower);
|
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, info.m_lower_idx, info.m_lower);
|
||||||
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
|
|
||||||
}
|
}
|
||||||
if (!upper_inf) {
|
if (info.m_has_upper) {
|
||||||
res.push_back(p_upper);
|
res.push_back(info.m_upper);
|
||||||
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
|
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, info.m_upper_idx, info.m_upper);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
Add one or two literals that specify in which cell of variable y the current interpretation is.
|
Add one or two literals that specify in which cell of variable y the current interpretation is.
|
||||||
One literal is added for the cases:
|
One literal is added for the cases:
|
||||||
|
|
@ -1071,88 +1091,20 @@ namespace nlsat {
|
||||||
! (y > root_i(p1)) or !(y < root_j(p2))
|
! (y > root_i(p1)) or !(y < root_j(p2))
|
||||||
*/
|
*/
|
||||||
void add_cell_lits(polynomial_ref_vector & ps, var y) {
|
void add_cell_lits(polynomial_ref_vector & ps, var y) {
|
||||||
SASSERT(m_assignment.is_assigned(y));
|
cell_root_info info(m_pm);
|
||||||
bool lower_inf = true;
|
find_cell_roots(ps, y, info);
|
||||||
bool upper_inf = true;
|
if (info.m_has_eq) {
|
||||||
scoped_anum_vector & roots = m_roots_tmp;
|
add_root_literal(atom::ROOT_EQ, y, info.m_eq_idx, info.m_eq);
|
||||||
scoped_anum lower(m_am);
|
return;
|
||||||
scoped_anum upper(m_am);
|
|
||||||
anum const & y_val = m_assignment.value(y);
|
|
||||||
TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, y); tout << " -> ";
|
|
||||||
m_am.display_decimal(tout, y_val); tout << "\n";);
|
|
||||||
polynomial_ref p_lower(m_pm);
|
|
||||||
unsigned i_lower = UINT_MAX;
|
|
||||||
polynomial_ref p_upper(m_pm);
|
|
||||||
unsigned i_upper = UINT_MAX;
|
|
||||||
polynomial_ref p(m_pm);
|
|
||||||
unsigned sz = ps.size();
|
|
||||||
for (unsigned k = 0; k < sz; k++) {
|
|
||||||
p = ps.get(k);
|
|
||||||
if (max_var(p) != y)
|
|
||||||
continue;
|
|
||||||
roots.reset();
|
|
||||||
// Variable y is assigned in m_assignment. We must temporarily unassign it.
|
|
||||||
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
|
|
||||||
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
|
|
||||||
unsigned num_roots = roots.size();
|
|
||||||
bool all_lt = true;
|
|
||||||
for (unsigned i = 0; i < num_roots; i++) {
|
|
||||||
int s = m_am.compare(y_val, roots[i]);
|
|
||||||
TRACE(nlsat_explain,
|
|
||||||
m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n";
|
|
||||||
m_am.display_decimal(tout << "with y_val:", y_val);
|
|
||||||
tout << "\nsign " << s << "\n";
|
|
||||||
tout << "poly: " << p << "\n";
|
|
||||||
);
|
|
||||||
if (s == 0) {
|
|
||||||
// y_val == roots[i]
|
|
||||||
// add literal
|
|
||||||
// ! (y = root_i(p))
|
|
||||||
add_root_literal(atom::ROOT_EQ, y, i+1, p);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
else if (s < 0) {
|
|
||||||
// y_val < roots[i]
|
|
||||||
if (i > 0) {
|
|
||||||
// y_val > roots[j]
|
|
||||||
int j = i - 1;
|
|
||||||
if (lower_inf || m_am.lt(lower, roots[j])) {
|
|
||||||
lower_inf = false;
|
|
||||||
m_am.set(lower, roots[j]);
|
|
||||||
p_lower = p;
|
|
||||||
i_lower = j + 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (upper_inf || m_am.lt(roots[i], upper)) {
|
|
||||||
upper_inf = false;
|
|
||||||
m_am.set(upper, roots[i]);
|
|
||||||
p_upper = p;
|
|
||||||
i_upper = i + 1;
|
|
||||||
}
|
|
||||||
all_lt = false;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (all_lt && num_roots > 0) {
|
|
||||||
int j = num_roots - 1;
|
|
||||||
if (lower_inf || m_am.lt(lower, roots[j])) {
|
|
||||||
lower_inf = false;
|
|
||||||
m_am.set(lower, roots[j]);
|
|
||||||
p_lower = p;
|
|
||||||
i_lower = j + 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
if (info.m_has_lower) {
|
||||||
if (!lower_inf) {
|
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, info.m_lower_idx, info.m_lower);
|
||||||
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
|
|
||||||
}
|
}
|
||||||
if (!upper_inf) {
|
if (info.m_has_upper) {
|
||||||
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
|
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, info.m_upper_idx, info.m_upper);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
\brief Return true if all polynomials in ps are univariate in x.
|
\brief Return true if all polynomials in ps are univariate in x.
|
||||||
*/
|
*/
|
||||||
|
|
|
||||||
|
|
@ -9,7 +9,7 @@ def_module_params('nlsat',
|
||||||
('lazy', UINT, 0, "how lazy the solver is."),
|
('lazy', UINT, 0, "how lazy the solver is."),
|
||||||
('reorder', BOOL, True, "reorder variables."),
|
('reorder', BOOL, True, "reorder variables."),
|
||||||
('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
|
('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
|
||||||
('log_lemma_smtrat', BOOL, False, "use indexed SMT-LIB root expressions when logging lemmas"),
|
('log_lemma_smtrat', BOOL, False, "log lemmas to be readable by smtrat"),
|
||||||
('dump_mathematica', BOOL, False, "display lemmas as matematica"),
|
('dump_mathematica', BOOL, False, "display lemmas as matematica"),
|
||||||
('check_lemmas', BOOL, False, "check lemmas on the fly using an independent nlsat solver"),
|
('check_lemmas', BOOL, False, "check lemmas on the fly using an independent nlsat solver"),
|
||||||
('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."),
|
('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."),
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue