mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

cast, updated nlexplain

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-03-19 12:29:55 -07:00
parent 730f9ad9b7
commit 70d2263a85
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/nlsat/nlsat_explain.cpp
View file

@ -277,6 +277,7 @@ namespace nlsat {
} }
}; };
void add_zero_assumption(polynomial_ref& p) { void add_zero_assumption(polynomial_ref& p) {
// If p is of the form p1^n1 * ... * pk^nk, // If p is of the form p1^n1 * ... * pk^nk,
// then only the factors that are zero in the current interpretation needed to be considered. // then only the factors that are zero in the current interpretation needed to be considered.
@ -300,7 +301,7 @@ namespace nlsat {
} }
} }
} }
if (!is_linear) { if (!is_linear) {
scoped_anum_vector& roots = m_roots_tmp; scoped_anum_vector& roots = m_roots_tmp;
roots.reset(); roots.reset();
@ -312,6 +313,7 @@ namespace nlsat {
int s = m_am.compare(x_val, roots[i]); int s = m_am.compare(x_val, roots[i]);
if (s != 0) if (s != 0)
continue; continue;
TRACE("nlsat_explain", tout << "adding (zero assumption) root " << "\n");
add_root_literal(atom::ROOT_EQ, x, i + 1, p); add_root_literal(atom::ROOT_EQ, x, i + 1, p);
return; return;
} }
@ -321,12 +323,11 @@ namespace nlsat {
} }
} }
SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it. SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it.
literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data()); literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data());
l.neg(); l.neg();
TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";); TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";);
add_literal(l); add_literal(l);
} }
void add_simple_assumption(atom::kind k, poly * p, bool sign = false) { void add_simple_assumption(atom::kind k, poly * p, bool sign = false) {