mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-06 19:12:45 +00:00
Code Activity

add parameter to suppress/enable levelwise

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-03 12:54:53 -07:00
parent e7888b303b
commit a9d7a307ba
4 changed files with 14 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/nlsat/levelwise.cpp
View file

@ -155,12 +155,9 @@ namespace nlsat {
- For factors with level == m_n: add an_del(p) and isolate their indexed roots over the sample;
sort those roots and for each adjacent pair coming from distinct polynomials add
ord_inv(resultant(p_j, p_{j+1})) to Q.
- If any constructed polynomial (resultant, discriminant, etc.) is nullified on the sample,
fail immediately.
- If any constructed polynomial is nullified on the sample, that is all coefficients are zeroes, then fail.
Result: Q = { sgn_inv(p) | level(p) < m_n }
∪ { an_del(p) | level(p) == m_n }
∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }.
Result: Q = { sgn_inv(p) | level(p) < m_n } ∪ { an_del(p) | level(p) == m_n } ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }.
*/
// Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
void collect_level_properties(std::vector<poly*> & ps_of_n_level) {
@ -342,8 +339,6 @@ namespace nlsat {
}
collect_E(p_non_null);
// Ensure m_I can hold interval for this level
SASSERT(m_I.size() > m_level);
std::sort(m_E.begin(), m_E.end(), [&](root_function const& a, root_function const& b){
return m_am.lt(a.val, b.val);
});

11
src/nlsat/nlsat_explain.cpp
View file

@ -1146,8 +1146,10 @@ namespace nlsat {
var x = m_todo.extract_max_polys(ps);
if (!levelwise_single_cell(ps, max_x)) { // on levelwise_single_cell failure continue with cdcac
polynomial_ref_vector samples(m_pm);
if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x))
return;
polynomial_ref_vector samples(m_pm);
polynomial_ref_vector samples(m_pm);
if (x < max_x)
@ -1692,9 +1694,10 @@ namespace nlsat {
SASSERT(check_already_added());
SASSERT(num > 0);
TRACE(nlsat_explain,
tout << "[explain] set of literals is infeasible in the current interpretation\n";
tout << "the infeasible clause:\n";
display(tout, m_solver, num, ls) << "\n";
m_solver.display_assignment(tout);
m_solver.display_assignment(tout << "assignment:\n");
);
if (max_var(num, ls) == 0 && !m_assignment.is_assigned(0)) {
TRACE(nlsat_explain, tout << "all literals use unassigned max var; returning justification\n";);

6
src/nlsat/nlsat_solver.cpp
View file

@ -244,7 +244,7 @@ namespace nlsat {
// statistics
stats m_stats;
std::string m_debug_known_solution_file_name;
bool m_apply_lws;
imp(solver& s, ctx& c):
m_ctx(c),
m_solver(s),
@ -304,6 +304,7 @@ namespace nlsat {
m_check_lemmas = p.check_lemmas();
m_variable_ordering_strategy = p.variable_ordering_strategy();
m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
m_apply_lws = p.apply_levelwise();
m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
m_cell_sample = p.cell_sample();
@ -4621,6 +4622,7 @@ namespace nlsat {
assumption solver::join(assumption a, assumption b) {
return (m_imp->m_asm.mk_join(static_cast<imp::_assumption_set>(a), static_cast<imp::_assumption_set>(b)));
}
bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
};

2
src/nlsat/nlsat_solver.h
View file

@ -246,7 +246,7 @@ namespace nlsat {
static void collect_param_descrs(param_descrs & d);
const assignment& sample() const;
assignment& sample();
bool apply_levelwise() const;
void reset();
void collect_statistics(statistics & st);
void reset_statistics();