katamaran icon indicating copy to clipboard operation
katamaran copied to clipboard

Split positions of all user-defined predicates into input and outputs

Open skeuchel opened this issue 1 year ago • 0 comments

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.

skeuchel avatar Nov 14 '23 12:11 skeuchel