Use const refs to reduce copying.

These are things that have been found by `clang-tidy`.

src/ast/proofs/proof_utils.h

@@ -88,7 +88,7 @@ class elim_aux_assertions {
 
     app_ref m_aux;
 public:
-    elim_aux_assertions(app_ref aux) : m_aux(aux) {}
+    elim_aux_assertions(app_ref aux) : m_aux(std::move(aux)) {}
 
     void mk_or_core(expr_ref_vector &args, expr_ref &res)
     {

src/cmd_context/cmd_context.h

@@ -125,7 +125,7 @@ class stream_ref {
     std::ostream * m_stream;
     bool           m_owner;
 public:
-    stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
+    stream_ref(const std::string& n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
     ~stream_ref() { reset(); }
     void set(char const * name);
     void set(std::ostream& strm);

src/duality/duality.h

@@ -66,7 +66,7 @@ namespace Duality {
 
         bool is_variable(const Term &t);
 
-        FuncDecl SuffixFuncDecl(Term t, int n);
+        FuncDecl SuffixFuncDecl(const Term &t, int n);
 
 
         Term SubstRecHide(hash_map<ast, Term> &memo, const Term &t, int number);

src/duality/duality_rpfp.cpp

@@ -2157,7 +2157,7 @@ namespace Duality {
         std::vector<Term> la_pos_vars;
         bool fixing;
     
-        void IndexLAcoeff(const Term &coeff1, const Term &coeff2, Term t, int id) {
+        void IndexLAcoeff(const Term &coeff1, const Term &coeff2, const Term &t, int id) {
             Term coeff = coeff1 * coeff2;
             coeff = coeff.simplify();
             Term is_pos = (coeff >= ctx.int_val(0));
@@ -3303,7 +3303,7 @@ namespace Duality {
     // This returns a new FuncDel with same sort as top-level function
     // of term t, but with numeric suffix appended to name.
 
-    Z3User::FuncDecl Z3User::SuffixFuncDecl(Term t, int n)
+    Z3User::FuncDecl Z3User::SuffixFuncDecl(const Term &t, int n)
     {
         std::string name = t.decl().name().str() + "_" + string_of_int(n);
         std::vector<sort> sorts;

src/duality/duality_solver.cpp

@@ -107,7 +107,7 @@ namespace Duality {
 
     struct InternalError {
         std::string msg;
-        InternalError(const std::string _msg)
+        InternalError(const std::string & _msg)
             : msg(_msg) {}
     };
 

src/duality/duality_wrapper.h

@@ -191,7 +191,7 @@ namespace Duality {
         sort int_sort();
         sort real_sort();
         sort bv_sort(unsigned sz);
-        sort array_sort(sort d, sort r);
+        sort array_sort(const sort & d, const sort & r);
 
         func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
@@ -763,11 +763,11 @@ namespace Duality {
         unsigned size() const;
         func_decl operator[](unsigned i) const;
 
-        expr get_const_interp(func_decl f) const {
+        expr get_const_interp(const func_decl & f) const {
             return ctx().cook(m_model->get_const_interp(to_func_decl(f.raw())));
         }
 
-        func_interp get_func_interp(func_decl f) const {
+        func_interp get_func_interp(const func_decl & f) const {
             return func_interp(ctx(),m_model->get_func_interp(to_func_decl(f.raw())));
         }
 
@@ -1169,7 +1169,7 @@ namespace Duality {
         ::sort *s = m().mk_sort(m_arith_fid, REAL_SORT);
         return sort(*this, s);
     }
-    inline sort context::array_sort(sort d, sort r) {
+    inline sort context::array_sort(const sort & d, const sort & r) {
         parameter params[2]  = { parameter(d), parameter(to_sort(r)) };
         ::sort * s =  m().mk_sort(m_array_fid, ARRAY_SORT, 2, params);
         return sort(*this, s);
@@ -1274,11 +1274,11 @@ namespace Duality {
     class TermTree {
     public:
 
-        TermTree(expr _term){
+        TermTree(const expr &_term){
             term = _term;
         }
 
-        TermTree(expr _term, const std::vector<TermTree *> &_children){
+        TermTree(const expr &_term, const std::vector<TermTree *> &_children){
             term = _term;
             children = _children;
         }
@@ -1302,9 +1302,9 @@ namespace Duality {
             return num;
         }
 
-        inline void setTerm(expr t){term = t;}
+        inline void setTerm(const expr &t){term = t;}
 
-        inline void addTerm(expr t){terms.push_back(t);}
+        inline void addTerm(const expr &t){terms.push_back(t);}
 
         inline void setChildren(const std::vector<TermTree *> & _children){
             children = _children;

src/muz/base/dl_context.cpp

@@ -400,7 +400,7 @@ namespace datalog {
         }
         uint64 res;
         if (!try_get_sort_constant_count(srt, res)) {
-            sort_size sz = srt->get_num_elements();
+            const sort_size & sz = srt->get_num_elements();
             if (sz.is_finite()) {
                 res = sz.size();
             }
@@ -411,7 +411,7 @@ namespace datalog {
         return res;
     }
 
-    void context::set_argument_names(const func_decl * pred, svector<symbol> var_names)
+    void context::set_argument_names(const func_decl * pred, const svector<symbol> & var_names)
     {
         SASSERT(!m_argument_var_names.contains(pred));
         m_argument_var_names.insert(pred, var_names);

src/muz/base/dl_context.h

@@ -368,7 +368,7 @@ namespace datalog {
            These names are used when printing out the relations to make the output conform 
            to the one of bddbddb.
         */
-        void set_argument_names(const func_decl * pred, svector<symbol> var_names);
+        void set_argument_names(const func_decl * pred, const svector<symbol> & var_names);
         symbol get_argument_name(const func_decl * pred, unsigned arg_index);
 
         void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 

src/muz/base/dl_util.cpp

@@ -547,7 +547,7 @@ namespace datalog {
     //
     // -----------------------------------
 
-    void get_file_names(std::string directory, std::string extension, bool traverse_subdirs, 
+    void get_file_names(std::string directory, const std::string & extension, bool traverse_subdirs,
             string_vector & res) {
 
         if(directory[directory.size()-1]!='\\' && directory[directory.size()-1]!='/') {
@@ -595,7 +595,7 @@ namespace datalog {
 #endif
     }
 
-    bool file_exists(std::string name) {
+    bool file_exists(const std::string & name) {
         struct stat st;
         if(stat(name.c_str(),&st) == 0) {
             return true;
@@ -603,7 +603,7 @@ namespace datalog {
         return false;
     }
 
-    bool is_directory(std::string name) {
+    bool is_directory(const std::string & name) {
         if(!file_exists(name)) {
             return false;
         }
@@ -612,7 +612,7 @@ namespace datalog {
         return (status.st_mode&S_IFDIR)!=0;
     }
 
-    std::string get_file_name_without_extension(std::string name) {
+    std::string get_file_name_without_extension(const std::string & name) {
         size_t slash_index = name.find_last_of("\\/");
         size_t dot_index = name.rfind(".");
         size_t ofs = (slash_index==std::string::npos) ? 0 : slash_index+1;

src/muz/base/dl_util.h

@@ -290,7 +290,7 @@ namespace datalog {
     }
 
     template<class T>
-    void project_out_vector_columns(T & container, const unsigned_vector removed_cols) {
+    void project_out_vector_columns(T & container, const unsigned_vector & removed_cols) {
         project_out_vector_columns(container, removed_cols.size(), removed_cols.c_ptr());
     }
 
@@ -342,7 +342,7 @@ namespace datalog {
     }
 
     template<class T>
-    void permutate_by_cycle(T & container, const unsigned_vector permutation_cycle) {
+    void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
         permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.c_ptr());
     }
 
@@ -578,13 +578,13 @@ namespace datalog {
     //
     // -----------------------------------
 
-    void get_file_names(std::string directory, std::string extension, bool traverse_subdirs, 
+    void get_file_names(std::string directory, const std::string & extension, bool traverse_subdirs, 
         string_vector & res);
 
-    bool file_exists(std::string name);
+    bool file_exists(const std::string & name);
-    bool is_directory(std::string name);
+    bool is_directory(const std::string & name);
 
-    std::string get_file_name_without_extension(std::string name);
+    std::string get_file_name_without_extension(const std::string & name);
 
     // -----------------------------------
     //

src/muz/fp/datalog_parser.cpp

@@ -1303,7 +1303,7 @@ private:
         }
     }
 
-    void parse_rules_file(std::string fname) {
+    void parse_rules_file(const std::string & fname) {
         SASSERT(file_exists(fname));
         flet<std::string> flet_cur_file(m_current_file, fname);
 
@@ -1347,7 +1347,7 @@ private:
         return true;
     }
 
-    void parse_rel_file(std::string fname) {
+    void parse_rel_file(const std::string & fname) {
         SASSERT(file_exists(fname));
 
         IF_VERBOSE(10, verbose_stream() << "Parsing relation file " << fname << "\n";);
@@ -1496,7 +1496,7 @@ private:
         return true;
     }
 
-    void parse_map_file(std::string fname) {
+    void parse_map_file(const std::string & fname) {
         SASSERT(file_exists(fname));
 
         IF_VERBOSE(10, verbose_stream() << "Parsing map file " << fname << "\n";);

src/muz/rel/dl_finite_product_relation.cpp

@@ -1924,7 +1924,7 @@ namespace datalog {
         }
     }
 
-    void finite_product_relation::extract_table_fact(const relation_fact rf, table_fact & tf) const {
+    void finite_product_relation::extract_table_fact(const relation_fact & rf, table_fact & tf) const {
         const relation_signature & sig = get_signature();
         relation_manager & rmgr = get_manager();
 
@@ -1940,7 +1940,7 @@ namespace datalog {
         tf.push_back(0);
     }
 
-    void finite_product_relation::extract_other_fact(const relation_fact rf, relation_fact & of) const {
+    void finite_product_relation::extract_other_fact(const relation_fact & rf, relation_fact & of) const {
         of.reset();
         unsigned o_sz = m_other_sig.size();
         for(unsigned i=0; i<o_sz; i++) {

src/muz/rel/dl_finite_product_relation.h

@@ -281,11 +281,11 @@ namespace datalog {
            \brief Extract the values of table non-functional columns from the relation fact.
            The value of the functional column which determines index of the inner relation is undefined.
          */
-        void extract_table_fact(const relation_fact rf, table_fact & tf) const;
+        void extract_table_fact(const relation_fact & rf, table_fact & tf) const;
         /**
            \brief Extract the values of the inner relation columns from the relation fact.
          */
-        void extract_other_fact(const relation_fact rf, relation_fact & of) const;
+        void extract_other_fact(const relation_fact & rf, relation_fact & of) const;
 
         relation_base * mk_empty_inner();
         relation_base * mk_full_inner(func_decl* pred);

src/muz/rel/dl_instruction.cpp

@@ -168,7 +168,7 @@ namespace datalog {
     }
 
 
-    void instruction::display_indented(execution_context const & _ctx, std::ostream & out, std::string indentation) const {
+    void instruction::display_indented(execution_context const & _ctx, std::ostream & out, const std::string & indentation) const {
         out << indentation;
         rel_context const& ctx = _ctx.get_rel_context();
         display_head_impl(_ctx, out);
@@ -191,7 +191,7 @@ namespace datalog {
         reg_idx m_reg;
     public:
         instr_io(bool store, func_decl_ref pred, reg_idx reg)
-            : m_store(store), m_pred(pred), m_reg(reg) {}
+            : m_store(store), m_pred(std::move(pred)), m_reg(reg) {}
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
             if (m_store) {
@@ -348,7 +348,7 @@ namespace datalog {
             out << "while";
             print_container(m_controls, out);
         }
-        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const {
+        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const {
             m_body->display_indented(ctx, out, indentation+"    ");
         }
     };
@@ -1182,7 +1182,7 @@ namespace datalog {
         }
     }
 
-    void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, std::string indentation) const {
+    void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, const std::string & indentation) const {
         rel_context const& ctx = _ctx.get_rel_context();
         instr_seq_type::const_iterator it = m_data.begin();
         instr_seq_type::const_iterator end = m_data.end();

src/muz/rel/dl_instruction.h

@@ -150,7 +150,7 @@ namespace datalog {
             return m_reg_annotation.find(reg, res);
         }
 
-        void set_register_annotation(reg_idx reg, std::string str) {
+        void set_register_annotation(reg_idx reg, const std::string & str) {
             m_reg_annotation.insert(reg, str);
         }
 
@@ -233,7 +233,7 @@ namespace datalog {
 
            Each line must be prepended by \c indentation and ended by a newline character.
         */
-        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const {}
+        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const {}
         void log_verbose(execution_context& ctx);
 
     public:
@@ -249,7 +249,7 @@ namespace datalog {
         void display(execution_context const& ctx, std::ostream & out) const {
             display_indented(ctx, out, "");
         }
-        void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const;
+        void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const;
 
         static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt);
         /**
@@ -359,7 +359,7 @@ namespace datalog {
         void display(execution_context const & ctx, std::ostream & out) const {
             display_indented(ctx, out, "");
         }
-        void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const;
+        void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const;
 
         unsigned num_instructions() const { return m_data.size(); }
     };

src/muz/rel/dl_mk_explanations.cpp

@@ -454,7 +454,7 @@ namespace datalog {
             : m_manager(ctx.get_manager()), 
               m_subst(ctx.get_var_subst()), 
               m_col_idx(col_idx), 
-              m_new_rule(new_rule) {}
+              m_new_rule(std::move(new_rule)) {}
 
         virtual void operator()(relation_base & r0) {
             explanation_relation & r = static_cast<explanation_relation &>(r0);

src/muz/rel/dl_product_relation.cpp

@@ -488,7 +488,7 @@ namespace datalog {
         ptr_vector<relation_transformer_fn> m_transforms;
     public:
         transform_fn(relation_signature s, unsigned num_trans, relation_transformer_fn** trans):
-          m_sig(s),
+          m_sig(std::move(s)),
           m_transforms(num_trans, trans) {}
 
           ~transform_fn() { dealloc_ptr_vector_content(m_transforms); }

src/muz/rel/dl_relation_manager.h

@@ -289,7 +289,7 @@ namespace datalog {
         relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t, 
             const unsigned * permutation);
         relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t, 
-                const unsigned_vector permutation) {
+                const unsigned_vector & permutation) {
             SASSERT(t.get_signature().size()==permutation.size());
             return mk_permutation_rename_fn(t, permutation.c_ptr());
         }
@@ -343,7 +343,7 @@ namespace datalog {
 
         relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 
             const unsigned * identical_cols);
-        relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, const unsigned_vector identical_cols) {
+        relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, const unsigned_vector & identical_cols) {
             return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
         }
 
@@ -468,7 +468,7 @@ namespace datalog {
            of column number.
         */
         table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned * permutation);
-        table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned_vector permutation) {
+        table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned_vector & permutation) {
             SASSERT(t.get_signature().size()==permutation.size());
             return mk_permutation_rename_fn(t, permutation.c_ptr());
         }
@@ -522,7 +522,7 @@ namespace datalog {
 
         table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt, 
             const unsigned * identical_cols);
-        table_mutator_fn * mk_filter_identical_fn(const table_base & t, const unsigned_vector identical_cols) {
+        table_mutator_fn * mk_filter_identical_fn(const table_base & t, const unsigned_vector & identical_cols) {
             return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
         }
 

src/muz/rel/dl_sieve_relation.h

@@ -108,7 +108,7 @@ namespace datalog {
 
         sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns, 
             relation_base * inner_rel);
-        sieve_relation * mk_from_inner(const relation_signature & s, const svector<bool> inner_columns, 
+        sieve_relation * mk_from_inner(const relation_signature & s, const svector<bool> & inner_columns, 
                 relation_base * inner_rel) {
             SASSERT(inner_columns.size()==s.size());
             return mk_from_inner(s, inner_columns.c_ptr(), inner_rel);

src/muz/rel/dl_table_relation.cpp

@@ -240,7 +240,7 @@ namespace datalog {
 
             const table_relation & tr_src = static_cast<const table_relation &>(src);
             relation_manager & rmgr = tr_src.get_manager();
-            relation_signature sig = tr_src.get_signature();
+            const relation_signature & sig = tr_src.get_signature();
             SASSERT(tgt.get_signature()==sig);
             SASSERT(!delta || delta->get_signature()==sig);
             

src/muz/spacer/spacer_context.cpp

@@ -3418,7 +3418,7 @@ expr_ref context::get_constraints (unsigned level)
     return m_pm.mk_and (constraints);
 }
 
-void context::add_constraints (unsigned level, expr_ref c)
+void context::add_constraints (unsigned level, const expr_ref& c)
 {
     if (!c.get()) { return; }
     if (m.is_true(c)) { return; }

src/muz/spacer/spacer_context.h

@@ -833,7 +833,7 @@ public:
     pob& get_root() const { return m_pob_queue.get_root(); }
 
     expr_ref get_constraints (unsigned lvl);
-    void add_constraints (unsigned lvl, expr_ref c);
+    void add_constraints (unsigned lvl, const expr_ref& c);
 };
 
 inline bool pred_transformer::use_native_mbp () {return ctx.use_native_mbp ();}

src/muz/spacer/spacer_matrix.cpp

@@ -42,7 +42,7 @@ namespace spacer
         return m_num_cols;
     }
 
-    rational spacer_matrix::get(unsigned int i, unsigned int j)
+    const rational& spacer_matrix::get(unsigned int i, unsigned int j)
     {
         SASSERT(i < m_num_rows);
         SASSERT(j < m_num_cols);
@@ -50,7 +50,7 @@ namespace spacer
         return m_matrix[i][j];
     }
 
-    void spacer_matrix::set(unsigned int i, unsigned int j, rational v)
+    void spacer_matrix::set(unsigned int i, unsigned int j, const rational& v)
     {
         SASSERT(i < m_num_rows);
         SASSERT(j < m_num_cols);

src/muz/spacer/spacer_matrix.h

@@ -30,8 +30,8 @@ namespace spacer {
         unsigned num_rows();
         unsigned num_cols();
 
-        rational get(unsigned i, unsigned j);
+        const rational& get(unsigned i, unsigned j);
-        void set(unsigned i, unsigned j, rational v);
+        void set(unsigned i, unsigned j, const rational& v);
 
         unsigned perform_gaussian_elimination();
 

src/muz/spacer/spacer_unsat_core_learner.cpp

@@ -301,7 +301,7 @@ public:
     void operator()(quantifier*) {}
 };
 
-void unsat_core_learner::collect_symbols_b(expr_set axioms_b)
+void unsat_core_learner::collect_symbols_b(const expr_set& axioms_b)
 {
     expr_mark visited;
     collect_pure_proc proc(m_symbols_b);

src/muz/spacer/spacer_unsat_core_learner.h

@@ -82,7 +82,7 @@ namespace spacer {
     private:
         ptr_vector<unsat_core_plugin> m_plugins;
         func_decl_set m_symbols_b; // symbols, which occur in any b-asserted formula
-        void collect_symbols_b(expr_set axioms_b);
+        void collect_symbols_b(const expr_set& axioms_b);
 
         ast_mark m_a_mark;
         ast_mark m_b_mark;

src/smt/smt_context.cpp

@@ -1791,7 +1791,7 @@ namespace smt {
         }
     }
 
-    void context::set_conflict(b_justification js, literal not_l) {
+    void context::set_conflict(const b_justification & js, literal not_l) {
         if (!inconsistent()) {
             TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
             m_conflict = js;

src/smt/smt_context.h

@@ -897,7 +897,7 @@ namespace smt {
         void trace_assign(literal l, b_justification j, bool decision) const;
 
     public:
-        void assign(literal l, b_justification j, bool decision = false) {
+        void assign(literal l, const b_justification & j, bool decision = false) {
             SASSERT(l != false_literal);
             SASSERT(l != null_literal);
             switch (get_assignment(l)) {
@@ -998,9 +998,9 @@ namespace smt {
 
         void assign_quantifier(quantifier * q);
 
-        void set_conflict(b_justification js, literal not_l);
+        void set_conflict(const b_justification & js, literal not_l);
 
-        void set_conflict(b_justification js) {
+        void set_conflict(const b_justification & js) {
             set_conflict(js, null_literal);
         }