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

Add nlsat.factor option. This is a workaround for the slow factorization procedure.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-02 21:18:02 -08:00
parent 8a69e8a283
commit 70baa3c8c9
4 changed files with 25 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/nlsat/nlsat_explain.cpp
View file

@ -42,7 +42,8 @@ namespace nlsat {
bool m_simplify_cores; bool m_simplify_cores;
bool m_full_dimensional; bool m_full_dimensional;
bool m_minimize_cores; bool m_minimize_cores;
bool m_factor;
struct todo_set { struct todo_set {
polynomial::cache & m_cache; polynomial::cache & m_cache;
polynomial_ref_vector m_set; polynomial_ref_vector m_set;
@ -568,21 +569,22 @@ namespace nlsat {
elim_vanishing(p); elim_vanishing(p);
if (is_const(p)) if (is_const(p))
return; return;
#if 1 if (m_factor) {
TRACE("nlsat_explain", tout << "adding factors of\n"; display(tout, p); tout << "\n";); TRACE("nlsat_explain", tout << "adding factors of\n"; display(tout, p); tout << "\n";);
factor(p, m_factors); factor(p, m_factors);
polynomial_ref f(m_pm); polynomial_ref f(m_pm);
for (unsigned i = 0; i < m_factors.size(); i++) { for (unsigned i = 0; i < m_factors.size(); i++) {
f = m_factors.get(i); f = m_factors.get(i);
elim_vanishing(f); elim_vanishing(f);
if (!is_const(f)) { if (!is_const(f)) {
TRACE("nlsat_explain", tout << "adding factor:\n"; display(tout, f); tout << "\n";); TRACE("nlsat_explain", tout << "adding factor:\n"; display(tout, f); tout << "\n";);
m_todo.insert(f); m_todo.insert(f);
}
} }
} }
#else else {
m_todo.insert(normalize(p)); m_todo.insert(p);
#endif }
} }
/** /**
@ -1344,6 +1346,10 @@ namespace nlsat {
m_imp->m_minimize_cores = f; m_imp->m_minimize_cores = f;
} }
void explain::set_factor(bool f) {
m_imp->m_factor = f;
}
void explain::operator()(unsigned n, literal const * ls, scoped_literal_vector & result) { void explain::operator()(unsigned n, literal const * ls, scoped_literal_vector & result) {
(*m_imp)(n, ls, result); (*m_imp)(n, ls, result);
} }

1
src/nlsat/nlsat_explain.h
View file

@ -40,6 +40,7 @@ namespace nlsat {
void set_simplify_cores(bool f); void set_simplify_cores(bool f);
void set_full_dimensional(bool f); void set_full_dimensional(bool f);
void set_minimize_cores(bool f); void set_minimize_cores(bool f);
void set_factor(bool f);
/** /**
\brief Given a set of literals ls[0], ... ls[n-1] s.t. \brief Given a set of literals ls[0], ... ls[n-1] s.t.

4
src/nlsat/nlsat_params.pyg
View file

@ -10,5 +10,7 @@ def_module_params('nlsat',
('randomize', BOOL, True, "randomize selection of a witness in nlsat."), ('randomize', BOOL, True, "randomize selection of a witness in nlsat."),
('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts."), ('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts."),
('shuffle_vars', BOOL, False, "use a random variable order."), ('shuffle_vars', BOOL, False, "use a random variable order."),
('seed', UINT, 0, "random seed."))) ('seed', UINT, 0, "random seed."),
('factor', BOOL, True, "factor polynomials produced during conflict resolution.")
))

1
src/nlsat/nlsat_solver.cpp
View file

@ -212,6 +212,7 @@ namespace nlsat {
m_ism.set_seed(m_random_seed); m_ism.set_seed(m_random_seed);
m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_simplify_cores(m_simplify_cores);
m_explain.set_minimize_cores(min_cores); m_explain.set_minimize_cores(min_cores);
m_explain.set_factor(p.factor());
m_am.updt_params(p.p); m_am.updt_params(p.p);
} }