feat(pigeons): initial library version (#337)

* feat(pigeons): initial library version

* fix tools nix build

Author: chrjabs

.config/lingo.dic

@@ -1,4 +1,4 @@
-39
+47
 accessor
 al
 AllDifferent
@@ -10,14 +10,19 @@ bitwise
 boolean
 cardinality
 changelog
+checkable
 children's
 comparator
 decrementing
 encoding/S
+equioptimal
+equisatisfiable
 et
 executable/S
+formatter
 hasher
 incrementing
+initializer/S
 inprocessing
 irredundant
 learnt
@@ -28,6 +33,9 @@ parser/S
 preprocessing
 propagations
 recurse/S
+redundance
+reflexivity
+reification/S
 satisfiability
 satisfiable
 struct/S

.github/workflows/ci.yml

@@ -32,6 +32,7 @@ jobs:
       - kissat-tests
       - kissat-test-all-features
       - minisat-tests
+      - pigeons-tests
       - pyapi-tests
       - pyapi-stubs
       - tools-tests
@@ -55,6 +56,7 @@ jobs:
           echo "kissat-tests: ${{ needs.kissat-tests.result }}"
           echo "kissat-test-all-features: ${{ needs.kissat-test-all-features.result }}"
           echo "minisat-tests: ${{ needs.minisat-tests.result }}"
+          echo "pigeons-tests: ${{ needs.pigeons-tests.result }}"
           echo "pyapi-tests: ${{ needs.pyapi-tests.result }}"
           echo "pyapi-stubs: ${{ needs.pyapi-stubs.result }}"
           echo "tools-tests: ${{ needs.tools-tests.result }}"
@@ -439,6 +441,42 @@ jobs:
       - name: Test suite
         run: cargo nextest run --profile ci -p rustsat-minisat --verbose
 
+  pigeons-tests:
+    name: Pigeons test suite
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
+    needs:
+      - build-workspace
+    steps:
+      - uses: actions/checkout@v4
+      - name: Determine Rust version
+        id: rust-versions
+        shell: bash
+        run: scripts/rust-versions.sh >> "$GITHUB_OUTPUT"
+      - uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: ${{ steps.rust-versions.outputs.toolchain }}
+      - uses: taiki-e/install-action@nextest
+      - uses: Swatinem/rust-cache@v2
+        with:
+          shared-key: "toolchain-workspace"
+          save-if: false
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: 3.12
+      - name: Install VeriPB
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          set -e
+          sudo apt-get install libgmp-dev
+          pip install https://gitlab.com/MIAOresearch/software/VeriPB/-/archive/version2/VeriPB-version2.zip
+          echo "VERIPB_CHECKER=$(which veripb)" >> "$GITHUB_ENV"
+      - name: Test suite
+        run: cargo nextest run --profile ci -p pigeons --verbose
+
   pyapi-tests:
     name: PyAPI test suite
     strategy:

Cargo.lock

@@ -10,6 +10,7 @@ members = [
   "capi",
   "pyapi",
   "batsat",
+  "pigeons",
 ]
 resolver = "2"
 
@@ -33,6 +34,7 @@ git2 = "0.20.1"
 glob = "0.3.2"
 itertools = "0.14.0"
 nom = "7.1.3"
+pigeons = { version = "0.1.0", path = "./pigeons" }
 termcolor = "1.4.1"
 thiserror = "2.0.12"
 rand = "0.9.0"

Cargo.toml

@@ -0,0 +1,16 @@
+* #variable= 16 #constraint= 15
+1 y_x1_5 1 y_x1_6 1 y_x1_7 1 y_x1_8 1 y_x1_9 >= 1 ;
+1 y_x2_5 1 y_x2_6 1 y_x2_7 1 y_x2_8 1 y_x2_9 >= 1 ;
+1 y_x3_8 1 y_x3_9 >= 1 ;
+1 y_x4_8 1 y_x4_9 >= 1 ;
+1 y_x5_8 1 y_x5_9 >= 1 ;
+-1 y_x1_5 -1 y_x1_6 -1 y_x1_7 -1 y_x1_8 -1 y_x1_9 >= -1 ;
+-1 y_x2_5 -1 y_x2_6 -1 y_x2_7 -1 y_x2_8 -1 y_x2_9 >= -1 ;
+-1 y_x3_8 -1 y_x3_9 >= -1 ;
+-1 y_x4_8 -1 y_x4_9 >= -1 ;
+-1 y_x5_8 -1 y_x5_9 >= -1 ;
+-1 y_x1_5 -1 y_x2_5 >= -1 ;
+-1 y_x1_6 -1 y_x2_6 >= -1 ;
+-1 y_x1_7 -1 y_x2_7 >= -1 ;
+-1 y_x1_8 -1 y_x2_8 -1 y_x3_8 -1 y_x4_8 -1 y_x5_8 >= -1 ;
+-1 y_x1_9 -1 y_x2_9 -1 y_x3_9 -1 y_x4_9 -1 y_x5_9 >= -1 ;