mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-27 20:38:42 +00:00
Code Activity

remove unused functionality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-23 08:58:05 -08:00
parent cc0def2309
commit c32b6135a1
3 changed files with 23 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/nla_coi.cpp
View file

@ -1,4 +1,12 @@
/*++
Copyright (c) 2025 Microsoft Corporation
Author:
Lev Nachmanson (levnach)
Nikolaj Bjorner (nbjorner)
--*/
#include "math/lp/nla_core.h"
#include "math/lp/nla_coi.h"

13
src/math/lp/nla_coi.h
View file

@ -1,4 +1,17 @@
/*++
Copyright (c) 2025 Microsoft Corporation
Abstract:
Class for computing the cone of influence for NL constraints.
It includes variables that come from monomials that have incorrect evaluation and
transitively all constraints and variables that are connected.
Author:
Lev Nachmanson (levnach)
Nikolaj Bjorner (nbjorner)
--*/
#pragma once
namespace nla {

26
src/math/lp/nra_solver.cpp
View file

@ -26,11 +26,6 @@ typedef nla::mon_eq mon_eq;
typedef nla::variable_map_type variable_map_type;
struct solver::imp {
struct model_bound {
lp::lpvar v;
rational r;
bool is_lower;
};
lp::lar_solver& lra;
reslimit& m_limit;
@ -41,8 +36,6 @@ struct solver::imp {
scoped_ptr<scoped_anum> m_tmp1, m_tmp2;
nla::coi m_coi;
nla::core& m_nla_core;
unsigned m_max_constraint_index = 0;
vector<model_bound> m_model_bounds;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core):
lra(s),
@ -61,8 +54,6 @@ struct solver::imp {
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
m_values = alloc(scoped_anum_vector, am());
m_lp2nl.reset();
m_model_bounds.reset();
m_max_constraint_index = 0;
}
// Create polynomial definition for variable v used in setup_assignment_solver.
@ -255,19 +246,8 @@ struct solver::imp {
m_nlsat->get_core(core);
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
for (auto c : core) {
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
TRACE(nra, tout << "core index " << idx << " " << m_max_constraint_index << "\n");
if (idx <= m_max_constraint_index)
ex.push_back(idx);
else {
idx -= m_max_constraint_index;
auto const& [v, bound, is_lower] = m_model_bounds[idx];
TRACE(nra, tout << "bound violated for v" << v << (is_lower ? " >= " : " <= ") << bound << "\n");
if (is_lower)
lemma |= nla::ineq(v, lp::lconstraint_kind::LE, bound - 1);
else
lemma |= nla::ineq(v, lp::lconstraint_kind::GE, bound + 1);
}
unsigned idx = static_cast<unsigned>(static_cast<imp *>(c) - this);
ex.push_back(idx);
}
lemma &= ex;
@ -334,7 +314,6 @@ struct solver::imp {
}
void add_constraint(unsigned idx) {
m_max_constraint_index = std::max(m_max_constraint_index, idx);
auto& c = lra.constraints()[idx];
auto& pm = m_nlsat->pm();
auto k = c.kind();
@ -359,7 +338,6 @@ struct solver::imp {
}
nlsat::literal add_constraint(polynomial::polynomial *p, unsigned idx, lp::lconstraint_kind k) {
m_max_constraint_index = std::max(m_max_constraint_index, idx);
polynomial::polynomial *ps[1] = {p};
bool is_even[1] = {false};
nlsat::literal lit;