mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 13:56:03 +00:00
Code Activity

fix factorization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-08 08:32:28 -07:00
parent 5340b23d1b
commit 55ded3db60
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/nlsat/nlsat_solver.cpp
View file

@ -2937,7 +2937,8 @@ namespace nlsat {
void simplify_literals() { void simplify_literals() {
u_map<literal> b2l; u_map<literal> b2l;
scoped_literal_vector lits(m_solver); scoped_literal_vector lits(m_solver);
polynomial_ref_vector factors(m_pm); polynomial_ref p(m_pm);
polynomial::factors factors(m_pm);
ptr_buffer<poly> ps; ptr_buffer<poly> ps;
buffer<bool> is_even; buffer<bool> is_even;
unsigned num_atoms = m_atoms.size(); unsigned num_atoms = m_atoms.size();
@ -2949,10 +2950,11 @@ namespace nlsat {
is_even.reset(); is_even.reset();
for (unsigned i = 0; i < a.size(); ++i) { for (unsigned i = 0; i < a.size(); ++i) {
factors.reset(); factors.reset();
m_cache.factor(a.p(i), factors); p = a.p(i);
for (auto q : factors) { factor(p, factors);
ps.push_back(q); for (unsigned i = 0; i < factors.distinct_factors(); ++i) {
is_even.push_back(a.is_even(i)); ps.push_back(factors[i]);
is_even.push_back(a.is_even(i) || (factors.get_degree(i) % 2 == 0));
} }
} }
literal l = mk_ineq_literal(a.get_kind(), ps.size(), ps.data(), is_even.data(), true); literal l = mk_ineq_literal(a.get_kind(), ps.size(), ps.data(), is_even.data(), true);