mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

constify a few functions

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-04-03 09:44:31 -07:00
parent 4c353ec720
commit 67e9d74653
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/bv_decl_plugin.cpp
View file

@ -766,7 +766,7 @@ bool bv_recognizers::is_zero(expr const * n) const {
return decl->get_parameter(0).get_rational().is_zero();
}
bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) const {
if (!is_extract(e)) return false;
low = get_extract_low(e);
high = get_extract_high(e);
@ -774,7 +774,7 @@ bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, ex
return true;
}
bool bv_recognizers::is_bv2int(expr const* e, expr*& r) {
bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const {
if (!is_bv2int(e)) return false;
r = to_app(e)->get_arg(0);
return true;