The Z3 C API provides a low-level interface to Z3 datatypes (F-algebras, really). The Z3 Python binding attempts to OOPify that to some extent using Python reflection. Once we make more progress along the lines of something like "Liquid Smalltalk", it will be meaningful to design an idiomatic API for F-algebras. Right now, I am not sure which layers (Z3/SMT? Fixpoint? Sprite?) call for such idiomatic language. On the one hand, this Z3 API is just used internally by F.Data and then in turn Data. On the other hand, the Deterministic Interpreter for Jib instantiates Z3 ASTs directly and thus it also will need this Z3-level API.
The present Issue is the correct forum for all discussions pertaining such Smalltalk API (limited to the Z3/SMT level, not Liquid).
The Z3 C API provides a low-level interface to Z3 datatypes (F-algebras, really). The Z3 Python binding attempts to OOPify that to some extent using Python reflection. Once we make more progress along the lines of something like "Liquid Smalltalk", it will be meaningful to design an idiomatic API for F-algebras. Right now, I am not sure which layers (Z3/SMT? Fixpoint? Sprite?) call for such idiomatic language. On the one hand, this Z3 API is just used internally by
F.Dataand then in turnData. On the other hand, the Deterministic Interpreter for Jib instantiates Z3 ASTs directly and thus it also will need this Z3-level API.The present Issue is the correct forum for all discussions pertaining such Smalltalk API (limited to the Z3/SMT level, not Liquid).