mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-29 10:49:23 +00:00
Code Activity

adding proof hint output

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-18 19:26:19 +02:00
parent eb10ab1633
commit 6485808b49
6 changed files with 191 additions and 137 deletions
Download patch file Download diff file Expand all files Collapse all files

237
src/ast/rewriter/finite_set_axioms.cpp
View file

@ -24,6 +24,11 @@ Revision History:
#include "ast/array_decl_plugin.h"
#include "ast/rewriter/finite_set_axioms.h"
std::ostream& operator<<(std::ostream& out, theory_axiom const& ax) {
return out << "axiom";
}
// a ~ set.empty => not (x in a)
// x is an element, generate axiom that x is not in any empty set of x's type
void finite_set_axioms::in_empty_axiom(expr *x) {
@ -33,9 +38,9 @@ void finite_set_axioms::in_empty_axiom(expr *x) {
expr_ref empty_set(u.mk_empty(elem_sort), m);
expr_ref x_in_empty(u.mk_in(x, empty_set), m);
expr_ref_vector clause(m);
clause.push_back(m.mk_not(x_in_empty));
m_add_clause(clause);
theory_axiom ax(m, "finite-set", "in-empty");
ax.clause.push_back(m.mk_not(x_in_empty));
m_add_clause(ax);
}
// a := set.union(b, c)
@ -44,30 +49,29 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) {
expr* b = nullptr, *c = nullptr;
if (!u.is_union(a, b, c))
return;
expr_ref_vector clause(m);
theory_axiom ax(m, "finite-set", "in-union");
expr_ref x_in_a(u.mk_in(x, a), m);
expr_ref x_in_b(u.mk_in(x, b), m);
expr_ref x_in_c(u.mk_in(x, c), m);
// (x in a) => (x in b) or (x in c)
expr_ref_vector clause1(m);
clause1.push_back(m.mk_not(x_in_a));
clause1.push_back(x_in_b);
clause1.push_back(x_in_c);
m_add_clause(clause1);
ax.clause.push_back(m.mk_not(x_in_a));
ax.clause.push_back(x_in_b);
ax.clause.push_back(x_in_c);
m_add_clause(ax);
// (x in b) => (x in a)
expr_ref_vector clause2(m);
clause2.push_back(m.mk_not(x_in_b));
clause2.push_back(x_in_a);
m_add_clause(clause2);
theory_axiom ax2(m, "finite-set", "in-union");
ax2.clause.push_back(m.mk_not(x_in_b));
ax2.clause.push_back(x_in_a);
m_add_clause(ax2);
// (x in c) => (x in a)
expr_ref_vector clause3(m);
clause3.push_back(m.mk_not(x_in_c));
clause3.push_back(x_in_a);
m_add_clause(clause3);
theory_axiom ax3(m, "finite-set", "in-union");
ax3.clause.push_back(m.mk_not(x_in_c));
ax3.clause.push_back(x_in_a);
m_add_clause(ax3);
}
// a := set.intersect(b, c)
@ -82,23 +86,23 @@ void finite_set_axioms::in_intersect_axiom(expr *x, expr *a) {
expr_ref x_in_c(u.mk_in(x, c), m);
// (x in a) => (x in b)
expr_ref_vector clause1(m);
clause1.push_back(m.mk_not(x_in_a));
clause1.push_back(x_in_b);
m_add_clause(clause1);
theory_axiom ax1(m, "finite-set", "in-intersect");
ax1.clause.push_back(m.mk_not(x_in_a));
ax1.clause.push_back(x_in_b);
m_add_clause(ax1);
// (x in a) => (x in c)
expr_ref_vector clause2(m);
clause2.push_back(m.mk_not(x_in_a));
clause2.push_back(x_in_c);
m_add_clause(clause2);
theory_axiom ax2(m, "finite-set", "in-intersect");
ax2.clause.push_back(m.mk_not(x_in_a));
ax2.clause.push_back(x_in_c);
m_add_clause(ax2);
// (x in b) and (x in c) => (x in a)
expr_ref_vector clause3(m);
clause3.push_back(m.mk_not(x_in_b));
clause3.push_back(m.mk_not(x_in_c));
clause3.push_back(x_in_a);
m_add_clause(clause3);
theory_axiom ax3(m, "finite-set", "in-intersect");
ax3.clause.push_back(m.mk_not(x_in_b));
ax3.clause.push_back(m.mk_not(x_in_c));
ax3.clause.push_back(x_in_a);
m_add_clause(ax3);
}
// a := set.difference(b, c)
@ -113,23 +117,23 @@ void finite_set_axioms::in_difference_axiom(expr *x, expr *a) {
expr_ref x_in_c(u.mk_in(x, c), m);
// (x in a) => (x in b)
expr_ref_vector clause1(m);
clause1.push_back(m.mk_not(x_in_a));
clause1.push_back(x_in_b);
m_add_clause(clause1);
theory_axiom ax1(m, "finite-set", "in-difference");
ax1.clause.push_back(m.mk_not(x_in_a));
ax1.clause.push_back(x_in_b);
m_add_clause(ax1);
// (x in a) => not (x in c)
expr_ref_vector clause2(m);
clause2.push_back(m.mk_not(x_in_a));
clause2.push_back(m.mk_not(x_in_c));
m_add_clause(clause2);
theory_axiom ax2(m, "finite-set", "in-difference");
ax2.clause.push_back(m.mk_not(x_in_a));
ax2.clause.push_back(m.mk_not(x_in_c));
m_add_clause(ax2);
// (x in b) and not (x in c) => (x in a)
expr_ref_vector clause3(m);
clause3.push_back(m.mk_not(x_in_b));
clause3.push_back(x_in_c);
clause3.push_back(x_in_a);
m_add_clause(clause3);
theory_axiom ax3(m, "finite-set", "in-difference");
ax3.clause.push_back(m.mk_not(x_in_b));
ax3.clause.push_back(x_in_c);
ax3.clause.push_back(x_in_a);
m_add_clause(ax3);
}
// a := set.singleton(b)
@ -141,27 +145,27 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
expr_ref x_in_a(u.mk_in(x, a), m);
theory_axiom ax(m, "finite-set", "in-singleton");
if (x == b) {
// If x and b are syntactically identical, then (x in a) is always true
expr_ref_vector clause(m);
clause.push_back(x_in_a);
m_add_clause(clause);
ax.clause.push_back(x_in_a);
m_add_clause(ax);
return;
}
expr_ref x_eq_b(m.mk_eq(x, b), m);
// (x in a) => (x == b)
expr_ref_vector clause1(m);
clause1.push_back(m.mk_not(x_in_a));
clause1.push_back(x_eq_b);
m_add_clause(clause1);
ax.clause.push_back(m.mk_not(x_in_a));
ax.clause.push_back(x_eq_b);
m_add_clause(ax);
ax.clause.reset();
// (x == b) => (x in a)
expr_ref_vector clause2(m);
clause2.push_back(m.mk_not(x_eq_b));
clause2.push_back(x_in_a);
m_add_clause(clause2);
ax.clause.push_back(m.mk_not(x_eq_b));
ax.clause.push_back(x_in_a);
m_add_clause(ax);
}
// a := set.range(lo, hi)
@ -177,23 +181,23 @@ void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
expr_ref x_le_hi(arith.mk_le(x, hi), m);
// (x in a) => (lo <= x)
expr_ref_vector clause1(m);
clause1.push_back(m.mk_not(x_in_a));
clause1.push_back(lo_le_x);
m_add_clause(clause1);
theory_axiom ax1(m, "finite-set", "in-range");
ax1.clause.push_back(m.mk_not(x_in_a));
ax1.clause.push_back(lo_le_x);
m_add_clause(ax1);
// (x in a) => (x <= hi)
expr_ref_vector clause2(m);
clause2.push_back(m.mk_not(x_in_a));
clause2.push_back(x_le_hi);
m_add_clause(clause2);
theory_axiom ax2(m, "finite-set", "in-range");
ax2.clause.push_back(m.mk_not(x_in_a));
ax2.clause.push_back(x_le_hi);
m_add_clause(ax2);
// (lo <= x) and (x <= hi) => (x in a)
expr_ref_vector clause3(m);
clause3.push_back(m.mk_not(lo_le_x));
clause3.push_back(m.mk_not(x_le_hi));
clause3.push_back(x_in_a);
m_add_clause(clause3);
theory_axiom ax3(m, "finite-set", "in-range");
ax3.clause.push_back(m.mk_not(lo_le_x));
ax3.clause.push_back(m.mk_not(x_le_hi));
ax3.clause.push_back(x_in_a);
m_add_clause(ax3);
}
// a := set.map(f, b)
@ -224,10 +228,10 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) {
expr_ref fx_in_a(u.mk_in(fx, a), m);
// (x in b) => f(x) in a
expr_ref_vector clause(m);
clause.push_back(m.mk_not(x_in_b));
clause.push_back(fx_in_a);
m_add_clause(clause);
theory_axiom ax(m, "finite-set", "in-map-image");
ax.clause.push_back(m.mk_not(x_in_b));
ax.clause.push_back(fx_in_a);
m_add_clause(ax);
}
// a := set.filter(p, b)
@ -245,23 +249,23 @@ void finite_set_axioms::in_filter_axiom(expr *x, expr *a) {
expr_ref px(autil.mk_select(p, x), m);
// (x in a) => (x in b)
expr_ref_vector clause1(m);
clause1.push_back(m.mk_not(x_in_a));
clause1.push_back(x_in_b);
m_add_clause(clause1);
theory_axiom ax1(m, "finite-set", "in-filter");
ax1.clause.push_back(m.mk_not(x_in_a));
ax1.clause.push_back(x_in_b);
m_add_clause(ax1);
// (x in a) => p(x)
expr_ref_vector clause2(m);
clause2.push_back(m.mk_not(x_in_a));
clause2.push_back(px);
m_add_clause(clause2);
theory_axiom ax2(m, "finite-set", "in-filter");
ax2.clause.push_back(m.mk_not(x_in_a));
ax2.clause.push_back(px);
m_add_clause(ax2);
// (x in b) and p(x) => (x in a)
expr_ref_vector clause3(m);
clause3.push_back(m.mk_not(x_in_b));
clause3.push_back(m.mk_not(px));
clause3.push_back(x_in_a);
m_add_clause(clause3);
theory_axiom ax3(m, "finite-set", "in-filter");
ax3.clause.push_back(m.mk_not(x_in_b));
ax3.clause.push_back(m.mk_not(px));
ax3.clause.push_back(x_in_a);
m_add_clause(ax3);
}
// a := set.singleton(b)
@ -275,10 +279,10 @@ void finite_set_axioms::size_singleton_axiom(expr *a) {
expr_ref size_a(u.mk_size(a), m);
expr_ref one(arith.mk_int(1), m);
expr_ref eq(m.mk_eq(size_a, one), m);
expr_ref_vector clause(m);
clause.push_back(eq);
m_add_clause(clause);
theory_axiom ax(m, "finite-set", "size-singleton");
ax.clause.push_back(eq);
m_add_clause(ax);
}
void finite_set_axioms::subset_axiom(expr* a) {
@ -288,16 +292,16 @@ void finite_set_axioms::subset_axiom(expr* a) {
expr_ref intersect_bc(u.mk_intersect(b, c), m);
expr_ref eq(m.mk_eq(intersect_bc, b), m);
expr_ref_vector clause1(m);
clause1.push_back(m.mk_not(a));
clause1.push_back(eq);
m_add_clause(clause1);
expr_ref_vector clause2(m);
clause2.push_back(a);
clause2.push_back(m.mk_not(eq));
m_add_clause(clause2);
theory_axiom ax1(m, "finite-set", "subset");
ax1.clause.push_back(m.mk_not(a));
ax1.clause.push_back(eq);
m_add_clause(ax1);
theory_axiom ax2(m, "finite-set", "subset");
ax2.clause.push_back(a);
ax2.clause.push_back(m.mk_not(eq));
m_add_clause(ax2);
}
void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
@ -309,8 +313,15 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
expr_ref diff_in_b(u.mk_in(diff_ab, b), m);
// (a != b) => (x in diff_ab != x in diff_ba)
expr_ref_vector clause(m);
clause.push_back(a_eq_b);
clause.push_back(m.mk_not(m.mk_iff(diff_in_a, diff_in_b)));
m_add_clause(clause);
theory_axiom ax(m, "finite-set", "extensionality");
ax.clause.push_back(a_eq_b);
ax.clause.push_back(m.mk_not(diff_in_a));
ax.clause.push_back(m.mk_not(diff_in_b));
m_add_clause(ax);
theory_axiom ax2(m, "finite-set", "extensionality");
ax2.clause.push_back(m.mk_not(a_eq_b));
ax2.clause.push_back(diff_in_a);
ax2.clause.push_back(diff_in_b);
m_add_clause(ax2);
}

26
src/ast/rewriter/finite_set_axioms.h
View file

@ -12,17 +12,39 @@ Abstract:
--*/
struct theory_axiom {
expr_ref_vector clause;
vector<parameter> params;
unsigned weight = 0; // can be used to prioritize instantiation of axioms
theory_axiom(ast_manager& m, symbol const& th): clause(m) {
params.push_back(parameter(th));
}
theory_axiom(ast_manager &m, symbol const &th, symbol const& rule) : clause(m) {
params.push_back(parameter(th));
params.push_back(parameter(rule));
}
theory_axiom(ast_manager &m, char const *th, char const *rule) : clause(m) {
params.push_back(parameter(symbol(th)));
params.push_back(parameter(symbol(rule)));
}
theory_axiom(ast_manager &m) : clause(m) {
}
};
std::ostream &operator<<(std::ostream &out, theory_axiom const &ax);
class finite_set_axioms {
ast_manager& m;
finite_set_util u;
std::function<void(expr_ref_vector const &)> m_add_clause;
std::function<void(theory_axiom const &)> m_add_clause;
public:
finite_set_axioms(ast_manager &m) : m(m), u(m) {}
void set_add_clause(std::function<void(expr_ref_vector const &)> &ac) {
void set_add_clause(std::function<void(theory_axiom const &)> &ac) {
m_add_clause = ac;
}

6
src/smt/smt_clause_proof.cpp
View file

@ -158,8 +158,10 @@ namespace smt {
for (literal l : ante)
m_lits.push_back(ctx.literal2expr(~l));
m_lits.push_back(ctx.literal2expr(lit));
proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
update(clause_proof::status::th_lemma, m_lits, pr);
auto st = clause_proof::status::th_lemma;
auto pr = justification2proof(st, &const_cast<justification &>(jst));
// proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
update(st, m_lits, pr);
}
void clause_proof::del(clause& c) {

3
src/smt/smt_justification.cpp
View file

@ -351,8 +351,9 @@ namespace smt {
proof * ext_theory_propagation_justification::mk_proof(conflict_resolution & cr) {
ptr_buffer<proof> prs;
if (!antecedent2proof(cr, prs))
if (!antecedent2proof(cr, prs)) {
return nullptr;
}
context & ctx = cr.get_context();
ast_manager & m = cr.get_manager();
expr_ref fact(m);

50
src/smt/theory_finite_set.cpp
View file

@ -29,9 +29,9 @@ namespace smt {
m_axioms(m), m_find(*this)
{
// Setup the add_clause callback for axioms
std::function<void(expr_ref_vector const &)> add_clause_fn =
[this](expr_ref_vector const& clause) {
this->add_clause(clause);
std::function<void(theory_axiom const &)> add_clause_fn =
[this](theory_axiom const &ax) {
this->add_clause(ax);
};
m_axioms.set_add_clause(add_clause_fn);
}
@ -101,7 +101,7 @@ namespace smt {
ctx.push_trail(push_back_trail(m_var_data[v]->m_parent_setops));
}
}
else if (u.is_map(e) || u.is_select(e)) {
else if (u.is_map(e) || u.is_filter(e)) {
NOT_IMPLEMENTED_YET();
}
return r;
@ -322,7 +322,8 @@ namespace smt {
for (unsigned i = 0; i < m_clauses.watch[idx].size(); ++i) {
TRACE(finite_set, tout << " watch[" << i << "] size: " << m_clauses.watch[i].size() << "\n";);
auto clause_idx = m_clauses.watch[idx][i];
auto &clause = m_clauses.axioms[clause_idx];
auto &ax = m_clauses.axioms[clause_idx];
auto &clause = ax.clause;
if (any_of(clause, [&](expr *lit) { return ctx.find_assignment(lit) == l_true; })) {
TRACE(finite_set, tout << " satisfied\n";);
m_clauses.watch[idx][j++] = clause_idx;
@ -398,7 +399,8 @@ namespace smt {
void theory_finite_set::activate_clause(unsigned clause_idx) {
TRACE(finite_set, tout << "activate_clause: " << clause_idx << "\n";);
auto &clause = m_clauses.axioms[clause_idx];
auto &ax = m_clauses.axioms[clause_idx];
auto &clause = ax.clause;
if (any_of(clause, [&](expr *e) { return ctx.find_assignment(e) == l_true; }))
return;
if (clause.size() <= 1) {
@ -444,7 +446,8 @@ namespace smt {
unsigned index;
unwatch_clause(theory_finite_set &th, unsigned index) : th(th), index(index) {}
void undo() override {
auto &clause = th.m_clauses.axioms[index];
auto &ax = th.m_clauses.axioms[index];
auto &clause = ax.clause;
expr *w1 = clause.get(0);
expr *w2 = clause.get(1);
bool w1neg = th.m.is_not(w1, w1);
@ -566,10 +569,10 @@ namespace smt {
}
}
void theory_finite_set::add_clause(expr_ref_vector const& clause) {
TRACE(finite_set, tout << "add_clause: " << clause << "\n");
void theory_finite_set::add_clause(theory_axiom const& ax) {
TRACE(finite_set, tout << "add_clause: " << ax << "\n");
ctx.push_trail(push_back_vector(m_clauses.axioms));
m_clauses.axioms.push_back(clause);
m_clauses.axioms.push_back(ax);
m_stats.m_num_axioms_created++;
}
@ -689,7 +692,8 @@ namespace smt {
return false;
}
bool theory_finite_set::assert_clause(expr_ref_vector const &clause) {
bool theory_finite_set::assert_clause(theory_axiom const &ax) {
auto const &clause = ax.clause;
expr *unit = nullptr;
unsigned undef_count = 0;
for (auto e : clause) {
@ -708,14 +712,28 @@ namespace smt {
if (undef_count == 1) {
TRACE(finite_set, tout << " propagate unit: " << mk_pp(unit, m) << "\n" << clause << "\n";);
auto lit = mk_literal(unit);
literal_vector core;
literal_vector antecedent;
for (auto e : clause) {
if (e != unit)
core.push_back(~mk_literal(e));
antecedent.push_back(~mk_literal(e));
}
m_stats.m_num_axioms_propagated++;
ctx.assign(lit, ctx.mk_justification(
theory_propagation_justification(get_id(), ctx, core.size(), core.data(), lit)));
enode_pair_vector eqs;
auto just = ext_theory_propagation_justification(get_id(), ctx, antecedent.size(), antecedent.data(), eqs.size(), eqs.data(), lit, ax.params.size(),
ax.params.data());
auto bjust = ctx.mk_justification(just);
if (ctx.clause_proof_active()) {
// assume all justifications is a non-empty list of symbol parameters
proof_ref pr(m);
expr_ref_vector args(m);
for (unsigned i = 1; i < ax.params.size(); ++i)
args.push_back(m.mk_app(ax.params[i].get_symbol(), 0, nullptr, m.mk_proof_sort()));
pr = m.mk_app(ax.params[0].get_symbol(), args.size(), args.data(), m.mk_proof_sort());
justification_proof_wrapper jp(ctx, pr.get(), false);
ctx.get_clause_proof().propagate(lit, jp, antecedent);
jp.del_eh(m);
}
ctx.assign(lit, bjust);
return true;
}
bool is_conflict = (undef_count == 0);
@ -727,7 +745,7 @@ namespace smt {
literal_vector lclause;
for (auto e : clause)
lclause.push_back(mk_literal(e));
ctx.mk_th_axiom(get_id(), lclause);
ctx.mk_th_axiom(get_id(), lclause, ax.params.size(), ax.params.data());
return true;
}

6
src/smt/theory_finite_set.h
View file

@ -107,7 +107,7 @@ namespace smt {
};
struct theory_clauses {
vector<expr_ref_vector> axioms; // vector of created theory axioms
vector<theory_axiom> axioms; // vector of created theory axioms
unsigned aqhead = 0; // queue head of created axioms
unsigned_vector squeue; // propagation queue of axioms to be added to the solver
unsigned sqhead = 0; // head into propagation queue axioms to be added to solver
@ -172,8 +172,8 @@ namespace smt {
// Helper methods for axiom instantiation
void add_membership_axioms(expr* elem, expr* set);
void add_clause(expr_ref_vector const& clause);
bool assert_clause(expr_ref_vector const &clause);
void add_clause(theory_axiom const& ax);
bool assert_clause(theory_axiom const &ax);
void activate_clause(unsigned index);
bool activate_unasserted_clause();
void add_immediate_axioms(app *atom);