remove spurious copies and inc_refs around ref_vector

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -35,7 +35,7 @@ public:
         fail_if_proof_generation("ackermannize", g);
         TRACE("ackermannize", g->display(tout << "in\n"););
 
-        expr_ref_vector flas(m);
+        ptr_vector<expr> flas;
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
         lackr lackr(m, m_p, m_st, flas, nullptr);

src/ackermannization/ackr_model_converter.cpp

@@ -134,7 +134,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
         info->abstract(arg, aarg);
         expr_ref arg_value(m);
         evaluator(aarg, arg_value);
-        args.push_back(arg_value);
+        args.push_back(std::move(arg_value));
     }
     if (fi->get_entry(args.c_ptr()) == nullptr) {
         TRACE("ackr_model",

src/ackermannization/lackr.cpp

@@ -23,8 +23,8 @@
 #include "ast/for_each_expr.h"
 #include "model/model_smt2_pp.h"
 
-lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas,
+lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
-    solver * uffree_solver)
+             const ptr_vector<expr>& formulas, solver * uffree_solver)
     : m_m(m)
     , m_p(p)
     , m_formulas(formulas)
@@ -173,11 +173,10 @@ void lackr::abstract() {
     }
     m_info->seal();
     // perform abstraction of the formulas
-    const unsigned sz = m_formulas.size();
+    for (expr * f : m_formulas) {
-    for (unsigned i = 0; i < sz; ++i) {
         expr_ref a(m_m);
-        m_info->abstract(m_formulas.get(i), a);
+        m_info->abstract(f, a);
-        m_abstr.push_back(a);
+        m_abstr.push_back(std::move(a));
     }
 }
 
@@ -249,13 +248,9 @@ lbool lackr::lazy() {
 // Collect all uninterpreted terms, skipping 0-arity.
 //
 bool lackr::collect_terms() {
-    ptr_vector<expr> stack;
+    ptr_vector<expr> stack = m_formulas;
     expr *           curr;
     expr_mark        visited;
-    for(unsigned i = 0; i < m_formulas.size(); ++i) {
-        stack.push_back(m_formulas.get(i));
-        TRACE("lackr", tout << "infla: " <<mk_ismt2_pp(m_formulas.get(i), m_m, 2) <<  "\n";);
-    }
 
     while (!stack.empty()) {
         curr = stack.back();

src/ackermannization/lackr.h

@@ -42,8 +42,8 @@ struct lackr_stats {
 **/
 class lackr {
     public:
-        lackr(ast_manager& m, params_ref p, lackr_stats& st,
+        lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
-            expr_ref_vector& formulas, solver * uffree_solver);
+              const ptr_vector<expr>& formulas, solver * uffree_solver);
         ~lackr();
         void updt_params(params_ref const & _p);
 
@@ -82,7 +82,7 @@ class lackr {
         typedef ackr_helper::app_set       app_set;
         ast_manager&                         m_m;
         params_ref                           m_p;
-        expr_ref_vector                      m_formulas;
+        const ptr_vector<expr>&              m_formulas;
         expr_ref_vector                      m_abstr;
         fun2terms_map                        m_fun2terms;
         ackr_info_ref                        m_info;

src/api/api_context.cpp

@@ -218,10 +218,9 @@ namespace api {
             // Corner case bug: n may be in m_last_result, and this is the only reference to n.
             // When, we execute reset() it is deleted
             // To avoid this bug, I bump the reference counter before reseting m_last_result
-            m().inc_ref(n);
+            ast_ref node(n, m());
             m_last_result.reset();
-            m_last_result.push_back(n);
+            m_last_result.push_back(std::move(node));
-            m().dec_ref(n);
         }
         else {
             m_ast_trail.push_back(n);

src/ast/ast_smt2_pp.cpp

@@ -1199,7 +1199,7 @@ void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, pa
     for (unsigned i = 0; i < sz; ++i) {
         format_ref fr(fm(m));        
         pr(es[i], num_vars, var_prefix, fr, var_names);
-        fmts.push_back(fr);
+        fmts.push_back(std::move(fr));
     }
     r = mk_seq<format**, f2f>(m, fmts.c_ptr(), fmts.c_ptr() + fmts.size(), f2f());
 }

src/ast/fpa/fpa2bv_converter.cpp

@@ -3108,12 +3108,12 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
         expr_ref exp_bv(m), exp_all_ones(m);
         exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
         exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits)));
-        m_extra_assertions.push_back(exp_all_ones);
+        m_extra_assertions.push_back(std::move(exp_all_ones));
 
         expr_ref sig_bv(m), sig_is_non_zero(m);
         sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
         sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
-        m_extra_assertions.push_back(sig_is_non_zero);
+        m_extra_assertions.push_back(std::move(sig_is_non_zero));
     }
 
     TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);

src/ast/rewriter/bv_trailing.cpp

@@ -125,7 +125,7 @@ struct bv_trailing::imp {
         for (unsigned i = 0; i < num; ++i) {
             expr * const curr = a->get_arg(i);
             VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1));
-            new_args.push_back(tmp);
+            new_args.push_back(std::move(tmp));
         }
         result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr());
         return to_rm;
@@ -150,7 +150,7 @@ struct bv_trailing::imp {
         numeral c_val;
         unsigned c_sz;
         if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
-            new_args.push_back(tmp);
+            new_args.push_back(std::move(tmp));
         const unsigned sz = m_util.get_bv_size(coefficient);
         const unsigned new_sz = sz - retv;
 
@@ -204,7 +204,7 @@ struct bv_trailing::imp {
         expr_ref_vector new_args(m);
         for (unsigned j = 0; j < i; ++j)
             new_args.push_back(a->get_arg(j));
-        if (new_last) new_args.push_back(new_last);
+        if (new_last) new_args.push_back(std::move(new_last));
         result = new_args.size() == 1 ? new_args.get(0)
                                       : m_util.mk_concat(new_args.size(), new_args.c_ptr());
         return retv;

src/ast/substitution/substitution.cpp

@@ -196,16 +196,16 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
             expr_ref_vector pats(m_manager), no_pats(m_manager);
             for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
                 subst.apply(num_actual_offsets, deltas, expr_offset(q->get_pattern(i), off), s1, t1, er);
-                pats.push_back(er);
+                pats.push_back(std::move(er));
             }
             for (unsigned i = 0; i < q->get_num_no_patterns(); ++i) {
                 subst.apply(num_actual_offsets, deltas, expr_offset(q->get_no_pattern(i), off), s1, t1, er);
-                no_pats.push_back(er);
+                no_pats.push_back(std::move(er));
             }
             subst.apply(num_actual_offsets, deltas, body, s1, t1, er);
             er = m_manager.update_quantifier(q, pats.size(), pats.c_ptr(), no_pats.size(), no_pats.c_ptr(), er);
             m_todo.pop_back();
-            m_new_exprs.push_back(er);
+            m_new_exprs.push_back(std::move(er));
             m_apply_cache.insert(n, er);            
             break;
         }            

src/qe/qe_lite.cpp

@@ -320,8 +320,8 @@ namespace eq {
                        << "sz is " << sz << "\n"
                        << "subst_map[inx]: " << mk_pp(m_subst_map.get(inx), m) << "\n";);
                 SASSERT(m_subst_map.get(inx) == nullptr);
-                m_subst_map[inx] = r;
                 m_subst.update_inv_binding_at(inx, r);
+                m_subst_map[inx] = std::move(r);
             }
         }
 
@@ -470,7 +470,7 @@ namespace eq {
                             m_var2pos[idx] = i;
                             def_count++;
                             largest_vinx = std::max(idx, largest_vinx);
-                            m_new_exprs.push_back(t);
+                            m_new_exprs.push_back(std::move(t));
                         }
                         else if (!m.is_value(m_map[idx])) {
                             // check if the new definition is simpler
@@ -482,7 +482,7 @@ namespace eq {
                                 m_pos2var[i] = idx;
                                 m_var2pos[idx] = i;
                                 m_map[idx] = t;
-                                m_new_exprs.push_back(t);
+                                m_new_exprs.push_back(std::move(t));
                           }
                           // -- prefer ground
                           else if (is_app(t) && to_app(t)->is_ground() &&
@@ -492,7 +492,7 @@ namespace eq {
                               m_pos2var[i] = idx;
                               m_var2pos[idx] = i;
                               m_map[idx] = t;
-                              m_new_exprs.push_back(t);
+                              m_new_exprs.push_back(std::move(t));
                           }
                           // -- prefer constants
                           else if (is_uninterp_const(t)
@@ -501,7 +501,7 @@ namespace eq {
                               m_pos2var[i] = idx;
                               m_var2pos[idx] = i;
                               m_map[idx] = t;
-                              m_new_exprs.push_back(t);
+                              m_new_exprs.push_back(std::move(t));
                           }
                           TRACE ("qe_def",
                                  tout << "Replacing definition of VAR " << idx << " from "

src/smt/smt_context.cpp

@@ -1594,7 +1594,7 @@ namespace smt {
         for (literal lit : m_assigned_literals) {
             expr_ref e(m_manager);
             literal2expr(lit, e);
-            assignments.push_back(e);
+            assignments.push_back(std::move(e));
         }
     }
 
@@ -4180,7 +4180,7 @@ namespace smt {
             SASSERT(get_justification(guess.var()).get_kind() == b_justification::AXIOM);
             expr_ref lit(m_manager);
             literal2expr(guess, lit);
-            result.push_back(lit);
+            result.push_back(std::move(lit));
         }
     }
 

src/smt/smt_context.h

@@ -1115,8 +1115,6 @@ namespace smt {
 
         void internalize_assertions();
 
-        void assert_assumption(expr * a);
-
         bool validate_assumptions(expr_ref_vector const& asms);
 
         void init_assumptions(expr_ref_vector const& asms);
@@ -1129,8 +1127,6 @@ namespace smt {
 
         void reset_assumptions();
 
-        void reset_clause();
-
         void add_theory_assumptions(expr_ref_vector & theory_assumptions);
 
         lbool mk_unsat_core(lbool result);
@@ -1585,8 +1581,6 @@ namespace smt {
 
         //proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); }
 
-        void get_assumptions_core(ptr_vector<expr> & result);
-
         void get_assertions(ptr_vector<expr> & result) { m_asserted_formulas.get_assertions(result); }
 
         void display(std::ostream & out) const;

src/smt/smt_context_pp.cpp

@@ -409,11 +409,11 @@ namespace smt {
         for (unsigned i = 0; i < num_antecedents; i++) {
             literal l = antecedents[i];
             literal2expr(l, n);
-            fmls.push_back(n);
+            fmls.push_back(std::move(n));
         }
         if (consequent != false_literal) {
             literal2expr(~consequent, n);
-            fmls.push_back(n);
+            fmls.push_back(std::move(n));
         }
         if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
         visitor.collect(fmls);

src/smt/smt_justification.cpp

@@ -281,7 +281,7 @@ namespace smt {
         for (unsigned i = 0; i < m_num_literals; i++) {
             expr_ref l(m);
             ctx.literal2expr(m_literals[i], l);
-            lits.push_back(l);
+            lits.push_back(std::move(l));
         }
         if (lits.size() == 1)
             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr());
@@ -407,12 +407,7 @@ namespace smt {
         for (unsigned i = 0; i < m_num_literals; i++) {
             bool sign   = GET_TAG(m_literals[i]) != 0;
             expr * v    = UNTAG(expr*, m_literals[i]);
-            expr_ref l(m);
+            lits.push_back(sign ? m.mk_not(v) : v);
-            if (sign) 
-                l       = m.mk_not(v);
-            else
-                l       = v;
-            lits.push_back(l);
         }
         if (lits.size() == 1)
             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr());

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -62,7 +62,7 @@ public:
 
         TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
         // running implementation
-        expr_ref_vector flas(m);
+        ptr_vector<expr> flas;
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
         scoped_ptr<solver> uffree_solver = setup_sat();

src/util/ref_vector.h

@@ -99,6 +99,13 @@ public:
         return *this;
     }
 
+    template <typename W, typename M>
+    ref_vector_core& push_back(obj_ref<W,M> && n) {
+        m_nodes.push_back(n.get());
+        n.steal();
+        return *this;
+    }
+
     void pop_back() {
         SASSERT(!m_nodes.empty());
         T * n = m_nodes.back();
@@ -253,6 +260,13 @@ public:
             return *this;
         }
 
+        template <typename W, typename M>
+        element_ref & operator=(obj_ref<W,M> && n) {
+            m_manager.dec_ref(m_ref);
+            m_ref = n.steal();
+            return *this;
+        }
+
         T * get() const {
             return m_ref;
         }
@@ -288,9 +302,8 @@ public:
         return *this;
     }
     
-private:
     // prevent abuse:
-    ref_vector & operator=(ref_vector const & other);
+    ref_vector & operator=(ref_vector const & other) = delete;
 };
 
 template<typename T>