Feature request: Python API

[shaobo-he]

Hello sv-witnesses developers,

I was wondering if it makes sense to provide Python APIs (e.g., witness node classes with methods to create/manipulate them). I think it would benefit the users significantly. For example, verifier developers could use them to represent their error traces and analyze them. Processing Python classes is personally preferred than GraphML formats.

Thanks,
Shaobo

[MartinSpiessl]

Hi Shaobo,

Sure, if you need that then I would say just go for it! In the end GraphML is an XML based format, so you can already read in the witness as XML in python and inspect/manipulate the nodes as such.

This repository is mainly for documenting the format, but of course we can also collect common utility functionality around the format.

For example @SvenUmbricht recently added a linter for the witness format that includes a python class representing a witness, have a look at:
https://github.com/sosy-lab/sv-witnesses/blob/master/lint/witnesslint/witness.py

Some of the fields in that class are filled when the witness is linted. The class is not designed to be reused in a general context, but I think if there is use for this then we could generalize this code to be more useful for other purposes.

Can you describe in more detail what your current use case for such a functionality would be? It is often easier to develop things if we divide the functionality into small chunks and implement them incrementally.

[shaobo-he]

Thank you for your quick response, @MartinSpiessl

Can you describe in more detail what your current use case for such a functionality would be? It is often easier to develop things if we divide the functionality into small chunks and implement them incrementally.

I guess what I want is Python classes to represent witnesses (for our case, violation witnesses). With them, I can convert the verifier output into objects in these classes and let them dump into GraphML, JSON, or whatever format the users fancy.