Add package for z3 and boolector for formal?

[RobertBaruch]

The Z3 solver for formal verification is quite fast (on some platforms) compared to the default for symbiyosys. On other platforms, boolector is better.

Compilation instructions at https://symbiyosys.readthedocs.io/en/latest/quickstart.html

I'd try to contribute if someone could point me to a clear step-by-step guide. I can also just try to keep attempting pull requests and seeing what the errors from Travis are :)

[mithro]

You can test locally, ./conda-env.sh build <path to your meta file> then once that works you do the Travis thing until green.

[RobertBaruch]

Hmm, now that I finally have docker locally working and compiling things, it seems that in building formal/symbiyosys, z3 and boolector are also built anyway. So obsoleting this issue.

[mithro]

@RobertBaruch I'm actually going to reopen this as z3 and boolector probably should be their own packages.

[RobertBaruch]

I'll take a shot at this.

[RobertBaruch]

I haven't been able to figure out how to compile z3 on windows. It's possible, but relies on a Python script from z3: python mk_make.py, which creates the appropriate makefiles for your OS. The problem is that the script relies on os.name to detect the OS, and it always comes up as nt, which is Windows, which generates a makefile for nmake, which I can't figure out how to install using conda.

Apparently the script could theoretically detect Mingw, but I don't know how to get python to run under conda while also reporting os.name as posix.

[RobertBaruch]

The alternative is just to download the built z3 windows version -- after all, why build z3 if it's already built -- but I have no idea how to conda, so I also have no idea how to just repackage a release for conda.

[RobertBaruch]

Welp, I have some conda files that Travis seems to feel compiles z3 for OSX, Linux, and Windows. Unfortunately I ended up having to pin the release at 4.8.7 because there doesn't seem to be an easy way to compile for Windows. So instead it compiles for OSX and Linux, and just downloads the built version from github for Windows.

Will work on boolector now.

[RobertBaruch]

Was able to get z3 compiling under Windows, so we can compile z3 from head. Still working on boolector for Windows.