From 70785a095e22c5d698faa20915959f9573508714 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Feb 2024 15:25:25 +0100 Subject: [PATCH] function as const-ref --- src/sat/smt/polysat_egraph.cpp | 4 ++-- src/sat/smt/polysat_solver.h | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index 5c14aa752..56246c97b 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -114,13 +114,13 @@ namespace polysat { m_bv_plugin->super_slices(b, consume_slice); } - void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function& consume_eq) { + void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function const& consume_eq) { euf::theory_var v = m_pddvar2var[pv]; euf::theory_var w = m_pddvar2var[pw]; m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq); } - void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function& consume_eq) { + void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function const& consume_eq) { euf::theory_var v = m_pddvar2var[pv]; expr_ref val(bv.mk_numeral(slice.value, slice.length), m); euf::enode* b = ctx.get_egraph().find(val); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 3f42381c6..c70a89989 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -111,8 +111,8 @@ namespace polysat { sat::check_result intblast(); - void explain_slice(pvar v, pvar w, unsigned offset, std::function& consume); - void explain_fixed(pvar v, fixed_slice const& s, std::function& consume_eq); + void explain_slice(pvar v, pvar w, unsigned offset, std::function const& consume); + void explain_fixed(pvar v, fixed_slice const& s, std::function const& consume_eq); // internalize bool visit(expr* e) override;