search

uwdb / Cosette

Cosette is an automated SQL solver.
BSD 2-Clause "Simplified" License
662 stars 54 forks source link

support AVG #55

Closed stechu closed 6 years ago

stechu commented 6 years ago

Can be supported as an uninterpreted function in Coq and interpreted in Rosette.

Mestway commented 6 years ago

Note that rosette side support only symbolic integer not symbolic floats. I suggest adding avg as an uninterpreted function during verification.

stechu commented 6 years ago

@Mestway ahh, that's right. uninterpreted in Rosette should be ok, too.