From 757b7c66efa6b8e081489b3c6105d324ff009beb Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 6 Feb 2018 14:29:54 +0700 Subject: [PATCH] Remove unnecessary value parameter copies. --- src/ast/rewriter/bv_bounds.cpp | 12 +++++----- src/ast/rewriter/bv_bounds.h | 16 +++++++------- src/duality/duality.h | 2 +- src/duality/duality_rpfp.cpp | 2 +- src/interp/iz3mgr.h | 28 ++++++++++++------------ src/util/lp/core_solver_pretty_printer.h | 2 +- src/util/lp/mps_reader.h | 18 +++++++-------- 7 files changed, 40 insertions(+), 40 deletions(-) diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp index fd263efb2..0a32f8bc2 100644 --- a/src/ast/rewriter/bv_bounds.cpp +++ b/src/ast/rewriter/bv_bounds.cpp @@ -449,7 +449,7 @@ bool bv_bounds::add_constraint(expr* e) { return m_okay; } -bool bv_bounds::add_bound_unsigned(app * v, numeral a, numeral b, bool negate) { +bool bv_bounds::add_bound_unsigned(app * v, const numeral& a, const numeral& b, bool negate) { TRACE("bv_bounds", tout << "bound_unsigned " << mk_ismt2_pp(v, m_m) << ": " << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;); const unsigned bv_sz = m_bv_util.get_bv_size(v); const numeral& zero = numeral::zero(); @@ -472,7 +472,7 @@ bool bv_bounds::add_bound_unsigned(app * v, numeral a, numeral b, bool negate) { } } -bv_bounds::conv_res bv_bounds::convert_signed(app * v, numeral a, numeral b, bool negate, vector& nis) { +bv_bounds::conv_res bv_bounds::convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector& nis) { TRACE("bv_bounds", tout << "convert_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;); const unsigned bv_sz = m_bv_util.get_bv_size(v); SASSERT(a <= b); @@ -496,7 +496,7 @@ bv_bounds::conv_res bv_bounds::convert_signed(app * v, numeral a, numeral b, boo } } -bool bv_bounds::add_bound_signed(app * v, numeral a, numeral b, bool negate) { +bool bv_bounds::add_bound_signed(app * v, const numeral& a, const numeral& b, bool negate) { TRACE("bv_bounds", tout << "bound_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~" : " ") << a << ";" << b << std::endl;); const unsigned bv_sz = m_bv_util.get_bv_size(v); SASSERT(a <= b); @@ -519,7 +519,7 @@ bool bv_bounds::add_bound_signed(app * v, numeral a, numeral b, bool negate) { } } -bool bv_bounds::bound_lo(app * v, numeral l) { +bool bv_bounds::bound_lo(app * v, const numeral& l) { SASSERT(in_range(v, l)); TRACE("bv_bounds", tout << "lower " << mk_ismt2_pp(v, m_m) << ":" << l << std::endl;); // l <= v @@ -530,7 +530,7 @@ bool bv_bounds::bound_lo(app * v, numeral l) { return m_okay; } -bool bv_bounds::bound_up(app * v, numeral u) { +bool bv_bounds::bound_up(app * v, const numeral& u) { SASSERT(in_range(v, u)); TRACE("bv_bounds", tout << "upper " << mk_ismt2_pp(v, m_m) << ":" << u << std::endl;); // v <= u @@ -541,7 +541,7 @@ bool bv_bounds::bound_up(app * v, numeral u) { return m_okay; } -bool bv_bounds::add_neg_bound(app * v, numeral a, numeral b) { +bool bv_bounds::add_neg_bound(app * v, const numeral& a, const numeral& b) { TRACE("bv_bounds", tout << "negative bound " << mk_ismt2_pp(v, m_m) << ":" << a << ";" << b << std::endl;); bv_bounds::interval negative_interval(a, b); SASSERT(m_bv_util.is_bv(v)); diff --git a/src/ast/rewriter/bv_bounds.h b/src/ast/rewriter/bv_bounds.h index 4a7226fa7..775941d1d 100644 --- a/src/ast/rewriter/bv_bounds.h +++ b/src/ast/rewriter/bv_bounds.h @@ -49,11 +49,11 @@ public: // bounds addition methods **/ bool add_constraint(expr* e); - bool bound_up(app * v, numeral u); // v <= u - bool bound_lo(app * v, numeral l); // l <= v - inline bool add_neg_bound(app * v, numeral a, numeral b); // not (a<=v<=b) - bool add_bound_signed(app * v, numeral a, numeral b, bool negate); - bool add_bound_unsigned(app * v, numeral a, numeral b, bool negate); + bool bound_up(app * v, const numeral& u); // v <= u + bool bound_lo(app * v, const numeral& l); // l <= v + inline bool add_neg_bound(app * v, const numeral& a, const numeral& b); // not (a<=v<=b) + bool add_bound_signed(app * v, const numeral& a, const numeral& b, bool negate); + bool add_bound_unsigned(app * v, const numeral& a, const numeral& b, bool negate); public: bool is_sat(); ///< Determine if the set of considered constraints is satisfiable. bool is_okay(); @@ -70,7 +70,7 @@ protected: enum conv_res { CONVERTED, UNSAT, UNDEF }; conv_res convert(expr * e, vector& nis, bool negated); conv_res record(app * v, numeral lo, numeral hi, bool negated, vector& nis); - conv_res convert_signed(app * v, numeral a, numeral b, bool negate, vector& nis); + conv_res convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector& nis); typedef vector intervals; typedef obj_map intervals_map; @@ -83,7 +83,7 @@ protected: bool m_okay; bool is_sat(app * v); bool is_sat_core(app * v); - inline bool in_range(app *v, numeral l); + inline bool in_range(app *v, const numeral& l); inline bool is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val); void record_singleton(app * v, numeral& singleton_value); inline bool to_bound(const expr * e) const; @@ -99,7 +99,7 @@ inline bool bv_bounds::to_bound(const expr * e) const { && !m_bv_util.is_numeral(e); } -inline bool bv_bounds::in_range(app *v, bv_bounds::numeral n) { +inline bool bv_bounds::in_range(app *v, const bv_bounds::numeral& n) { const unsigned bv_sz = m_bv_util.get_bv_size(v); const bv_bounds::numeral zero(0); const bv_bounds::numeral mod(rational::power_of_two(bv_sz)); diff --git a/src/duality/duality.h b/src/duality/duality.h index e8f36a0cd..71687c648 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -725,7 +725,7 @@ namespace Duality { /** Determines the value in the counterexample of a symbol occuring in the transformer formula of * a given edge. */ - Term Eval(Edge *e, Term t); + Term Eval(Edge *e, const Term& t); /** Return the fact derived at node p in a counterexample. */ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index b6dd42f00..5ddc196c8 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1494,7 +1494,7 @@ namespace Duality { /** Determines the value in the counterexample of a symbol occuring in the transformer formula of * a given edge. */ - RPFP::Term RPFP::Eval(Edge *e, Term t) + RPFP::Term RPFP::Eval(Edge *e, const Term& t) { Term tl = Localize(e, t); return dualModel.eval(tl); diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 0ad751326..8de1a44e8 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -245,7 +245,7 @@ class iz3mgr { /** Methods for destructing ast. */ - int num_args(ast t){ + int num_args(const ast& t){ ast_kind dk = t.raw()->get_kind(); switch(dk){ case AST_APP: @@ -285,7 +285,7 @@ class iz3mgr { return res; } - symb sym(ast t){ + symb sym(const ast& t){ raw_ast *_ast = t.raw(); return is_app(_ast) ? to_app(_ast)->get_decl() : 0; } @@ -302,7 +302,7 @@ class iz3mgr { } } - type get_type(ast t){ + type get_type(const ast& t){ return m().get_sort(to_expr(t.raw())); } @@ -442,23 +442,23 @@ class iz3mgr { bool is_farkas_coefficient_negative(const ast &proof, int n); - bool is_true(ast t){ + bool is_true(const ast& t){ return op(t) == True; } - bool is_false(ast t){ + bool is_false(const ast& t){ return op(t) == False; } - bool is_iff(ast t){ + bool is_iff(const ast& t){ return op(t) == Iff; } - bool is_or(ast t){ + bool is_or(const ast& t){ return op(t) == Or; } - bool is_not(ast t){ + bool is_not(const ast& t){ return op(t) == Not; } @@ -472,7 +472,7 @@ class iz3mgr { // Some constructors that simplify things - ast mk_not(ast x){ + ast mk_not(const ast& x){ opr o = op(x); if(o == True) return make(False); if(o == False) return make(True); @@ -480,7 +480,7 @@ class iz3mgr { return make(Not,x); } - ast mk_and(ast x, ast y){ + ast mk_and(const ast& x, const ast& y){ opr ox = op(x); opr oy = op(y); if(ox == True) return y; @@ -491,7 +491,7 @@ class iz3mgr { return make(And,x,y); } - ast mk_or(ast x, ast y){ + ast mk_or(const ast& x, const ast& y){ opr ox = op(x); opr oy = op(y); if(ox == False) return y; @@ -502,7 +502,7 @@ class iz3mgr { return make(Or,x,y); } - ast mk_implies(ast x, ast y){ + ast mk_implies(const ast& x, const ast& y){ opr ox = op(x); opr oy = op(y); if(ox == True) return y; @@ -537,7 +537,7 @@ class iz3mgr { return make(And,conjs); } - ast mk_equal(ast x, ast y){ + ast mk_equal(const ast& x, const ast& y){ if(x == y) return make(True); opr ox = op(x); opr oy = op(y); @@ -550,7 +550,7 @@ class iz3mgr { return make(Equal,x,y); } - ast z3_ite(ast x, ast y, ast z){ + ast z3_ite(const ast& x, const ast& y, const ast& z){ opr ox = op(x); opr oy = op(y); opr oz = op(z); diff --git a/src/util/lp/core_solver_pretty_printer.h b/src/util/lp/core_solver_pretty_printer.h index 20b2c1cbe..87c528792 100644 --- a/src/util/lp/core_solver_pretty_printer.h +++ b/src/util/lp/core_solver_pretty_printer.h @@ -86,7 +86,7 @@ public: unsigned get_column_width(unsigned column); - unsigned regular_cell_width(unsigned row, unsigned column, std::string name) { + unsigned regular_cell_width(unsigned row, unsigned column, const std::string & name) { return regular_cell_string(row, column, name).size(); } diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h index 1b020407d..916e56322 100644 --- a/src/util/lp/mps_reader.h +++ b/src/util/lp/mps_reader.h @@ -95,7 +95,7 @@ inline vector string_split(const std::string &source, const char *d return results; } -inline vector split_and_trim(std::string line) { +inline vector split_and_trim(const std::string &line) { auto split = string_split(line, " \t", false); vector ret; for (auto s : split) { @@ -127,9 +127,9 @@ class mps_reader { std::string m_name; bound * m_bound; unsigned m_index; - column(std::string name, unsigned index): m_name(name), - m_bound(nullptr), - m_index(index) { + column(const std::string &name, unsigned index): m_name(name), + m_bound(nullptr), + m_index(index) { } }; @@ -140,7 +140,7 @@ class mps_reader { unsigned m_index; T m_right_side; T m_range; - row(row_type type, std::string name, unsigned index) : + row(row_type type, const std::string &name, unsigned index) : m_type(type), m_name(name), m_index(index), @@ -254,7 +254,7 @@ class mps_reader { } while (m_is_OK); } - void read_column_by_columns(std::string column_name, std::string column_data) { + void read_column_by_columns(const std::string & column_name, std::string column_data) { // uph, let us try to work with columns if (column_data.size() >= 22) { std::string ss = column_data.substr(0, 8); @@ -283,7 +283,7 @@ class mps_reader { } } - void read_column(std::string column_name, std::string column_data){ + void read_column(const std::string & column_name, const std::string & column_data){ auto tokens = split_and_trim(column_data); for (unsigned i = 0; i < tokens.size() - 1; i+= 2) { auto row_name = tokens[i]; @@ -421,7 +421,7 @@ class mps_reader { } - void read_bound_by_columns(std::string colstr) { + void read_bound_by_columns(const std::string & colstr) { if (colstr.size() < 14) { (*m_message_stream) << "line is too short" << std::endl; (*m_message_stream) << m_line << std::endl; @@ -763,7 +763,7 @@ public: } } - mps_reader(std::string file_name): + mps_reader(const std::string & file_name): m_is_OK(true), m_file_name(file_name), m_file_stream(file_name),