mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Add more tracing to sign_det_isolate_roots

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-10 09:17:22 -08:00
parent eca78aa9c6
commit 872165fa55
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1820,6 +1820,7 @@ namespace realclosure {
} }
TRACE("rcf_sign_det", TRACE("rcf_sign_det",
tout << "Final state\n"; tout << "Final state\n";
display_poly(tout, p_sz, p); tout << "\n";
tout << M_s; tout << M_s;
for (unsigned j = 0; j < scs.size(); j++) { for (unsigned j = 0; j < scs.size(); j++) {
display_sign_conditions(tout, scs[j]); display_sign_conditions(tout, scs[j]);
@ -1828,6 +1829,10 @@ namespace realclosure {
tout << "qs:\n"; tout << "qs:\n";
for (unsigned j = 0; j < qs.size(); j++) { for (unsigned j = 0; j < qs.size(); j++) {
display_poly(tout, qs.size(j), qs.coeffs(j)); tout << "\n"; display_poly(tout, qs.size(j), qs.coeffs(j)); tout << "\n";
}
tout << "prs:\n";
for (unsigned j = 0; j < prs.size(); j++) {
display_poly(tout, prs.size(j), prs.coeffs(j)); tout << "\n";
}); });
// TODO: create the extension objects using // TODO: create the extension objects using