Development happens here

.clang-tidy

@@ -31,7 +31,7 @@ Checks: >
   performance-unnecessary-copy-initialization,
   readability-const-return-type,
   readability-container-size-empty,
-  readability-convert-member-functions-to-static,
+  -readability-convert-member-functions-to-static,
   readability-else-after-return,
   readability-identifier-naming,
   readability-make-member-function-const,
@@ -40,7 +40,7 @@ Checks: >
   readability-redundant-member-init,
   readability-redundant-smartptr-get,
   readability-redundant-string-cstr,
-  readability-simplify-boolean-expr
+  -readability-simplify-boolean-expr
 
 CheckOptions:
 - key: bugprone-assert-side-effect.AssertMacros
@@ -74,6 +74,10 @@ CheckOptions:
   value: 'CamelCase'
 - key: readability-identifier-naming.VariableCase
   value: 'lower_case'
+- key: readability-identifier-naming.ConstexprVariableCase
+  value: 'UPPER_CASE'
+- key: readability-identifier-naming.GlobalConstantCase
+  value: 'UPPER_CASE'
 
 HeaderFilterRegex: '^./src/.*'
 

.github/workflows/release.yml

@@ -13,15 +13,33 @@ jobs:
       fail-fast: true
 
       matrix:
-        os: [ubuntu-latest, ubuntu-24.04-arm, macos-15, macos-15-intel]
+        os: [ubuntu-latest, ubuntu-24.04-arm, macos-15, macos-15-intel, windows-latest]
         build_type: [Release]
 
     steps:
+    - name: Set up MSYS2
+      if: contains(matrix.os, 'windows')
+      uses: msys2/setup-msys2@v2
+      with:
+        msystem: MINGW64
+        update: true
+        install: >-
+          mingw-w64-x86_64-gcc
+          mingw-w64-x86_64-cmake
+          mingw-w64-x86_64-ninja
+          mingw-w64-x86_64-gmp
+          mingw-w64-x86_64-mpfr
+          mingw-w64-x86_64-zlib
+          mingw-w64-x86_64-pkgconf
+          make
+
     - uses: actions/setup-python@v5
+      if: "!contains(matrix.os, 'windows')"
       with:
         python-version: '3.10'
 
     - name: Install python dependencies
+      if: "!contains(matrix.os, 'windows')"
       run: |
         pip install numpy lit
 
@@ -63,12 +81,14 @@ jobs:
       run: sudo apt-get update && sudo apt-get install -yq help2man libgmp-dev libmpfr-dev perl
 
     - name: Setup ccache
+      if: "!contains(matrix.os, 'windows')"
       uses: hendrikmuhs/ccache-action@v1
       with:
         key: release-${{ matrix.os }}-${{ matrix.build_type }}
         max-size: 500M
 
     - name: Checkout & build cereal
+      if: "!contains(matrix.os, 'windows')"
       run: |
         wget https://github.com/USCiLab/cereal/archive/v1.3.2.tar.gz
         tar xvf v1.3.2.tar.gz
@@ -86,6 +106,7 @@ jobs:
         cd ..
 
     - name: Checkout armadillo static
+      if: "!contains(matrix.os, 'windows')"
       run: |
         wget https://sourceforge.net/projects/arma/files/armadillo-14.0.2.tar.xz
         tar xvf armadillo-14.0.2.tar.xz
@@ -97,6 +118,7 @@ jobs:
         cd ../..
 
     - name: Checkout & build ensmallen
+      if: "!contains(matrix.os, 'windows')"
       run: |
         wget https://github.com/mlpack/ensmallen/archive/refs/tags/2.22.2.tar.gz
         tar xvf 2.22.2.tar.gz
@@ -109,12 +131,14 @@ jobs:
         cd ../..
 
     - name: Checkout mlpack
+      if: "!contains(matrix.os, 'windows')"
       uses: actions/checkout@v4
       with:
         repository: mlpack/mlpack
         ref: 4.6.2
         path: mlpack
     - name: Build mlpack
+      if: "!contains(matrix.os, 'windows')"
       run: |
         cd mlpack
         mkdir build
@@ -128,7 +152,8 @@ jobs:
       with:
         path: project
         submodules: 'true'
-    - name: Build project
+    - name: Build project (non-Windows)
+      if: "!contains(matrix.os, 'windows')"
       run: |
         cd project
         mkdir -p build && cd build
@@ -141,10 +166,26 @@ jobs:
         -S ..
         cmake --build . --config ${{matrix.build_type}} -v
 
+    - name: Build project (Windows)
+      if: contains(matrix.os, 'windows')
+      shell: msys2 {0}
+      run: |
+        cd project
+        mkdir -p build && cd build
+        cmake \
+        -DCMAKE_BUILD_TYPE=${{ matrix.build_type }} \
+        -DBUILD_SHARED_LIBS=OFF \
+        -DEXTRA_SYNTH=OFF \
+        -G Ninja \
+        -S ..
+        cmake --build . --config ${{matrix.build_type}} -v
+
     - name: Test
+      if: "!contains(matrix.os, 'windows')"
       run: ctest -C ${{matrix.build_type}} --verbose
 
-    - name: run it to check it executes
+    - name: run it to check it executes (non-Windows)
+      if: "!contains(matrix.os, 'windows')"
       run: |
         echo "Running version command"
         ./project/build/arjun --version
@@ -153,6 +194,18 @@ jobs:
         ./project/build/arjun --help
         echo $?
 
+    - name: run it to check it executes (Windows)
+      if: contains(matrix.os, 'windows')
+      shell: msys2 {0}
+      run: |
+        EXE=./project/build/arjun.exe
+        echo "Running: $EXE --version"
+        $EXE --version
+        echo $?
+        echo "Running: $EXE --help"
+        $EXE --help
+        echo $?
+
     - name: Determine artifact name
       id: artifact
       shell: bash
@@ -166,9 +219,12 @@ jobs:
           echo "name=arjun-mac-arm64" >> "$GITHUB_OUTPUT"
         elif [[ "$OS" == "macos-15-intel" ]]; then
           echo "name=arjun-mac-x86_64" >> "$GITHUB_OUTPUT"
+        elif [[ "$OS" == "windows-latest" ]]; then
+          echo "name=arjun-windows-x86_64" >> "$GITHUB_OUTPUT"
         fi
 
-    - name: Package artifact
+    - name: Package artifact (non-Windows)
+      if: "!contains(matrix.os, 'windows')"
       run: |
         mkdir -p dist
         cp project/build/arjun dist/
@@ -177,6 +233,17 @@ jobs:
         cp -r project/build/include dist/ 2>/dev/null || true
         tar czf ${{ steps.artifact.outputs.name }}.tar.gz -C dist .
 
+    - name: Package artifact (Windows)
+      if: contains(matrix.os, 'windows')
+      shell: msys2 {0}
+      run: |
+        mkdir -p dist
+        cp project/build/arjun.exe dist/
+        cp project/build/test-synth.exe dist/ 2>/dev/null || true
+        cp -r project/build/lib dist/ 2>/dev/null || true
+        cp -r project/build/include dist/ 2>/dev/null || true
+        tar czf ${{ steps.artifact.outputs.name }}.tar.gz -C dist .
+
     - name: Upload artifact for release job
       uses: actions/upload-artifact@v4
       with:

.gitignore

@@ -7,7 +7,6 @@ examples
 neovide_backtraces.log
 /result
 /.ccls-cache
-CLAUDE.md
 .claude
 perf*
 output
@@ -17,3 +16,4 @@ html/*.css
 html/*.wasm
 html/*.ts
 
+/scripts/data/__pycache__

CLAUDE.md

@@ -0,0 +1,144 @@
+# Arjun
+
+Minimal-independent-set calculator and CNF minimizer. Preprocessor for
+[GANAK](https://github.com/meelgroup/ganak) and
+[ApproxMC](https://github.com/meelgroup/ApproxMC). Also performs
+Boolean-function **synthesis** (Manthan-style counterexample-guided repair)
+for defining relationships between variables.
+
+## Building
+
+ALWAYS build with `make -j12` from `build/` — otherwise it's slow.
+
+```
+cd build && ./build_norm.sh
+```
+
+Dependencies (cadical, cryptominisat, sbva, treedecomp) are typically sibling
+checkouts under `../` and are pointed at via the cmake configuration already
+present in `build/`. If cmake needs to be re-run, use `scripts/build_norm.sh`
+or `scripts/build_release.sh`.
+
+## Running
+
+From `build/`:
+
+```
+./arjun --verb 2 --synth --synthbve 1 --extend 1 --minimize 1 --debugsynth --samples 1 out/fuzzTest_596.cnf
+```
+
+Useful top-level flags:
+- `--synth` — enable synthesis (Manthan)
+- `--debugsynth` — emit intermediate AIGs (`*-simplified_cnf.aig`,
+  `*-autarky.aig`, `*-manthan.aig`, `*-final.aig`) for debugging
+- `--verb N` — verbosity (0–2)
+
+## Quick A/B benchmarking: `scripts/run_elim_bench.sh`
+
+One-line sanity bench for comparing simplification tweaks. Runs `arjun` on a
+CNF and prints a single line with the headline counts (vars, indep, optind,
+bin cls, long cls, lits, time).
+
+Run from `build/` (where `arjun` and `count_literals.py` live):
+
+```
+../scripts/run_elim_bench.sh <cnf[.gz]> [extra arjun args...]
+```
+
+Extra args are forwarded to `arjun`. The simplified CNF is written to
+`/tmp/arjun_elim_out` and the full log to `/tmp/arjun_elim.log`. Typical
+workflow: run it on the same CNF before and after a change and diff the
+output lines.
+
+## After every build ALWAYS run the fuzzers
+
+From `build/`:
+
+```
+./fuzz_synth.py --num 1500
+./fuzz_aig_to_cnf --num 1000
+./fuzz_aig_rewrite --num 1000
+./fuzz_unate_def_rep.py 300
+```
+
+All must pass before reporting a change as complete. `fuzz_unate_def_rep.py`
+forces `--unatedef 1 --unatedefrep 1` on every iteration and verifies the
+`*-unsat_unate_def_rep.aig` output AIG via `test-synth`; the general
+`fuzz_synth.py` only randomizes those flags so the rep-pass output is not
+always exercised.
+
+## Source layout (`src/`)
+
+- `arjun.{h,cpp}` — public API, the `AIG` class, and the `SimplifiedCNF`
+  container. AIG nodes are `std::shared_ptr<AIG>` (`aig_ptr`). Every AIG
+  node carries a monotonic `uint64_t nid` assigned at construction; use
+  `nid` for ordering/hashing, never the raw pointer (ASLR makes pointers
+  non-deterministic across runs).
+- `manthan.{h,cpp}`, `manthan_learn.{h,cpp}` — counterexample-guided
+  synthesis / repair loop. Hot path for large benchmarks.
+- `aig_rewrite.{h,cpp}` — structural hashing, CSE, absorption, ITE
+  flattening. Runs before Manthan and between repair rounds.
+- `aig_to_cnf.{h,cpp}` — Tseitin encoding with fanout-based helper
+  suppression, k-ary AND/OR fusion, ITE / MUX3 detection.
+- `puura.{h,cpp}` — SharpSAT-td-derived simplification.
+- `autarky.cpp`, `backward.cpp`, `extend.cpp`, `minimize.cpp`,
+  `unate_def.cpp` — independent-set extraction passes.
+- `metasolver.h`, `metasolver2.h`, `cachedsolver.h` — SAT-solver wrappers
+  used by Manthan.
+- `test_aig_rewrite.cpp`, `test_aig_to_cnf.cpp`, `test-synth.cpp` —
+  correctness checkers.
+- `aig_fuzzer.cpp`, `aig_to_cnf_fuzzer.cpp` — fuzzers.
+
+## Determinism
+
+The same binary must produce bit-identical output across runs and machines.
+Do not introduce pointer-address-dependent ordering (`operator<` on
+`shared_ptr`, `std::hash<T*>`, `reinterpret_cast<uintptr_t>` of a pointer).
+For AIG nodes, order/hash on `AIG::nid` via the `aig_nid_less` comparator
+(in `aig_rewrite.cpp`) or `AigPtrHash` (in `aig_rewrite.h` / `aig_to_cnf.h`).
+
+## Debug outputs
+
+When `--debugsynth` is passed, intermediate AIGs are written next to the
+input CNF with suffixes `-simplified_cnf.aig`, `-autarky.aig`,
+`-minim_idep_synt.aig`, `-manthan.aig`, `-final.aig`. `test-synth` verifies
+each stage's AIG against the original CNF and is invoked automatically by
+`fuzz_synth.py`.
+
+## Debugging issues
+
+When debugging a bug (assertion, wrong answer, crash, non-determinism), use
+the full toolbox — don't stop at the first technique that gives a hint.
+Expected workflow:
+
+1. **Fuzzing** — reproduce / narrow down with `fuzz_synth.py`,
+   `fuzz_aig_to_cnf`, `fuzz_aig_rewrite` (see "After every build"). Fuzzers
+   generate minimal failing inputs much faster than reasoning from a large
+   user-supplied CNF.
+2. **`scripts/cnf_delta.py`** — clause-level delta debugger for DIMACS CNFs.
+   Given a failing CNF and an oracle script that exits 0 iff the bug still
+   reproduces, it does plain ddmin on the clause list, preserving headers,
+   comments, and the `c p show … 0` projection line. Typical use: write a
+   tiny bash oracle that runs `arjun` with the bug-triggering flags and
+   greps stderr for the assertion text, then run
+   `./cnf_delta.py bug.cnf bug_min.cnf /tmp/oracle.sh`. Always minimize
+   before filing a repro or committing a bug CNF to the repo.
+3. **`SLOW_DEBUG`** (`src/constants.h:50`) — uncomment to enable expensive
+   internal invariant checks (`SLOW_DEBUG_DO(...)` blocks). Turn this on
+   whenever an assertion fires or an output looks wrong; it will often fail
+   earlier and closer to the real cause.
+4. **`VERBOSE_DEBUG`** (`src/constants.h:51`) — uncomment to enable verbose
+   trace prints guarded by `VERBOSE_DEBUG_DO(...)` / `verbose_debug_enabled`.
+   Use together with a delta-debugged small CNF so the traces stay readable.
+5. **valgrind** — run under `valgrind --error-exitcode=1` (and
+   `--track-origins=yes` for uninitialized reads) for any suspected memory
+   issue. Undefined behavior here often manifests as non-determinism on
+   larger inputs.
+6. **gdb** — for assertion failures and crashes, run under `gdb --args
+   ./arjun ...`, `run`, then `bt` / `frame N` / `p` to inspect state at the
+   failure point. Pair with `SLOW_DEBUG` so gdb stops at the invariant
+   break, not downstream at a confusing symptom.
+
+Default loop for a tricky bug: fuzz → delta-debug the failing CNF with
+`cnf_delta.py` → rebuild with `SLOW_DEBUG` (and `VERBOSE_DEBUG` if needed) →
+valgrind / gdb on the minimized CNF.

CMakeLists.txt

@@ -530,6 +530,18 @@ endif()
 # -----------------------------------------------------------------------------
 set(ARJUN_EXPORT_NAME "arjunTargets")
 
+# enable_testing() must run in the top-level CMakeLists BEFORE any
+# add_subdirectory() calls that register tests with add_test(), otherwise
+# the nested add_test() invocations land in a scope that ctest never sees
+# and `make test` reports "No tests were found".
+if(ENABLE_TESTING)
+    enable_testing()
+    message(STATUS "Testing is enabled")
+    set(UNIT_TEST_EXE_SUFFIX "Tests" CACHE STRING "Suffix for Unit test executable")
+else()
+    message(WARNING "Testing is disabled")
+endif()
+
 add_subdirectory(src)
 
 # -----------------------------------------------------------------------------
@@ -545,17 +557,6 @@ add_custom_target(uninstall_arjun
     COMMAND ${CMAKE_COMMAND} -P ${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake
 )
 
-if(ENABLE_TESTING)
-    enable_testing()
-
-    message(STATUS "Testing is enabled")
-    set(UNIT_TEST_EXE_SUFFIX "Tests" CACHE STRING "Suffix for Unit test executable")
-    #add_subdirectory(tests)
-
-else()
-    message(WARNING "Testing is disabled")
-endif()
-
 # -----------------------------------------------------------------------------
 # Export our targets so that other CMake based projects can interface with
 # the build of arjun in the build-tree