mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 11:37:54 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-20 08:02:31 -07:00
parent d15c0e396e
commit 5d08ebdffd
5 changed files with 10 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1544,6 +1544,7 @@ lbool core::check() {
scoped_limits sl(m_reslim); scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim); sl.push_child(&m_nra_lim);
ret = m_nra.check_assignment(); ret = m_nra.check_assignment();
IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";);
} }
if (no_effect()) { if (no_effect()) {

2
src/math/lp/nra_solver.cpp
View file

@ -358,6 +358,8 @@ struct solver::imp {
default: default:
UNREACHABLE(); UNREACHABLE();
} }
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
} }
m_nla_core.set_use_nra_model(true); m_nla_core.set_use_nra_model(true);
break; break;

8
src/nlsat/nlsat_explain.cpp
View file

@ -2316,6 +2316,10 @@ namespace nlsat {
m_imp->m_simplify_cores = f; m_imp->m_simplify_cores = f;
} }
void explain::set_linear_project(bool f) {
m_imp->m_linear_project = f;
}
void explain::set_full_dimensional(bool f) { void explain::set_full_dimensional(bool f) {
m_imp->m_full_dimensional = f; m_imp->m_full_dimensional = f;
} }
@ -2336,10 +2340,6 @@ namespace nlsat {
(*m_imp)(n, ls, result); (*m_imp)(n, ls, result);
} }
void explain::linear_project(unsigned n, literal const* ls, scoped_literal_vector& result) {
m_imp->linear_project(n, ls, result);
}
void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) { void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->project(x, n, ls, result); m_imp->project(x, n, ls, result);
} }

2
src/nlsat/nlsat_explain.h
View file

@ -66,8 +66,6 @@ namespace nlsat {
*/ */
void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result); void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result);
void linear_project(unsigned n, literal const* ls, scoped_literal_vector& result);
/** /**
\brief projection for a given variable. \brief projection for a given variable.

4
src/nlsat/nlsat_solver.cpp
View file

@ -2078,7 +2078,9 @@ namespace nlsat {
// assignment does not satisfy the constraints -> create lemma // assignment does not satisfy the constraints -> create lemma
SASSERT(best_literal != null_literal); SASSERT(best_literal != null_literal);
m_lazy_clause.reset(); m_lazy_clause.reset();
m_explain.linear_project(1, &best_literal, m_lazy_clause); m_explain.set_linear_project(true);
m_explain.main_operator(1, &best_literal, m_lazy_clause);
m_explain.set_linear_project(false);
m_lazy_clause.push_back(~best_literal); m_lazy_clause.push_back(~best_literal);
core.clear(); core.clear();