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

fix unsoundness bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-01 14:45:15 -07:00
parent 869643a551
commit 04c55c34e5
2 changed files with 32 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/math/polynomial/polynomial.cpp
View file

@ -6317,6 +6317,27 @@ namespace polynomial {
return R.mk(); return R.mk();
} }
// x*q = p
//
// md = degree of x in p
// P = m0 + ...
// m0 = x^dm*m1
// m1 * p^dm * q^{md - dm}
// P' = m1 + ...
// property would be that x*q = p => P > 0 <=> P' > 0
// requires that q > 0
// Reasoning:
// P > 0
// <=> { since q > 0 }
// q^md * P > 0
// <=>
// q^md*x^dm*m0 + .. > 0
// <=>
// q^{md-dm}*(xq)^dm*m0 + ... > 0
// <=>
// q^{md-dm}*p^dm + .. > 0
// <=>
// P' > 0
void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result) { void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result) {
unsigned md = degree(r, x); unsigned md = degree(r, x);
if (md == 0) { if (md == 0) {

15
src/nlsat/nlsat_solver.cpp
View file

@ -2742,10 +2742,8 @@ namespace nlsat {
while (elim_uncnstr()) while (elim_uncnstr())
; ;
while (fm()) while (fm())
; ;
if (!solve_eqs()) if (!solve_eqs())
return false; return false;
@ -3017,6 +3015,8 @@ namespace nlsat {
if (apply_fm_equality(x, clauses, lo, hi)) if (apply_fm_equality(x, clauses, lo, hi))
return true; return true;
return false;
if (!all_solved) if (!all_solved)
return false; return false;
@ -3104,6 +3104,13 @@ namespace nlsat {
a1 = m_asm.mk_join(a1, a2); a1 = m_asm.mk_join(a1, a2);
m_lemma_assumptions = a1; m_lemma_assumptions = a1;
polynomial_ref A(l.A), B(l.B);
if (m_pm.is_neg(l.A)) {
A = -A;
B = -B;
}
// TODO: this can also replace solve_eqs // TODO: this can also replace solve_eqs
for (auto c : clauses) { for (auto c : clauses) {
if (c->is_removed()) if (c->is_removed())
@ -3114,7 +3121,7 @@ namespace nlsat {
m_lemma.reset(); m_lemma.reset();
bool is_tautology = false; bool is_tautology = false;
for (literal lit : *c) { for (literal lit : *c) {
lit = substitute_var(x, l.A, l.B, lit); lit = substitute_var(x, A, B, lit);
m_lemma.push_back(lit); m_lemma.push_back(lit);
if (lit == true_literal) if (lit == true_literal)
is_tautology = true; is_tautology = true;
@ -3126,7 +3133,7 @@ namespace nlsat {
IF_VERBOSE(3, IF_VERBOSE(3,
if (cls) { if (cls) {
verbose_stream() << "x" << x << " * " << l.A << " = " << l.B << "\n"; m_display_var(verbose_stream(), x) << " * " << l.A << " = " << l.B << "\n";
display(verbose_stream(), *c) << " -> "; display(verbose_stream(), *c) << " -> ";
display(verbose_stream(), *cls) << "\n"; display(verbose_stream(), *cls) << "\n";
}); });