mismatch in parsing symbol table of AIG ASCII format? about lorina

[hriener]

Thank you for your question.

A failing test case or a complete example with expected and actual output would be helpful.

I tried to translate your question in some example code:

struct test_reader : public aiger_reader
{
  explicit test_reader() {}

  void on_input( uint32_t pos, uint32_t literal ) const override
  {
    fmt::print( "[i] on_input: pos = {}, index = {}, literal = {}\n",
                pos, literal/2, literal );
    inputs.emplace_back( std::make_tuple( pos, literal ) );
  }
  
  void on_input_name( uint32_t pos, std::string const& name ) const override
  {
    fmt::print( "[i] on_input_name: pos = {}, name = \"{}\"\n", pos, name );
    input_names.emplace( pos, name );
  }
  
  mutable std::vector<std::tuple<uint32_t, uint32_t>> inputs;  
  mutable std::map<uint32_t, std::string> input_names;  
}; /* test_reader */

std::string aiger_file{
  "aag 38 4 0 0 0\n"
  "12\n"
  "10\n"
  "76\n"
  "72\n"
  "i0 symbol_of_12\n"
  "i1 symbol_of_10\n"
  "i2 symbol_of_76\n"
  "i3 symbol_of_72\n"};

std::istringstream iss( aiger_file );
test_reader reader;
auto const result = read_ascii_aiger( iss, reader );
assert( result == return_code::success );

for ( const auto& inputs : reader.inputs )
{
  fmt::print( "i{} {} with name \"{}\"\n",
              std::get<0>( inputs ), std::get<1>( inputs ),
              reader.input_names[std::get<0>( inputs )] );
}

The example produces the following output on my system:

[i] on_input: pos = 0, index = 6, literal = 12
[i] on_input: pos = 1, index = 5, literal = 10
[i] on_input: pos = 2, index = 38, literal = 76
[i] on_input: pos = 3, index = 36, literal = 72
[i] on_input_name: pos = 0, name = "symbol_of_12"
[i] on_input_name: pos = 1, name = "symbol_of_10"
[i] on_input_name: pos = 2, name = "symbol_of_76"
[i] on_input_name: pos = 3, name = "symbol_of_72"
i0 12 with name "symbol_of_12"
i1 10 with name "symbol_of_10"
i2 76 with name "symbol_of_76"
i3 72 with name "symbol_of_72"

What output would you expect instead?

[mfernan2]

Thanks for the explanation. I think I understand the source of my confusion:

1. I had interpreted "index" in on_input_name to refer to variable index, but from your example it's actually position. On reinspection it looks like lorina uses "literal" to refer to variable indexes.

2. I was reading in my AIG via Mockturtle. I think Mockturtle's aiger_reader inheritor incorrectly does not override on_input. It looks to me like it assumes the inputs come linearly in order starting from 1 (the insertion loop in on_header). Do you agree? If so, I can file an issue over there instead.

[hriener]

1. Yes, the name index is misleading in lorina's reader visitor. I will change it to position. Thank you for pointing this out.
2. mockturtle's AIGER reader is designed for the binary AIGER format, which is more restricted than the ASCII format. These restrictions allow storing the benchmarks more compactly. One simplifying assumption is that the inputs are always 1, ..., I, such that they do not need to be stored in the benchmark at all but can be immediately extracted from the M I L O A header.

You could try to use the AIGER tools to convert your benchmark from ASCII to binary AIGER. Mockturtle should then be able to read it.

[mfernan2]

Sorry I had both an AIG and AAG version of this file and neglected to notice that I was passing the AIG to mockturtle, but quoting from the AAG here. I think you're correct that there's no issue here. Sorry for the noise and thanks for clearing up my confusion.