Add ExtAvy to formal Images

README.md

@@ -14,6 +14,7 @@ A collection of Dockerfiles for easy use of various free & open-source tools. Ha
 * Boolector
 * Bitwuzla
 * Super Prove
+* Avy
 
 ## ghdl-formal.Dockerfile
 
@@ -47,6 +48,7 @@ Risc-V toolchain to develop programs for [NEORV32](https://github.com/stnolting/
 * [Z3](https://github.com/Z3Prover/z3)
 * [Yices 2](https://yices.csl.sri.com/)
 * [CVC4](https://cvc4.github.io/)
+* [Avy](https://bitbucket.org/arieg/extavy)
 * [Boolector](https://boolector.github.io/)
 * [Bitwuzla](https://bitwuzla.github.io/)
 * [Super Prove](https://github.com/berkeley-abc/super_prove)

ghdl-formal.Dockerfile

@@ -52,6 +52,8 @@ RUN apt-get update -qq && \
     make \
     python3 \
     libssl-dev \
+    libboost-program-options1.67.0 \
+    strace \
     libpython2.7 && \
     apt-get -y upgrade && apt-get autoclean && apt-get clean && apt-get -y autoremove && \
     update-ca-certificates && \
@@ -61,4 +63,4 @@ RUN apt-get update -qq && \
 COPY --from=symbiyosys-ghdlsynth /opt /opt
 
 # Enhance path variable
-ENV PATH "/opt/ghdl/bin:/opt/symbiyosys/bin:/opt/yosys/bin:/opt/z3/bin:/opt/yices2/bin:/opt/cvc4/bin:/opt/boolector/bin:/opt/bitwuzla/bin:/opt/super_prove/bin:$PATH"
+ENV PATH "/opt/ghdl/bin:/opt/symbiyosys/bin:/opt/yosys/bin:/opt/z3/bin:/opt/yices2/bin:/opt/avy/bin:/opt/cvc4/bin:/opt/boolector/bin:/opt/bitwuzla/bin:/opt/super_prove/bin:$PATH"

symbiyosys.Dockerfile

@@ -41,6 +41,7 @@ RUN apt-get update -qq && \
 FROM yosys AS symbiyosys
 
 COPY packages/suprove /root/suprove
+COPY packages/avy.patch /root/avy.patch
 
 RUN apt-get update -qq && \
     DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
@@ -53,6 +54,7 @@ RUN apt-get update -qq && \
     python-setuptools \
     python-pip \
     python-wheel \
+    libboost-program-options-dev \
     mercurial && \
     apt-get autoclean && apt-get clean && apt-get -y autoremove && \
     rm -rf /var/lib/apt/lists/* && \
@@ -113,5 +115,16 @@ RUN apt-get update -qq && \
     ninja package && \
     tar -C /opt -xzf super_prove*.tar.gz && \
     mv /root/suprove /opt/super_prove/bin/ && \
-    chmod +x /opt/super_prove/bin/suprove && \
+    chmod +x /opt/super_prove/bin/suprove
+
+RUN cd /root && \
+    git clone https://bitbucket.org/arieg/extavy.git && \
+    cd extavy && \
+    git checkout new_quip && \
+    git submodule update --init && \
+    mkdir build; cd build && \
+    cmake -DCMAKE_BUILD_TYPE=Debug .. && \
+    make -j$(nproc) && \
+    mkdir -p /opt/avy/bin && \
+    cp -r avy/src/av* /opt/avy/bin/ && \
     rm -rf /root/*