search

shingarov / MachineArithmetic

A mathematical foundation for Smalltalk-25
MIT License
17 stars 6 forks source link

[Z3] Implement parameter-related types (`PARAM_DESCRS` and friends) #252

Closed shingarov closed 4 months ago

shingarov commented 8 months ago

Right now, attempt to call Z3Solver>>getParamDescrs or related APIs, will result in exception:

API not (yet) supported: Type PARAM_DESCRS not (yet) supported.

Support for these APIs is required before we can play with setting different solving tactics (for example to prove Gauss over bv32).

janvrany commented 8 months ago

Half-baked support for PARAM_DESCRS is here: https://github.com/janvrany/MachineArithmetic/tree/pr/add-Z3ParameterDescriptionSet

Will finish it later as there are more pressing things.