feat: update monabs#14
Conversation
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request transitions the monadic predicate abstraction core functions from Z3-specific implementations to PySMT, facilitating broader solver support. It introduces a new core_lit_filter algorithm and updates existing unary and disjunctive check functions to track solver calls and handle timeouts. The testing infrastructure is also overhauled with a new script for benchmarking SMT2 files, and utility modules for logging, configuration, and file collection are added. Feedback focuses on addressing potential import errors in the test script, removing trailing whitespaces, refining exception handling to avoid broad try-except blocks, resolving type hint mismatches, and cleaning up wildcard imports and commented-out code.
| from cores.unary_check_pysmt import ( | ||
| unary_check, | ||
| unary_check_cached, | ||
| unary_check_incremental, | ||
| unary_check_incremental_cached, | ||
| ) | ||
| from aria.monabs.cores.dis_check_pysmt import ( | ||
| from cores.dis_check_pysmt import ( | ||
| disjunctive_check_cached, | ||
| disjunctive_check_incremental_cached, | ||
| ) | ||
| from aria.monabs.cores.con_check_pysmt import ( | ||
| conjunctive_check, | ||
| conjunctive_check_incremental, | ||
| from cores.new_check_pysmt import ( | ||
| core_lit_filter, | ||
| ) | ||
|
|
||
| from utils.logger import setup_logger | ||
| from utils.parse_monabs_pysmt import parse_monabs_pysmt | ||
| from utils.utils import collect_smt2_files | ||
| import utils.config as cf |
There was a problem hiding this comment.
The imports from cores and utils are direct, which assumes that the script is run from a directory where cores and utils are subdirectories. Since this script is in the tests directory, these imports will likely fail depending on how the script is executed. To make this script a runnable module, you should use relative imports.
For example:
from ..cores.unary_check_pysmt import (
# ...
)
from ..utils.logger import setup_logger
# ...This will allow running the script with a command like python -m aria.monabs.tests.test_pysmt_monabs.
| return "sat" | ||
| if res is False: | ||
| return "unsat" | ||
|
|
There was a problem hiding this comment.
There is a trailing whitespace on this line which should be removed to maintain code style consistency.
| return "unknown" |
| except Exception: | ||
| pass |
There was a problem hiding this comment.
Using a broad except Exception: pass is risky as it can silently swallow any and all errors that might occur within the try block, making debugging difficult. This pattern is repeated multiple times in this file (e.g., lines 54-57, 103-105, 114-117). It would be better to catch more specific exceptions that you expect might be raised by pysmt operations, or at least log the exception if you intend to suppress it.
| """ | ||
| if solver_calls is None: | ||
| solver_calls = [0] | ||
|
|
There was a problem hiding this comment.
There is a trailing whitespace on this line which should be removed to maintain code style consistency.
| solver_calls = [0] |
| else: # timeout or unknown | ||
| results[i] = 2 | ||
|
|
||
| return results, solver_calls[0] |
There was a problem hiding this comment.
The function signature specifies a return type of Tuple[List[int], int], but the results variable is typed as List[Optional[int]]. While the logic seems to ensure all None values are replaced, this can cause issues with static type checkers like mypy. To resolve this, you could cast the results list to List[int] before returning.
Example with cast:
from typing import cast, List, Optional, Tuple
...
return cast(List[int], results), solver_calls[0]| results[i] = 2 | ||
| solver.pop() | ||
|
|
||
| return results, solver_calls[0] |
There was a problem hiding this comment.
Similar to the unary_check_cached function, there's a type hint mismatch here. The function is declared to return Tuple[List[int], int], but results is of type List[Optional[int]]. This can lead to type checker errors. Consider using typing.cast to assert the correct type upon returning.
Example with cast:
from typing import cast, List, Optional, Tuple
...
return cast(List[int], results), solver_calls[0]|
|
||
| def process_file(args) -> Dict: | ||
| filepath, timeout_ms = args | ||
| print("[Debug] Processing file:", filepath) |
There was a problem hiding this comment.
This appears to be a debug print statement. For better logging control and consistency, consider using the configured logger instead. If this is intended for user-facing progress, print is fine but the [Debug] prefix might be misleading.
| from .logger import * | ||
| from .parse_monabs_pysmt import * | ||
| from .utils import * | ||
| from .config import * |
There was a problem hiding this comment.
Using wildcard imports (*) is generally discouraged as it can pollute the module's namespace and make it difficult to trace where functions and variables are coming from. It's better to use explicit imports.
For example:
from .logger import setup_logger
from .parse_monabs_pysmt import parse_monabs_pysmt
from .utils import collect_smt2_files
from .config import MIN_LENGTHThis makes the code more readable and maintainable.
| from .logger import * | |
| from .parse_monabs_pysmt import * | |
| from .utils import * | |
| from .config import * | |
| from .logger import setup_logger | |
| from .parse_monabs_pysmt import parse_monabs_pysmt | |
| from .utils import collect_smt2_files | |
| from .config import MIN_LENGTH |
| # if __name__ == "__main__": | ||
| # filepath = "/home/xjn/MPA/MPA/data/bash/cons_6043.smt2" | ||
| # precond, constraints = parse_monabs_pysmt(filepath) | ||
| # print("Precondition:", precond) | ||
| # print("Number of constraints:", constraints) |
There was a problem hiding this comment.
This block of commented-out code seems to be for testing or debugging purposes. It should be removed before merging to keep the codebase clean.
2 participants
No description provided.