mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

improved diagnostics

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-22 16:23:47 -08:00
parent 8d4e7fac6b
commit 125a82bea5
3 changed files with 43 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nra_solver.cpp
View file

@ -158,6 +158,8 @@ struct solver::imp {
for (unsigned i : m_term_set)
add_term(i);
TRACE("nra", m_nlsat->display(tout));
lbool r = l_undef;
try {
r = m_nlsat->check();
@ -200,7 +202,7 @@ struct solver::imp {
for (auto c : core) {
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
ex.push_back(idx);
TRACE("arith", tout << "ex: " << idx << "\n";);
TRACE("nra", lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";);
}
nla::new_lemma lemma(m_nla_core, __FUNCTION__);
lemma &= ex;

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

@ -1285,10 +1285,7 @@ namespace polynomial {
}
});
monomial_table new_table;
monomial_table::iterator it = m_monomials.begin();
monomial_table::iterator end = m_monomials.end();
for (; it != end; ++it) {
monomial * m = *it;
for (monomial * m : m_monomials) {
m->rename(sz, xs);
SASSERT(!new_table.contains(m));
new_table.insert(m);

63
src/nlsat/nlsat_solver.cpp
View file

@ -810,15 +810,20 @@ namespace nlsat {
void check_lemma(unsigned n, literal const* cls, bool is_valid, assumption_set a) {
TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n";
display(tout););
IF_VERBOSE(0, display(verbose_stream() << "check lemma: ", n, cls) << "\n");
IF_VERBOSE(0, display(verbose_stream() << "check lemma " << (is_valid?"valid: ":"consequence: "), n, cls) << "\n");
for (clause* c : m_learned) IF_VERBOSE(1, display(verbose_stream() << "lemma: ", *c) << "\n");
solver solver2(m_ctx);
scoped_suspend_rlimit _limit(m_rlimit);
ctx c(m_rlimit, m_ctx.m_params, m_ctx.m_incremental);
solver solver2(c);
imp& checker = *(solver2.m_imp);
checker.m_check_lemmas = false;
checker.m_log_lemmas = false;
checker.m_inline_vars = false;
auto pconvert = [&](poly* p) {
return convert(m_pm, p, checker.m_pm);
};
// need to translate Boolean variables and literals
scoped_bool_vars tr(checker);
for (var x = 0; x < m_is_int.size(); ++x) {
@ -834,10 +839,10 @@ namespace nlsat {
else if (a->is_ineq_atom()) {
ineq_atom& ia = *to_ineq_atom(a);
unsigned sz = ia.size();
ptr_vector<poly> ps;
polynomial_ref_vector ps(checker.m_pm);
bool_vector is_even;
for (unsigned i = 0; i < sz; ++i) {
ps.push_back(ia.p(i));
ps.push_back(pconvert(ia.p(i)));
is_even.push_back(ia.is_even(i));
}
bv = checker.mk_ineq_atom(ia.get_kind(), sz, ps.data(), is_even.data());
@ -847,7 +852,7 @@ namespace nlsat {
if (r.x() >= max_var(r.p())) {
// permutation may be reverted after check completes,
// but then root atoms are not used in lemmas.
bv = checker.mk_root_atom(r.get_kind(), r.x(), r.i(), r.p());
bv = checker.mk_root_atom(r.get_kind(), r.x(), r.i(), pconvert(r.p()));
}
}
else {
@ -872,7 +877,6 @@ namespace nlsat {
literal nlit(tr[lit.var()], !lit.sign());
checker.mk_clause(1, &nlit, nullptr);
}
IF_VERBOSE(0, verbose_stream() << "check\n";);
lbool r = checker.check();
if (r == l_true) {
for (bool_var b : tr) {
@ -902,15 +906,21 @@ namespace nlsat {
TRACE("nlsat", display(tout << "violdated tautology clause: ", *c) << "\n";);
}
}
throw default_exception("lemma did not check");
UNREACHABLE();
}
}
void log_lemma(std::ostream& out, clause const& cls) {
display_smt2(out);
log_lemma(out, cls.size(), cls.data(), false);
}
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
if (!is_valid)
display_smt2(out);
out << "(assert (not ";
display_smt2(out, cls) << "))\n";
display(out << "(echo \"#" << m_lemma_count << " ", cls) << "\")\n";
display_smt2(out, n, cls) << "))\n";
display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n";
out << "(check-sat)\n(reset)\n";
}
@ -935,7 +945,7 @@ namespace nlsat {
if (learned && m_log_lemmas) {
log_lemma(verbose_stream(), *cls);
}
if (learned && m_check_lemmas) {
if (learned && m_check_lemmas && false) {
check_lemma(cls->size(), cls->data(), false, cls->assumptions());
}
if (learned)
@ -1634,7 +1644,7 @@ namespace nlsat {
restore_order();
}
CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout););
CTRACE("nlsat", r == l_false, display(tout););
CTRACE("nlsat", r == l_false, display(tout << "unsat\n"););
SASSERT(r != l_true || check_satisfied(m_clauses));
return r;
}
@ -1838,6 +1848,8 @@ namespace nlsat {
display(tout, m_lazy_clause.size(), m_lazy_clause.data()) << "\n";);
if (m_check_lemmas) {
check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), true, nullptr);
log_lemma(verbose_stream(), m_lazy_clause.size(), m_lazy_clause.data(), true);
m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr));
}
@ -2076,7 +2088,7 @@ namespace nlsat {
TRACE("nlsat", tout << "new lemma:\n"; display(tout, m_lemma.size(), m_lemma.data()); tout << "\n";
tout << "found_decision: " << found_decision << "\n";);
if (false && m_check_lemmas) {
if (m_check_lemmas) {
check_lemma(m_lemma.size(), m_lemma.data(), false, m_lemma_assumptions.get());
}
@ -2371,13 +2383,9 @@ namespace nlsat {
}
bool can_reorder() const {
for (clause* c : m_learned) {
if (has_root_atom(*c)) return false;
}
for (clause* c : m_clauses) {
if (has_root_atom(*c)) return false;
}
return m_patch_var.empty();
return m_patch_var.empty()
&& all_of(m_learned, [&](clause* c) { return !has_root_atom(*c); })
&& all_of(m_clauses, [&](clause* c) { return !has_root_atom(*c); });
}
/**
@ -2900,7 +2908,8 @@ namespace nlsat {
var mx = max_var(p0);
if (mx >= m_is_int.size()) return false;
for (var x = 0; x <= mx; ++x) {
if (m_is_int[x]) continue;
if (is_int(x))
continue;
if (1 == m_pm.degree(p0, x)) {
p = m_pm.coeff(p0, x, 1, q);
if (!m_pm.is_const(p))
@ -2944,10 +2953,10 @@ namespace nlsat {
unsigned sz = m_atoms.size();
for (bool_var b = 0; b < sz; b++) {
if (m_atoms[b] == nullptr && m_bvalues[b] != l_undef) {
out << "b" << b << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << "\n";
out << "b" << b << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << " @" << m_levels[b] << "\n";
}
else if (m_atoms[b] != nullptr && m_bvalues[b] != l_undef) {
display(out << "b" << b << " ", *m_atoms[b]) << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << "\n";
display(out << "b" << b << " ", *m_atoms[b]) << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << " @" << m_levels[b] << "\n";
}
}
TRACE("nlsat_bool_assignment",
@ -3330,6 +3339,12 @@ namespace nlsat {
return display(out, c, m_display_var);
}
std::ostream& display_smt2(std::ostream & out, unsigned n, literal const* ls) const {
return display_smt2(out, n, ls, display_var_proc());
}
std::ostream& display_smt2(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const {
if (num == 0) {
out << "false";
@ -3486,7 +3501,7 @@ namespace nlsat {
std::ostream& display_smt2_arith_decls(std::ostream & out) const {
unsigned sz = m_is_int.size();
for (unsigned i = 0; i < sz; i++) {
if (m_is_int[i])
if (is_int(i))
out << "(declare-fun x" << i << " () Int)\n";
else
out << "(declare-fun x" << i << " () Real)\n";