mirror of
https://github.com/Z3Prover/z3
synced 2025-11-22 05:36:41 +00:00
improve logging
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
7443b6e874
commit
b8fb10ecc6
6 changed files with 99 additions and 40 deletions
|
|
@ -2772,9 +2772,12 @@ namespace algebraic_numbers {
|
|||
return out;
|
||||
}
|
||||
|
||||
std::ostream& display_root_smt2(std::ostream & out, numeral const & a) {
|
||||
template<typename Printer>
|
||||
std::ostream& display_root_common(std::ostream & out, numeral const & a, char const* var_name, bool no_power, Printer&& printer) {
|
||||
SASSERT(var_name != nullptr);
|
||||
if (is_zero(a)) {
|
||||
out << "(root-obj x 1)";
|
||||
auto poly_printer = [&](std::ostream& dst) { dst << var_name; };
|
||||
return printer(out, poly_printer, 1u);
|
||||
}
|
||||
else if (a.is_basic()) {
|
||||
mpq const & v = basic_value(a);
|
||||
|
|
@ -2782,25 +2785,53 @@ namespace algebraic_numbers {
|
|||
qm().set(neg_n, v.numerator());
|
||||
qm().neg(neg_n);
|
||||
mpz coeffs[2] = { std::move(neg_n), qm().dup(v.denominator()) };
|
||||
out << "(root-obj ";
|
||||
upm().display_smt2(out, 2, coeffs, "x");
|
||||
out << " 1)"; // first root of the polynomial d*# - n
|
||||
auto poly_printer = [&](std::ostream& dst) {
|
||||
if (no_power)
|
||||
upm().display_smt2_no_power(dst, 2, coeffs, var_name);
|
||||
else
|
||||
upm().display_smt2(dst, 2, coeffs, var_name);
|
||||
};
|
||||
std::ostream& r = printer(out, poly_printer, 1u); // first root of d*x - n
|
||||
qm().del(coeffs[0]);
|
||||
qm().del(coeffs[1]);
|
||||
return r;
|
||||
}
|
||||
else {
|
||||
algebraic_cell * c = a.to_algebraic();
|
||||
out << "(root-obj ";
|
||||
upm().display_smt2(out, c->m_p_sz, c->m_p, "x");
|
||||
auto poly_printer = [&](std::ostream& dst) {
|
||||
if (no_power)
|
||||
upm().display_smt2_no_power(dst, c->m_p_sz, c->m_p, var_name);
|
||||
else
|
||||
upm().display_smt2(dst, c->m_p_sz, c->m_p, var_name);
|
||||
};
|
||||
if (c->m_i == 0) {
|
||||
// undefined
|
||||
c->m_i = upm().get_root_id(c->m_p_sz, c->m_p, lower(c)) + 1;
|
||||
}
|
||||
SASSERT(c->m_i > 0);
|
||||
out << " " << c->m_i;
|
||||
out << ")";
|
||||
return printer(out, poly_printer, c->m_i);
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& display_root_smt2(std::ostream & out, numeral const & a) {
|
||||
auto printer = [&](std::ostream& dst, auto const& poly_printer, unsigned idx) -> std::ostream& {
|
||||
dst << "(root-obj ";
|
||||
poly_printer(dst);
|
||||
dst << " " << idx << ")";
|
||||
return dst;
|
||||
};
|
||||
return display_root_common(out, a, "x", false, printer);
|
||||
}
|
||||
|
||||
std::ostream& display_root_smtrat(std::ostream & out, numeral const & a, char const* var_name) {
|
||||
SASSERT(var_name != nullptr);
|
||||
auto printer = [&](std::ostream& dst, auto const& poly_printer, unsigned idx) -> std::ostream& {
|
||||
dst << "(root ";
|
||||
poly_printer(dst);
|
||||
dst << " " << idx << " " << var_name << ")";
|
||||
return dst;
|
||||
};
|
||||
return display_root_common(out, a, var_name, true, printer);
|
||||
}
|
||||
|
||||
std::ostream& display_interval(std::ostream & out, numeral const & a) {
|
||||
|
|
@ -3167,6 +3198,10 @@ namespace algebraic_numbers {
|
|||
return m_imp->display_root_smt2(out, a);
|
||||
}
|
||||
|
||||
std::ostream& manager::display_root_smtrat(std::ostream & out, numeral const & a, char const* var_name) const {
|
||||
return m_imp->display_root_smtrat(out, a, var_name);
|
||||
}
|
||||
|
||||
void manager::reset_statistics() {
|
||||
m_imp->reset_statistics();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -345,6 +345,12 @@ namespace algebraic_numbers {
|
|||
*/
|
||||
std::ostream& display_root_smt2(std::ostream & out, numeral const & a) const;
|
||||
|
||||
/**
|
||||
\brief Display algebraic number using an SMT-RAT style root expression: (root p i x)
|
||||
where the final argument denotes the variable bound to this root.
|
||||
*/
|
||||
std::ostream& display_root_smtrat(std::ostream & out, numeral const & a, char const* var_name) const;
|
||||
|
||||
/**
|
||||
\brief Display algebraic number in Mathematica format.
|
||||
*/
|
||||
|
|
@ -495,4 +501,3 @@ inline std::ostream & operator<<(std::ostream & out, interval_pp const & n) {
|
|||
n.m.display_interval(out, n.n);
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1159,67 +1159,89 @@ namespace upolynomial {
|
|||
}
|
||||
}
|
||||
|
||||
static void display_smt2_var_power(std::ostream & out, char const * var_name, unsigned k, bool allow_power) {
|
||||
SASSERT(k > 0);
|
||||
if (k == 1) {
|
||||
out << var_name;
|
||||
}
|
||||
else if (allow_power) {
|
||||
out << "(^ " << var_name << " " << k << ")";
|
||||
}
|
||||
else {
|
||||
out << "(*";
|
||||
for (unsigned i = 0; i < k; ++i)
|
||||
out << " " << var_name;
|
||||
out << ")";
|
||||
}
|
||||
}
|
||||
|
||||
static void display_smt2_monomial(std::ostream & out, numeral_manager & m, mpz const & n,
|
||||
unsigned k, char const * var_name) {
|
||||
unsigned k, char const * var_name, bool allow_power) {
|
||||
if (k == 0) {
|
||||
display_smt2_mumeral(out, m, n);
|
||||
}
|
||||
else if (m.is_one(n)) {
|
||||
if (k == 1)
|
||||
out << var_name;
|
||||
else
|
||||
out << "(^ " << var_name << " " << k << ")";
|
||||
display_smt2_var_power(out, var_name, k, allow_power);
|
||||
}
|
||||
else {
|
||||
out << "(* ";
|
||||
display_smt2_mumeral(out, m, n);
|
||||
out << " ";
|
||||
if (k == 1)
|
||||
out << var_name;
|
||||
else
|
||||
out << "(^ " << var_name << " " << k << ")";
|
||||
display_smt2_var_power(out, var_name, k, allow_power);
|
||||
out << ")";
|
||||
}
|
||||
}
|
||||
|
||||
// Display p as an s-expression
|
||||
std::ostream& core_manager::display_smt2(std::ostream & out, unsigned sz, numeral const * p, char const * var_name) const {
|
||||
static std::ostream& display_smt2_core(std::ostream & out, core_manager const& cm, unsigned sz, numeral const * p, char const * var_name, bool allow_power) {
|
||||
if (sz == 0) {
|
||||
out << "0";
|
||||
return out;
|
||||
}
|
||||
|
||||
if (sz == 1) {
|
||||
display_smt2_mumeral(out, m(), p[0]);
|
||||
display_smt2_mumeral(out, cm.m(), p[0]);
|
||||
return out;
|
||||
}
|
||||
|
||||
unsigned non_zero_idx = UINT_MAX;
|
||||
unsigned num_non_zeros = 0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
if (m().is_zero(p[i]))
|
||||
if (cm.m().is_zero(p[i]))
|
||||
continue;
|
||||
non_zero_idx = i;
|
||||
num_non_zeros ++;
|
||||
}
|
||||
|
||||
if (num_non_zeros == 1) {
|
||||
SASSERT(non_zero_idx != UINT_MAX && non_zero_idx >= 1);
|
||||
display_smt2_monomial(out, m(), p[non_zero_idx], non_zero_idx, var_name);
|
||||
if (num_non_zeros == 1 && non_zero_idx != UINT_MAX) {
|
||||
if (non_zero_idx == 0) {
|
||||
display_smt2_mumeral(out, cm.m(), p[0]);
|
||||
return out;
|
||||
}
|
||||
display_smt2_monomial(out, cm.m(), p[non_zero_idx], non_zero_idx, var_name, allow_power);
|
||||
return out;
|
||||
}
|
||||
|
||||
out << "(+";
|
||||
unsigned i = sz;
|
||||
while (i > 0) {
|
||||
--i;
|
||||
if (!m().is_zero(p[i])) {
|
||||
if (!cm.m().is_zero(p[i])) {
|
||||
out << " ";
|
||||
display_smt2_monomial(out, m(), p[i], i, var_name);
|
||||
display_smt2_monomial(out, cm.m(), p[i], i, var_name, allow_power);
|
||||
}
|
||||
}
|
||||
return out << ")";
|
||||
}
|
||||
|
||||
// Display p as an s-expression
|
||||
std::ostream& core_manager::display_smt2(std::ostream & out, unsigned sz, numeral const * p, char const * var_name) const {
|
||||
return display_smt2_core(out, *this, sz, p, var_name, true);
|
||||
}
|
||||
|
||||
std::ostream& core_manager::display_smt2_no_power(std::ostream & out, unsigned sz, numeral const * p, char const * var_name) const {
|
||||
return display_smt2_core(out, *this, sz, p, var_name, false);
|
||||
}
|
||||
|
||||
bool core_manager::eq(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2) {
|
||||
if (sz1 != sz2)
|
||||
return false;
|
||||
|
|
@ -3117,4 +3139,3 @@ namespace upolynomial {
|
|||
return out;
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -468,6 +468,7 @@ namespace upolynomial {
|
|||
std::ostream& display_smt2(std::ostream & out, numeral_vector const & p, char const * var_name = "x") const {
|
||||
return display_smt2(out, p.size(), p.data(), var_name);
|
||||
}
|
||||
std::ostream& display_smt2_no_power(std::ostream & out, unsigned sz, numeral const * p, char const * var_name = "x") const;
|
||||
};
|
||||
|
||||
class scoped_set_z {
|
||||
|
|
@ -917,4 +918,3 @@ namespace upolynomial {
|
|||
};
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -295,14 +295,6 @@ namespace nlsat {
|
|||
if (maxx == null_var)
|
||||
return;
|
||||
SASSERT(m_assignment.is_assigned(maxx));
|
||||
|
||||
// Make sure its discriminant does not vanish at the model.
|
||||
polynomial_ref disc(m_pm);
|
||||
disc = discriminant(q, maxx);
|
||||
int const disc_sign = sign(disc);
|
||||
SASSERT(disc_sign != 0);
|
||||
if (disc_sign == 0)
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
undef_var_assignment partial(m_assignment, maxx);
|
||||
scoped_anum_vector & roots = m_roots_tmp;
|
||||
|
|
@ -319,7 +311,7 @@ namespace nlsat {
|
|||
}
|
||||
if (root_idx == 0)
|
||||
return; // there are no root functions and therefore no constraints aer generated
|
||||
|
||||
|
||||
TRACE(nlsat_explain,
|
||||
tout << "adding zero-assumption root literal for ";
|
||||
display_var(tout, maxx); tout << " using root[" << root_idx << "] of " << q << "\n";);
|
||||
|
|
|
|||
|
|
@ -3368,6 +3368,12 @@ namespace nlsat {
|
|||
m_am.to_rational(m_assignment.value(x), q);
|
||||
m_am.qm().display_smt2(out, q, false);
|
||||
}
|
||||
else if (m_log_lemma_smtrat) {
|
||||
std::ostringstream var_name;
|
||||
proc(var_name, x);
|
||||
std::string name = var_name.str();
|
||||
m_am.display_root_smtrat(out, m_assignment.value(x), name.c_str());
|
||||
}
|
||||
else {
|
||||
m_am.display_root_smt2(out, m_assignment.value(x));
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue