add 'cvc4' workflow and dockerfile

Author: tmeissner

.github/workflows/cvc4.yml

@@ -0,0 +1,57 @@
+# Authors:
+#   Unai Martinez-Corral
+#   Torsten Meissner
+#
+# Copyright 2020-2021 Unai Martinez-Corral <[email protected]>
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier: Apache-2.0
+
+name: 'cvc4'
+
+on:
+  pull_request:
+  push:
+  schedule:
+    - cron: '0 0 * * 5'
+  workflow_dispatch:
+  repository_dispatch:
+    types: [ cvc4 ]
+
+env:
+  DOCKER_BUILDKIT: 1
+
+jobs:
+
+  cvc4:
+    runs-on: ubuntu-latest
+    steps:
+
+    - uses: actions/checkout@v2
+
+    - run: echo "$(pwd)/.github/bin" >> $GITHUB_PATH
+
+    - run: dockerBuild pkg:cvc4 cvc4
+
+    - run: dockerTestPkg cvc4
+
+    - name: Login to DockerHub
+      if: github.event_name != 'pull_request' && github.repository == 'hdl/containers'
+      uses: docker/login-action@v1
+      with:
+        username: ${{ secrets.DOCKER_USER }}
+        password: ${{ secrets.DOCKER_PASS }}
+
+    - run: dockerPush pkg:cvc4
+      if: github.event_name != 'pull_request' && github.repository == 'hdl/containers'

cvc4.dockerfile

@@ -0,0 +1,46 @@
+# Authors:
+#   Unai Martinez-Corral
+#   Torsten Meissner
+#
+# Copyright 2021 Unai Martinez-Corral <[email protected]>
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier: Apache-2.0
+
+FROM hdlc/build:build AS build
+
+RUN mkdir /usr/share/man/man1 \
+ && apt-get update -qq \
+ && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
+    cmake \
+    openjdk-11-jre-headless \
+    libgmp-dev \
+    python3-toml \
+ && apt-get autoclean && apt-get clean && apt-get -y autoremove \
+ && update-ca-certificates  \
+ && rm -rf /var/lib/apt/lists/*
+
+RUN mkdir /tmp/cvc4 && cd /tmp/cvc4 \
+&& curl -fsSL https://codeload.github.com/CVC4/CVC4/tar.gz/master | tar xzf - --strip-components=1 \
+&& ./contrib/get-antlr-3.4 \
+&& ./contrib/get-cadical \
+&& ./configure.sh --cadical \
+&& cd build \
+&& make -j$(nproc) \
+&& make DESTDIR=/opt/cvc4 install
+
+#---
+
+FROM scratch
+COPY --from=build /opt/cvc4 /cvc4

doc/index.adoc

@@ -35,7 +35,6 @@ To Do:
 
 * https://github.com/khoapham/bitman[BitMan]
 * https://hdl.github.io/awesome/items/cocotb[cocotb]
-* https://github.com/CVC4/CVC4[CVC4]
 * https://hdl.github.io/awesome/items/ecpprog[ecpprog]
 * https://hdl.github.io/awesome/items/fujprog[fujprog]
 * https://hdl.github.io/awesome/items/iverilog[iverilog]
@@ -121,6 +120,12 @@ include::shield_gha.adoc[]
 * {blank}
 +
 --
+:workflow: cvc4
+include::shield_gha.adoc[]
+--
+* {blank}
++
+--
 :workflow: superprove
 include::shield_gha.adoc[]
 --

doc/tools.yml

@@ -27,6 +27,16 @@ boolector:
 
 #---
 
+cvc4:
+  url: 'https://hdl.github.io/awesome/items/cvc4'
+  pkg:
+    - 'cvc4'
+  in:
+    - 'formal'
+    - 'formal:all'
+
+#---
+
 ghdl:
   url: 'https://hdl.github.io/awesome/items/ghdl'
   pkg:

formal.dockerfile

@@ -35,6 +35,7 @@ FROM min AS latest
 
 COPY --from=hdlc/pkg:yices2 /yices2 /
 COPY --from=hdlc/pkg:boolector /boolector /
+COPY --from=hdlc/pkg:cvc4 /cvc4 /
 
 #---
 

graph/graph.dot

@@ -27,6 +27,7 @@ digraph G {
   { node [shape=note, color=dodgerblue, fontcolor=dodgerblue]
     d_base             [label="base"];
     d_boolector        [label="boolector"];
+    d_cvc4             [label="cvc4"];
     d_formal           [label="formal"];
     d_ghdl             [label="ghdl"];
     d_ghdlYosysPlugin  [label="ghdl-yosys-plugin"];
@@ -63,6 +64,7 @@ digraph G {
     }
     { node [color=mediumblue, fontcolor=mediumblue]
       "pkg:boolector"
+      "pkg:cvc4"
       "pkg:ghdl"
       "pkg:ghdl-yosys-plugin"
       "pkg:gtkwave"
@@ -342,6 +344,20 @@ digraph G {
     "pkg:boolector" -> "t_pkg:boolector";
   }
 
+  subgraph cluster_cvc4 {
+    { rank=same
+      node [shape=cylinder, color=grey, fontcolor=grey]
+      "p_cvc4_scratch" [label="scratch"]
+      "p_cvc4_build:build" [label="build:build"]
+    }
+
+    d_cvc4 -> "pkg:cvc4" [style=dotted];
+
+    "t_pkg:cvc4" [shape=folder, color=red, fontcolor=red, label="cvc4.pkg"];
+
+    "pkg:cvc4" -> "t_pkg:cvc4";
+  }
+
   subgraph cluster_superprove {
     { rank=same
       node [shape=cylinder, color=grey, fontcolor=grey]
@@ -388,6 +404,7 @@ digraph G {
     { rank=same
       node [shape=cylinder, color=grey, fontcolor=grey]
       "p_formal_boolector" [label="pkg:boolector"]
+      "p_formal_cvc4" [label="pkg:cvc4"]
       "p_formal_ghdl" [label="ghdl:yosys"]
       "p_formal_symbiyosys" [label="pkg:symbiyosys"]
       "p_formal_superprove" [label="pkg:superprove"]
@@ -429,6 +446,7 @@ digraph G {
 
   { rank=same
     d_boolector
+    d_cvc4
     d_superprove
     d_symbiyosys
     d_yices2
@@ -442,9 +460,13 @@ digraph G {
   "build:build" -> "p_boolector_build:build" -> d_boolector;
   "scratch" -> "p_boolector_scratch" -> d_boolector;
 
+  "build:build" -> "p_cvc4_build:build" -> d_cvc4;
+  "scratch" -> "p_cvc4_scratch" -> d_cvc4;
+
   "ghdl:yosys" -> "p_formal_ghdl" -> d_formal;
   "pkg:symbiyosys" -> "p_formal_symbiyosys" -> d_formal;
   "pkg:boolector" -> "p_formal_boolector" -> d_formal;
+  "pkg:cvc4" -> "p_formal_cvc4" -> d_formal;
   "pkg:yices2" -> "p_formal_yices2" -> d_formal;
   "pkg:superprove" -> "p_formal_superprove" -> d_formal;
   "pkg:z3" -> "p_formal_z3" -> d_formal;
@@ -505,6 +527,8 @@ digraph G {
 
     "p_boolector_scratch" -> "pkg:boolector";
 
+    "p_cvc4_scratch" -> "pkg:cvc4";
+
     "p_ghdl_scratch" -> "pkg:ghdl";
     "p_ghdl_build:base" -> "ghdl";
 
@@ -553,6 +577,7 @@ digraph G {
 
     {
       "p_formal_boolector",
+      "p_formal_cvc4",
       "p_formal_yices2"
     } -> "formal";
 

test/cvc4.pkg.sh

@@ -0,0 +1,28 @@
+#!/bin/sh
+
+# Authors:
+#   Unai Martinez-Corral
+#
+# Copyright 2020-2021 Unai Martinez-Corral <[email protected]>
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier: Apache-2.0
+
+set -e
+
+cd $(dirname "$0")
+
+./_tree.sh
+
+./_todo.sh