1# Using Boolector with Docker 2 3Boolector has support for executing Boolector "input files" (e.g., `.smt2`) 4files via the use of a Docker container. The base container used is Alpine 5Linux. 6 7This guide assumes that the reader is familiar with both Docker and Boolector, 8and are able to install the necessary prerequisites to run Docker. 9 10 11## Building the Docker image 12 13To build the Docker image locally, you can perform the following: 14 15``` 16git clone https://github.com/Boolector/boolector.git 17cd boolector 18docker build -t btor/btor -f contrib/docker/Dockerfile . 19``` 20 21This will then build you a fresh Docker image, with Boolector's current master 22branch built inside. 23 24If you wish to build a version of Boolector using a different repository or a 25different branch, you can specify this as part of Docker's build arguments: 26 27``` 28# default arguments 29UPSTREAM=https://github.com/Boolector/boolector/archive 30BRANCH=master 31docker build -t btor/btor \ 32 -f contrib/docker/Dockerfile \ 33 --build-arg UPSTREAM=${UPSTREAM} \ 34 --build-arg BRANCH=${BRANCH} . 35``` 36 37## Using Docker to run `.smt2` files 38 39As Boolector is able to read SMT-LIB v2 files via `stdin`, this means that it 40is extremely easy to run Boolector against a `.smt2` file. For example: 41 42``` 43# Assuming you're at the root of a Boolector clone 44cat src/tests/log/modelgensmt227.smt2 | docker run -i --rm btor/btor -m 45``` 46 47Alternatively, to see Boolector's help: 48 49``` 50docker run -i --rm btor/btor --help 51``` 52 53*Note*: the `ENTRYPOINT` specified in the Boolector `Dockerfile` tells it to run 54`boolector` without any arguments. You can specify additional arguments to 55Boolector via your Docker `run` command. 56 57### Sharing files to the container 58 59The Boolector Docker image (by default) does not have access to your "host" 60file-system, which is why `cat` was necessary to pipe in the contents of your 61`.smt2` file into the image. 62 63If you wish to allow the containerised version of Boolector to able to read 64files from the host file-system, you can use Docker's `-v` flag to mount a 65shared volume: 66 67``` 68# Assuming you're at the root of a Boolector clone 69docker run --rm -i -v $(pwd):/tmp btor/btor -m /tmp/test/log/modelgensmt227.smt2 70``` 71 72*Note*: the current working directory (`pwd`) has been mapped to `/tmp` within 73the container -- hence why the file-path to the SMT2LIB file you wish to run 74starts with `/tmp`. 75 76 77## Using Docker to work with Boolector's Python API 78 79The Boolector Docker image has been built with support for Boolector's Python 80API, however as the entry-point for the image is to run `boolector` (the 81application), then slightly more work is required to work with Python inside of 82the container: 83 84``` 85# Assuming you're at the root of a Boolector clone 86docker run -it -v $(pwd):/tmp --entrypoint=/bin/bash btor/btor -i 87 88# Note: you are now inside of the container and not the host! 89 90# Run a Python script using pyboolector 91python /tmp/examples/api/python/api_usage_examples.py 92 93# Leave the container! 94exit 95``` 96 97*Note*: if you wish to use the containerised Python directly with files on your 98host file-system, you can customise the `ENTRYPOINT` specified in Boolector's 99`Dockerfile` (i.e., rather than running `boolector`, you can run `python`). 100 101