mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

enable proof objects for PB

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-02 13:53:55 -07:00
parent 5e3303ae85
commit dc8ec50137
1 changed files with 26 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/smt/theory_pb.cpp
View file

@ -752,9 +752,10 @@ namespace smt {
class theory_pb::card_justification : public justification {
card& m_card;
family_id m_fid;
literal m_lit;
public:
card_justification(card& c, family_id fid)
: justification(true), m_card(c), m_fid(fid) {}
card_justification(card& c, literal lit, family_id fid)
: justification(true), m_card(c), m_fid(fid), m_lit(lit) {}
card& get_card() { return m_card; }
@ -769,7 +770,28 @@ namespace smt {
return m_fid;
}
virtual proof* mk_proof(smt::conflict_resolution& cr) { return 0; }
virtual proof* mk_proof(smt::conflict_resolution& cr) {
ptr_buffer<proof> prs;
ast_manager& m = cr.get_context().get_manager();
expr_ref fact(m);
cr.get_context().literal2expr(m_lit, fact);
bool all_valid = true;
proof* pr = nullptr;
pr = cr.get_proof(m_card.lit());
all_valid &= pr != nullptr;
prs.push_back(pr);
for (unsigned i = m_card.k(); i < m_card.size(); ++i) {
pr = cr.get_proof(~m_card.lit(i));
all_valid &= pr != nullptr;
prs.push_back(pr);
}
if (!all_valid) {
return nullptr;
}
else {
return m.mk_th_lemma(m_fid, fact, prs.size(), prs.c_ptr());
}
}
};
@ -959,7 +981,7 @@ namespace smt {
m_stats.m_num_propagations++;
TRACE("pb", tout << "#prop: " << c.num_propagations() << " - " << c.lit() << " => " << l << "\n";);
SASSERT(validate_unit_propagation(c));
ctx.assign(l, ctx.mk_justification(card_justification(c, get_id())));
ctx.assign(l, ctx.mk_justification(card_justification(c, l, get_id())));
}
void theory_pb::clear_watch(card& c) {