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

gcd reduce and use c().val for sign constraints

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-01 18:42:34 -07:00
parent 018cb3c734
commit e709885e72
3 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.clang-format
View file

@ -8,7 +8,7 @@ BasedOnStyle: LLVM
IndentWidth: 4
TabWidth: 4
UseTab: Never
IndentCaseLabels: false

12
src/math/lp/nla_stellensatz.cpp
View file

@ -308,8 +308,8 @@ namespace nla {
}
bound_assumptions bounds{"units"};
for (auto v : vars) {
if (m_values[v] == 1 || m_values[v] == -1) {
bound_assumption b(v, lp::lconstraint_kind::EQ, m_values[v]);
if (c().val(v) == 1 || c().val(v) == -1) {
bound_assumption b(v, lp::lconstraint_kind::EQ, c().val(v));
bounds.bounds.push_back(b);
}
}
@ -396,7 +396,7 @@ namespace nla {
rational stellensatz::mvalue(lp::lar_term const &t) const {
rational r(0);
for (auto cv : t)
r += m_values[cv.j()] * cv.coeff();
r += c().val(cv.j()) * cv.coeff();
return r;
}
@ -474,6 +474,7 @@ namespace nla {
}
}
bool stellensatz::is_new_inequality(vector<std::pair<rational, lpvar>> lhs, lp::lconstraint_kind k,
rational const &rhs) {
std::stable_sort(lhs.begin(), lhs.end(),
@ -487,6 +488,7 @@ namespace nla {
return true;
}
lp::constraint_index stellensatz::add_ineq(
justification const& just, lp::lar_term & t, lp::lconstraint_kind k,
rational const & rhs_) {
@ -494,6 +496,7 @@ namespace nla {
auto coeffs = t.coeffs_as_vector();
gcd_normalize(coeffs, k, rhs);
if (!is_new_inequality(coeffs, k, rhs))
return lp::null_ci;
@ -546,7 +549,6 @@ namespace nla {
for (auto ci : constraints.indices())
insert_monomials_from_constraint(ci);
auto &constraints = m_solver.lra().constraints();
unsigned initial_false_constraints = m_false_constraints.size();
for (unsigned it = 0; it < m_false_constraints.size(); ++it) {
@ -562,6 +564,7 @@ namespace nla {
continue;
for (auto v : vars) {
if (v >= m_occurs.size())
continue;
for (unsigned cidx = 0; cidx < m_occurs[v].size(); ++cidx) {
@ -598,6 +601,7 @@ namespace nla {
// Eventually it can saturate to full pseudo-elimination of mx.
// or better: a conflict or a solution.
IF_VERBOSE(3, verbose_stream() << "saturate2\n");
auto &constraints = m_solver.lra().constraints();
for (auto ci : constraints.indices())

1
src/math/lp/nla_stellensatz.h
View file

@ -211,6 +211,7 @@ namespace nla {
lbool add_bounds(svector<lpvar> const &vars, vector<bound_assumption> &bounds);
void saturate_constraints();
void saturate_constraints2();
void eliminate(lpvar mi);
void ext_resolve(lpvar j, lp::constraint_index lo, lp::constraint_index hi);