katamaran
katamaran copied to clipboard
Split positions of all user-defined predicates into input and outputs
The heap predicates have a field that indicates which predicates are precise, and for those it splits up the arguments into inputs and outpus.
https://github.com/katamaran-project/katamaran/blob/b7d951c28fc8a0ef6297b91b3531df98b7ee52f0/theories/Syntax/Predicates.v#L56-L69
I wonder why we went with that definition instead of defining inputs and outputs positions for all predicates uniformly. I think this would improve the code.