Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support loading *.aig files in binary format #130

Merged
merged 4 commits into from
Jan 14, 2023
Merged

Support loading *.aig files in binary format #130

merged 4 commits into from
Jan 14, 2023

Conversation

masinag
Copy link
Contributor

@masinag masinag commented Jan 14, 2023

Resolves #129

Main contributions:

  • the parser.load function reads the file in binary mode

  • the parser.parse function expects either:

    • a string
    • a list of strings
    • a byte array

    In either case, the input is transformed into a stream of bytes, which is consumed by the parsers. I chose this solution since if the file is in aig format, then the list of and gates may contain bytes interpreted as the \n character. Thus, splitting the string by the \n character would not have worked.

The parsers have been modified as follows:

  • the parse_header consumes the stream until the next \n and then it tries to match the regex as before. Additionally, it checks whether the header starts with aag or aig and sets the binary_mode boolean attribute of Header accordingly;
  • the parse_input works as before in case of aag files. In case of aig files, it adds the inputs 2, 4, ... 2 * (n_inputs);
  • the parse_latches works as before in case of aag files. In case of aig files, it reads just one or two integers. I am not so sure if having two integers (one to set the initial value of the latch) is allowed in the binary format (I am not sure even if it is allowed in the ASCII format);
  • the parse_output works as before in both cases;
  • the parse and is the one involving most of the changes: in case of aig files, it consumes the stream one byte at a time, reading the gates as https://github.com/arminbiere/aiger/blob/5f8ce5ca5fc42a06e5d713309f99195a740ac2b4/aiger.c#L2376
  • the parse_symbol and parse_comment work basically as before

@masinag
Copy link
Contributor Author

masinag commented Jan 14, 2023

I also aligned the parsing of the And gates with the others, so that it does not decrement the state.header.num_ands but rather it keeps a list of And gates into the State, and it checks for the property state.remaining_ands

@mvcisback
Copy link
Owner

Great! I'll review when I have a chance this weekend.

My initial skim didn't show anything concerning and overall it looks solid.

@mvcisback mvcisback merged commit 465c96a into mvcisback:main Jan 14, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Support for aig files
2 participants