Skip to content

bv_varidt now has next member #1586

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
kroening wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

bv_varidt now has next member #1586

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6977408
netlist: use bv_varidt constructor
kroening Jan 12, 2026
e8b7111
bv_varidt now has next member
kroening Jan 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/ebmc/bdd_engine.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,7 @@ void bdd_enginet::allocate_vars(const var_mapt &var_map)
bit_nr<it.second.bits.size();
bit_nr++)
{
bv_varidt bv_varid(it.first, bit_nr);
bv_varidt bv_varid{it.first, bit_nr, false};
vars[bv_varid].is_input=
it.second.is_input() || it.second.is_nondet();
}
Expand Down
36 changes: 19 additions & 17 deletions src/trans-netlist/bv_varid.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,31 +17,31 @@ class bv_varidt
{
public:
irep_idt id;
unsigned bit_nr;

std::size_t bit_nr;
bool next;

friend bool operator==(const bv_varidt &i1, const bv_varidt &i2)
{
return i1.id==i2.id && i1.bit_nr==i2.bit_nr;
return i1.id == i2.id && i1.bit_nr == i2.bit_nr && i1.next == i2.next;
}

friend bool operator<(const bv_varidt &i1, const bv_varidt &i2)
{
if(i1.id==i2.id)
return i1.bit_nr<i2.bit_nr;

return i1.id<i2.id;
{
if(i1.bit_nr == i2.bit_nr)
return i1.next < i2.next;
else
return i1.bit_nr < i2.bit_nr;
}
else
return i1.id < i2.id;
}

inline bv_varidt(
const irep_idt &_id,
unsigned _bit_nr):
id(_id),
bit_nr(_bit_nr)
{ }

inline bv_varidt():bit_nr(0)

inline bv_varidt(const irep_idt &_id, std::size_t _bit_nr, bool _next)
: id(_id), bit_nr(_bit_nr), next(_next)
{ }

std::string as_string() const;
};

Expand All @@ -53,7 +53,9 @@ static inline std::ostream & operator<< (std::ostream &out, const bv_varidt &v)
struct bv_varidt_hash
{
size_t operator()(const bv_varidt &bv_varid) const
{ return hash_string(bv_varid.id)^bv_varid.bit_nr; }
{
return hash_string(bv_varid.id) ^ bv_varid.bit_nr ^ bv_varid.next;
Copy link
Collaborator

@tautschnig tautschnig Jan 12, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this perhaps use the hash function helpers from irep_hash.h instead of naively XOR-ing values? bit_nr will only ever have some of the least-significant bits set, and next will only ever be 0 or 1. Alas, only id will make use of all bits, while the other two will only ever affect a small subset of the bits. In contrast, hash_combine would take care of rotating and distributing bits.

}
};

#endif
33 changes: 11 additions & 22 deletions src/trans-netlist/trans_to_netlist.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -331,14 +331,11 @@ void convert_trans_to_netlistt::operator()(
v_it!=dest.var_map.map.end();
v_it++)
{
bv_varidt bv_varid;
bv_varid.id=v_it->first;
var_mapt::vart &var=v_it->second;

for(bv_varid.bit_nr=0;
bv_varid.bit_nr<var.bits.size();
bv_varid.bit_nr++)
for(std::size_t bit_nr = 0; bit_nr < var.bits.size(); bit_nr++)
{
bv_varidt bv_varid{v_it->first, bit_nr, false};
var_mapt::vart::bitt &bit=var.bits[bv_varid.bit_nr];
lhs_entryt &entry=lhs_map[bv_varid];
entry.bit=&bit;
Expand Down Expand Up @@ -395,13 +392,11 @@ void convert_trans_to_netlistt::operator()(

if(it==dest.var_map.reverse_map.end())
{
bv_varidt varid;
varid.id="nondet";
varid.bit_nr=dest.var_map.nondets.size();
bv_varidt varid{"nondet", dest.var_map.nondets.size(), false};
var_mapt::vart &var=dest.var_map.map[varid.id];
var.add_bit().current=literalt(n, false);
var.vartype=var_mapt::vart::vartypet::NONDET;
dest.var_map.reverse_map[n]=varid;
dest.var_map.reverse_map.emplace(n, varid);
dest.var_map.nondets.insert(n);
}
}
Expand Down Expand Up @@ -603,15 +598,12 @@ void convert_trans_to_netlistt::convert_lhs_rec(
PRECONDITION(from <= to);

if(expr.id()==ID_symbol)
{
bv_varidt bv_varid;

bv_varid.id=to_symbol_expr(expr).get_identifier();
{
auto identifier = to_symbol_expr(expr).get_identifier();

for(bv_varid.bit_nr=from;
bv_varid.bit_nr<=to;
bv_varid.bit_nr++)
for(std::size_t bit_nr = from; bit_nr <= to; bit_nr++)
{
bv_varidt bv_varid{identifier, bit_nr, false};
lhs_mapt::iterator it=lhs_map.find(bv_varid);

if(it==lhs_map.end())
Expand Down Expand Up @@ -772,14 +764,11 @@ void convert_trans_to_netlistt::add_equality_rec(
lhs.id()==ID_symbol)
{
bool next=lhs.id()==ID_next_symbol;
auto identifier = lhs.get(ID_identifier);

bv_varidt bv_varid;
bv_varid.id=lhs.get(ID_identifier);

for(bv_varid.bit_nr=lhs_from;
bv_varid.bit_nr!=(lhs_to+1);
bv_varid.bit_nr++)
for(std::size_t bit_nr = lhs_from; bit_nr != (lhs_to + 1); bit_nr++)
{
bv_varidt bv_varid{identifier, bit_nr, false};
lhs_mapt::iterator it=
lhs_map.find(bv_varid);

Expand Down
4 changes: 1 addition & 3 deletions src/trans-netlist/var_map.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,9 +59,7 @@ void var_mapt::add(

if(var.is_latch() || var.is_input())
{
bv_varidt &reverse=reverse_map[v_current];
reverse.id=id;
reverse.bit_nr=bit_nr;
reverse_map.emplace(v_current, bv_varidt{id, bit_nr, false});
}
}

Expand Down
Loading