mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge pull request #1478 from waywardmonkeys/unnecessary-value-param-fixes

Browse source 
Remove unnecessary value parameter copies.
This commit is contained in:
Nikolaj Bjorner 2018-02-09 02:20:47 -08:00 committed by GitHub
parent d3a98aee94 757b7c66ef
commit 2b847478a2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 40 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/bv_bounds.cpp
View file

@ -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<ninterval>& nis) {
bv_bounds::conv_res bv_bounds::convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector<ninterval>& 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));

16
src/ast/rewriter/bv_bounds.h
View file

@ -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<ninterval>& nis, bool negated);
conv_res record(app * v, numeral lo, numeral hi, bool negated, vector<ninterval>& nis);
conv_res convert_signed(app * v, numeral a, numeral b, bool negate, vector<ninterval>& nis);
conv_res convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector<ninterval>& nis);
typedef vector<interval> intervals;
typedef obj_map<app, intervals*> 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));

2
src/duality/duality.h
View file

@ -725,7 +725,7 @@ namespace Duality {
/** Determines the value in the counterexample of a symbol occurring 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. */

2
src/duality/duality_rpfp.cpp
View file

@ -1494,7 +1494,7 @@ namespace Duality {
/** Determines the value in the counterexample of a symbol occurring 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);

28
src/interp/iz3mgr.h
View file

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

2
src/util/lp/core_solver_pretty_printer.h
View file

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

18
src/util/lp/mps_reader.h
View file

@ -95,7 +95,7 @@ inline vector<std::string> string_split(const std::string &source, const char *d
return results;
}
inline vector<std::string> split_and_trim(std::string line) {
inline vector<std::string> split_and_trim(const std::string &line) {
auto split = string_split(line, " \t", false);
vector<std::string> 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),