mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 09:21:56 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-13 15:09:16 -07:00
parent 842e2c79dc
commit 658cf36f09
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/levelwise.cpp
View file

@ -633,13 +633,17 @@ or
add_to_Q_if_new(property(prop_enum::an_del, p.poly), m_level); add_to_Q_if_new(property(prop_enum::an_del, p.poly), m_level);
} }
/* Rule 4.8. Let i ∈ N>0 , R ⊆ Ri /* Rule 4.8. Let i ∈ N>0 , R ⊆ Ri
, s ∈ Ri−1 , s ∈ R_{i−1}
, p ∈ Q[x1, . . . , xi ], level(p) = i, and I be a symbolic interval , p ∈ Q[x1, . . . , xi ], level(p) = i, and I be a symbolic interval
of level i. Assume that p is irreducible, and I = (section, b). of level i. Assume that p is irreducible, and I = (section, b).
Let Q := an_sub(i − 1)(R) ∧ connected(i − 1)(R) ∧ repr(I, s)(R) ∧ an_del(b.p)(R). Let Q := an_sub(i − 1)(R) ∧ connected(i − 1)(R) ∧ repr(I, s)(R) ∧ an_del(b.p)(R).
Q, b.p= p ⊢ sgn_inv(p)(R) Q, b.p= p ⊢ sgn_inv(p)(R)
Q, b.p ̸= p, ord_inv(resxi (b.p, p))(R) ⊢ sgn_inv(p)(R)*/ Q, b.p ̸= p, ord_inv(resxi (b.p, p))(R) ⊢ sgn_inv(p)(R)*/
NOT_IMPLEMENTED_YET(); if (m_I[m_level].section == true) {
NOT_IMPLEMENTED_YET();
} else {
NOT_IMPLEMENTED_YET();
}
} }
/* /*