mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-24 02:49:38 +00:00
Code Activity

fix a bug with non-adding ldcf

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-11 16:15:42 -10:00
parent bbece87183
commit a35fe109ac
2 changed files with 683 additions and 692 deletions
Download patch file Download diff file Expand all files Collapse all files

1366
src/nlsat/levelwise.cpp
View file

File diff suppressed because it is too large Load diff

9
src/nlsat/nlsat_solver.cpp
View file

@ -242,7 +242,8 @@ namespace nlsat {
unsigned m_stages; unsigned m_stages;
unsigned m_irrational_assignments; // number of irrational witnesses unsigned m_irrational_assignments; // number of irrational witnesses
unsigned m_levelwise_calls; unsigned m_levelwise_calls;
unsigned m_levelwise_successes; unsigned m_levelwise_failures;
unsigned m_lws_initial_fail;
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); } stats() { reset(); }
}; };
@ -2780,7 +2781,7 @@ namespace nlsat {
st.update("nlsat simplifications", m_stats.m_simplifications); st.update("nlsat simplifications", m_stats.m_simplifications);
st.update("nlsat irrational assignments", m_stats.m_irrational_assignments); st.update("nlsat irrational assignments", m_stats.m_irrational_assignments);
st.update("levelwise calls", m_stats.m_levelwise_calls); st.update("levelwise calls", m_stats.m_levelwise_calls);
st.update("levelwise successes", m_stats.m_levelwise_successes); st.update("levelwise failures", m_stats.m_levelwise_failures);
} }
void reset_statistics() { void reset_statistics() {
@ -4646,8 +4647,8 @@ namespace nlsat {
void solver::record_levelwise_result(bool success) { void solver::record_levelwise_result(bool success) {
m_imp->m_stats.m_levelwise_calls++; m_imp->m_stats.m_levelwise_calls++;
if (success) if (!success)
m_imp->m_stats.m_levelwise_successes++; m_imp->m_stats.m_levelwise_failures++;
} }
bool solver::has_root_atom(clause const& c) const { bool solver::has_root_atom(clause const& c) const {