Fixing up synthesis framework

.github/workflows/build.yml

@@ -3,6 +3,8 @@ name: build
 on:
   pull_request:
     branches: [ "*" ]
+  push:
+    branches: [ "master" ]
 
 jobs:
   build:
@@ -71,7 +73,7 @@ jobs:
 
     - name: Install dependencies for Linux
       if: contains(matrix.os, 'ubuntu')
-      run: sudo apt-get update && sudo apt-get install -yq help2man libgmp-dev libmpfr-dev
+      run: sudo apt-get update && sudo apt-get install -yq help2man libgmp-dev libmpfr-dev perl
 
     - name: Checkout Cadical
       uses: actions/checkout@v4
@@ -115,7 +117,7 @@ jobs:
       uses: actions/checkout@v4
       with:
         repository: msoos/cryptominisat
-        ref: master
+        ref: working-on-synth
         path: cryptominisat
         submodules: 'true'
     - name: Build CMS
@@ -207,6 +209,21 @@ jobs:
         sudo make install
         cd ../..
 
+    - name: Checkout EvalMaxSAT
+      uses: actions/checkout@v4
+      with:
+        repository: meelgroup/EvalMaxSAT
+        ref: master
+        path: EvalMaxSAT
+    - name: Build EvalMaxSAT
+      run: |
+        cd EvalMaxSAT
+        mkdir build
+        cd build
+        cmake -DCMAKE_BUILD_TYPE=${{ matrix.build_type }} -DSTATICCOMPILE=${{ matrix.staticcompile }} ..
+        cmake --build . --config ${{matrix.build_type}} -v
+        cd ../..
+
     - uses: actions/checkout@v4
       with:
         path: project
@@ -233,6 +250,12 @@ jobs:
         ./project/build/arjun --help
         echo $?
 
+    - name: Check licenses
+      if: contains(matrix.os, 'ubuntu')
+      run: |
+        echo "Checking licenses"
+        cd ../scripts/license_check
+        ./check_all_licenses.sh
 
     - name: Upload Artifact - Linux
       if: contains(matrix.os, 'ubuntu') && matrix.staticcompile == 'ON' && !contains(matrix.os, 'arm')
@@ -241,6 +264,7 @@ jobs:
         name: arjun-linux-amd64
         path: |
           project/build/arjun
+          project/build/test-synth
           project/build/lib/*
           project/build/include/*
 
@@ -251,16 +275,18 @@ jobs:
         name: arjun-linux-arm64
         path: |
           project/build/arjun
+          project/build/test-synth
           project/build/lib/*
           project/build/include/*
 
     - name: Upload Artifact - Mac arm
-      if: matrix.os == 'macos-14' && matrix.staticcompile == 'ON'
+      if: matrix.os == 'macos-15' && matrix.staticcompile == 'ON'
       uses: actions/upload-artifact@v4
       with:
         name: arjun-mac-arm64
         path: |
           project/build/arjun
+          project/build/test-synth
           project/build/lib/*
           project/build/include/*
 
@@ -271,5 +297,6 @@ jobs:
         name: arjun-mac-x86_64
         path: |
           project/build/arjun
+          project/build/test-synth
           project/build/lib/*
           project/build/include/*

.github/workflows/nix.yml

@@ -3,6 +3,8 @@ name: nix build
 on:
   pull_request:
     branches: [ "*" ]
+  push:
+    branches: [ "master" ]
 
 jobs:
   tests:

.gitignore

@@ -9,3 +9,6 @@ neovide_backtraces.log
 /.ccls-cache
 CLAUDE.md
 .claude
+perf*
+output
+out/

.vimsettings.vim

@@ -0,0 +1,7 @@
+autocmd Filetype h setlocal tabstop=2 shiftwidth=2 softtabstop=2
+autocmd Filetype hpp setlocal tabstop=2 shiftwidth=2 softtabstop=2
+autocmd Filetype c setlocal tabstop=2 shiftwidth=2 softtabstop=2
+autocmd Filetype cpp setlocal tabstop=2 shiftwidth=2 softtabstop=2
+set shiftwidth=4
+setlocal shiftwidth=4
+nnoremap cc :e %:p:s,.h$,.X123X,:s,.cpp$,.h,:s,.X123X$,.cpp,<CR>

CMakeLists.txt

@@ -77,7 +77,8 @@ endforeach()
 project (arjun)
 set(CMAKE_CXX_EXTENSIONS OFF)
 set(CMAKE_C_STANDARD 99)
-set(CMAKE_CXX_STANDARD 20)
+set(CMAKE_CXX_STANDARD 23)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_POSITION_INDEPENDENT_CODE ON)
 enable_language( CXX )
 enable_language( C )
@@ -122,6 +123,7 @@ if (SYNTH)
         PATHS ${CMAKE_CURRENT_SOURCE_DIR}/../cadical/build/
         NAMES cadical
         REQUIRED)
+    find_package(EvalMaxSAT REQUIRED)
 endif()
 
 macro(add_sanitize_option flagname)
@@ -193,13 +195,13 @@ endif()
 if (NOT MSVC)
     add_compile_options( -g)
 
-    add_compile_options("$<$<CONFIG:RelWithDebInfo>:-O3>")
-
+    add_compile_options("$<$<CONFIG:RelWithDebInfo>:-O2>")
     add_compile_options("$<$<CONFIG:Release>:-O3>")
     add_compile_options("$<$<CONFIG:Release>:-g0>")
     add_compile_options("$<$<CONFIG:Release>:-DNDEBUG>")
 
-    add_compile_options("$<$<CONFIG:DEBUG>:-O0>")
+    add_compile_options("$<$<CONFIG:Debug>:-O0>")
+    add_compile_options("$<$<CONFIG:Debug>:-D_GLIBCXX_ASSERTIONS>")
 
 else()
     # see https://msdn.microsoft.com/en-us/library/fwkeyyhe.aspx for details
@@ -214,7 +216,7 @@ else()
     add_compile_options("$<$<CONFIG:Release>:/NDEBUG>")
     add_compile_options("$<$<CONFIG:Release>:/ZI>")
 
-    add_compile_options("$<$<CONFIG:DEBUG>:/Od>")
+    add_compile_options("$<$<CONFIG:Debug>:/Od>")
 
     if (STATICCOMPILE)
         # We statically link to reduce dependencies
@@ -280,6 +282,8 @@ if (NOT WIN32)
     add_cxx_flag_if_supported("-msse4.2")
     add_cxx_flag_if_supported("-mpopcnt")
     add_cxx_flag_if_supported("-mpclmul")
+    add_cxx_flag_if_supported("-ggdb3")
+    add_cxx_flag_if_supported("-fno-omit-frame-pointer") # it's useful to have frame pointers for profiling, even in release builds
     if (CMAKE_BUILD_TYPE STREQUAL "Release")
         # add_cxx_flag_if_supported("-flto")
         # add_link_flag_if_supported("-flto")
@@ -288,9 +292,6 @@ if (NOT WIN32)
         add_cxx_flag_if_supported("-Wextra")
         add_cxx_flag_if_supported("-Wunused")
         add_cxx_flag_if_supported("-Wsign-compare")
-        add_cxx_flag_if_supported("-fno-omit-frame-pointer")
-        add_cxx_flag_if_supported("-g")
-        add_cxx_flag_if_supported("-ggdb3")
         add_cxx_flag_if_supported("-Wtype-limits")
         add_cxx_flag_if_supported("-Wuninitialized")
         add_cxx_flag_if_supported("-Wno-deprecated")

cmake/FindGMP.cmake

@@ -1,4 +1,4 @@
-include(FindPkgConfig)
+find_package(PkgConfig)
 pkg_check_modules(PC_GMP "gmp")
 
 set(GMP_DEFINITIONS ${PC_GMP_CFLAGS_OTHER})

cmake/FindMLPACK.cmake

@@ -1,4 +1,4 @@
-include(FindPkgConfig)
+find_package(PkgConfig)
 pkg_check_modules(PC_MLPACK "mlpack")
 
 set(MLPACK_DEFINITIONS ${PC_MLPACK_CFLAGS_OTHER})

flake.nix

@@ -11,13 +11,17 @@
       inputs.nixpkgs.follows = "nixpkgs";
     };
     cryptominisat = {
-      url = "github:msoos/cryptominisat/master";
+      url = "github:msoos/cryptominisat/working-on-synth";
       inputs.nixpkgs.follows = "nixpkgs";
     };
     sbva = {
       url = "github:meelgroup/sbva/master";
       inputs.nixpkgs.follows = "nixpkgs";
     };
+    evalmaxsat = {
+      url = "github:meelgroup/EvalMaxSAT/master";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
   };
   outputs =
     {
@@ -27,6 +31,7 @@
       cadiback,
       cryptominisat,
       sbva,
+      evalmaxsat,
     }:
     let
       inherit (nixpkgs) lib;
@@ -85,6 +90,7 @@
           fetchFromGitHub,
           cmake,
           sbva,
+          evalmaxsat,
           zlib,
           gmp,
           mpfr,
@@ -115,6 +121,7 @@
           buildInputs = [
             zlib
             sbva
+            evalmaxsat
             gmp
             mpfr
             cadiback
@@ -140,6 +147,7 @@
             cadiback = cadiback.packages.${system}.cadiback;
             cryptominisat5 = cryptominisat.packages.${system}.cryptominisat5;
             sbva = sbva.packages.${system}.sbva;
+            evalmaxsat = evalmaxsat.packages.${system}.evalmaxsat;
           };
         in
         {