mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 13:39:28 +00:00
Code Activity

add smt debug output for nla_core

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-09-21 19:23:42 +03:00
parent ce53e06e29
commit dcdae5a61c
3 changed files with 124 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -1381,6 +1381,8 @@ lbool core::check() {
TRACE(nla_solver, tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";);
IF_VERBOSE(5, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
CTRACE(nla_solver, ret == l_undef, tout << "Monomials\n"; print_monics(tout););
CTRACE(nla_solver, ret == l_undef, display_smt(tout););
// if (ret == l_undef) IF_VERBOSE(0, display_smt(verbose_stream()));
return ret;
}

4
src/math/lp/nla_core.h
View file

@ -115,6 +115,9 @@ class core {
bool is_pseudo_linear(monic const& m) const;
void refine_pseudo_linear(monic const& m);
std::ostream& display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const;
std::ostream& display_declarations_smt(std::ostream& out) const;
public:
// constructor
core(lp::lar_solver& s, params_ref const& p, reslimit&);
@ -230,6 +233,7 @@ public:
std::ostream & display_row(std::ostream& out, lp::row_strip<lp::mpq> const& row) const;
std::ostream & display(std::ostream& out);
std::ostream& display_smt(std::ostream& out);
std::ostream & print_ineq(const ineq & in, std::ostream & out) const;
std::ostream & print_var(lpvar j, std::ostream & out) const;
std::ostream & print_monics(std::ostream & out) const;

118
src/math/lp/nla_pp.cpp
View file

@ -315,4 +315,122 @@ std::ostream& core::display(std::ostream& out) {
for (auto& m : m_emons)
print_monic(m, out);
return out;
}
std::ostream& core::display_smt(std::ostream& out) {
out << "(set-option :unsat_core true)\n";
display_declarations_smt(out);
unsigned id = 0;
for (auto& c : lra.constraints().active())
display_constraint_smt(out, id++, c);
out << "(check-sat)\n";
out << "(get-unsat-core)\n";
out << "(reset)\n";
return out;
}
std::ostream& core::display_declarations_smt(std::ostream& out) const {
for (unsigned v = 0; v < lra.column_count(); ++v) {
if (is_monic_var(v)) {
out << "(define-const x" << v << " ";
out << (lra.var_is_int(v) ? "Int" : "Real");
auto const& m = m_emons[v];
out << " (*";
for (auto w : m.vars())
out << " x" << w;
out << ")";
out << "); " << val(v) << " = ";
rational p(1);
for (auto w : m.vars())
p *= val(v);
out << p;
out << "\n";
}
else {
out << "(declare-const x" << v << " ";
out << (lra.var_is_int(v) ? "Int" : "Real");
out << "); " << val(v) << "\n";
}
}
return out;
}
std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const {
auto k = c.kind();
auto rhs = c.rhs();
auto lhs = c.coeffs();
auto sz = lhs.size();
rational den = denominator(rhs);
for (auto [coeff, v] : lhs)
den = lcm(den, denominator(coeff));
rhs *= den;
auto value_of = [&](lp::lpvar v) {
if (is_monic_var(v)) {
auto& m = m_emons[v];
rational p(1);
for (auto w : m.vars())
p *= val(w);
return p;
}
return val(v);
};
switch (k) {
case lp::lconstraint_kind::LE:
out << "(assert (! (<= ";
break;
case lp::lconstraint_kind::GE:
out << "(assert (! (>= ";
break;
case lp::lconstraint_kind::LT:
out << "(assert (! (< ";
break;
case lp::lconstraint_kind::GT:
out << "(assert (! (> ";
break;
case lp::lconstraint_kind::EQ:
out << "(assert (! (= ";
break;
default:
UNREACHABLE(); // unreachable
}
rational lhs_val(0);
if (lhs.size() > 1)
out << "(+";
for (auto [coeff, v] : lhs) {
auto c = coeff * den;
if (c == 1)
out << " x" << v;
else
out << " (* " << c << " x" << v << ")";
lhs_val += value_of(v) * c;
}
if (lhs.size() > 1)
out << ")";
out << " " << rhs << ") :named a" << id << ")); ";
bool evaluation = true;
switch (k) {
case lp::lconstraint_kind::LE:
evaluation = lhs_val <= rhs;
break;
case lp::lconstraint_kind::GE:
evaluation = lhs_val >= rhs;
break;
case lp::lconstraint_kind::LT:
evaluation = lhs_val < rhs;
break;
case lp::lconstraint_kind::GT:
evaluation = lhs_val > rhs;
break;
case lp::lconstraint_kind::EQ:
evaluation = lhs_val == rhs;
break;
default:
UNREACHABLE(); // unreachable
}
out << (evaluation ? "true" : "false");
out << "\n";
return out;
}