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/ast/macros/quasi_macros.cpp

@@ -262,7 +262,7 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
                                                   f->get_arity(), f->get_domain(),
                                                   f->get_range());
     expr_ref f_else(m.mk_app(fd, m_new_vars.size(), m_new_vars.data()), m);
-    expr_ref ite(m.mk_ite(m.mk_and(m_new_eqs.size(), m_new_eqs.data()), t, f_else), m);
+    expr_ref ite(m.mk_ite(m.mk_and(m_new_eqs), t, f_else), m);
 
     expr_ref eq(m.mk_eq(appl, ite), m);
 

src/ast/proofs/proof_checker.cpp

@@ -170,7 +170,7 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
                 }
             }
             expr_ref rewrite_cond(m);
-            rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
+            rewrite_cond = m.mk_or(rewrite_eq);
             side_conditions.push_back(rewrite_cond.get());
             return true;
         }
@@ -431,7 +431,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                 }
             }
             expr_ref rewrite_cond(m);
-            rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.data());
+            rewrite_cond = m.mk_or(rewrite_eq);
             side_conditions.push_back(rewrite_cond.get());
             return true;
         }
@@ -819,7 +819,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             fmls[i] = premise1;
         }
         fmls[0] = premise0;
-        premise0 = m.mk_or(fmls.size(), fmls.data());
+        premise0 = m.mk_or(fmls);
         if (is_forall(conclusion)) {
             quantifier* q = to_quantifier(conclusion);
             premise0 = m.mk_iff(premise0, q->get_expr());
@@ -861,7 +861,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
         args.append(a->get_num_args(), a->get_args());
         lit = args[position].get();
         args[position] = m.mk_false();
-        e = m.mk_or(args.size(), args.data());
+        e = m.mk_or(args);
     }
     else if (m.is_implies(e, body, head)) {
         expr* const* heads = &head;
@@ -880,14 +880,14 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
             args.append(num_heads, heads);
             lit = args[position].get();
             args[position] = m.mk_false();
-            e = m.mk_implies(body, m.mk_or(args.size(), args.data()));
+            e = m.mk_implies(body, m.mk_or(args));
         }
         else {
             position -= num_heads;
             args.append(num_bodies, bodies);
             lit = m.mk_not(args[position].get());
             args[position] = m.mk_true();
-            e = m.mk_implies(m.mk_and(args.size(), args.data()), head);
+            e = m.mk_implies(m.mk_and(args), head);
         }
     }
     else if (position == 0) {

src/ast/proofs/proof_utils.cpp

@@ -556,7 +556,7 @@ public:
                     clause = m_literals[0];
                 }
                 else {
-                    clause = m.mk_or(m_literals.size(), m_literals.data());
+                    clause = m.mk_or(m_literals);
                 }
                 tmp = m.mk_lemma(tmp, clause);
                 m_refs.push_back(tmp);

src/ast/rewriter/bv_bounds.cpp

@@ -320,8 +320,8 @@ br_status bv_bounds::rewrite(unsigned limit, func_decl * f, unsigned num, expr *
     switch (nargs.size()) {
         case 0: result = negated ? m_m.mk_false() : m_m.mk_true(); return BR_DONE;
         case 1: result = nargs.get(0); return BR_DONE;
-        default: result = negated ? m_m.mk_or(nargs.size(), nargs.data())
+        default: result = negated ? m_m.mk_or(nargs)
-                                  : m_m.mk_and(nargs.size(), nargs.data());
+                                  : m_m.mk_and(nargs);
                  return BR_DONE;
     }
 }

src/ast/rewriter/elim_bounds.cpp

@@ -188,7 +188,7 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
         new_body = atoms[0];
         break;
     default:
-        new_body = m.mk_or(atoms.size(), atoms.data());
+        new_body = m.mk_or(atoms);
         break;
     }
     quantifier_ref new_q(m);

src/ast/rewriter/pb_rewriter.cpp

@@ -170,7 +170,7 @@ expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) {
     expr_ref fml2 = translate_pb2lia(vars, e2);    
     tmp = m.mk_not(m.mk_eq(fml1, fml2));
     fmls.push_back(tmp);
-    tmp = m.mk_and(fmls.size(), fmls.data());
+    tmp = m.mk_and(fmls);
     return tmp;
 }
 

src/cmd_context/tactic_cmds.cpp

@@ -368,10 +368,10 @@ public:
                         if (formulas.size() == 1)
                             or_args.push_back(formulas[0]);
                         else
-                            or_args.push_back(m.mk_and(formulas.size(), formulas.data()));
+                            or_args.push_back(m.mk_and(formulas));
                     }
                     expr_ref assertion_ref(m);
-                    assertion_ref = m.mk_or(or_args.size(), or_args.data());
+                    assertion_ref = m.mk_or(or_args);
                     expr * assertions[1] = { assertion_ref.get() };
                     ctx.display_smt2_benchmark(ctx.regular_stream(), 1, assertions);
                 }

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());
+        guard = mk_and(guards);
-        rest  = mk_and(m, rests.size(),  rests.data());        
+        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";);
         

src/opt/maxcore.cpp

@@ -719,7 +719,7 @@ public:
             max_resolve(core, w);
             break;
         }
-        fml = mk_not(m, mk_and(m, core.size(), core.data()));
+        fml = mk_not(m, mk_and(m, core));
         add(fml);
         // save small cores such that lex-combinations of maxres can reuse these cores.
         if (core.size() <= 2) {

src/opt/opt_context.cpp

@@ -998,7 +998,7 @@ namespace opt {
             else if (is_objective(r->form(i)))
                 fmls.push_back(r->form(i));
             else
-                fmls.push_back(m.mk_implies(mk_and(m, deps.size(), deps.data()), r->form(i)));
+                fmls.push_back(m.mk_implies(mk_and(m, deps), r->form(i)));
         }        
         if (r->inconsistent()) {
             ptr_vector<expr> core_elems;

src/opt/opt_parse.cpp

@@ -134,7 +134,7 @@ class wcnf {
             if (parsed_lit < 0) p = m.mk_not(p);
             ors.push_back(p);
         }
-        result = to_app(mk_or(m, ors.size(), ors.data()));
+        result = to_app(mk_or(ors));
         return result;
     }
 
@@ -153,7 +153,7 @@ class wcnf {
                 p = m.mk_not(p);
             ors.push_back(p);
         }
-        result = to_app(mk_or(m, ors.size(), ors.data()));
+        result = to_app(mk_or(ors));
         return result;
     }
     

src/qe/lite/qe_lite_tactic.cpp

@@ -550,7 +550,7 @@ namespace qel {
         void flatten_definitions(expr_ref_vector& conjs) {
             TRACE(qe_lite,
                   expr_ref tmp(m);
-                  tmp = m.mk_and(conjs.size(), conjs.data());
+                  tmp = m.mk_and(conjs);
                   tout << mk_pp(tmp, m) << "\n";);
             for (unsigned i = 0; i < conjs.size(); ++i) {
                 expr* c = conjs[i].get();
@@ -586,7 +586,7 @@ namespace qel {
             }
             TRACE(qe_lite,
                   expr_ref tmp(m);
-                  tmp = m.mk_and(conjs.size(), conjs.data());
+                  tmp = m.mk_and(conjs);
                   tout << "after flatten\n" << mk_pp(tmp, m) << "\n";);
         }
 
@@ -665,7 +665,7 @@ namespace qel {
 
                 if (!m_order.empty()) {
                     expr_ref r(m), new_r(m);
-                    r = m.mk_and(conjs.size(), conjs.data());
+                    r = m.mk_and(conjs);
                     create_substitution(largest_vinx + 1);
                     new_r = m_subst(r, m_subst_map.size(), m_subst_map.data());
                     m_rewriter(new_r);
@@ -1550,7 +1550,7 @@ namespace fm {
             if (lits.size() == 1)
                 return to_app(lits[0]);
             else
-                return m.mk_or(lits.size(), lits.data());
+                return m.mk_or(lits);
         }
 
         var mk_var(expr * t) {

src/qe/nlqsat.cpp

@@ -858,7 +858,7 @@ namespace qe {
             ptr_vector<expr> fmls;
             expr_ref fml(m);
             in->get_formulas(fmls);
-            fml = mk_and(m, fmls.size(), fmls.data());
+            fml = mk_and(m, fmls);
             if (m_mode == elim_t) {
                 fml = m.mk_not(fml);
             }                         

src/qe/qe_datatype_plugin.cpp

@@ -388,7 +388,7 @@ namespace qe {
                 expr* l_i = l->get_arg(i);
                 conj.push_back(m.mk_eq(l_i, r_i));                
             }
-            expr* e = m.mk_and(conj.size(), conj.data());
+            expr* e = m.mk_and(conj);
             m_map.insert(a, e, nullptr);
             TRACE(qe, tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
             return true;

src/qe/qsat.cpp

@@ -1282,7 +1282,7 @@ namespace qe {
             expr_ref_vector defs(m);
             expr_ref fml(m);
             in->get_formulas(fmls);
-            fml = mk_and(m, fmls.size(), fmls.data());
+            fml = mk_and(m, fmls);
             
             // for now:
             // fail if cores.  (TBD)

src/sat/sat_solver/inc_sat_solver.cpp

@@ -352,7 +352,7 @@ public:
                 expr_ref_vector args(m);
                 args.push_back(::mk_not(m, a));
                 args.append(to_app(t)->get_num_args(), to_app(t)->get_args());
-                assert_expr_core(m.mk_or(args.size(), args.data()));
+                assert_expr_core(m.mk_or(args));
             }
             else {
                 m_is_cnf = false;

src/smt/qi_queue.cpp

@@ -273,7 +273,7 @@ namespace smt {
             ptr_vector<expr> args;
             args.push_back(m.mk_not(q));
             args.append(to_app(s_instance)->get_num_args(), to_app(s_instance)->get_args());
-            lemma = m.mk_or(args.size(), args.data());
+            lemma = m.mk_or(args);
         }
         else if (m.is_false(s_instance)) {
             lemma = m.mk_not(q);

src/smt/smt_clause.cpp

@@ -122,7 +122,7 @@ namespace smt {
             args.push_back(bool_var2expr_map[lit.var()]);
             if (lit.sign()) args[args.size()-1] = m.mk_not(args.back());
         }
-        expr_ref disj(m.mk_or(args.size(), args.data()), m);
+        expr_ref disj(m.mk_or(args), m);
         return out << mk_pp(disj, m, 3);
     }
 

src/smt/smt_conflict_resolution.cpp

@@ -1348,7 +1348,7 @@ namespace smt {
         switch (lits.size()) {
         case 0:  fact = nullptr; break;
         case 1:  fact = lits[0]; break;
-        default: fact = m.mk_or(lits.size(), lits.data());
+        default: fact = m.mk_or(lits);
         }
         if (fact == nullptr)
             m_lemma_proof = pr;

src/smt/smt_implied_equalities.cpp

@@ -550,7 +550,7 @@ namespace smt {
                 eqs.push_back(eq_lit);
                 m_solver.assert_expr(m.mk_implies(eq_lit, eq));
             }
-            m_solver.assert_expr(m.mk_not(m.mk_and(eqs.size(), eqs.c_ptr())));
+            m_solver.assert_expr(m.mk_not(m.mk_and(eqs)));
             lbool is_sat = m_solver.check_sat(0,0);
             switch(is_sat) {
             case l_false:

src/smt/smt_internalizer.cpp

@@ -1605,7 +1605,7 @@ namespace smt {
         if (root_gate)
             new_lits.push_back(m.mk_not(root_gate));
         SASSERT(num_lits > 1);
-        expr * fact        = m.mk_or(new_lits.size(), new_lits.data());
+        expr * fact        = m.mk_or(new_lits);
         return m.mk_def_axiom(fact);
         
     }

src/smt/smt_justification.cpp

@@ -281,7 +281,7 @@ namespace smt {
         if (lits.size() == 1)
             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.data());
         else
-            return m.mk_th_lemma(m_th_id, m.mk_or(lits.size(), lits.data()), 0, nullptr, m_params.size(), m_params.data());
+            return m.mk_th_lemma(m_th_id, m.mk_or(lits), 0, nullptr, m_params.size(), m_params.data());
     }
 
     proof * theory_propagation_justification::mk_proof(conflict_resolution & cr) {
@@ -436,7 +436,7 @@ namespace smt {
         if (lits.size() == 1)
             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.data());
         else
-            return m.mk_th_lemma(m_th_id, m.mk_or(lits.size(), lits.data()), 0, nullptr, m_params.size(), m_params.data());
+            return m.mk_th_lemma(m_th_id, m.mk_or(lits), 0, nullptr, m_params.size(), m_params.data());
     }
 
 };

src/smt/smt_model_checker.cpp

@@ -152,7 +152,7 @@ namespace smt {
         for (expr * e : universe) {
             eqs.push_back(m.mk_eq(sk, e));
         }
-        expr_ref fml(m.mk_or(eqs.size(), eqs.data()), m);
+        expr_ref fml(m.mk_or(eqs), m);
         m_aux_context->assert_expr(fml);
     }
 
@@ -319,7 +319,7 @@ namespace smt {
             diseqs.push_back(m.mk_not(m.mk_eq(sk, sk_value)));
         }
         expr_ref blocking_clause(m);
-        blocking_clause = m.mk_or(diseqs.size(), diseqs.data());
+        blocking_clause = m.mk_or(diseqs);
         TRACE(model_checker, tout << "blocking clause:\n" << mk_ismt2_pp(blocking_clause, m) << "\n";);
         m_aux_context->assert_expr(blocking_clause);
         return true;

src/smt/smt_model_finder.cpp

@@ -2562,7 +2562,7 @@ namespace smt {
                 eqs.push_back(m.mk_eq(sk, val));
             }
             expr_ref new_cnstr(m);
-            new_cnstr = m.mk_or(eqs.size(), eqs.data());
+            new_cnstr = m.mk_or(eqs);
             TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";);
             aux_ctx->assert_expr(new_cnstr);
             asserted_something = true;

src/smt/tactic/ctx_solver_simplify_tactic.cpp

@@ -104,7 +104,7 @@ protected:
             return;
         ptr_vector<expr> fmls;
         g.get_formulas(fmls);
-        fml = mk_and(m, fmls.size(), fmls.data());
+        fml = mk_and(m, fmls);
         m_solver.push();
         reduce(fml);
         m_solver.pop(1);
@@ -122,7 +122,7 @@ protected:
             // enable_trace("after_search");
             m_solver.push();
             expr_ref fml1(m);
-            fml1 = mk_and(m, fmls.size(), fmls.data());
+            fml1 = mk_and(m, fmls);
             fml1 = m.mk_iff(fml, fml1);
             fml1 = m.mk_not(fml1);
             m_solver.assert_expr(fml1);

src/smt/theory_dense_diff_logic_def.h

@@ -1093,7 +1093,7 @@ namespace smt {
         else {
             // 
             expr_ref_vector const& core = m_objective_assignments[v];
-            f = m.mk_and(core.size(), core.data());
+            f = m.mk_and(core);
             if (is_strict) {
                 f = m.mk_not(f);
             }
@@ -1109,7 +1109,7 @@ namespace smt {
             }
             else {
                 expr_ref_vector const& core = m_objective_assignments[v];
-                f = m.mk_and(core.size(), core.data());
+                f = m.mk_and(core);
             }
         }
         else {

src/smt/theory_diff_logic_def.h

@@ -1353,7 +1353,7 @@ expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool
     else {
         // 
         expr_ref_vector const& core = m_objective_assignments[v];
-        f = m.mk_and(core.size(), core.data());
+        f = m.mk_and(core);
         if (is_strict) {
             f = m.mk_not(f);
         }
@@ -1369,7 +1369,7 @@ expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool
         }
         else {
             expr_ref_vector const& core = m_objective_assignments[v];
-            f = m.mk_and(core.size(), core.data());            
+            f = m.mk_and(core);            
         }
     }
     else {
@@ -1399,7 +1399,7 @@ expr_ref theory_diff_logic<Ext>::mk_ge(generic_model_converter& fm, theory_var v
     ptr_vector<expr> formulas(ctx.get_num_asserted_formulas(), ctx.get_asserted_formulas());
     model_implicant impl_extractor(m);
     expr_ref_vector implicants = impl_extractor.minimize_literals(formulas, mdl);
-    return m.mk_and(o, m.mk_not(m.mk_and(implicants.size(), implicants.c_ptr())));
+    return m.mk_and(o, m.mk_not(m.mk_and(implicants)));
 #endif
 
 template<typename Ext>

src/smt/theory_pb.cpp

@@ -1280,7 +1280,7 @@ namespace smt {
                 ctx.literal2expr(lits[i], tmp);
                 es.push_back(tmp);
             }
-            tmp = m.mk_or(es.size(), es.data());
+            tmp = m.mk_or(es);
             bool_var v = ctx.b_internalized(tmp)?ctx.get_bool_var(tmp):ctx.mk_bool_var(tmp);
             return literal(v);
         }
@@ -1292,7 +1292,7 @@ namespace smt {
                 ctx.literal2expr(lits[i], tmp);
                 es.push_back(tmp);
             }
-            tmp = m.mk_and(es.size(), es.data());
+            tmp = m.mk_and(es);
             bool_var v = ctx.b_internalized(tmp)?ctx.get_bool_var(tmp):ctx.mk_bool_var(tmp);
             return literal(v);
         }
@@ -1624,7 +1624,7 @@ namespace smt {
                 literal lit = cls.get_literal(i);
                 args.push_back(literal2expr(lit));
             }
-            result = m.mk_or(args.size(), args.data());
+            result = m.mk_or(args);
             break;
         }
         case b_justification::BIN_CLAUSE:
@@ -2025,7 +2025,7 @@ namespace smt {
             for (literal lit : m_antecedents) {
                 args.push_back(literal2expr(lit));
             }
-            B = m.mk_not(m.mk_and(args.size(), args.data()));
+            B = m.mk_not(m.mk_and(args));
             validate_implies(A, B); );
         return true;
     }

src/smt/theory_wmaxsat.cpp

@@ -254,7 +254,7 @@ namespace smt {
                   //ctx.display(tout);                      
                   );
         }
-        expr_ref result(m.mk_or(disj.size(), disj.data()), m);
+        expr_ref result(m.mk_or(disj), m);
         TRACE(opt,
               tout << result << " weight: " << weight << "\n";
               tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);

src/tactic/arith/factor_tactic.cpp

@@ -77,7 +77,7 @@ class factor_tactic : public tactic {
             if (args.size() == 1)
                 result = args[0];
             else
-                result = m.mk_or(args.size(), args.data());
+                result = m.mk_or(args);
         }
 
         decl_kind flip(decl_kind k) {
@@ -161,9 +161,9 @@ class factor_tactic : public tactic {
             if (args.size() == 1)
                 result = args[0];
             else if (strict)
-                result = m.mk_and(args.size(), args.data());
+                result = m.mk_and(args);
             else
-                result = m.mk_or(args.size(), args.data());
+                result = m.mk_or(args);
         }
 
         br_status factor(func_decl * f, expr * lhs, expr * rhs, expr_ref & result) {

src/tactic/arith/fm_tactic.cpp

@@ -967,7 +967,7 @@ class fm_tactic : public tactic {
             if (lits.size() == 1)
                 return to_app(lits[0]);
             else
-                return m.mk_or(lits.size(), lits.data());
+                return m.mk_or(lits);
         }
         
         var mk_var(expr * t) {

src/tactic/arith/lia2card_tactic.cpp

@@ -341,7 +341,7 @@ public:
         if (!m.is_true(e)) {
             es.push_back(e);
         }
-        result = mk_and(m, es.size(), es.data());
+        result = mk_and(es);
         if (!m.is_true(e)) {
             es.pop_back();
         }

src/tactic/arith/pb2bv_tactic.cpp

@@ -293,7 +293,7 @@ private:
                     switch (m_cls.size()) {
                     case 0:  m_result.push_back(m.mk_false()); break;
                     case 1:  m_result.push_back(m_cls[0]); break;
-                    default: m_result.push_back(m.mk_or(m_cls.size(), m_cls.data()));
+                    default: m_result.push_back(m.mk_or(m_cls));
                     }
                     return;
                 }
@@ -380,7 +380,7 @@ private:
                 for (unsigned i = 0; i < m_p.size(); ++i) {
                     args.push_back(mon_lit2lit(m_p[i]));
                 }             
-                r = m.mk_or(args.size(), args.data());
+                r = m.mk_or(args);
                 return;
             }
         

src/tactic/bv/elim_small_bv_tactic.cpp

@@ -173,8 +173,8 @@ class elim_small_bv_tactic : public tactic {
                       for (unsigned k = 0; k < new_bodies.size(); ++k)
                           tout << mk_ismt2_pp(new_bodies[k].get(), m) << std::endl; );
                 
-                body = is_forall(q) ? m.mk_and(new_bodies.size(), new_bodies.data()) :
+                body = is_forall(q) ? m.mk_and(new_bodies) :
-                    m.mk_or(new_bodies.size(), new_bodies.data());
+                    m.mk_or(new_bodies);
                 SASSERT(is_well_sorted(m, body));
                 
                 proof_ref pr(m);

src/tactic/core/occf_tactic.cpp

@@ -175,7 +175,7 @@ class occf_tactic : public tactic {
                 }
                 if (keep != nullptr)
                     new_lits.push_back(keep);
-                g->update(i, m.mk_or(new_lits.size(), new_lits.data()), nullptr, d);
+                g->update(i, m.mk_or(new_lits), nullptr, d);
             }
             g->inc_depth();
             result.push_back(g.get());

src/tactic/core/symmetry_reduce_tactic.cpp

@@ -164,7 +164,7 @@ private:
         for (unsigned i = 0; i < g.size(); ++i) {
             conjs.push_back(g.form(i));
         }
-        fml = m.mk_and(conjs.size(), conjs.data());
+        fml = m.mk_and(conjs);
         normalize(fml);
     }
 

src/test/doc.cpp

@@ -173,7 +173,7 @@ class test_doc_cls {
             default: break;
             }
         }
-        result = mk_and(m, conjs.size(), conjs.data());
+        result = mk_and(conjs);
         return result;
     }
 
@@ -197,7 +197,7 @@ class test_doc_cls {
                 break;
             }
         }
-        result = mk_and(m, conjs.size(), conjs.data());
+        result = mk_and(conjs);
         return result;
     }
 
@@ -208,7 +208,7 @@ class test_doc_cls {
         for (unsigned i = 0; i < d.neg().size(); ++i) {
             conjs.push_back(m.mk_not(to_formula(d.neg()[i], m2)));
         }
-        result = mk_and(m, conjs.size(), conjs.data());
+        result = mk_and(conjs);
         return result;
     }
 
@@ -218,7 +218,7 @@ class test_doc_cls {
         for (unsigned i = 0; i < ud.size(); ++i) {
             disjs.push_back(to_formula(ud[i], m2));
         }
-        result = mk_or(m, disjs.size(), disjs.data());
+        result = mk_or(disjs);
         return result;
     }
 
@@ -299,7 +299,7 @@ class test_doc_cls {
             fmls.push_back(m.mk_not(mk_conj(*t)));
             d->neg().push_back(t);
         }
-        fml1 = mk_and(m, fmls.size(), fmls.data());
+        fml1 = mk_and(fmls);
         bool_vector to_merge(N, false);
         bit_vector discard_cols;
         discard_cols.resize(N, false);
@@ -321,7 +321,7 @@ class test_doc_cls {
             }
         }
         eqs.push_back(to_formula(*d, dm));
-        fml1 = mk_and(m, eqs.size(), eqs.data());
+        fml1 = mk_and(eqs);
         if (dm.merge(*d, lo, 1, equalities, discard_cols)) {
             fml2 = to_formula(*d, dm);
         }

src/test/hilbert_basis.cpp

@@ -163,13 +163,13 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
             }
             eqs.push_back(m.mk_eq(xs[j].get(), a.mk_add(sum.size(), sum.data())));
         }
-        fml = m.mk_and(eqs.size(), eqs.data());
+        fml = m.mk_and(eqs);
         if (!names.empty()) {
             fml = m.mk_exists(names.size(), sorts.data(), names.data(), fml);
         }
         fmls.push_back(fml);
     }
-    fml1 = m.mk_or(fmls.size(), fmls.data());
+    fml1 = m.mk_or(fmls);
     fmls.reset();
 
     sz = hb.get_num_ineqs();
@@ -194,7 +194,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
             fmls.push_back(a.mk_ge(lhs, rhs));
         }
     }
-    fml2 = m.mk_and(fmls.size(), fmls.data());
+    fml2 = m.mk_and(fmls);
     fml = m.mk_eq(fml1, fml2);
 
     bounds.reset();
@@ -204,7 +204,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
         }
     }
     if (!bounds.empty()) {
-        fml = m.mk_implies(m.mk_and(bounds.size(), bounds.data()), fml);
+        fml = m.mk_implies(m.mk_and(bounds), fml);
     }
     return fml;
 

src/test/pdd_solver.cpp

@@ -114,10 +114,10 @@ namespace dd {
                 for (unsigned i = 0; i < args.size(); ++i) {
                     args[i] = mk_not(m, args.get(i));
                 }
-                g = m.mk_not(m.mk_and(args.size(), args.data()));
+                g = m.mk_not(m.mk_and(args));
             }
             else if (m.is_and(a)) {
-                g = m.mk_and(args.size(), args.data());
+                g = m.mk_and(args);
                 trail.push_back(g);
             }
             else if (m.is_eq(a)) {

src/test/quant_solve.cpp

@@ -60,7 +60,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards)
     //    fml <=> guard_1 \/ guard_2 \/ ... 
     ast_manager& m = guards.get_manager();
     expr_ref tmp(m), fml2(m);
-    tmp = m.mk_or(guards.size(), guards.c_ptr());
+    tmp = m.mk_or(guards);
     expr* _x = x;
     std::cout << mk_pp(fml, m) << "\n";
     expr_abstract(m, 0, 1, &_x, fml, fml2);

src/test/udoc_relation.cpp

@@ -900,7 +900,7 @@ public:
             repl(tmp);
             disj.push_back(tmp);
         }
-        fml = mk_or(m, disj.size(), disj.data());
+        fml = mk_or(disj);
     }
 
     void apply_filter(udoc_relation& t, app* cond) {