Skip to content

Commit

Permalink
smtr: Structs have local scope
Browse files Browse the repository at this point in the history
Also unique_name can take field_name directly.
  • Loading branch information
KrystalDelusion authored and aiju committed Sep 3, 2024
1 parent a2abbcb commit d6c5e13
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions backends/functional/smtlib_rosette.cc
Original file line number Diff line number Diff line change
Expand Up @@ -75,15 +75,16 @@ class SmtrStruct {
};
idict<IdString> field_names;
vector<Field> fields;
SmtrScope &scope;
SmtrScope &global_scope;
SmtrScope local_scope;
public:
std::string name;
SmtrStruct(std::string name, SmtrScope &scope) : scope(scope), name(name) {}
SmtrStruct(std::string name, SmtrScope &scope) : global_scope(scope), local_scope(), name(name) {}
void insert(IdString field_name, SmtrSort sort) {
field_names(field_name);
auto base_name = scope.unique_name("\\" + RTLIL::unescape_id(field_name));
auto base_name = local_scope.unique_name(field_name);
auto accessor = name + "-" + base_name;
scope.reserve(accessor);
global_scope.reserve(accessor);
fields.emplace_back(Field{sort, accessor, base_name});
}
void write_definition(SExprWriter &w) {
Expand Down

0 comments on commit d6c5e13

Please sign in to comment.