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

fix the build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-25 14:19:51 -10:00
parent 7ffc5d9eb1
commit e84844a873
2 changed files with 2 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

72
src/nlsat/nlsat_explain.cpp
View file

@ -54,76 +54,6 @@ namespace nlsat {
assignment const & sample() const { return m_solver.sample(); }
assignment & sample() { return m_solver.sample(); }
struct todo_set {
polynomial::cache & m_cache;
polynomial_ref_vector m_set;
svector<char> m_in_set;
todo_set(polynomial::cache & u):m_cache(u), m_set(u.pm()) {}
void reset() {
pmanager & pm = m_set.m();
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; ++i) {
m_in_set[pm.id(m_set.get(i))] = false;
}
m_set.reset();
}
void insert(poly * p) {
pmanager & pm = m_set.m();
p = m_cache.mk_unique(p);
unsigned pid = pm.id(p);
if (m_in_set.get(pid, false))
return;
m_in_set.setx(pid, true, false);
m_set.push_back(p);
}
bool empty() const { return m_set.empty(); }
// Return max variable in todo_set
var max_var() const {
pmanager & pm = m_set.m();
var max = null_var;
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; ++i) {
var x = pm.max_var(m_set.get(i));
SASSERT(x != null_var);
if (max == null_var || x > max)
max = x;
}
return max;
}
/**
\brief Remove the maximal polynomials from the set and store
them in max_polys. Return the maximal variable
*/
var extract_max_polys(polynomial_ref_vector & max_polys) {
max_polys.reset();
var x = max_var();
pmanager & pm = m_set.m();
unsigned sz = m_set.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; ++i) {
poly * p = m_set.get(i);
var y = pm.max_var(p);
SASSERT(y <= x);
if (y == x) {
max_polys.push_back(p);
m_in_set[pm.id(p)] = false;
}
else {
m_set.set(j, p);
j++;
}
}
m_set.shrink(j);
return x;
}
};
// temporary field for store todo set of polynomials
todo_set m_todo;
@ -774,7 +704,7 @@ namespace nlsat {
auto c = polynomial_ref(this->m_pm);
for (unsigned j = 0; j <= n; ++j) {
c = m_pm.coeff(s, x, j);
if (sign(c, sample(), m_am) != 0)
if (nlsat::sign(c, sample(), m_am) != 0)
return false;
}
return true;

2
src/nlsat/nlsat_solver.cpp
View file

@ -1143,7 +1143,7 @@ namespace nlsat {
// Create a separate reslimit for the checker with 10 second timeout
reslimit checker_rlimit;
cancel_eh<reslimit> eh(checker_rlimit);
scoped_timer timer(10000, &eh);
scoped_timer timer(1000, &eh);
ctx c(checker_rlimit, m_ctx.m_params, m_ctx.m_incremental);
solver solver2(c);