search

souffle-lang / souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
http://souffle-lang.github.io/
Universal Permissive License v1.0
924 stars 208 forks source link

Souffle `explain` is unimplemented for ADTs. #2187

Open markww opened 2 years ago

markww commented 2 years ago

Our project would like to use explain to generate a proof tree for our analysis. It appears that our use of ADTs is blocking us from being able to use explain, as it is unimplemented for ADTs:

https://github.com/souffle-lang/souffle/blob/d70cf1ec0568d7817de5dfecddf555647537ef89/src/ast2ram/provenance/SubproofGenerator.cpp#L238

Would it be possible to implement that branch and have ADT support in explain?

b-scholz commented 2 years ago

It would not be too hard to implement it. We would need to port part of the I/O system (i.e. type system description etc.).

I would be able to guide you. Would you like to implement it?

Cypher1 commented 2 years ago

Hey @b-scholz, I'm Jay (J for short) and I work with @markww .

I'm having a look into this at the moment (scoping upcoming work in Raksha) and would love to hear from you about approaching this. Would you be able to summarize your thoughts here?

Alternatively, I'm in Sydney and would be able to sync over a video call if that would help :)

b-scholz commented 2 years ago

@Cypher1 i have sent Mark the first steps - please let me know whether you need more help.

Cypher1 commented 2 years ago

Thank you!

AdiHarif commented 3 months ago

Is this fixed\being worked on?

I would like to use provenance with ADTs as well, willing to take a swing at implementing it if necessary.

b-scholz commented 3 months ago

Any help would be more than appreciated!