mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

re-introduce option to dump arithmetic lemmas to std-out

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-14 13:54:56 -08:00
parent 8515cebd19
commit 31d4ba0009
5 changed files with 37 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/theory_arith_params.cpp
View file

@ -37,6 +37,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
m_arith_auto_config_simplex = p.arith_auto_config_simplex();
m_arith_validate = p.arith_validate();
m_arith_dump_lemmas = p.arith_dump_lemmas();
m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials();
m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds();
m_nl_arith_cross_nested = p.arith_nl_cross_nested();
@ -97,4 +98,5 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_nl_arith_optimize_bounds);
DISPLAY_PARAM(m_nl_arith_cross_nested);
DISPLAY_PARAM(m_arith_validate);
DISPLAY_PARAM(m_arith_dump_lemmas);
}

1
src/smt/params/theory_arith_params.h
View file

@ -83,6 +83,7 @@ struct theory_arith_params {
unsigned m_arith_propagation_threshold = UINT_MAX;
bool m_arith_validate = false;
bool m_arith_dump_lemmas = false;
arith_pivot_strategy m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_SMALLEST;
// used in diff-logic

2
src/smt/smt_context.h
View file

@ -1469,7 +1469,7 @@ namespace smt {
unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
literal consequent = false_literal, symbol const& logic = symbol::null) const;
literal consequent = false_literal, symbol const& logic = symbol::null, enode* x = nullptr, enode* y = nullptr) const;
unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,

7
src/smt/smt_context_pp.cpp
View file

@ -456,6 +456,7 @@ namespace smt {
literal2expr(~consequent, n);
fmls.push_back(std::move(n));
}
if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
visitor.collect(fmls);
visitor.display_decls(out);
@ -475,7 +476,7 @@ namespace smt {
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, symbol const& logic) const {
literal consequent, symbol const& logic, enode* x, enode* y) const {
ast_pp_util visitor(m);
expr_ref_vector fmls(m);
visitor.collect(fmls);
@ -490,6 +491,10 @@ namespace smt {
n = m.mk_eq(p.first->get_expr(), p.second->get_expr());
fmls.push_back(n);
}
if (x && y) {
expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m);
fmls.push_back(m.mk_not(eq));
}
if (consequent != false_literal) {
literal2expr(~consequent, n);
fmls.push_back(n);

33
src/smt/theory_lra.cpp
View file

@ -2396,7 +2396,9 @@ public:
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& ps) {
if (params().m_arith_validate)
VERIFY(validate_assign(lit, core, eqs));
VERIFY(validate_assign(lit));
if (params().m_arith_dump_lemmas)
dump_assign_lemma(lit);
if (core.size() < small_lemma_size() && eqs.empty()) {
m_core2.reset();
for (auto const& c : core) {
@ -3433,7 +3435,9 @@ public:
if (params().m_arith_validate)
VERIFY(validate_conflict(m_core, m_eqs));
VERIFY(validate_conflict());
if (params().m_arith_dump_lemmas)
dump_conflict();
if (is_conflict) {
ctx().set_conflict(
ctx().mk_justification(
@ -3747,8 +3751,25 @@ public:
}
};
void dump_assign_lemma(literal lit) {
m_core.push_back(~lit);
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
m_core.pop_back();
std::cout << "(reset)\n";
}
bool validate_conflict(literal_vector const& core, svector<enode_pair> const& eqs) {
void dump_conflict() {
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data());
std::cout << "(reset)\n";
}
void dump_eq(enode* x, enode* y) {
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal, symbol::null, x, y);
std::cout << "(reset)\n";
}
bool validate_conflict() {
if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true;
VERIFY(!m_core.empty() || !m_eqs.empty());
@ -3758,11 +3779,11 @@ public:
cancel_eh<reslimit> eh(m.limit());
scoped_timer timer(1000, &eh);
bool result = l_true != nctx.check();
CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, core.size(), core.data(), eqs.size(), eqs.data(), false_literal););
CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal););
return result;
}
bool validate_assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs) {
bool validate_assign(literal lit) {
if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true;
scoped_arith_mode _sa(ctx().get_fparams());
context nctx(m, ctx().get_fparams(), ctx().get_params());
@ -3772,7 +3793,7 @@ public:
cancel_eh<reslimit> eh(m.limit());
scoped_timer timer(1000, &eh);
bool result = l_true != nctx.check();
CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, core.size(), core.data(), eqs.size(), eqs.data(), lit);
CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
display(tout););
return result;
}