Refactor mk_and/mk_or call sites to use vector overloads (#8286)

* Initial plan

* Refactor mk_and and mk_or call sites to use overloaded methods

Changed 130 call sites across 64 files to use vector overloads directly instead of manually passing .size() and .data()/.c_ptr()

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Revert mk_or changes for ptr_buffer/ptr_vector (no overload exists in ast_util.h)

* Fix compilation errors from mk_and/mk_or refactoring

Fixed type mismatches by:
- Removing m parameter for expr_ref_vector (ast_util.h has mk_and/mk_or(expr_ref_vector) overloads)
- Reverting changes for ref_buffer types (no overload exists in ast_util.h, only in ast.h for m.mk_and)
- Verified build succeeds and Z3 works correctly

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix test files to use correct mk_and/mk_or overloads

Changed test/doc.cpp and test/udoc_relation.cpp to use mk_and(expr_ref_vector) and mk_or(expr_ref_vector) without m parameter

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/muz/base/dl_rule.cpp

@@ -564,7 +564,7 @@ namespace datalog {
         switch (body.size()) {
         case 0:  break;
         case 1:  fml = m.mk_implies(body[0].get(), fml); break;
-        default: fml = m.mk_implies(m.mk_and(body.size(), body.data()), fml); break;
+        default: fml = m.mk_implies(m.mk_and(body), fml); break;
         }
 
         m_free_vars.reset();        

src/muz/base/hnf.cpp

@@ -450,7 +450,7 @@ private:
         case 1: 
             return app_ref(m.mk_implies(body[0], head), m);
         default:
-            return app_ref(m.mk_implies(m.mk_and(body.size(), body.data()), head), m);
+            return app_ref(m.mk_implies(m.mk_and(body), head), m);
         }        
     }
 

src/muz/ddnf/ddnf.cpp

@@ -850,7 +850,7 @@ namespace datalog {
                 result = eqs[0].get();
                 break;
             default:
-                result = m.mk_or(eqs.size(), eqs.data());
+                result = m.mk_or(eqs);
                 break;
             }
         }

src/muz/fp/horn_tactic.cpp

@@ -160,13 +160,13 @@ class horn_tactic : public tactic {
             }
             if (head) {
                 if (!is_implication(f)) {
-                    f = m.mk_and(body.size(), body.data());
+                    f = m.mk_and(body);
                     f = m.mk_implies(f, head);
                 }
                 return IS_RULE;
             }
             else {
-                f = m.mk_and(body.size(), body.data());
+                f = m.mk_and(body);
                 return IS_QUERY;
             }
         }

src/muz/rel/aig_exporter.cpp

@@ -125,7 +125,7 @@ namespace datalog {
                     exprs.push_back(e);
                 }
 
-                transition_function.push_back(m.mk_and(exprs.size(), exprs.data()));
+                transition_function.push_back(m.mk_and(exprs));
             }
         }
 
@@ -140,11 +140,11 @@ namespace datalog {
                     exprs.push_back(m.mk_eq(get_latch_var(i, m_latch_varsp), I->second[i]));
                 }
 
-                transition_function.push_back(m.mk_and(exprs.size(), exprs.data()));
+                transition_function.push_back(m.mk_and(exprs));
             }
         }
 
-        expr *tr = m.mk_or(transition_function.size(), transition_function.data());
+        expr *tr = m.mk_or(transition_function);
         aig_ref aig = m_aigm.mk_aig(tr);
         expr_ref aig_expr(m);
         m_aigm.to_formula(aig, aig_expr);
@@ -186,10 +186,10 @@ namespace datalog {
             for (func_decl* pred : preds) {
                 exprs.reset();
                 assert_pred_id(pred, m_ruleid_var_set, exprs);
-                output.push_back(m.mk_and(exprs.size(), exprs.data()));
+                output.push_back(m.mk_and(exprs));
             }
 
-            expr *out = m.mk_or(output.size(), output.data());
+            expr *out = m.mk_or(output);
             aig = m_aigm.mk_aig(out);
             m_aigm.to_formula(aig, aig_expr);
             output_id = expr_to_aig(aig_expr);

src/muz/rel/check_relation.cpp

@@ -39,7 +39,7 @@ namespace datalog {
         for (unsigned i = 0; i < sig.size(); ++i) {
             conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), f[i]));
         }
-        return expr_ref(mk_and(m, conjs.size(), conjs.data()), m);
+        return expr_ref(mk_and(conjs), m);
     }
 
     expr_ref check_relation::ground(expr* fml) const {
@@ -535,7 +535,7 @@ namespace datalog {
                 unsigned c2 = m_cols[i];
                 conds.push_back(m.mk_eq(m.mk_var(c1, sig[c1]), m.mk_var(c2, sig[c2])));
             }
-            cond = mk_and(m, conds.size(), conds.data());
+            cond = mk_and(conds);
             r.consistent_formula();
             (*m_filter)(r.rb());
             p.verify_filter(r.m_fml, r.rb(), cond);
@@ -720,7 +720,7 @@ namespace datalog {
             v2 = m.mk_var(c2, sig2[c2]);
             eqs.push_back(m.mk_eq(v1, v2));
         }
-        negf = mk_and(m, eqs.size(), eqs.data());
+        negf = mk_and(eqs);
         ptr_vector<sort> rev_sig2(sig2.size(), sig2.data());
         rev_sig2.reverse();
         svector<symbol> names;

src/muz/rel/dl_compiler.cpp

@@ -677,7 +677,7 @@ namespace datalog {
 
         // enforce interpreted tail predicates
         if (!tail.empty()) {
-            app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.data()), m);
+            app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail), m);
 
             // check if there are any columns to remove
             unsigned_vector remove_columns;

src/muz/rel/dl_finite_product_relation.cpp

@@ -2367,7 +2367,7 @@ namespace datalog {
             }
             sh(tmp, fact_sz-1, tmp);
             conjs.push_back(tmp);
-            disjs.push_back(m.mk_and(conjs.size(), conjs.data()));
+            disjs.push_back(m.mk_and(conjs));
         }
         bool_rewriter(m).mk_or(disjs.size(), disjs.data(), fml);
     }

src/muz/rel/doc.cpp

@@ -711,7 +711,7 @@ expr_ref doc_manager::to_formula(ast_manager & m, tbv const& src) {
             break;            
         }        
     }
-    result = mk_and(m, conj.size(), conj.data());
+    result = mk_and(conj);
     return result;    
 }
 
@@ -726,7 +726,7 @@ expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
     for (unsigned i = 0; i < src.neg().size(); ++i) {
         conj.push_back(m.mk_not(to_formula(m, src.neg()[i])));
     }
-    result = mk_and(m, conj.size(), conj.data());
+    result = mk_and(conj);
     return result;
 }
     

src/muz/rel/rel_context.cpp

@@ -261,7 +261,7 @@ namespace datalog {
             }
             SASSERT(!m_last_result_relation);
             if (some_non_empty) {
-                m_answer = mk_and(m, ans.size(), ans.data());
+                m_answer = mk_and(ans);
                 if (is_approx) {
                     TRACE(dl, tout << "approx\n";);
                     res = l_undef;

src/muz/rel/udoc_relation.cpp

@@ -109,7 +109,7 @@ namespace datalog {
         for (unsigned i = 0; i < m_elems.size(); ++i) {
             disj.push_back(to_formula(m_elems[i]));
         }
-        fml = mk_or(m, disj.size(), disj.data());
+        fml = mk_or(disj);
     }
     expr_ref udoc_relation::to_formula(doc const& d) const {
         ast_manager& m = get_plugin().get_ast_manager();
@@ -119,7 +119,7 @@ namespace datalog {
         for (unsigned i = 0; i < d.neg().size(); ++i) {
             conjs.push_back(m.mk_not(to_formula(d.neg()[i])));
         }
-        result = mk_and(m, conjs.size(), conjs.data());
+        result = mk_and(conjs);
         return result;
     }
     expr_ref udoc_relation::to_formula(tbv const& t) const {
@@ -168,7 +168,7 @@ namespace datalog {
                 }
             }
         }
-        result = mk_and(m, conjs.size(), conjs.data());
+        result = mk_and(conjs);
         return result;
     }
 
@@ -664,8 +664,8 @@ namespace datalog {
                 rests.push_back(g);
             }
         }
-        guard = mk_and(m, guards.size(), guards.data());
-        rest  = mk_and(m, rests.size(),  rests.data());        
+        guard = mk_and(guards);
+        rest  = mk_and(rests);        
     }
     void udoc_relation::extract_equalities(expr* g, expr_ref& rest, subset_ints& equalities,
                                            unsigned_vector& roots) const {
@@ -683,7 +683,7 @@ namespace datalog {
                 conds.pop_back();
             }
         }
-        rest = mk_and(m, conds.size(), conds.data());
+        rest = mk_and(conds);
     }
 
     void udoc_relation::extract_equalities(

src/muz/spacer/spacer_context.cpp

@@ -2592,7 +2592,7 @@ bool context::validate() {
                 for (unsigned j = utsz; j < tsz; ++j) {
                     fmls.push_back(r.get_tail(j));
                 }
-                tmp = m.mk_and(fmls.size(), fmls.data());
+                tmp = m.mk_and(fmls);
                 svector<symbol> names;
                 expr_free_vars fv;
                 fv (tmp);
@@ -4227,7 +4227,7 @@ bool context::check_invariant(unsigned lvl, func_decl* fn)
     if (m.is_true(inv)) { return true; }
     pt.add_premises(m_rels, lvl, conj);
     conj.push_back(m.mk_not(inv));
-    expr_ref fml(m.mk_and(conj.size(), conj.data()), m);
+    expr_ref fml(m.mk_and(conj), m);
     ctx->assert_expr(fml);
     lbool result = ctx->check_sat(0, nullptr);
     TRACE(spacer, tout << "Check invariant level: " << lvl << " " << result

src/muz/spacer/spacer_proof_utils.cpp

@@ -815,7 +815,7 @@ namespace spacer {
 
         // make unit resolution proof step
         // expr_ref tmp(m);
-        // tmp = mk_or(m, pf_fact.size(), pf_fact.c_ptr());
+        // tmp = mk_or(m, pf_fact);
         // proof* res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), tmp);
         proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.data());
         m_pinned.push_back(res);

src/muz/spacer/spacer_qe_project.cpp

@@ -952,7 +952,7 @@ class arith_project_util {
         if (new_fml) {
             fml = new_fml;
             // add in eqs
-            fml = m.mk_and(fml, m.mk_and(eqs.size(), eqs.data()));
+            fml = m.mk_and(fml, m.mk_and(eqs));
         } else {
             // unchanged
             SASSERT(eqs.empty());
@@ -1023,7 +1023,7 @@ class arith_project_util {
                 lits.push_back(
                     a.mk_lt(t2, a.mk_numeral(abs(num_val), a.mk_int())));
 
-                new_fml = m.mk_and(lits.size(), lits.data());
+                new_fml = m.mk_and(lits);
             }
         } else if (!is_app(fml)) {
             new_fml = fml;
@@ -1656,7 +1656,7 @@ class array_project_eqs_util {
         lits.append(m_idx_lits_v);
         lits.append(m_aux_lits_v);
         lits.push_back(fml);
-        fml = m.mk_and(lits.size(), lits.data());
+        fml = m.mk_and(lits);
 
         if (m_subst_term_v) {
             m_true_sub_v.insert(m_v, m_subst_term_v);
@@ -1859,7 +1859,7 @@ class array_select_reducer {
         expr_ref_vector lits(m);
         lits.append(m_idx_lits);
         lits.push_back(fml);
-        fml = m.mk_and(lits.size(), lits.data());
+        fml = m.mk_and(lits);
         // simplify all trivial expressions introduced
         m_rw(fml);
 
@@ -2074,7 +2074,7 @@ class array_project_selects_util {
         expr_ref_vector lits(m);
         lits.append(m_idx_lits);
         lits.push_back(fml);
-        fml = m.mk_and(lits.size(), lits.data());
+        fml = m.mk_and(lits);
 
         // substitute for sel terms
         m_sub(fml);

src/muz/tab/tab_context.cpp

@@ -567,7 +567,7 @@ namespace tb {
             }
             fml = vs(g.get_constraint(), vars.size(), vars.data());
             fmls.push_back(fml);
-            m_precond = m.mk_and(fmls.size(), fmls.data());
+            m_precond = m.mk_and(fmls);
             IF_VERBOSE(2,
                        verbose_stream() << "setup-match: ";
                        for (unsigned i = 0; i < m_preds.size(); ++i) {

src/muz/transforms/dl_mk_array_blast.cpp

@@ -227,10 +227,10 @@ namespace datalog {
                 for (unsigned j = 0; j < args1.size(); ++j) {
                     eqs.push_back(m.mk_eq(args1[j], args2[j]));
                 }
-                conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.data()), m.mk_eq(v1, v2)));
+                conjs.push_back(m.mk_implies(m.mk_and(eqs), m.mk_eq(v1, v2)));
             }
         }
-        body = m.mk_and(conjs.size(), conjs.data());        
+        body = m.mk_and(conjs);        
         m_rewriter(body);   
         return true;
     }
@@ -278,7 +278,7 @@ namespace datalog {
             return false;        
         }
         expr_ref fml1(m), fml2(m), body(m), head(m);
-        body = m.mk_and(new_conjs.size(), new_conjs.data());
+        body = m.mk_and(new_conjs);
         head = r.get_head();
         sub(body);
         m_rewriter(body);

src/muz/transforms/dl_mk_array_eq_rewrite.cpp

@@ -99,7 +99,7 @@ namespace datalog {
             res_conjs.push_back(tmp);
         }
         proof_ref pr(m);
-        m_src_manager->mk_rule(m.mk_implies(m.mk_and(res_conjs.size(), res_conjs.data()), r.get_head()), pr, dest, r.name());
+        m_src_manager->mk_rule(m.mk_implies(m.mk_and(res_conjs), r.get_head()), pr, dest, r.name());
     }
 
     // NSB Code review: use substitution facility, such as expr_safe_replace or expr_replacer.

src/muz/transforms/dl_mk_array_instantiation.cpp

@@ -100,7 +100,7 @@ namespace datalog {
             new_tail.push_back(m.mk_eq(kv.m_value, tmp));
         }
         proof_ref pr(m);
-        src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.data()), new_head), pr, dest, r.name());
+        src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail), new_head), pr, dest, r.name());
     }
 
     expr_ref mk_array_instantiation::create_head(app* old_head)  {

src/muz/transforms/dl_mk_interp_tail_simplifier.cpp

@@ -347,11 +347,11 @@ namespace datalog {
             }
             else {
                 if (m.is_and(f)) {
-                    result = m.mk_and(m_app_args.size(), m_app_args.data());
+                    result = m.mk_and(m_app_args);
                 }
                 else {
                     SASSERT(m.is_or(f));
-                    result = m.mk_or(m_app_args.size(), m_app_args.data());
+                    result = m.mk_or(m_app_args);
                 }
             }
 
@@ -529,7 +529,7 @@ namespace datalog {
                 m_itail_members.push_back(r->get_tail(i));
                 SASSERT(!r->is_neg_tail(i));
             }
-            itail = m.mk_and(m_itail_members.size(), m_itail_members.data());
+            itail = m.mk_and(m_itail_members);
             modified = true;
         }
 

src/muz/transforms/dl_mk_quantifier_abstraction.cpp

@@ -340,7 +340,7 @@ namespace datalog {
                 tail.push_back(r.get_tail(j));
             }
             head = mk_head(source, *result, r.get_head(), cnt);
-            fml = m.mk_implies(m.mk_and(tail.size(), tail.data()), head);
+            fml = m.mk_implies(m.mk_and(tail), head);
             proof_ref pr(m);
             rm.mk_rule(fml, pr, *result, r.name());
             TRACE(dl, result->last()->display(m_ctx, tout););

src/muz/transforms/dl_mk_quantifier_instantiation.cpp

@@ -202,7 +202,7 @@ namespace datalog {
         m_terms.reset();
         m_var2cnst.reset();
         m_cnst2var.reset();
-        fml = m.mk_and(conjs.size(), conjs.data());
+        fml = m.mk_and(conjs);
 
         for (unsigned i = 0; i < sorts.size(); ++i) {
             var = m.mk_var(i, sorts[i]);
@@ -211,7 +211,7 @@ namespace datalog {
             m_cnst2var.insert(cnst, var);
         }
 
-        fml = m.mk_and(conjs.size(), conjs.data());
+        fml = m.mk_and(conjs);
         m_var2cnst(fml);
         collect_egraph(fml);
 
@@ -221,7 +221,7 @@ namespace datalog {
         for (auto & kv : m_funs) dealloc(kv.m_value);
         m_funs.reset();
 
-        fml = m.mk_and(conjs.size(), conjs.data());
+        fml = m.mk_and(conjs);
         fml = m.mk_implies(fml, r.get_head());
         TRACE(dl, r.display(m_ctx, tout); tout << mk_pp(fml, m) << "\n";);