zkincaid / duet

Duet: static analysis for unbounded concurrency
http://duet.cs.toronto.edu
MIT License
23 stars 17 forks source link

Support for sup-lin chc. Removed most normalization from srkZ3 parsin… #25

Open JakeSilverman opened 3 years ago

JakeSilverman commented 3 years ago

…g. QLIALift. Various chc helper functions

Note that this push add a few "TODOS" for locations that need to be touched up after the arrays as first order types is pushed. Additionally, it adds a "construct" function to the Formula module that duplicates a function that already exists in the arrays as first order types PR.