mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

include linear moves

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-24 17:56:34 -07:00
parent d6b89ba2d5
commit 32c3a5af67
2 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/sls/sls_arith_base.cpp
View file

@ -1062,6 +1062,7 @@ namespace sls {
auto const& [w, c, monomial] = get_mul(v);
for (auto [w, p] : monomial)
i.m_nonlinear.push_back({ w, { {v, coeff, p} } });
i.m_is_linear = false;
}
else
i.m_nonlinear.push_back({ v, { { v, coeff, 1 } } });
@ -1755,7 +1756,14 @@ namespace sls {
find_quadratic_moves(*ineq, x, a, b, ineq->m_args_value);
else
;
}
}
if (!ineq->m_is_linear) {
for (auto const& [coeff, x] : ineq->m_args) {
if (is_fixed(x))
continue;
find_linear_moves(*ineq, x, coeff, ineq->m_args_value);
}
}
}
template<typename num_t>

1
src/ast/sls/sls_arith_base.h
View file

@ -63,6 +63,7 @@ namespace sls {
vector<std::pair<var_t, vector<nonlinear_coeff>>> m_nonlinear;
ineq_kind m_op = ineq_kind::LE;
num_t m_args_value;
bool m_is_linear = true;
bool is_true() const;
std::ostream& display(std::ostream& out) const;