Include cadical in some CI workflows

zhassan-aws · zhassan-aws · commit b1fb76906e69 · 2023-02-09T17:04:55.000-08:00
diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
@@ -92,7 +92,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
-          make -C src minisat2-download
+          make -C src minisat2-download cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
@@ -118,7 +118,7 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build with make
         run: |
-          make -C src       -j2
+          make -C src       -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
           make -C unit      -j2
           make -C jbmc/src  -j2
           make -C jbmc/unit -j2
@@ -223,7 +223,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
       - name: Check that doc task works
         run: ninja -C build doc
       - name: Zero ccache stats and limit in size
@@ -260,7 +260,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
-          make -C src minisat2-download
+          make -C src minisat2-download cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
@@ -290,7 +290,7 @@ jobs:
           make -C src/cpp library_check
       - name: Build with make
         run: |
-          make -C src       -j2
+          make -C src       -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
           make -C unit      -j2
           make -C jbmc/src  -j2
           make -C jbmc/unit -j2
@@ -348,7 +348,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
       - name: Check that doc task works
         run: ninja -C build doc
       - name: Zero ccache stats and limit in size
@@ -439,7 +439,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+        run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
@@ -482,8 +482,8 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build using Make
         run: |
-          make -C src minisat2-download
-          make -C src -j3 CXX="ccache clang++"
+          make -C src minisat2-download cadical-download
+          make -C src -j3 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
           make -C jbmc/src -j3 CXX="ccache clang++"
           make -C unit "CXX=ccache clang++"
           make -C jbmc/unit "CXX=ccache clang++"
diff --git a/.gitignore b/.gitignore
@@ -74,6 +74,7 @@ jbmc/regression/**/tests-symex-driven-loading.log
 
 # libs downloaded by make [name]-download
 minisat*/
+cadical*/
 glucose-syrup/
 
 # flex/bison generated files
diff --git a/Dockerfile b/Dockerfile
@@ -10,6 +10,7 @@ RUN echo 'tzdata tzdata/Areas select Etc' | debconf-set-selections; \
     echo 'tzdata tzdata/Zones/Etc select UTC' | debconf-set-selections; \
     apt-get update && apt-get upgrade -y && apt-get install --no-install-recommends -y \
     cmake \
+    make \
     ninja-build \
     gcc \
     g++ \
diff --git a/scripts/cadical-1.4.1-patch b/scripts/cadical-1.4.1-patch
@@ -0,0 +1,34 @@
+diff --git a/scripts/make-build-header.sh b/scripts/make-build-header.sh
+index e8f6746..1290024 100755
+--- a/scripts/make-build-header.sh
++++ b/scripts/make-build-header.sh
+@@ -20,7 +20,7 @@ warning () {
+ 
+ #--------------------------------------------------------------------------#
+ 
+-[ ! -f VERSION -a ! -f ../VERSION ] && \
++[ ! -f VERSION.txt -a ! -f ../VERSION.txt ] && \
+ die "needs to be called from build sub-directory"
+ 
+ [ -f makefile ] || \
+@@ -29,7 +29,7 @@ warning "could not find 'makefile'"
+ #--------------------------------------------------------------------------#
+ # The version.
+ #
+-VERSION="`cat ../VERSION`"
++VERSION="`cat ../VERSION.txt`"
+ if [ x"$VERSION" = x ]
+ then
+   warning "could not determine 'VERSION'"
+diff --git a/src/lookahead.cpp b/src/lookahead.cpp
+index 9e8a16b..3d5721a 100644
+--- a/src/lookahead.cpp
++++ b/src/lookahead.cpp
+@@ -390,6 +390,7 @@ int Internal::lookahead_probing() {
+ CubesWithStatus Internal::generate_cubes(int depth, int min_depth) {
+   if (!active() || depth == 0) {
+     CubesWithStatus cubes;
++    cubes.status = 0;
+     cubes.cubes.push_back(std::vector<int>());
+     return cubes;
+   }
diff --git a/scripts/cadical_CMakeLists.txt b/scripts/cadical_CMakeLists.txt
@@ -0,0 +1,27 @@
+file(GLOB sources "src/*.cpp" "src/*.hpp" "src/*.h")
+# Remove "app" sources from list
+list(REMOVE_ITEM sources
+    "${CMAKE_CURRENT_SOURCE_DIR}/src/cadical.cpp"
+    "${CMAKE_CURRENT_SOURCE_DIR}/src/mobical.cpp"
+)
+
+add_library(cadical ${sources})
+
+# Pass -DNBUILD to disable including the version information, which is not
+# needed since cbmc doesn't run the cadical binary
+target_compile_options(cadical PUBLIC -DNBUILD)
+
+set_target_properties(
+    cadical
+    PROPERTIES
+    CXX_STANDARD 11
+    CXX_STANDARD_REQUIRED true
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+)
+
+target_include_directories(cadical
+    PUBLIC
+    ${CMAKE_CURRENT_SOURCE_DIR}/src
+)
+
+target_link_libraries(cadical util)
diff --git a/src/Makefile b/src/Makefile
@@ -177,7 +177,11 @@ cadical-download:
 	@$(TAR) xfz $(cadical_release).tar.gz
 	@rm -Rf ../cadical
 	@mv cadical-$(cadical_release) ../cadical
-	@cd ../cadical && CXX=$(CXX) ./configure -O3 -s && make -j
+	@(cd ../cadical; patch -p1 < ../scripts/cadical-1.4.1-patch)
+	@(cd ../cadical && ./configure)
+  # Need to rename VERSION so that it isn't picked up by `#include<version>` on
+  # macOS which is case insensitive
+	@(cd ../cadical && mv VERSION VERSION.txt)
 	@$(RM) $(cadical_release).tar.gz
 
 doc :
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -66,6 +66,7 @@ ifneq ($(CADICAL),)
   CADICAL_INCLUDE=-I $(CADICAL)/src
   CADICAL_LIB=$(CADICAL)/build/libcadical$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_CADICAL
+  CLEANFILES += $(CADICAL_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(CADICAL_LIB))
 endif
 
 SRC = $(BOOLEFORCE_SRC) \
@@ -275,6 +276,9 @@ endif
 solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
 	$(LINKLIB)
 
+../../cadical/build/libcadical$(LIBEXT):
+	$(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS)"
+
 -include smt2/smt2_solver$(DEPEXT)
 
 smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \
