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