c5f633dfa2
Basic structure for the integration of Z3 into Congress. Defines a Z3Theory as an alternative to nonrecursive theories. Defines a Z3Context for executing Z3Theory content. Z3 must be installed manually and is not in the requirements devstack will install Z3 if ENABLE_CONGRESS_Z3 is set. Limitations: * No built-ins * Typechecking does not support sub-typing (will be done later through built-ins). Partially-implements: blueprint alternative-engine-z3 Change-Id: I87ff439a3ed4a3e83c78c98add7d94275f716a01 |
||
---|---|---|
.. | ||
notes | ||
source |