mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

logging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-23 20:18:21 -07:00
parent f4fd94747c
commit 3fcd9e64c7
2 changed files with 34 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/nlsat/nlsat_explain.cpp
View file

@ -188,7 +188,7 @@ namespace nlsat {
unsigned lidx = l.index(); unsigned lidx = l.index();
if (m_already_added_literal.get(lidx, false)) if (m_already_added_literal.get(lidx, false))
return; return;
TRACE("nlsat_explain", tout << "adding literal: " << lidx << "\n"; m_solver.display(tout, l); tout << "\n";); TRACE("nlsat_explain", tout << "adding literal: " << lidx << "\n"; m_solver.display(tout, l) << "\n";);
m_already_added_literal.setx(lidx, true, false); m_already_added_literal.setx(lidx, true, false);
m_result->push_back(l); m_result->push_back(l);
} }
@ -619,10 +619,15 @@ namespace nlsat {
void psc(polynomial_ref & p, polynomial_ref & q, var x) { void psc(polynomial_ref & p, polynomial_ref & q, var x) {
polynomial_ref_vector & S = m_psc_tmp; polynomial_ref_vector & S = m_psc_tmp;
polynomial_ref s(m_pm); polynomial_ref s(m_pm);
TRACE("nlsat_explain", tout << "computing psc of\n"; display(tout, p); tout << "\n"; display(tout, q); tout << "\n";);
psc_chain(p, q, x, S); psc_chain(p, q, x, S);
unsigned sz = S.size(); unsigned sz = S.size();
TRACE("nlsat_explain", tout << "computing psc of\n"; display(tout, p); tout << "\n"; display(tout, q); tout << "\n";
for (unsigned i = 0; i < sz; ++i) {
s = S.get(i);
tout << "psc: " << s << "\n";
});
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
s = S.get(i); s = S.get(i);
TRACE("nlsat_explain", tout << "processing psc(" << i << ")\n"; display(tout, s); tout << "\n";); TRACE("nlsat_explain", tout << "processing psc(" << i << ")\n"; display(tout, s); tout << "\n";);
@ -634,7 +639,7 @@ namespace nlsat {
TRACE("nlsat_explain", tout << "done, psc is a constant\n";); TRACE("nlsat_explain", tout << "done, psc is a constant\n";);
return; return;
} }
if (sign(s) == 0) { if (sign(s) == polynomial::sign_zero) {
TRACE("nlsat_explain", tout << "psc vanished, adding zero assumption\n";); TRACE("nlsat_explain", tout << "psc vanished, adding zero assumption\n";);
add_zero_assumption(s); add_zero_assumption(s);
continue; continue;
@ -825,6 +830,7 @@ namespace nlsat {
#else #else
int s = sign(p); int s = sign(p);
if (!is_const(p)) { if (!is_const(p)) {
TRACE("nlsat_explain", tout << p << "\n";);
add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
} }
return s; return s;
@ -833,6 +839,11 @@ namespace nlsat {
/** /**
Auxiliary function to linear roots. Auxiliary function to linear roots.
y > root[1](-2*y - z)
y > -z/2
y + z/2 > 0
2y + z > 0
*/ */
void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) { void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) {
polynomial_ref p_prime(m_pm); polynomial_ref p_prime(m_pm);
@ -898,8 +909,13 @@ namespace nlsat {
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots); m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
unsigned num_roots = roots.size(); unsigned num_roots = roots.size();
for (unsigned i = 0; i < num_roots; i++) { for (unsigned i = 0; i < num_roots; i++) {
TRACE("nlsat_explain", tout << "comparing root: "; m_am.display_decimal(tout, roots[i]); tout << "\n";);
int s = m_am.compare(y_val, 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) { if (s == 0) {
// y_val == roots[i] // y_val == roots[i]
// add literal // add literal
@ -931,11 +947,15 @@ namespace nlsat {
} }
} }
} }
if (!lower_inf) if (!lower_inf) {
TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_lower << "\n";);
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower); add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
if (!upper_inf) }
if (!upper_inf) {
TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_upper << "\n";);
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, i_upper, p_upper);
}
} }
/** /**
@ -1076,7 +1096,7 @@ namespace nlsat {
new_lit = l; new_lit = l;
return; return;
} }
TRACE("nlsat_simplify_core", tout << "trying to simplify literal\n"; display(tout, l); tout << "\nusing equation\n"; TRACE("nlsat_simplify_core", display(tout << "trying to simplify literal\n", l) << "\nusing equation\n";
m_pm.display(tout, info.m_eq, m_solver.display_proc()); tout << "\n";); m_pm.display(tout, info.m_eq, m_solver.display_proc()); tout << "\n";);
int atom_sign = 1; int atom_sign = 1;
bool modified_lit = false; bool modified_lit = false;
@ -1348,7 +1368,9 @@ namespace nlsat {
var max_x = max_var(m_ps); var max_x = max_var(m_ps);
TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";); TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";);
elim_vanishing(m_ps); elim_vanishing(m_ps);
TRACE("nlsat_explain", tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";);
project(m_ps, max_x); project(m_ps, max_x);
TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";);
} }
void process2(unsigned num, literal const * ls) { void process2(unsigned num, literal const * ls) {

6
src/nlsat/nlsat_solver.cpp
View file

@ -652,9 +652,11 @@ namespace nlsat {
SASSERT(i > 0); SASSERT(i > 0);
SASSERT(x >= max_var(p)); SASSERT(x >= max_var(p));
SASSERT(k == atom::ROOT_LT || k == atom::ROOT_GT || k == atom::ROOT_EQ || k == atom::ROOT_LE || k == atom::ROOT_GE); SASSERT(k == atom::ROOT_LT || k == atom::ROOT_GT || k == atom::ROOT_EQ || k == atom::ROOT_LE || k == atom::ROOT_GE);
polynomial_ref p1(m_pm); polynomial_ref p1(m_pm), uniq_p(m_pm);
p1 = m_pm.flip_sign_if_lm_neg(p); // flipping the sign of the polynomial will not change its roots. p1 = m_pm.flip_sign_if_lm_neg(p); // flipping the sign of the polynomial will not change its roots.
poly * uniq_p = m_cache.mk_unique(p1); uniq_p = m_cache.mk_unique(p1);
TRACE("nlsat_solver", tout << p1 << " " << uniq_p << "\n";);
void * mem = m_allocator.allocate(sizeof(root_atom)); void * mem = m_allocator.allocate(sizeof(root_atom));
root_atom * new_atom = new (mem) root_atom(k, x, i, uniq_p); root_atom * new_atom = new (mem) root_atom(k, x, i, uniq_p);
root_atom * old_atom = m_root_atoms.insert_if_not_there(new_atom); root_atom * old_atom = m_root_atoms.insert_if_not_there(new_atom);