mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-02 07:16:17 +00:00
Code Activity

[WIP] Refactor NLSAT solver to use structured bindings for variable bounds (#8425)

Browse source 
* Initial plan

* Refactor NLSAT solver to use structured bindings for variable bounds

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-28 19:42:40 -08:00 • committed by GitHub
parent ebed679287
commit 0b1d30e86f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_solver.cpp
View file

@ -1979,9 +1979,7 @@ namespace nlsat {
<< " :propagations " << m_stats.m_propagations
<< " :clauses " << m_clauses.size()
<< " :learned " << m_learned.size() << ")\n");
for (auto const& b : bounds) {
var x = b.first;
rational lo = b.second;
for (auto const& [x, lo] : bounds) {
rational hi = lo + 1; // rational::one();
bool is_even = false;
polynomial_ref p(m_pm);