SyGuS-Org / tools

A set of basic tools for manipulating SyGuS benchmarks
22 stars 4 forks source link

Fix Incorrect Location for start_location when token is at start of line #12

Open Theomat opened 1 year ago

Theomat commented 1 year ago

Hi,

There is an issue with the Location when the token is at the start of the line.

How to reproduce?

Take any file of the https://github.com/SyGuS-Org/benchmarks where the grammar start at the beginning of a new line. Parse it and run the symbol table builder. Then checking the grammar.start_location should yield a negative column index. Here is a snippet:


use_v1: bool = False
if use_v1:
    from parsing.v1.parser import SygusV1Parser
    parser = SygusV1Parser()
else:
    from parsing.v2.parser import SygusV2Parser
    parser = SygusV2Parser()
content: str = my_file_content
program = parser.parse(content)
symbol_table = SymbolTableBuilder.run(program)
key, val = list(symbol_table.synth_functions.items())[0]
grammar: Grammar = val.synthesis_grammar
start = grammar.start_location
print(start)

The Fix

Well, we simply distinguish the case when the token is at the beginning of a line. We check for pos < 0 since in the code when the function is called we take a position and remove 1 so if we are at the start of a line pos is 0 -1 so -1.

Why does a minor error like this matter?

Because people can continue to build up on the SyGus specification with the available tools such as using the parser and then modifying the original files with the help of Location.