mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

add generic theory lemma in default case.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-17 10:17:08 -07:00
parent a25247aa7b
commit 98fe2e637a
3 changed files with 21 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/sat/smt/euf_proof.cpp
View file

@ -166,7 +166,24 @@ namespace euf {
return m.mk_app(f, args); return m.mk_app(f, args);
} }
smt_proof_hint* solver::mk_smt_clause(symbol const& n, unsigned nl, literal const* lits) {
if (!use_drat())
return nullptr;
push(value_trail(m_lit_tail));
push(restore_size_trail(m_proof_literals));
for (unsigned i = 0; i < nl; ++i)
m_proof_literals.push_back(~lits[i]);
m_lit_head = m_lit_tail;
m_eq_head = m_eq_tail;
m_deq_head = m_deq_tail;
m_lit_tail = m_proof_literals.size();
m_eq_tail = m_proof_eqs.size();
m_deq_tail = m_proof_deqs.size();
return new (get_region()) smt_proof_hint(n, m_lit_head, m_lit_tail, m_eq_head, m_eq_tail, m_deq_head, m_deq_tail);
}
smt_proof_hint* solver::mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd, expr_pair const* deqs) { smt_proof_hint* solver::mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd, expr_pair const* deqs) {
if (!use_drat()) if (!use_drat())

1
src/sat/smt/euf_solver.h
View file

@ -404,6 +404,7 @@ namespace euf {
smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, expr* a, expr* b) { expr_pair e(a, b); return mk_smt_hint(n, 1, &lit, 0, nullptr, 1, &e); } smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, expr* a, expr* b) { expr_pair e(a, b); return mk_smt_hint(n, 1, &lit, 0, nullptr, 1, &e); }
smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, enode* a, enode* b) { return mk_smt_prop_hint(n, lit, a->get_expr(), b->get_expr()); } smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, enode* a, enode* b) { return mk_smt_prop_hint(n, lit, a->get_expr(), b->get_expr()); }
smt_proof_hint* mk_smt_hint(symbol const& n, enode* a, enode* b) { expr_pair e(a->get_expr(), b->get_expr()); return mk_smt_hint(n, 0, nullptr, 1, &e); } smt_proof_hint* mk_smt_hint(symbol const& n, enode* a, enode* b) { expr_pair e(a->get_expr(), b->get_expr()); return mk_smt_hint(n, 0, nullptr, 1, &e); }
smt_proof_hint* mk_smt_clause(symbol const& n, unsigned nl, literal const* lits);
th_proof_hint* mk_cc_proof_hint(sat::literal_vector const& ante, app* a, app* b); th_proof_hint* mk_cc_proof_hint(sat::literal_vector const& ante, app* a, app* b);
th_proof_hint* mk_tc_proof_hint(sat::literal const* ternary_clause); th_proof_hint* mk_tc_proof_hint(sat::literal const* ternary_clause);
sat::status mk_tseitin_status(sat::literal a, sat::literal b); sat::status mk_tseitin_status(sat::literal a, sat::literal b);

4
src/sat/smt/sat_th.cpp
View file

@ -160,7 +160,9 @@ namespace euf {
} }
bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) { bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) {
SASSERT(!ctx.use_drat() || ps); // - very far from true, and isn't a requirement if (ctx.use_drat() && !ps)
ps = ctx.mk_smt_clause(name(), n, lits);
bool was_true = false; bool was_true = false;
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
was_true |= is_true(lits[i]); was_true |= is_true(lits[i]);