mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

track proof hints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-27 16:34:00 -08:00
parent ac8efad7e1
commit 47b2113260
3 changed files with 20 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/polysat_internalize.cpp
View file

@ -625,10 +625,10 @@ namespace polysat {
auto sz_e = hi - lo + 1;
auto sz_x = bv.get_bv_size(x);
auto eq0 = eq_internalize(e, bv.mk_numeral(0, sz_e));
auto gelo = mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(lo), sz_x), x));
add_clause(eq0, gelo);
auto gelo = mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(lo), sz_x), x));
add_clause(eq0, gelo, mk_proof_hint("extract-1"));
if (hi + 1 == sz_e)
add_clause(~eq0, ~gelo);
add_clause(~eq0, ~gelo, mk_proof_hint("extract-2"));
}
void solver::internalize_concat(app* e) {

11
src/sat/smt/polysat_solver.cpp
View file

@ -339,7 +339,7 @@ namespace polysat {
for (auto lit : lits)
if (s().value(lit) == l_true)
return false;
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), nullptr));
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), mk_proof_hint(name)));
return true;
}
@ -393,4 +393,13 @@ namespace polysat {
r = bv.mk_bv_add(r, pdd2expr(p.lo()));
return expr_ref(r, m);
}
expr* solver::polysat_proof::get_hint(euf::solver& s) const {
auto& m = s.get_manager();
return m.mk_app(symbol(name), 0, nullptr, m.mk_proof_sort());
}
solver::polysat_proof* solver::mk_proof_hint(char const* name) {
return new (get_region()) polysat_proof(name);
}
}

8
src/sat/smt/polysat_solver.h
View file

@ -49,12 +49,18 @@ namespace polysat {
~atom() { }
};
class polysat_proof : public euf::th_proof_hint {
// assume name is statically allocated
char const* name;
public:
polysat_proof(char const* name) : name(name) {}
~polysat_proof() override {}
expr* get_hint(euf::solver& s) const override { return nullptr; }
expr* get_hint(euf::solver& s) const override;
};
polysat_proof* mk_proof_hint(char const* name);
bv_util bv;
arith_util m_autil;
stats m_stats;