From 4068460a0fee32aeb5e8edc66712ada30ee9a5c1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Oct 2025 13:35:41 +0200 Subject: [PATCH] fix bogus axioms Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/finite_set_axioms.cpp | 6 ++++- src/smt/theory_finite_set.cpp | 31 +++++++++++++++++++------- src/smt/theory_finite_set.h | 3 +++ 3 files changed, 31 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index dd25a54f1..4bf29c087 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -230,14 +230,18 @@ void finite_set_axioms::in_range_axiom(expr* r) { if (!u.is_range(r, lo, hi)) return; theory_axiom* ax = alloc(theory_axiom, m, "range-bounds"); + arith_util a(m); + expr_ref lo_le_hi(a.mk_le(a.mk_sub(lo, hi), a.mk_int(0)), m); + m_rewriter(lo_le_hi); + ax->clause.push_back(m.mk_not(lo_le_hi)); ax->clause.push_back(u.mk_in(lo, r)); m_add_clause(ax); ax = alloc(theory_axiom, m, "range-bounds", r); + ax->clause.push_back(m.mk_not(lo_le_hi)); ax->clause.push_back(u.mk_in(hi, r)); m_add_clause(ax); - arith_util a(m); ax = alloc(theory_axiom, m, "range-bounds", r); ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(hi, a.mk_int(1)), r))); m_add_clause(ax); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index d9abb8756..205733907 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -228,12 +228,16 @@ namespace smt { ctx.attach_th_var(e, this, mk_var(e)); // Assert immediate axioms - // if (!ctx.relevancy()) - add_immediate_axioms(term); + if (!ctx.relevancy()) + add_immediate_axioms(term); return true; } + void theory_finite_set::relevant_eh(app* t) { + add_immediate_axioms(t); + } + void theory_finite_set::apply_sort_cnstr(enode* n, sort* s) { SASSERT(u.is_finite_set(s)); if (!is_attached_to_var(n)) @@ -248,9 +252,6 @@ namespace smt { /** * Every dissequality has to be supported by at distinguishing element. * - * TODO: we can avoid instantiating the extensionality axiom if we know statically that e1, e2 - * can never be equal (say, they have different cardinalities or they are finite sets by construction - * with elements that can differentiate the sets) */ 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"); @@ -263,10 +264,23 @@ namespace smt { std::swap(e1, e2); if (!is_new_axiom(e1, e2)) return; + if (are_forced_distinct(n1, n2)) + return; m_axioms.extensionality_axiom(e1, e2); } } + // + // TODO: add implementation that detects sets that are known to be distinct. + // for example, + // . x in a is assigned to true and y in b is assigned to false and x ~ y + // . or upper-bound(set.size(a)) < lower-bound(set.size(b)) + // where upper and lower bounds can be queried using arith_value + // + bool theory_finite_set::are_forced_distinct(enode* a, enode* b) { + return false; + } + /** * Final check for the finite set theory. * The Final Check method is called when the solver has assigned truth values to all Boolean variables. @@ -297,12 +311,13 @@ namespace smt { * These are unit clauses that can be added immediately. * - (set.in x set.empty) is false * - (set.subset S T) <=> (= (set.union S T) T) (or (= (set.intersect S T) S)) - * - * Other axioms: * - (set.singleton x) -> (set.in x (set.singleton x)) + * - (set.range lo hi) -> lo-1,hi+1 not in range, lo, hi in range if lo <= hi * + * + * Other axioms: * - (set.singleton x) -> (set.size (set.singleton x)) = 1 * - (set.empty) -> (set.size (set.empty)) = 0 - * - (set.range lo hi) -> lo-1,hi+1 not in range, lo, hi in range + */ void theory_finite_set::add_immediate_axioms(app* term) { expr *elem = nullptr, *set = nullptr; diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 359fc24f2..65928ac76 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -160,6 +160,7 @@ namespace smt { bool can_propagate() override; void propagate() override; void assign_eh(bool_var v, bool is_true) override; + void relevant_eh(app *n) override; theory * mk_fresh(context * new_ctx) override; char const * get_name() const override { return "finite_set"; } @@ -199,6 +200,8 @@ namespace smt { bool is_root(theory_var v) const { return m_find.is_root(v); } std::ostream &display_var(std::ostream &out, theory_var v) const; + + bool are_forced_distinct(enode *a, enode *b); public: theory_finite_set(context& ctx);