feat: add support for per-level alphabet in NFT#618
feat: add support for per-level alphabet in NFT#618tmokenc wants to merge 3 commits intoVeriFIT:develfrom
Conversation
This is a very naive implementation, not sure if it is actually correct or I missed something. (cherry picked from commit 705db38)
|
I think it would be cleaner if we had a single The abstract alphabet would probably have to allow for translating optionally on a specific level, so Most, if not all, of the additional functions here would then be unnecessary. |
|
I agree that it would be cleaner, reduce a lot of the confusion and potentially be better for the serialisation/deserialisation of the .mata format later on. I will work on it as soon as possible. |
|
@Adda0 Please take a look. I refactored the code to use This is my first C++ project, so I may have missed some conventions or done something in a way that is uncommon in C++. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## devel #618 +/- ##
==========================================
- Coverage 72.90% 72.83% -0.08%
==========================================
Files 45 45
Lines 6795 6832 +37
Branches 1538 1541 +3
==========================================
+ Hits 4954 4976 +22
- Misses 1227 1239 +12
- Partials 614 617 +3 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
| virtual std::string reverse_translate_symbol(Symbol symbol, size_t level) const { | ||
| (void)level; | ||
| return reverse_translate_symbol(symbol); | ||
| } |
There was a problem hiding this comment.
Side note: We definitely need to rename these monstrosities when we are refactoring alphabets. It is awful to work with this in a function call, e.g., something like minimize(nfa, nfa->alphabet.reverse_translate_symbol(symbol), true)...
| * @param[in] level Level on which the symbols should be retrieved. | ||
| * @return Set of symbols known to the alphabet on the given level. | ||
| */ | ||
| virtual utils::OrdVector<Symbol> get_alphabet_symbols(size_t level) const { |
There was a problem hiding this comment.
Might be easier to just use std::optional<Level> level and have one function for each of the operations. Also, definitely use Level instead of size_t everywhere for levels.
| * | ||
| * @param[in] level Level on which the alphabet should be cleared. | ||
| */ | ||
| virtual void clear(size_t level) { |
There was a problem hiding this comment.
For all of these functions, I would really rather just have one function with std::optional<Level> level = std::nullopt (including the default). Makes it a bit more concise and readable, IMO.
| * @return Resolved alphabet reference. | ||
| * @throws std::runtime_error If the level is invalid. | ||
| */ | ||
| const Alphabet& resolve_alphabet(size_t level) const; |
There was a problem hiding this comment.
Maybe get_alphabet_for_level(Level level)? resolve sounds like it does actually something complex rather than just returning an element from a vector.
|
It looks like you can ignore the failing CI actions. Not related. The approach and the interface look good to me overall. It is a schame we cannot hide the invalid operations (with/without levels) for specific alphabet types without something like std::variant etc. Maybe even exploring something like |
2 participants
This PR adds support for per-level alphabets in
mata::nft::Nft.The main addition is:
std::vector<Alphabet*> level_alphabetswith the following semantics:
Nftcan fallback to use the inheritednfa::Nfa::alphabetNft::alphabetis set tonullptr, and the per-level alphabets are stored inlevel_alphabetsThe PR also adds two helper functions:
alphabet_of_levelreturns the alphabet for a given level and falls back to the inheritedNfaalphabet when no level-specific alphabet is availableset_level_alphabetsto assign or update alphabetsThis PR does not yet introduce any changes to NFT operations or to the
.mataformat for NFTs. The.mataformat part likely deserves a separate discussion.