mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

take std::function as const reference

Browse source
This commit is contained in:
Jakob Rath 2024-02-07 15:16:44 +01:00
parent 74a91f691f
commit f0b0ce401e
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/euf/euf_bv_plugin.cpp
View file

@ -426,7 +426,7 @@ namespace euf {
push_merge(n0, n);
}
void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) {
void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer) {
m_todo.push_back({ n, 0 });
unsigned lo, hi;
expr* e;
@ -461,7 +461,7 @@ namespace euf {
clear_offsets();
}
void bv_plugin::super_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) {
void bv_plugin::super_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer) {
m_todo.push_back({ n, 0 });
unsigned lo, hi;
expr* e;
@ -500,7 +500,7 @@ namespace euf {
// Explain that a is a subslice of b at offset
// or that b is a subslice of a at offset
//
void bv_plugin::explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)>& consumer) {
void bv_plugin::explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)> const& consumer) {
if (width(a) < width(b))
std::swap(a, b);
SASSERT(width(a) >= width(b));

8
src/ast/euf/euf_bv_plugin.h
View file

@ -109,15 +109,15 @@ namespace euf {
void undo() override;
void set_ensure_th_var(std::function<void(enode*)>& f) { m_ensure_th_var = f; }
void set_ensure_th_var(std::function<void(enode*)> f) { m_ensure_th_var = std::move(f); }
std::ostream& display(std::ostream& out) const override;
void sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer);
void sub_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer);
void super_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer);
void super_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer);
void explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)>& consumer);
void explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)> const& consumer);
};
}