mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fixup theory_finite_set

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-15 15:02:58 +02:00
parent b4d41ffe81
commit 54980a38d4
2 changed files with 27 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/smt/theory_finite_set.cpp
View file

@ -39,7 +39,7 @@ namespace smt {
} }
bool theory_finite_set::internalize_atom(app * atom, bool gate_ctx) { bool theory_finite_set::internalize_atom(app * atom, bool gate_ctx) {
TRACE("finite_set", tout << "internalize_atom: " << mk_pp(atom, m) << "\n";); // TRACE(finite_set, tout << "internalize_atom: " << mk_pp(atom, m) << "\n";);
internalize_term(atom); internalize_term(atom);
@ -49,7 +49,7 @@ namespace smt {
auto n = ctx.get_enode(elem); auto n = ctx.get_enode(elem);
if (!m_elements.contains(n)) { if (!m_elements.contains(n)) {
m_elements.insert(n); m_elements.insert(n);
ctx.push_trail(insert_obj_trail(n)); ctx.push_trail(insert_obj_trail(m_elements, n));
} }
} }
@ -57,7 +57,7 @@ namespace smt {
} }
bool theory_finite_set::internalize_term(app * term) { bool theory_finite_set::internalize_term(app * term) {
TRACE("finite_set", tout << "internalize_term: " << mk_pp(term, m) << "\n";); // TRACE("finite_set", tout << "internalize_term: " << mk_pp(term, m) << "\n";);
// Internalize all arguments first // Internalize all arguments first
for (expr* arg : *term) for (expr* arg : *term)
@ -84,19 +84,19 @@ namespace smt {
} }
void theory_finite_set::new_eq_eh(theory_var v1, theory_var v2) { void theory_finite_set::new_eq_eh(theory_var v1, theory_var v2) {
TRACE("finite_set", tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";); // TRACE("finite_set", tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";);
// When two sets are equal, propagate membership constraints // When two sets are equal, propagate membership constraints
// This is handled by congruence closure, so no additional work needed here // This is handled by congruence closure, so no additional work needed here
} }
void theory_finite_set::new_diseq_eh(theory_var v1, theory_var v2) { void theory_finite_set::new_diseq_eh(theory_var v1, theory_var v2) {
TRACE("finite_set", tout << "new_diseq_eh: v" << v1 << " != v" << v2 << "\n";); // TRACE("finite_set", tout << "new_diseq_eh: v" << v1 << " != v" << v2 << "\n";);
// Disequalities could trigger extensionality axioms // Disequalities could trigger extensionality axioms
// For now, we rely on the final_check to handle this // For now, we rely on the final_check to handle this
} }
final_check_status theory_finite_set::final_check_eh() { final_check_status theory_finite_set::final_check_eh() {
TRACE("finite_set", tout << "final_check_eh\n";); // TRACE("finite_set", tout << "final_check_eh\n";);
// walk all parents of elem in congruence table. // walk all parents of elem in congruence table.
// if a parent is of the form elem' in S u T, or similar. // if a parent is of the form elem' in S u T, or similar.
@ -125,7 +125,7 @@ namespace smt {
} }
void theory_finite_set::instantiate_axioms(expr* elem, expr* set) { void theory_finite_set::instantiate_axioms(expr* elem, expr* set) {
TRACE("finite_set", tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); // TRACE("finite_set", tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";);
// Instantiate appropriate axiom based on set structure // Instantiate appropriate axiom based on set structure
if (u.is_empty(set)) { if (u.is_empty(set)) {
@ -162,14 +162,14 @@ namespace smt {
} }
void theory_finite_set::add_clause(expr_ref_vector const& clause) { void theory_finite_set::add_clause(expr_ref_vector const& clause) {
TRACE("finite_set", //TRACE("finite_set",
tout << "add_clause: " << clause << "\n"); // tout << "add_clause: " << clause << "\n");
// Convert expressions to literals and assert the clause // Convert expressions to literals and assert the clause
literal_vector lits; literal_vector lits;
for (expr* e : clause) { for (expr* e : clause) {
ctx.internalize(e, false); ctx.internalize(e, false);
literal lit = ctx.get_literal(lit_expr); literal lit = ctx.get_literal(e);
lits.push_back(lit); lits.push_back(lit);
} }
@ -188,13 +188,13 @@ namespace smt {
} }
void theory_finite_set::init_model(model_generator & mg) { void theory_finite_set::init_model(model_generator & mg) {
TRACE("finite_set", tout << "init_model\n";); // TRACE("finite_set", tout << "init_model\n";);
// Model generation will use default interpretation for sets // Model generation will use default interpretation for sets
// The model will be constructed based on the membership literals that are true // The model will be constructed based on the membership literals that are true
} }
model_value_proc * theory_finite_set::mk_value(enode * n, model_generator & mg) { model_value_proc * theory_finite_set::mk_value(enode * n, model_generator & mg) {
TRACE("finite_set", tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); // TRACE("finite_set", tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";);
// For now, return nullptr to use default model construction // For now, return nullptr to use default model construction
// A complete implementation would construct explicit set values // A complete implementation would construct explicit set values
@ -202,8 +202,17 @@ namespace smt {
return nullptr; return nullptr;
} }
void theory_finite_set::instantiate_false_lemma() {} bool theory_finite_set::instantiate_false_lemma() {
void theory_finite_set::instantiate_unit_propagation() {} // Implementation for instantiating false lemma
void theory_finite_set::instantiate_free_lemma() {} return false;
}
bool theory_finite_set::instantiate_unit_propagation() {
// Implementation for instantiating unit propagation
return false;
}
bool theory_finite_set::instantiate_free_lemma() {
// Implementation for instantiating free lemma
return false;
}
} // namespace smt } // namespace smt

6
src/smt/theory_finite_set.h
View file

@ -115,9 +115,9 @@ namespace smt {
// Helper methods for axiom instantiation // Helper methods for axiom instantiation
void instantiate_axioms(expr* elem, expr* set); void instantiate_axioms(expr* elem, expr* set);
void add_clause(expr_ref_vector const& clause); void add_clause(expr_ref_vector const& clause);
void instantiate_false_lemma(); bool instantiate_false_lemma();
void instantiate_unit_propagation(); bool instantiate_unit_propagation();
void instantiate_free_lemma(); bool instantiate_free_lemma();
public: public:
theory_finite_set(context& ctx); theory_finite_set(context& ctx);