mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 19:47:52 +00:00
Code Activity

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-20 07:53:43 -07:00
parent 964dd2a71a
commit d15c0e396e
3 changed files with 16 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/nlsat/nlsat_explain.cpp
View file

@ -45,8 +45,8 @@ namespace nlsat {
bool m_minimize_cores; bool m_minimize_cores;
bool m_factor; bool m_factor;
bool m_signed_project; bool m_signed_project;
bool m_linear_project;
bool m_cell_sample; bool m_cell_sample;
bool m_linear_project = false;
struct todo_set { struct todo_set {
@ -156,7 +156,6 @@ namespace nlsat {
m_full_dimensional = false; m_full_dimensional = false;
m_minimize_cores = false; m_minimize_cores = false;
m_signed_project = false; m_signed_project = false;
m_linear_project = false;
} }
std::ostream& display(std::ostream & out, polynomial_ref const & p) const { std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
@ -1413,7 +1412,7 @@ namespace nlsat {
* "More is Less: Adding Polynomials for Faster Explanations in NLSAT" * "More is Less: Adding Polynomials for Faster Explanations in NLSAT"
* in CADE30, 2025 * in CADE30, 2025
*/ */
void project_linear(polynomial_ref_vector & ps, var max_x) { void linear_project(polynomial_ref_vector & ps, var max_x) {
if (ps.empty()) if (ps.empty())
return; return;
m_todo.reset(); m_todo.reset();
@ -1434,7 +1433,7 @@ namespace nlsat {
x = m_todo.extract_max_polys(ps); x = m_todo.extract_max_polys(ps);
} }
while(!m_todo.empty()) { while (!m_todo.empty()) {
add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample);
if (all_univ(ps, x) && m_todo.empty()) { if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset(); m_todo.reset();
@ -1470,16 +1469,13 @@ namespace nlsat {
void project(polynomial_ref_vector & ps, var max_x) { void project(polynomial_ref_vector & ps, var max_x) {
if (m_linear_project) { if (m_linear_project)
project_linear(ps, max_x); linear_project(ps, max_x);
} else if (m_cell_sample)
else if (m_cell_sample) {
project_cdcac(ps, max_x); project_cdcac(ps, max_x);
} else
else {
project_original(ps, max_x); project_original(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) {
@ -2336,14 +2332,14 @@ namespace nlsat {
m_imp->m_signed_project = f; m_imp->m_signed_project = f;
} }
void explain::set_linear_project(bool f) {
m_imp->m_linear_project = f;
}
void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) { void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) {
(*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,6 +66,8 @@ 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.

5
src/nlsat/nlsat_solver.cpp
View file

@ -2074,14 +2074,11 @@ namespace nlsat {
if (best_literal == null_literal) if (best_literal == null_literal)
return satisfied; return satisfied;
return l_undef;
// 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.set_linear_project(true); m_explain.linear_project(1, &best_literal, m_lazy_clause);
m_explain.main_operator(1, &best_literal, m_lazy_clause);
m_explain.set_linear_project(false); // TODO: there should be a better way to control this.
m_lazy_clause.push_back(~best_literal); m_lazy_clause.push_back(~best_literal);
core.clear(); core.clear();