search

CatalaLang / catala

Programming language for literate programming law specification
https://catala-lang.org
Apache License 2.0
1.98k stars 78 forks source link

Finish Z3 encoding of Dcalc #182

Open denismerigoux opened 2 years ago

denismerigoux commented 2 years ago

Several parts of the Z3 encoding of Dcalc are missing and should be completed:

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L111

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L113

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L127

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L147

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L162-L164

And some others, neatly signaled by the failwith.

R1kM commented 2 years ago

While several components are still not or partially supported, the current encoding is sufficient to handle all variables from the "allocations_familiales" example. I'd suggest extending the current support for the missing constructs on an "on-demand" basis, i.e., when new Catala code leads to failures in the encoding.