mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 17:38:45 +00:00
Code Activity

Add root method (syntax sugar for isolate_roots)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-10 12:23:37 -08:00
parent 1a7d39f9a0
commit 71ab7759d1
1 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/realclosure/realclosure.cpp
View file

@ -800,6 +800,11 @@ namespace realclosure {
a.m_value = 0; a.m_value = 0;
} }
void del(numeral_vector & v) {
for (unsigned i = 0; i < v.size(); i++)
del(v[i]);
}
/** /**
\brief Return true if the given interval is smaller than 1/2^k \brief Return true if the given interval is smaller than 1/2^k
*/ */
@ -2261,7 +2266,18 @@ namespace realclosure {
p.push_back(0); p.push_back(0);
p.push_back(one()); p.push_back(one());
// TODO: invoke isolate_roots numeral_vector roots;
nz_isolate_roots(p.size(), p.c_ptr(), roots);
SASSERT(roots.size() == 1 || roots.size() == 2);
if (roots.size() == 1 || sign(roots[0].m_value) > 0) {
set(b, roots[0]);
}
else {
SASSERT(roots.size() == 2);
SASSERT(sign(roots[1].m_value) > 0);
set(b, roots[1]);
}
del(roots);
} }
/** /**