mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 06:46:11 +00:00
Code Activity

work on nl testing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-18 06:33:52 -10:00
parent 7aa1ba1905
commit 05029c6f03
3 changed files with 25 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_explain.cpp
View file

@ -1084,7 +1084,7 @@ namespace nlsat {
* "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection" * "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection"
* https://arxiv.org/abs/2003.00409 * https://arxiv.org/abs/2003.00409
*/ */
void project_cdcac(polynomial_ref_vector & ps, var max_x) { void project(polynomial_ref_vector & ps, var max_x) {
bool first = true; bool first = true;
if (ps.empty()) if (ps.empty())
return; return;
@ -1142,10 +1142,6 @@ namespace nlsat {
} }
void project(polynomial_ref_vector & ps, var max_x) {
project_cdcac(ps, max_x);
}
bool check_already_added() const { bool check_already_added() const {
for (bool b : m_already_added_literal) { for (bool b : m_already_added_literal) {
(void)b; (void)b;

24
src/nlsat/nlsat_solver.cpp
View file

@ -1092,7 +1092,7 @@ namespace nlsat {
} }
// Helper: Display unsound lemma failure information // Helper: Display unsound lemma failure information
void display_unsound_lemma(imp& checker, scoped_bool_vars& tr, unsigned n, literal const* cls) { void display_unsound_lemma(imp& checker, scoped_bool_vars& tr, unsigned n, literal const* cls, lazy_justification const* jst = nullptr) {
verbose_stream() << "\n"; verbose_stream() << "\n";
verbose_stream() << "========== UNSOUND LEMMA DETECTED ==========\n"; verbose_stream() << "========== UNSOUND LEMMA DETECTED ==========\n";
verbose_stream() << "Levelwise used for this conflict: " << (m_last_conflict_used_lws ? "YES" : "NO") << "\n"; verbose_stream() << "Levelwise used for this conflict: " << (m_last_conflict_used_lws ? "YES" : "NO") << "\n";
@ -1134,10 +1134,26 @@ namespace nlsat {
verbose_stream() << " = " << checker.value(tlit) << "\n"; verbose_stream() << " = " << checker.value(tlit) << "\n";
} }
verbose_stream() << "=============================================\n"; verbose_stream() << "=============================================\n";
if (jst) {
verbose_stream() << "Initial justification (lazy_justification):\n";
verbose_stream() << " Num literals: " << jst->num_lits() << "\n";
for (unsigned i = 0; i < jst->num_lits(); ++i) {
verbose_stream() << " jst lit[" << i << "]: ";
display(verbose_stream(), jst->lit(i));
verbose_stream() << "\n";
}
verbose_stream() << " Num clauses: " << jst->num_clauses() << "\n";
for (unsigned i = 0; i < jst->num_clauses(); ++i) {
verbose_stream() << " jst clause[" << i << "]: ";
display(verbose_stream(), jst->clause(i));
verbose_stream() << "\n";
}
verbose_stream() << "=============================================\n";
}
verbose_stream() << "ABORTING: Unsound lemma detected!\n"; verbose_stream() << "ABORTING: Unsound lemma detected!\n";
} }
void check_lemma(unsigned n, literal const* cls, assumption_set a) { void check_lemma(unsigned n, literal const* cls, assumption_set a, lazy_justification const* jst = nullptr) {
TRACE(nlsat, display(tout << "check lemma: ", n, cls) << "\n"; TRACE(nlsat, display(tout << "check lemma: ", n, cls) << "\n";
display(tout);); display(tout););
@ -1180,7 +1196,7 @@ namespace nlsat {
verbose_stream() << "Dumping lemma that internal checker thinks is not a tautology:\n"; verbose_stream() << "Dumping lemma that internal checker thinks is not a tautology:\n";
verbose_stream() << "Checker levelwise calls: " << checker.m_stats.m_levelwise_calls << "\n"; verbose_stream() << "Checker levelwise calls: " << checker.m_stats.m_levelwise_calls << "\n";
log_lemma(verbose_stream(), n, cls, true, "internal-check-fail"); log_lemma(verbose_stream(), n, cls, true, "internal-check-fail");
display_unsound_lemma(checker, tr, n, cls); display_unsound_lemma(checker, tr, n, cls, jst);
exit(1); exit(1);
} }
} }
@ -2402,7 +2418,7 @@ namespace nlsat {
if (m_check_lemmas) { if (m_check_lemmas) {
TRACE(nlsat, tout << "Checking lazy clause with " << m_lazy_clause.size() << " literals:\n"; TRACE(nlsat, tout << "Checking lazy clause with " << m_lazy_clause.size() << " literals:\n";
display(tout, m_lazy_clause.size(), m_lazy_clause.data()) << "\n";); display(tout, m_lazy_clause.size(), m_lazy_clause.data()) << "\n";);
check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), nullptr); check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), nullptr, &jst);
m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr)); m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr));
} }

6
src/test/nlsat.cpp
View file

@ -2505,12 +2505,14 @@ static void tst_unsound_lws_nullified2() {
} }
void tst_nlsat() { void tst_nlsat() {
tst_unsound_lws_p6236();
std::cout << "------------------\n";
tst_unsound_lws_disc_zero();
std::cout << "------------------\n";
tst_unsound_lws_nullified2(); tst_unsound_lws_nullified2();
std::cout << "------------------\n"; std::cout << "------------------\n";
tst_unsound_lws_nullified(); tst_unsound_lws_nullified();
std::cout << "------------------\n"; std::cout << "------------------\n";
tst_unsound_lws_p6236();
std::cout << "------------------\n";
tst_unsound_lws_ppblockterm(); tst_unsound_lws_ppblockterm();
std::cout << "------------------\n"; std::cout << "------------------\n";
tst_unsound_lws_n46(); tst_unsound_lws_n46();