mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge pull request #1466 from waywardmonkeys/reduce-copying

Browse source 
Use const refs to reduce copying.
This commit is contained in:
Nikolaj Bjorner 2018-02-05 16:37:44 -08:00 committed by GitHub
parent e332652989 177414c0ee
commit 2853558bc2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
28 changed files with 62 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/proofs/proof_utils.h
View file

@ -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)
{

2
src/cmd_context/cmd_context.h
View file

@ -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);

2
src/duality/duality.h
View file

@ -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);

4
src/duality/duality_rpfp.cpp
View file

@ -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;

2
src/duality/duality_solver.cpp
View file

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

16
src/duality/duality_wrapper.h
View file

@ -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;

4
src/muz/base/dl_context.cpp
View file

@ -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);

2
src/muz/base/dl_context.h
View file

@ -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,

8
src/muz/base/dl_util.cpp
View file

@ -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;

12
src/muz/base/dl_util.h
View file

@ -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 is_directory(std::string name);
bool file_exists(const 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);
// -----------------------------------
//

6
src/muz/fp/datalog_parser.cpp
View file

@ -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";);

4
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -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++) {

4
src/muz/rel/dl_finite_product_relation.h
View file

@ -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);

8
src/muz/rel/dl_instruction.cpp
View file

@ -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();

8
src/muz/rel/dl_instruction.h
View file

@ -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(); }
};

2
src/muz/rel/dl_mk_explanations.cpp
View file

@ -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);

2
src/muz/rel/dl_product_relation.cpp
View file

@ -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); }

8
src/muz/rel/dl_relation_manager.h
View file

@ -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());
}

2
src/muz/rel/dl_sieve_relation.h
View file

@ -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);

2
src/muz/rel/dl_table_relation.cpp
View file

@ -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);

2
src/muz/spacer/spacer_context.cpp
View file

@ -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; }

2
src/muz/spacer/spacer_context.h
View file

@ -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 ();}

4
src/muz/spacer/spacer_matrix.cpp
View file

@ -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);

4
src/muz/spacer/spacer_matrix.h
View file

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

2
src/muz/spacer/spacer_unsat_core_learner.cpp
View file

@ -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);

2
src/muz/spacer/spacer_unsat_core_learner.h
View file

@ -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;

2
src/smt/smt_context.cpp
View file

@ -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;

6
src/smt/smt_context.h
View file

@ -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);
}