bug fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/python/z3/z3.py

@@ -843,7 +843,7 @@ class FuncDeclRef(AstRef):
             elif k == Z3_PARAMETER_RATIONAL:
                 result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i)
             elif k == Z3_PARAMETER_SYMBOL:
-                result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i)
+                result[i] = _symbol2py(ctx, Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i))
             elif k == Z3_PARAMETER_SORT:
                 result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx)
             elif k == Z3_PARAMETER_AST:

src/ast/ast.cpp

@@ -3338,26 +3338,12 @@ proof * ast_manager::mk_th_lemma(
     if (proofs_disabled())
         return nullptr;
 
-    proof_ref pr(*this);
-    ptr_buffer<expr> args;
     vector<parameter> parameters;
     parameters.push_back(parameter(get_family_name(tid)));
-    for (unsigned i = 0; i < num_params; ++i) {
+    for (unsigned i = 0; i < num_params; ++i) 
-        auto const &p = params[i];
+        parameters.push_back(params[i]);        
-        parameters.push_back(p);
+    ptr_buffer<expr> args;
-        if (p.is_symbol())
-            args.push_back(mk_app(p.get_symbol(), 0, nullptr, mk_proof_sort()));
-        else if (p.is_ast() && is_expr(p.get_ast()))
-            args.push_back(to_expr(p.get_ast()));
-        else if (p.is_rational()) {
-            arith_util autil(*this);
-            args.push_back(autil.mk_real(p.get_rational()));
-        }     
-    }
-    pr = mk_app(get_family_name(tid), args.size(), args.data(), mk_proof_sort());
-    args.reset();
     args.append(num_proofs, (expr**) proofs);
-    args.push_back(pr.get());
     args.push_back(fact);
     return mk_app(basic_family_id, PR_TH_LEMMA, parameters.size(), parameters.data(), args.size(), args.data());
 }

src/ast/ast.h

@@ -2328,7 +2328,7 @@ public:
     unsigned get_num_parents(proof const * p) const {
         SASSERT(is_proof(p));
         unsigned n = p->get_num_args();
-        return p->get_decl()->get_decl_kind() == PR_TH_LEMMA ? n - 2 : !has_fact(p) ? n : n - 1;
+        return !has_fact(p) ? n : n - 1;
     }
     proof * get_parent(proof const * p, unsigned idx) const { SASSERT(is_proof(p)); return to_app(p->get_arg(idx)); }
     proof * mk_true_proof();

src/ast/finite_set_decl_plugin.cpp

@@ -70,7 +70,7 @@ void finite_set_decl_plugin::init() {
     m_sigs[OP_FINITE_SET_MAP]        = alloc(polymorphism::psig, m, "set.map",        2, 2, arrABsetA, setB);
     m_sigs[OP_FINITE_SET_FILTER]     = alloc(polymorphism::psig, m, "set.filter",     1, 2, arrABoolsetA, setA);
     m_sigs[OP_FINITE_SET_RANGE]      = alloc(polymorphism::psig, m, "set.range",      0, 2, intintT, setInt);
-    m_sigs[OP_FINITE_SET_DIFF]       = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, A);
+    m_sigs[OP_FINITE_SET_EXT]       = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, A);
 //    m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A);
 }
 
@@ -179,7 +179,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param
     case OP_FINITE_SET_MAP:
     case OP_FINITE_SET_FILTER:
     case OP_FINITE_SET_RANGE:
-    case OP_FINITE_SET_DIFF:
+    case OP_FINITE_SET_EXT:
         return mk_finite_set_op(k, arity, domain, range);
     default:
         return nullptr;

src/ast/finite_set_decl_plugin.h

@@ -47,7 +47,7 @@ enum finite_set_op_kind {
     OP_FINITE_SET_MAP,
     OP_FINITE_SET_FILTER,
     OP_FINITE_SET_RANGE,
-    OP_FINITE_SET_DIFF,
+    OP_FINITE_SET_EXT,
     OP_FINITE_SET_MAP_INVERSE,
     LAST_FINITE_SET_OP
 };
@@ -154,6 +154,11 @@ public:
     
     ast_manager& get_manager() const { return m_manager; }
 
+    sort *mk_finite_set_sort(sort *elem_sort) {
+        parameter param(elem_sort);
+        return m_manager.mk_sort(m_fid, FINITE_SET_SORT, 1, &param);
+    }
+
     app * mk_empty(sort* set_sort) {
         parameter param(set_sort);
         return m_manager.mk_app(m_fid, OP_FINITE_SET_EMPTY, 1, &param, 0, nullptr);
@@ -175,6 +180,10 @@ public:
         return m_manager.mk_app(m_fid, OP_FINITE_SET_DIFFERENCE, s1, s2);
     }
 
+    app *mk_ext(expr *s1, expr *s2) {
+        return m_manager.mk_app(m_fid, OP_FINITE_SET_EXT, s1, s2);
+    }
+
     app * mk_in(expr* elem, expr* set) {
         return m_manager.mk_app(m_fid, OP_FINITE_SET_IN, elem, set);
     }

src/ast/rewriter/finite_set_axioms.cpp

@@ -27,7 +27,10 @@ Revision History:
 
 
 std::ostream& operator<<(std::ostream& out, theory_axiom const& ax) {
-    return out << "axiom";
+    auto &m = ax.clause.get_manager();
+    for (auto e : ax.clause)
+        out << mk_pp(e, m) << " ";
+    return out;
 }
 
 // a ~ set.empty => not (x in a)
@@ -36,7 +39,8 @@ void finite_set_axioms::in_empty_axiom(expr *x) {
     // Generate: not (x in empty_set)
     // where empty_set is the empty set of x's type
     sort* elem_sort = x->get_sort();
-    expr_ref empty_set(u.mk_empty(elem_sort), m);
+    sort *set_sort = u.mk_finite_set_sort(elem_sort);
+    expr_ref empty_set(u.mk_empty(set_sort), m);
     expr_ref x_in_empty(u.mk_in(x, empty_set), m);
     
     theory_axiom* ax = alloc(theory_axiom, m, "in-empty", x);
@@ -357,7 +361,7 @@ void finite_set_axioms::subset_axiom(expr* a) {
 
 void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
     // a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b)
-    expr_ref diff_ab(u.mk_difference(a, b), m);
+    expr_ref diff_ab(u.mk_ext(a, b), m);
 
     expr_ref a_eq_b(m.mk_eq(a, b), m);
     expr_ref diff_in_a(u.mk_in(diff_ab, a), m);
@@ -370,9 +374,9 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
     ax->clause.push_back(m.mk_not(diff_in_b));
     m_add_clause(ax);
 
-    theory_axiom* ax2 = alloc(theory_axiom, m, "extensionality", a, b);
+    ax = alloc(theory_axiom, m, "extensionality", a, b);
-    ax2->clause.push_back(m.mk_not(a_eq_b));
+    ax->clause.push_back(a_eq_b);
-    ax2->clause.push_back(diff_in_a);
+    ax->clause.push_back(diff_in_a);
-    ax2->clause.push_back(diff_in_b);
+    ax->clause.push_back(diff_in_b);
-    m_add_clause(ax2);
+    m_add_clause(ax);
 }

src/ast/rewriter/finite_set_rewriter.cpp

@@ -11,7 +11,7 @@ Abstract:
 
 Author:
 
-    GitHub Copilot Agent 2025
+    Nikolaj Bjorner (nbjorner) - October 2025
 
 --*/
 
@@ -222,6 +222,44 @@ br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result)
         result = m.mk_eq(elem, singleton_elem);
         return BR_REWRITE1;
     }
+    // NB we don't rewrite (set.in x (set.union s t)) to (or (set.in x s) (set.in x t))
+    // because it creates two new sub-expressions. The expression (set.union s t) could
+    // be shared with other expressions so the net effect of this rewrite could be to create
+    // a larger formula for the solver.
+    return BR_FAILED;
+}
+
+
+/**
+* if a, b are set expressions we can create an on-the-fly heap for their min-elements
+* a, b are normalized to the form (set.union s t) or (set.empty) where 
+* s is a singleton or range expression such that every element in t are above s.
+* we distinguish numerical values from value expressions:
+* - for numerical values we use the ordering over numerals to pick minimal ranges
+* - for unique value expressions ranging over non-numerals use expression identifiers
+* - for other expressions use identifiers to sort expressions, but make sure to be inconclusive
+*   for set difference
+* We want mk_eq_core to produce a result true/false if the arguments are both (unique) values.
+* This allows to evaluate models for being well-formed conclusively.
+* 
+* A way to convert a set expression to a heap is as follows:
+* 
+* min({s}) = {s} u {}
+* min({}) = {}
+* min([l..u]) = [l..u] u {}
+* min(s u t) = 
+*   let range_s u s1 = min(s)
+*   let range_t u t1 = min(t)
+*   if range_s < range_t: 
+*        range_s u (t u s1)
+*   if range_t < range_t:
+*        range_t u (s u t1)
+*   if range_t n range_s != {}:
+*        min(range_t, range_s) u the rest ...
+*   etc.
+*/
+
+br_status finite_set_rewriter::mk_eq_core(expr* a, expr* b, expr_ref& result) {
 
     return BR_FAILED;
 }

src/ast/rewriter/finite_set_rewriter.h

@@ -55,5 +55,7 @@ public:
     finite_set_util& util() { return m_util; }
 
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);   
+
+    br_status mk_eq_core(expr *a, expr *b, expr_ref &result);
 };
 

src/ast/rewriter/th_rewriter.cpp

@@ -688,6 +688,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             st = m_ar_rw.mk_eq_core(a, b, result);
         else if (s_fid == m_seq_rw.get_fid())
             st = m_seq_rw.mk_eq_core(a, b, result);
+        else if (s_fid == m_fs_rw.get_fid())
+            st = m_fs_rw.mk_eq_core(a, b, result);
         if (st != BR_FAILED)
             return st;
         st = extended_bv_eq(a, b, result);

src/smt/theory_finite_set.cpp

@@ -344,6 +344,7 @@ namespace smt {
             if (u.is_size(e))
                 has_size = true;
         }
+        TRACE(finite_set, tout << "has-map " << has_map << " has-filter-size " << has_filter << has_size << "\n");
         if (has_map)
             return false; // todo use more expensive model check here
         if (has_filter && has_size)
@@ -408,12 +409,12 @@ namespace smt {
         // walk the watch list and try to find new watches or propagate
         unsigned j = 0;
         for (unsigned i = 0; i < m_clauses.watch[idx].size(); ++i) {
-            TRACE(finite_set, tout << " watch[" << i << "] size: " << m_clauses.watch[i].size() << "\n";);
+            TRACE(finite_set, tout << "watch[" << i << "] size: " << m_clauses.watch[i].size() << "\n";);
             auto clause_idx = m_clauses.watch[idx][i];
             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";);
+                TRACE(finite_set, tout << "satisfied\n";);
                 m_clauses.watch[idx][j++] = clause_idx;
                 continue; // clause is already satisfied
             }
@@ -445,7 +446,7 @@ namespace smt {
                 auto litid = 2 * lit->get_id() + litneg;              
                 m_clauses.watch.reserve(litid + 1);
                 m_clauses.watch[litid].push_back(clause_idx);
-                TRACE(finite_set, tout << "  new watch for " << mk_pp(lit, m) << "\n";);
+                TRACE(finite_set, tout << "new watch for " << mk_pp(lit, m) << "\n";);
                 found_swap = true;
                 break;
             }
@@ -454,7 +455,7 @@ namespace smt {
             // either all literals are false, or the other watch literal is propagating.
             m_clauses.squeue.push_back(clause_idx);
             ctx.push_trail(push_back_vector(m_clauses.squeue));
-            TRACE(finite_set, tout << "  propagate clause\n";);
+            TRACE(finite_set, tout << "propagate clause\n";);
             m_clauses.watch[idx][j++] = clause_idx;
             ++i;
             for (; i < m_clauses.watch[idx].size(); ++i)
@@ -630,11 +631,11 @@ namespace smt {
     void theory_finite_set::add_membership_axioms(expr *elem, expr *set) {
         TRACE(finite_set, tout << "add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";);
 
-        if (!is_new_axiom(elem, set))
+        try {
-            return;
-
             // Instantiate appropriate axiom based on set structure
-        if (u.is_empty(set)) {
+            if (!is_new_axiom(elem, set))
+                ;
+            else if (u.is_empty(set)) {
                 m_axioms.in_empty_axiom(elem);
             }
             else if (u.is_singleton(set)) {
@@ -659,10 +660,15 @@ namespace smt {
             else if (u.is_filter(set)) {
                 m_axioms.in_filter_axiom(elem, set);
             }
+        } catch (...) {
+            TRACE(finite_set, tout << "exception\n");
+            throw;
+        }
+        TRACE(finite_set, tout << "after add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";);
     }
 
     void theory_finite_set::add_clause(theory_axiom* ax) {
-        TRACE(finite_set, tout << "add_clause: " << ax << "\n");
+        TRACE(finite_set, tout << "add_clause: " << *ax << "\n");
         ctx.push_trail(push_back_vector(m_clauses.axioms));
         ctx.push_trail(new_obj_trail(ax));
         m_clauses.axioms.push_back(ax);
@@ -933,7 +939,7 @@ namespace smt {
         }
 
         if (undef_count == 1) {
-            TRACE(finite_set, tout << " propagate unit: " << mk_pp(unit, m) << "\n" << clause << "\n";);
+            TRACE(finite_set, tout << "propagate unit: " << mk_pp(unit, m) << "\n" << clause << "\n";);
             auto lit = mk_literal(unit);
             literal_vector antecedent;
             for (auto e : clause) {
@@ -951,15 +957,10 @@ namespace smt {
                 // only propagations that are processed by conflict resolution. 
                 // this misses conflicts at base level.
                 proof_ref pr(m);
-                expr_ref_vector args(m);
+                proof_ref_vector args(m);
-                for (auto const &p : ax->params) {
+                for (auto a : antecedent) 
-                    if (p.is_ast())
+                    args.push_back(m.mk_hypothesis(ctx.literal2expr(a)));          
-                        args.push_back(to_expr(p.get_ast()));
+                pr = m.mk_th_lemma(get_id(), unit, args.size(), args.data(), ax->params.size(), ax->params.data());
-                    else
-                        args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort()));
-                }
-                
-                pr = m.mk_app(m.get_family_name(get_family_id()), 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);
@@ -972,7 +973,7 @@ namespace smt {
             m_stats.m_num_axioms_conflicts++;
         else
             m_stats.m_num_axioms_case_splits++;
-        TRACE(finite_set, tout << " assert " << (is_conflict ? "conflict" : "case split") << clause << "\n";);
+        TRACE(finite_set, tout << "assert " << (is_conflict ? "conflict" : "case split") << clause << "\n";);
         literal_vector lclause;
         for (auto e : clause)
             lclause.push_back(mk_literal(e));