You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, the test cases for parsing list/set/tuple and in/not in operators to Z3 constraints only include tests for empty lists and tuples, but not sets. This is because the only way to represent an empty set in function preconditions is to use the set() function (since {} represents an empty dictionary). However, the parse_assertion function in contracts/__init__.py, which converts precondition docstrings to Python expressions, cannot infer the return value of set(). As a result, ExprWrapper, the class that converts function preconditions to Z3 expressions, skips preconditions that involve empty sets.
Proposed solution:
Enhance parse_assertion Function:
Modify the parse_assertion function to correctly infer the set() function as an empty set.
Add Unit Tests:
Update the container_list and container_expected lists in tests/test_z3_visitor.py to include the following test cases:
# Add to container_list:""" def in_empty_set(x: int): ''' Preconditions: - x in set() ''' pass """,
""" def not_in_empty_set(x: int): ''' Preconditions: - x not in set() ''' pass """,
# Add to container_expected:
[z3.BoolVal(False)],
[z3.BoolVal(True)],
The text was updated successfully, but these errors were encountered:
Currently, the test cases for parsing
list/set/tuple
andin/not in
operators to Z3 constraints only include tests for empty lists and tuples, but not sets. This is because the only way to represent an empty set in function preconditions is to use theset()
function (since{}
represents an empty dictionary). However, theparse_assertion
function incontracts/__init__.py
, which converts precondition docstrings to Python expressions, cannot infer the return value ofset()
. As a result,ExprWrapper
, the class that converts function preconditions to Z3 expressions, skips preconditions that involve empty sets.Proposed solution:
Modify the
parse_assertion
function to correctly infer theset()
function as an empty set.Update the
container_list
andcontainer_expected
lists intests/test_z3_visitor.py
to include the following test cases:The text was updated successfully, but these errors were encountered: