-
Notifications
You must be signed in to change notification settings - Fork 71
Description
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)],