Transpile declarative python to smt-lib2

[adsharma]

I've added some more syntax sugar via python3 with an eye towards making it an intermediate language (like Boogie and Viper) that gets transpiled to smt-lib v2 accepted by z3.

This commit transpiles python function declaration with ellipsis to declare-fun and supports BitVec

py2many/py2many@a6a4af1#diff-38cdc850a1734425b102597f554b6a584305ed0c2e19721db3e36785bdeb4b6f

Earlier commits added support for datatypes and simple function definitions (the Demorgan's law example)

With these changes, I'm hoping that z3 is more approachable to novice python programmers vs the approach taken by z3py (which is to add an API on top of z3 instead of transpiling).

Sample equation solving:

https://github.com/adsharma/py2many/pull/448/files#diff-46a43619db84bd840d1040a478de3c84ad58df3d83a624e78176c384009c1f52

Looking for collaborators in making educational material including jupyter notebooks.

Longer term ideas documented here: https://adsharma.github.io/pysmt/