search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Initial version of Dockerfile for Boolector #37

Closed aytey closed 5 years ago

aytey commented 5 years ago

Extremely simple "v0.1" of a Dockerfile that supports building and working with Boolector via a container.

This PR relies on PR #40, otherwise PicoSAT does not correct build under Docker.

mpreiner commented 5 years ago

@andrewvaughanj is there a way to have an Alpine/glibc build and not use the Windows workaround?

aytey commented 5 years ago

Alpine exclusively (excluding "hacks") uses musl libc. I can take a look at porting what I wrote to use (e.g.,) an Ubuntu or Debian base image instead (which would use glibc).

I agree relying on the Windows stuff isn't great, so I am happy to take a look at this (even though I do prefer Alpine for Docker-based used-cases for the majority of instances).

aytey commented 5 years ago

For reference, @mpreiner and I discussed the need for the Windows patches (that, effectively just remove some of glibc-specific signal stuff from a Boolector build), and it was agreed that we're okay to have these patches also applied for Docker.

aytey commented 5 years ago

I am temporarily closing this PR because it now has too many dependents.