Add patch file to get ExtAvy compiled

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"

packages/avy.patch

@@ -0,0 +1,36 @@
+diff --git a/src/ItpGlucose.h b/src/ItpGlucose.h
+index 657253d..66a0cd4 100644
+--- a/src/ItpGlucose.h
++++ b/src/ItpGlucose.h
+@@ -126,7 +126,7 @@ namespace avy
+     ::Glucose::Solver* get () { return m_pSat; }
+     
+     /// true if the context is decided 
+-    bool isSolved () { return m_Trivial || m_State || !m_State; }
++    bool isSolved () { return bool{m_Trivial || m_State || !m_State}; }
+ 
+     int core (int **out)
+     {
+@@ -182,7 +182,8 @@ namespace avy
+     bool getVarVal(int v)
+     {
+         ::Glucose::Var x = v;
+-        return tobool (m_pSat->modelValue(x));
++        boost::logic::tribool y = tobool (m_pSat->modelValue(x));
++        return bool{y};
+     }
+   };
+   
+diff --git a/src/ItpMinisat.h b/src/ItpMinisat.h
+index d145d7c..7514f31 100644
+--- a/src/ItpMinisat.h
++++ b/src/ItpMinisat.h
+@@ -124,7 +124,7 @@ namespace avy
+     ::Minisat::Solver* get () { return m_pSat.get (); }
+     
+     /// true if the context is decided 
+-    bool isSolved () { return m_Trivial || m_State || !m_State; }
++    bool isSolved () { return bool{m_Trivial || m_State || !m_State}; }
+ 
+     int core (int **out)
+     {

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/*