mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-21 09:34:43 +00:00
Code Activity

hook up different relation build strategies for lws

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-09 14:33:59 -10:00
parent 946f209b4c
commit d87d1d009f
4 changed files with 23 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/nlsat/levelwise.cpp
View file

@ -103,6 +103,21 @@ struct levelwise::impl {
m_I.reserve(m_n);
for (unsigned i = 0; i < m_n; ++i)
m_I.emplace_back(m_pm);
switch (m_solver.lws_relation_mode()) {
case 0:
m_relation_mode = biggest_cell;
break;
case 1:
m_relation_mode = chain;
break;
case 2:
m_relation_mode = lowest_degree;
break;
default:
m_relation_mode = chain;
break;
}
}
void fail() { throw nullified_poly_exception(); }
@ -289,7 +304,8 @@ struct levelwise::impl {
for (unsigned j = l + 1; j < n; ++j)
m_rel.add_pair(j - 1, j);
break;
case lowest_degree: {
case lowest_degree:
{
std::vector<unsigned> degs;
degs.reserve(n);
for (unsigned i = 0; i < n; ++i)

1
src/nlsat/nlsat_params.pyg
View file

@ -24,5 +24,6 @@ def_module_params('nlsat',
('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."),
('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
('lws', BOOL, True, "apply levelwise."),
('lws_rel_mode', UINT, 1, "relation mode for levelwise: 0 for biggest_cell, 1 for chain, 2 for lowest_degree"),
('canonicalize', BOOL, True, "canonicalize polynomials.")
))

4
src/nlsat/nlsat_solver.cpp
View file

@ -248,6 +248,7 @@ namespace nlsat {
stats m_stats;
std::string m_debug_known_solution_file_name;
bool m_apply_lws;
unsigned m_lws_relation_mode = 1;
imp(solver& s, ctx& c):
m_ctx(c),
m_solver(s),
@ -308,6 +309,7 @@ namespace nlsat {
m_variable_ordering_strategy = p.variable_ordering_strategy();
m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
m_apply_lws = p.lws();
m_lws_relation_mode = p.lws_rel_mode();
m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
m_cell_sample = p.cell_sample();
@ -4636,5 +4638,7 @@ namespace nlsat {
bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
unsigned solver::lws_relation_mode() const { return m_imp->m_lws_relation_mode; }
};

1
src/nlsat/nlsat_solver.h
View file

@ -248,6 +248,7 @@ namespace nlsat {
const assignment& sample() const;
assignment& sample();
bool apply_levelwise() const;
unsigned lws_relation_mode() const;
void reset();
void collect_statistics(statistics & st);
void reset_statistics();