fix: symbolic storage variables in counterexample + add path id to co… #578
Conversation
…unterexample for debugging/extra purposes
There was a problem hiding this comment.
Pull Request Overview
This PR fixes an issue where symbolic storage variables weren't properly displayed in counterexamples and adds path ID information to counterexample output for better debugging.
- Expands the regex pattern to capture storage variables in counterexample models
- Adds path ID information to counterexample output format
Reviewed Changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| src/halmos/solve.py | Updates regex pattern to capture storage variables with storage_*_00 pattern |
| src/halmos/main.py | Adds path ID display to counterexample output format |
There was a problem hiding this comment.
thanks for the contribution, @0kn0t! i've left a few comments.
|
|
||
| if model.is_valid: | ||
| print(color_error(f"Counterexample: {model}")) | ||
| print(color_error(f"Counterexample: [{path_id}] {model}")) |
There was a problem hiding this comment.
this prints as Counterexample: [N], but it might not be obvious to users what the number N means. could you make it to explicitly say that N is the path id?
| r""" | ||
| \(\s*define-fun\s+ # Match "(define-fun" | ||
| \|?((?:halmos_|p_)[^ |]+)\|?\s+ # Capture either halmos_* or p_*, optionally wrapped in "|" | ||
| \|?((?:halmos_|p_)[^ |]+|storage_[^ |]+_00)\|?\s+ # Capture halmos_* or p_* or storage_*_00 optionally wrapped in "|" |
There was a problem hiding this comment.
could you make including storage variables optional behind the --print-full-model flag?
for context: originally, storage variables used to be printed only when --print-full-model was enabled. that feature was somehow dropped in #437 (see the diff in __main__.py), and hasn't been brought back yet.
There was a problem hiding this comment.
also, it looks like the current regex doesn't cover storage mapping variables. could you confirm that as well?
fixes #577 (only doesnt work for yices)
also includes path id in counterexample (for debug or advanced use cases)