mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

use -> types

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-03-13 16:20:51 -07:00
parent 2fdf2233f9
commit c2f8dd9a02
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/polysat_egraph.cpp
View file

@ -35,7 +35,7 @@ namespace polysat {
// walk the egraph starting with pvar for suffix overlaps.
void solver::get_bitvector_suffixes(pvar pv, offset_slices& out) {
uint_set seen;
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool {
if (offset != 0)
return false;
for (auto sib : euf::enode_class(n)) {
@ -59,7 +59,7 @@ namespace polysat {
// walk the egraph starting with pvar for any overlaps.
void solver::get_bitvector_sub_slices(pvar pv, offset_slices& out) {
uint_set seen;
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool {
for (auto sib : euf::enode_class(n)) {
auto w = sib->get_th_var(get_id());
if (w == euf::null_theory_var)
@ -81,7 +81,7 @@ namespace polysat {
// walk the egraph for bit-vectors that contain pv.
void solver::get_bitvector_super_slices(pvar pv, offset_slices& out) {
uint_set seen;
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool {
for (auto sib : euf::enode_class(n)) {
auto w = sib->get_th_var(get_id());
if (w == euf::null_theory_var)
@ -105,7 +105,7 @@ namespace polysat {
void solver::get_fixed_bits(pvar pv, fixed_bits_vector& out) {
theory_var v = m_pddvar2var[pv];
euf::enode* b = var2enode(v);
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool {
auto r = n->get_root();
if (!r->interpreted())
return true;