mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity

use th-axioms to track origins of assertions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-27 19:08:44 -07:00
parent 5e2cefea9f
commit e35eab000c
2 changed files with 7 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_intblast.cpp
View file

@ -38,10 +38,6 @@ namespace smt {
theory_intblast::~theory_intblast() {} theory_intblast::~theory_intblast() {}
void theory_intblast::init() {
}
final_check_status theory_intblast::final_check_eh() { final_check_status theory_intblast::final_check_eh() {
for (auto e : m_translator.bv2int()) { for (auto e : m_translator.bv2int()) {
auto* n = ctx.get_enode(e); auto* n = ctx.get_enode(e);
@ -59,7 +55,7 @@ namespace smt {
auto b = mk_eq(sib->get_arg(0)->get_expr(), n->get_arg(0)->get_expr(), false); auto b = mk_eq(sib->get_arg(0)->get_expr(), n->get_arg(0)->get_expr(), false);
ctx.mark_as_relevant(a); ctx.mark_as_relevant(a);
ctx.mark_as_relevant(b); ctx.mark_as_relevant(b);
ctx.mk_clause(~a, b, nullptr); ctx.mk_th_axiom(m_id, ~a, b);
return final_check_status::FC_CONTINUE; return final_check_status::FC_CONTINUE;
} }
} }
@ -78,7 +74,7 @@ namespace smt {
if (nBv2int->get_root() != nxModN->get_root()) { if (nBv2int->get_root() != nxModN->get_root()) {
auto a = mk_eq(nBv2int->get_expr(), nxModN->get_expr(), false); auto a = mk_eq(nBv2int->get_expr(), nxModN->get_expr(), false);
ctx.mark_as_relevant(a); ctx.mark_as_relevant(a);
ctx.mk_clause(1, &a, nullptr); ctx.mk_th_axiom(m_id, 1, &a);
return final_check_status::FC_CONTINUE; return final_check_status::FC_CONTINUE;
} }
} }
@ -98,8 +94,8 @@ namespace smt {
auto hi = mk_literal(a.mk_le(w, a.mk_int(sz - 1))); auto hi = mk_literal(a.mk_le(w, a.mk_int(sz - 1)));
ctx.mark_as_relevant(lo); ctx.mark_as_relevant(lo);
ctx.mark_as_relevant(hi); ctx.mark_as_relevant(hi);
ctx.mk_clause(1, &lo, nullptr); ctx.mk_th_axiom(m_id, 1, &lo);
ctx.mk_clause(1, &hi, nullptr); ctx.mk_th_axiom(m_id, 1, &hi);
} }
return true; return true;
} }
@ -116,9 +112,8 @@ namespace smt {
auto a = mk_literal(e); auto a = mk_literal(e);
auto b = mk_literal(r); auto b = mk_literal(r);
ctx.mark_as_relevant(b); ctx.mark_as_relevant(b);
// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; ctx.mk_th_axiom(m_id, ~a, b);
ctx.mk_clause(~a, b, nullptr); ctx.mk_th_axiom(m_id, a, ~b);
ctx.mk_clause(a, ~b, nullptr);
} }
return true; return true;
} }
@ -174,6 +169,7 @@ namespace smt {
m_factory = alloc(bv_factory, m); m_factory = alloc(bv_factory, m);
mg.register_factory(m_factory); mg.register_factory(m_factory);
} }
model_value_proc* theory_intblast::mk_value(enode* n, model_generator& mg) { model_value_proc* theory_intblast::mk_value(enode* n, model_generator& mg) {
expr* e = n->get_expr(); expr* e = n->get_expr();
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));

1
src/smt/theory_intblast.h
View file

@ -53,7 +53,6 @@ namespace smt {
~theory_intblast() override; ~theory_intblast() override;
char const* get_name() const override { return "bv-intblast"; } char const* get_name() const override { return "bv-intblast"; }
void init() override;
smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_intblast, *new_ctx); } smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_intblast, *new_ctx); }
final_check_status final_check_eh() override; final_check_status final_check_eh() override;
void display(std::ostream& out) const override {} void display(std::ostream& out) const override {}