mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-01 14:50:59 -07:00
parent 9c006c4e42
commit 32de7c61fc
1 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/nlsat/levelwise.cpp
View file

@ -42,6 +42,8 @@ namespace nlsat {
factor(poly, factors); factor(poly, factors);
fn(factors[0]); fn(factors[0]);
} }
// todo: consider to keey polynomials in a set by using m_pm.eq
struct property { struct property {
prop_enum prop_tag; prop_enum prop_tag;
polynomial_ref poly; polynomial_ref poly;
@ -322,11 +324,21 @@ namespace nlsat {
// Part B of construct_interval: build (I, E, ≼) representation for level i // Part B of construct_interval: build (I, E, ≼) representation for level i
void build_representation() { void build_representation() {
// collect non-null polynomials (up to polynomial_manager equality)
std::vector<const poly*> p_non_null; std::vector<const poly*> p_non_null;
for (const auto & pr: to_vector(m_Q[m_level])) { for (auto & pr: to_vector(m_Q[m_level])) {
SASSERT(max_var(pr.poly) == m_level); SASSERT(max_var(pr.poly) == m_level);
if (pr.prop_tag == prop_enum::sgn_inv && !coeffs_are_zeroes_on_sample(pr.poly, m_pm, sample(), m_am )) if (pr.prop_tag == prop_enum::sgn_inv
p_non_null.push_back(pr.poly.get()); && !coeffs_are_zeroes_on_sample(pr.poly, m_pm, sample(), m_am )) {
TRACE(lws, tout << "adding:" << pr.poly.get() << "\n";);
poly* new_p = pr.poly.get();
auto it = std::find_if(p_non_null.begin(), p_non_null.end(),
[this, new_p](const poly* q){
return m_pm.eq(q, new_p);
});
if (it == p_non_null.end())
p_non_null.push_back(new_p);
}
} }
collect_E(p_non_null); collect_E(p_non_null);
@ -341,6 +353,9 @@ namespace nlsat {
// Step 1a: collect E the set of root functions on m_level // Step 1a: collect E the set of root functions on m_level
void collect_E(std::vector<const poly*> const& p_non_null) { void collect_E(std::vector<const poly*> const& p_non_null) {
TRACE(lws, tout << "enter\n";);
m_E.clear();
for (auto const* p0 : p_non_null) { for (auto const* p0 : p_non_null) {
auto* p = const_cast<poly*>(p0); auto* p = const_cast<poly*>(p0);
if (m_pm.max_var(p) != m_level) { if (m_pm.max_var(p) != m_level) {
@ -361,6 +376,7 @@ namespace nlsat {
for (unsigned k = 0; k < num_roots; ++k) for (unsigned k = 0; k < num_roots; ++k)
m_E.emplace_back(m_am, p, k + 1, roots[k]); m_E.emplace_back(m_am, p, k + 1, roots[k]);
} }
TRACE(lws, tout << "exit\n";);
} }
// add a property to m_Q if an equivalent one is not already present. // add a property to m_Q if an equivalent one is not already present.