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

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-14 11:55:21 -07:00
parent 7ffebbd60c
commit 52759c815e
1 changed files with 17 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/nlsat/levelwise.cpp
View file

@ -53,9 +53,7 @@ namespace nlsat {
} }
#ifdef Z3DEBUG #ifdef Z3DEBUG
bool check_prop_init() { bool check_prop_init() {
std::cout << "checked\n";
for (unsigned k = 0; k < prop_count(); ++k) for (unsigned k = 0; k < prop_count(); ++k)
if (m_prop_dom[k][k]) if (m_prop_dom[k][k])
return false; return false;
@ -124,7 +122,10 @@ namespace nlsat {
bool status; bool status;
}; };
bool dominates(prop_enum a, prop_enum b) { bool dominates(const property& a, const property& b) const {
return a.p == b.p && 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)]; return m_prop_dom[static_cast<unsigned>(a)][static_cast<unsigned>(b)];
} }
@ -139,11 +140,11 @@ namespace nlsat {
if (cand.empty()) return {}; if (cand.empty()) return {};
// Determine maxima w.r.t. ▹ using the transitive closure matrix // Determine maxima w.r.t. ▹ using the transitive closure matrix
// Dominance requires the same polynomial in both compared properties
std::vector<bool> dominated(cand.size(), false); std::vector<bool> dominated(cand.size(), false);
for (size_t i = 0; i < cand.size(); ++i) { for (size_t i = 0; i < cand.size(); ++i) {
for (size_t j = 0; j < cand.size(); ++j) { for (size_t j = 0; j < cand.size(); ++j) {
if (i != j && dominates(cand[j].prop, cand[i].prop)) { if (i != j && dominates(cand[j], cand[i])) {
dominated[i] = true; dominated[i] = true;
break; break;
} }
@ -171,19 +172,22 @@ namespace nlsat {
result_struct construct_interval() { result_struct construct_interval() {
result_struct ret; result_struct ret;
/*foreach q ∈ Q |i where q is the greatest element with respect to ▹ (from Definition 4.5) and q ̸= sgn_inv(p) for an irreducible p /*foreach q ∈ Q |i where q is the greatest element with respect to the relation (from Definition 4.5) and q ̸= sgn_inv(p) for an irreducible p
do do
2 Q := apply_pre(i, Q ,q,(s)) // Algorithm 3 2 Q := apply_pre(i, Q ,q,(s)) // Algorithm 3
3 if Q= FAIL then 3 if Q= FAIL then
4 return FAIL 4 return FAIL
*/ */
std::vector<property> to_refine = greatest_to_refine(); std::vector<property> to_refine = greatest_to_refine();
// refine using to_refine (TBD) // refine using to_refine (TBD)
return ret; return ret;
} }
// return an empty vector on failure // return an empty vector on failure
std::vector<symbolic_interval> single_cell() { std::vector<symbolic_interval> single_cell() {
std::vector<symbolic_interval> ret; std::vector<symbolic_interval> ret;
m_Q = seed_properties(); // Q is the set of properties on level m_n m_Q = seed_properties(); // Q is the set of properties on level m_n
for (unsigned i = m_n; i >= 1; i--) { for (unsigned i = m_n; i >= 1; i--) {
auto result = construct_interval(); auto result = construct_interval();