Repository navigation
Update rumba 1.0 - #4
Merged
Merged
Conversation
Rumba published 1.0.0, so take it from the registry rather than pinning a GitHub revision. The lockfile now records a checksum instead of a commit hash, and binbit is the only remaining git dependency. Two upstream changes reach us: The solver returns Result. simplify_mba is now fn(Expr, u8) -> Result<Expr, SolveError>; the four panics reachable from a solve became error variants. simplify_mba_catching_panic goes away with them, and with it the process-global panic-hook swap and the mutex that had to serialize every island simplification to make that swap safe. A SolveError means "Rumba declined this island", which lands on the same copy-it-structurally path the caught panic used to. Const payloads are plain u64. Expr::Const and Expr::Scale no longer wrap VarInt, and the varint module is now pub(crate), so make_mask is gone from the public API. Mask with & directly and keep a local mask_for_width.
MAX_RUMBA_VARIABLES counted island leaves at conversion time and abandoned the island past 20. Rumba's own MAX_VARS counts a different thing: the variable count of each linear sub-MBA after reduce_vars, checked inside solve_linear. reduce_vars can shrink that count, so a 25-leaf island may solve fine and we were refusing it; the nonlinear path can also grow it past the leaf count when hide_in_var re-enters the solver. The cap was neither an upper nor a lower bound on the limit it was mirroring, only a number that happened to match. It existed to dodge a panic, and the panic is gone: the same condition is now Err(TooManyVariables), already routed to the copy-it-structurally path. Nor was it guarding against blowup -- conversion is a linear walk over validated in-memory nodes, and Rumba's limit fires before the 2^t truth table is built. Both cap checks were also the only source of None in IslandConversion, so removing them collapses the Option threaded through convert, convert_child, children2, nary and named. boundary loses its Result too, having no fallible path left. Full CSV dataset suite (SMT_SERVER_RUMBA_FULL_DATASET=1) is unchanged.
Contributor
|
❤️ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The most significant difference in the API change is that rumba no longer panics :)