Include super_prove in SymbiYosys Image

ghdl-formal.Dockerfile

@@ -48,7 +48,8 @@ RUN apt-get update -qq && \
     libc6-dev \
     zlib1g-dev \
     make \
-    python3 && \
+    python3 \
+    libpython2.7 && \
     apt-get -y upgrade && apt-get autoclean && apt-get clean && apt-get -y autoremove && \
     update-ca-certificates && \
     rm -rf /var/lib/apt/lists/*
@@ -57,4 +58,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:$PATH"
+ENV PATH "/opt/ghdl/bin:/opt/symbiyosys/bin:/opt/yosys/bin:/opt/z3/bin:/opt/yices2/bin:/opt/cvc4/bin:/opt/boolector/bin:/opt/super_prove/bin:$PATH"

packages/fix_super_prove_build.txt

@@ -0,0 +1,25 @@
+diff -r bde167bca3cd Bip/Main_bip.cc
+--- a/Bip/Main_bip.cc	Thu Sep 14 01:44:08 2017 -0700
++++ b/Bip/Main_bip.cc	Thu Aug 08 15:02:00 2019 +0200
+@@ -508,8 +508,8 @@
+ void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis)
+ {
+     Vec<Pair<int,GLit> > ffs, pis;
+-    For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w));
+-    For_Gatetype(N, gate_PI  , w) pis.push(tuple(attr_PI  (w).number, w));
++    For_Gatetype(N, gate_Flop, w) ffs.push(::tuple(attr_Flop(w).number, w));
++    For_Gatetype(N, gate_PI  , w) pis.push(::tuple(attr_PI  (w).number, w));
+     sort(ffs);
+     sort(pis);
+
+diff -r bde167bca3cd MetaSat/MiniSat2/System.cc
+--- a/MetaSat/MiniSat2/System.cc	Thu Sep 14 01:44:08 2017 -0700
++++ b/MetaSat/MiniSat2/System.cc	Thu Aug 08 15:02:00 2019 +0200
+@@ -20,6 +20,7 @@
+
+ #include <signal.h>
+ #include <stdio.h>
++#include <stdlib.h>
+
+ #include "System.hh"
+

packages/suprove

@@ -0,0 +1,3 @@
+#!/bin/bash
+tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
+exec /opt/super_prove/bin/${tool}.sh "$@"

symbiyosys.Dockerfile

@@ -37,13 +37,21 @@ RUN apt-get update -qq && \
 
 FROM yosys AS symbiyosys
 
+COPY packages/suprove /root/suprove
+COPY packages/fix_super_prove_build.txt /root/fix_super_prove_build.txt
+
 RUN apt-get update -qq && \
     DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
     autoconf \
     gperf  \
     cmake \
     curl \
-    libgmp-dev && \
+    libgmp-dev \
+    ninja-build \
+    g++ \
+    python-setuptools \
+    python-pip \
+    mercurial && \
     apt-get autoclean && apt-get clean && apt-get -y autoremove && \
     rm -rf /var/lib/apt/lists/* && \
     cd /root && \
@@ -80,4 +88,18 @@ RUN apt-get update -qq && \
     mkdir /opt/boolector/bin && \
     cp build/bin/boolector /opt/boolector/bin/ && \
     cp build/bin/btor* /opt/boolector/bin/ && \
-    cp deps/btor2tools/bin/btorsim /opt/boolector/bin/
+    cp deps/btor2tools/bin/btorsim /opt/boolector/bin/ && \
+    cd /root && \
+    git clone --recursive https://github.com/sterin/super-prove-build && \
+    cd super-prove-build/abc-zz && \
+    patch -p1 < /root/fix_super_prove_build.txt && \
+    cd .. && \
+    mkdir build && \
+    cd build && \
+    cmake -DCMAKE_BUILD_TYPE=Release -G Ninja .. && \
+    ninja && \
+    ninja package && \
+    tar -C /opt -xzf super_prove*.tar.gz && \
+    mv /root/suprove /opt/super_prove/bin/ && \
+    chmod +x /opt/super_prove/bin/suprove && \
+    rm -rf /root/*