mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Remove unnecessary value parameter copies.

Browse source
This commit is contained in:
Bruce Mitchener 2018-02-06 14:29:54 +07:00
parent 3f7453f5c5
commit 757b7c66ef
7 changed files with 40 additions and 40 deletions
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));