Introduces c-minisat bindings example

.github/actions/base/action.yml

@@ -133,6 +133,10 @@ runs:
       if: runner.os == 'Windows'
       uses: ./.github/actions/build-manual-windows
 
+    - name: Build c-minisat example (Ubuntu)
+      if: runner.os == 'Linux'
+      uses: ./.github/actions/examples/c-minisat
+
     # Save the cache after building the project AND the manual.
     - name: Save cache
       uses: actions/cache/save@v4

.github/actions/examples/c-minisat/action.yml

@@ -0,0 +1,18 @@
+name: c-minisat Example
+description: Build and run the c-minisat example
+
+runs:
+  using: composite
+  steps:
+    - name: Install minisat
+      shell: bash
+      run: sudo apt-get update && sudo apt-get install -y minisat
+
+    - name: Initialize git submodules
+      shell: bash
+      run: git submodule update --init --recursive examples/c-minisat/minisat-c-bindings
+
+    - name: Run generation and build script
+      shell: bash
+      working-directory: ./examples/c-minisat
+      run: ./generate-and-run.sh

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "alternatives/c2hs"]
 	path = alternatives/tools/c2hs
 	url = https://github.com/haskell/c2hs.git
+[submodule "examples/c-minisat/minisat-c-bindings"]
+	path = examples/c-minisat/minisat-c-bindings
+	url = https://github.com/niklasso/minisat-c-bindings.git

examples/c-minisat/README.md

@@ -0,0 +1,54 @@
+# MiniSat Haskell Bindings
+
+This example demonstrates generating Haskell bindings for
+[MiniSat](https://github.com/niklasso/minisat-c-bindings), a minimalistic
+open-source SAT solver.
+
+## Prerequisites
+
+You need the MiniSat library installed on your system. For example, on NixOS:
+
+```bash
+nix-shell -p minisat
+```
+
+## Running the Example
+
+```bash
+./generate-and-run.sh
+```
+
+This script will:
+1. Build the minisat-c-bindings C library
+2. Create symbolic links for the shared library (see quirks below)
+3. Generate Haskell bindings using `hs-bindgen`
+4. Create `cabal.project.local` with the necessary configuration
+5. Build and run the example program
+
+## Quirks and Workarounds
+
+### 1. Shared Library Symlinks
+
+The build process creates `libminisat-c.so.1.0.0`, but the linker needs the
+standard naming convention symlinks:
+
+```bash
+ln -sf libminisat-c.so.1.0.0 libminisat-c.so
+ln -sf libminisat-c.so.1.0.0 libminisat-c.so.1
+```
+
+The `generate-and-run.sh` script handles this automatically. These symlinks
+follow Linux shared library naming conventions:
+
+- `libminisat-c.so` → linker name (used at compile time)
+- `libminisat-c.so.1` → soname (used at runtime)
+- `libminisat-c.so.1.0.0` → real name (actual library file)
+
+See [this explanation](https://stackoverflow.com/questions/663209/can-someone-explain-linux-library-naming/21462448#21462448)
+for more details.
+
+### 2. Linking Against the C Library
+
+The `.cabal` file includes `extra-libraries: minisat-c`, which tells the
+linker to link against `libminisat-c.so`. The library name should match the
+base name of the binary file (without the `lib` prefix and `.so` extension).

examples/c-minisat/generate-and-run.sh

@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+
+# Exit on first error
+set -e
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../.." && pwd)"
+
+echo "# "
+echo "# Building minisat C bindings"
+echo "# "
+
+cd "$SCRIPT_DIR/minisat-c-bindings"
+make
+
+echo "# "
+echo "# Creating symlinks for shared library"
+echo "# "
+
+cd "$SCRIPT_DIR/minisat-c-bindings/build/dynamic/lib"
+ln -sf libminisat-c.so.1.0.0 libminisat-c.so
+ln -sf libminisat-c.so.1.0.0 libminisat-c.so.1
+
+echo "# "
+echo "# Generating Haskell bindings"
+echo "# "
+
+cd "$PROJECT_ROOT"
+
+cabal run hs-bindgen-cli -- \
+    preprocess \
+    -I "$SCRIPT_DIR/minisat-c-bindings" \
+    --hs-output-dir "$SCRIPT_DIR/hs-project/src" \
+    --module Minisat.Generated \
+    "$SCRIPT_DIR/minisat-c-bindings/minisat.h"
+
+echo "# "
+echo "# Creating cabal.project.local"
+echo "# "
+
+cat > "$SCRIPT_DIR/hs-project/cabal.project.local" <<EOF
+package c-minisat
+    extra-include-dirs:
+        $SCRIPT_DIR/minisat-c-bindings
+      , $SCRIPT_DIR/minisat-c-bindings/build/dynamic/lib
+    extra-lib-dirs:
+        $SCRIPT_DIR/minisat-c-bindings
+      , $SCRIPT_DIR/minisat-c-bindings/build/dynamic/lib
+EOF
+
+echo "# "
+echo "# Done!"
+echo "# "
+echo "Running the project"
+cd $SCRIPT_DIR/hs-project
+export LD_LIBRARY_PATH=$SCRIPT_DIR/minisat-c-bindings/build/dynamic/lib:\$LD_LIBRARY_PATH
+cabal build
+cabal run c-minisat

examples/c-minisat/hs-project/LICENSE

@@ -0,0 +1,29 @@
+Copyright (c) 2024-2025, Well-Typed LLP and Anduril Industries Inc.
+
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of the copyright holder nor the names of its
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

examples/c-minisat/hs-project/app/Main.hs

@@ -0,0 +1,47 @@
+module Main where
+
+import Data.Functor (void)
+import Foreign.Ptr qualified as F
+
+import Minisat.Generated qualified as Minisat
+import Minisat.Generated.Safe qualified as Minisat
+
+-- Adds a list of literals
+--
+-- addClause [a, b, c] == a v b v c
+--
+-- multiple calls to addClause, e.g.
+--
+-- addClause [a, b] >> addClause [c, d] == (a v b) ∧ (c v d)
+--
+addClause :: F.Ptr Minisat.Minisat_solver -> [Minisat.Minisat_Lit] -> IO ()
+addClause s lits = do
+  Minisat.minisat_addClause_begin s
+  mapM_ (Minisat.minisat_addClause_addLit s) lits
+  void $ Minisat.minisat_addClause_commit s
+
+exampleSolver :: IO ()
+exampleSolver = do
+  minisatSolver <- Minisat.minisat_new
+
+  x1 <- Minisat.minisat_newLit minisatSolver
+  x2 <- Minisat.minisat_newLit minisatSolver
+  x3 <- Minisat.minisat_newLit minisatSolver
+
+  nx1 <- Minisat.minisat_negate x1
+  nx2 <- Minisat.minisat_negate x1
+  nx3 <- Minisat.minisat_negate x1
+
+  Minisat.minisat_addClause_begin minisatSolver
+
+  addClause minisatSolver [x1, x2]
+  addClause minisatSolver [nx1, x3]
+  addClause minisatSolver [nx2, nx3]
+
+  sat <- Minisat.minisat_solve minisatSolver 0 F.nullPtr
+  let satResult = Minisat.un_Minisat_bool sat /= 0
+  putStrLn ("Is (a v b) ∧ (c v d) satisfiable? " ++ show satResult)
+
+main :: IO ()
+main = do
+  exampleSolver

examples/c-minisat/hs-project/c-minisat.cabal

@@ -0,0 +1,112 @@
+cabal-version:      3.0
+-- The cabal-version field refers to the version of the .cabal specification,
+-- and can be different from the cabal-install (the tool) version and the
+-- Cabal (the library) version you are using. As such, the Cabal (the library)
+-- version used must be equal or greater than the version stated in this field.
+-- Starting from the specification version 2.2, the cabal-version field must be
+-- the first thing in the cabal file.
+
+-- Initial package description 'c-minisat' generated by
+-- 'cabal init'. For further documentation, see:
+--   http://haskell.org/cabal/users-guide/
+--
+-- The name of the package.
+name:               c-minisat
+
+-- The package version.
+-- See the Haskell package versioning policy (PVP) for standards
+-- guiding when and how versions should be incremented.
+-- https://pvp.haskell.org
+-- PVP summary:     +-+------- breaking API changes
+--                  | | +----- non-breaking API additions
+--                  | | | +--- code changes with no API change
+version:            0.1.0.0
+
+-- A short (one-line) description of the package.
+-- synopsis:
+
+-- A longer description of the package.
+-- description:
+
+-- The license under which the package is released.
+license:            BSD-3-Clause
+
+-- The file containing the license text.
+license-file:       LICENSE
+
+-- The package author(s).
+author:             Armando Santos
+
+-- An email address to which users can send suggestions, bug reports, and patches.
+maintainer:         [email protected]
+
+-- A copyright notice.
+-- copyright:
+build-type:         Simple
+
+-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.
+extra-doc-files:    CHANGELOG.md
+
+-- Extra source files to be distributed with the package, such as examples, or a tutorial module.
+-- extra-source-files:
+
+common warnings
+    ghc-options: -Wall
+
+library
+    -- Import common warning flags.
+    import:           warnings
+
+    -- Modules exported by the library.
+    exposed-modules:  Minisat.Generated
+                      Minisat.Generated.Safe
+                      Minisat.Generated.Unsafe
+                      Minisat.Generated.Global
+                      Minisat.Generated.FunPtr
+
+    -- Modules included in this library but not exported.
+    -- other-modules:
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends:    base,
+                      hs-bindgen-runtime
+
+    -- Directories containing source files.
+    hs-source-dirs:   src
+
+    -- Base language which the package is written in.
+    default-language: Haskell2010
+
+    extra-libraries: minisat-c
+
+executable c-minisat
+    -- Import common warning flags.
+    import:           warnings
+
+    -- .hs or .lhs file containing the Main module.
+    main-is:          Main.hs
+
+    -- Modules included in this executable, other than Main.
+    -- other-modules:
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends:
+        base,
+        c-minisat
+
+    -- extra-libraries: minisat-c
+
+    -- Directories containing source files.
+    hs-source-dirs:   app
+
+    -- Base language which the package is written in.
+    default-language: Haskell2010
+
+    default-extensions:
+      ImportQualifiedPost

examples/c-minisat/hs-project/cabal.project

@@ -0,0 +1,11 @@
+packages: .
+          ../../../ansi-diff
+          ../../../hs-bindgen-runtime
+          ../../../c-expr-runtime
+          ../../../c-expr-dsl
+          ../../../hs-bindgen
+
+source-repository-package
+    type: git
+    location: https://github.com/well-typed/libclang
+    tag: d4ae9a5fcca9ae71fcb4df2c0b0ea37c6b15c48c