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

v0.1 of nla saturation

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-09-26 23:05:02 +03:00
parent 3e9afb30af
commit fdac93fff3
3 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
.clang-format
View file

@ -8,6 +8,7 @@ BasedOnStyle: LLVM
IndentWidth: 4 IndentWidth: 4
TabWidth: 4 TabWidth: 4
UseTab: Never UseTab: Never
IndentCaseLabels: false

1
src/math/lp/nla_core.cpp
View file

@ -1318,6 +1318,7 @@ lbool core::check() {
return l_false; return l_false;
} }
if (no_effect() && lp_settings().m_enable_stellensatz) if (no_effect() && lp_settings().m_enable_stellensatz)
ret = m_stellensatz.saturate(); ret = m_stellensatz.saturate();

5
src/smt/theory_lra.cpp
View file

@ -3475,9 +3475,12 @@ public:
++m_stats.m_conflicts; ++m_stats.m_conflicts;
for (auto ev : m_explanation) for (auto ev : m_explanation)
set_evidence(ev.ci(), m_core, m_eqs); set_evidence(ev.ci(), m_core, m_eqs);
if (m_eqs.empty() && all_of(m_core, [&](literal l) { return ctx().get_assignment(l) == l_false; })) if (m_eqs.empty() && all_of(m_core, [&](literal l) { return ctx().get_assignment(l) == l_false; }))
is_conflict = true; is_conflict = true;
for (auto l : m_core) {
IF_VERBOSE(1, verbose_stream() << l << " " << ctx().get_assignment(l) << "\n");
}
TRACE(arith_conflict, TRACE(arith_conflict,
tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma"); tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma");
for (auto const& p : m_params) tout << " " << p; for (auto const& p : m_params) tout << " " << p;