Proposal: extend property format + parser to handle multiple networks

[MatthewDaggitt]

I am interested in verifying properties about multiple networks e.g.

1. prove that some network f is monotonic in one of its inputs in some region (two references to the same network).
2. prove that two networks are approximately equal up to some epsilon in some region

Having had a play around with the input parser, I think(?) this should be relatively simple. As I understand it, the engine doesn't have any concept of a network, only a system of constraints, so it should be enough to alter the parsing code to setup the system of constraints in the InputQuery object appropriately?

My tentative plan is as follows:

1. Extend the command line arguments to allow you to input multiple network files
2. Feed the networks one-by-one through the InputParser, but making sure to restart the indexing of the variables each time from one more than the previous input and output variable number.

For example if you have two networks:

• f with 2 inputs and 1 output
• g with 2 inputs and 2 outputs

then x0, x1/y0 would refer to the inputs/outputs f and x2, x3/y1, y2 refer to inputs/outputs of g

Question: before I embark on this, am I missing anything important? I'm not aware of any other verifiers out there that support this functionality currently....