mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

renaming

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-28 10:22:59 -10:00
parent 8ead9e753b
commit bd987e4399
1 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/nlsat/levelwise.cpp
View file

@ -35,11 +35,11 @@ namespace nlsat {
struct levelwise::impl {
struct property {
prop_enum prop;
polynomial_ref p;
polynomial_ref poly;
unsigned s_idx = -1; // index of the root function, if applicable; -1 means unspecified
unsigned level = -1; // -1 means unspecified
property(prop_enum pr, polynomial_ref const & pp, int si, int lvl) : prop(pr), p(pp), s_idx(si), level(lvl) {}
property(prop_enum pr, polynomial_ref const & pp) : prop(pr), p(pp), s_idx(-1), level(-1) {}
property(prop_enum pr, polynomial_ref const & pp, int si, int lvl) : prop(pr), poly(pp), s_idx(si), level(lvl) {}
property(prop_enum pr, polynomial_ref const & pp) : prop(pr), poly(pp), s_idx(-1), level(-1) {}
};
solver& m_solver;
polynomial_ref_vector const& m_P;
@ -155,7 +155,7 @@ namespace nlsat {
if (level < m_n)
Q.push_back(property(prop_enum::sgn_inv_irreducible, polynomial_ref(p, m_pm), /*s_idx*/0u, /* level */ level));
else if (level == m_n)
Q.push_back(property(prop_enum::an_del, polynomial_ref(p, m_pm), /* s_idx*/ 0u, level));
Q.push_back(property(prop_enum::an_del, polynomial_ref(p, m_pm), /* s_idx */ -1, level));
else {
SASSERT(level <= m_n);
}
@ -243,7 +243,7 @@ namespace nlsat {
};
bool dominates(const property& a, const property& b) const {
return a.p == b.p && dominates(a.prop, b.prop);
return a.poly == b.poly && dominates(a.prop, b.prop);
}
bool dominates(prop_enum a, prop_enum b) const {
return m_prop_dom[static_cast<unsigned>(a)][static_cast<unsigned>(b)];
@ -270,12 +270,12 @@ namespace nlsat {
}
std::ostream& display(std::ostream& out, const property & pr) {
out << "{prop:" << prop_name(pr.prop)
<< ", level:" << pr.level
<< ", s_idx:" << pr.s_idx;
if (pr.p) {
out << ", p:";
::nlsat::display(out, m_solver, pr.p);
out << "{prop:" << prop_name(pr.prop);
if (pr.level != -1) out << ", level:" << pr.level;
if (pr.s_idx != -1) out << ", s_idx:" << pr.s_idx;
if (pr.poly) {
out << ", poly:";
::nlsat::display(out, m_solver, pr.poly);
}
else {
out << ", p:null";
@ -311,7 +311,7 @@ namespace nlsat {
keys.reserve(cand.size());
for (size_t i = 0; i < cand.size(); ++i) {
if (!dominated[i]) {
keys.push_back(Key{ polynomial::manager::id(cand[i].p.get()), static_cast<unsigned>(cand[i].prop), i });
keys.push_back(Key{ polynomial::manager::id(cand[i].poly.get()), static_cast<unsigned>(cand[i].prop), i });
}
}
std::sort(keys.begin(), keys.end(), [](Key const& a, Key const& b){
@ -483,8 +483,8 @@ namespace nlsat {
void build_representation(unsigned i, result_struct& ret) {
std::vector<const poly*> p_non_null;
for (const auto & pr: m_Q) {
if (pr.prop == prop_enum::sgn_inv_irreducible && max_var(pr.p) == i && poly_is_not_nullified_at_sample_at_level(pr.p.get(), i))
p_non_null.push_back(pr.p.get());
if (pr.prop == prop_enum::sgn_inv_irreducible && max_var(pr.poly) == i && poly_is_not_nullified_at_sample_at_level(pr.poly.get(), i))
p_non_null.push_back(pr.poly.get());
}
std::vector<std::unique_ptr<bucket_t>> buckets;
std::vector<root_item_t> roots;
@ -516,7 +516,7 @@ namespace nlsat {
}
void apply_pre(const property& p) {
TRACE(levelwise, display(tout << "p:", p) << std::endl;);
TRACE(levelwise, display(tout << "property p:", p) << std::endl;);
NOT_IMPLEMENTED_YET();
}
// return an empty vector on failure, otherwis returns the cell representations with intervals