Merge pull request #346 from chrjabs/next-major

Next major version

Author: chrjabs

.config/abbreviations.dic

@@ -1,4 +1,4 @@
-29
+34
 AIJ
 API
 APIs
@@ -14,17 +14,22 @@ FFI
 FGT
 GBMO
 GCD
+IDRUP
 IJCAI
 IPASIR
 IPASIR's
 JSAT
+LIDRUP
+LRAT
 MCNF
 ModRef
 MOPB
 MSRV
 OPB
 PB
 PBO
+RUP
 SOICT
+VeriPB
 VMCAI
 WCNF

.config/lingo.dic

@@ -1,4 +1,4 @@
-38
+47
 accessor
 al
 AllDifferent
@@ -10,23 +10,32 @@ bitwise
 boolean
 cardinality
 changelog
+checkable
 children's
 comparator
 decrementing
 encoding/S
+equioptimal
+equisatisfiable
 et
 executable/S
+formatter
 hasher
 incrementing
+initializer/S
 inprocessing
 irredundant
 learnt
 localsearch
 natively
+nul
 parser/S
 preprocessing
 propagations
 recurse/S
+redundance
+reflexivity
+reification/S
 satisfiability
 satisfiable
 struct/S

.github/workflows/ci.yml

@@ -25,16 +25,20 @@ jobs:
       - rustsat-kani
       - batsat-tests
       - cadical-tests
+      - cadical-test-all-features
       - capi-tests
       - capi-header
       - glucose-tests
       - kissat-tests
+      - kissat-test-all-features
       - minisat-tests
+      - pigeons-tests
       - pyapi-tests
       - pyapi-stubs
       - tools-tests
       - docs
       - formatting
+      - code-spelling
     if: ${{ success() || failure() }}  # Run this job even if a dependency has failed.
     steps:
       - name: Job outcomes
@@ -45,16 +49,20 @@ jobs:
           echo "rustsat-kani: ${{ needs.rustsat-kani.result }}"
           echo "batsat-tests: ${{ needs.batsat-tests.result }}"
           echo "cadical-tests: ${{ needs.cadical-tests.result }}"
+          echo "cadical-test-all-features: ${{ needs.cadical-test-all-features.result }}"
           echo "capi-tests: ${{ needs.capi-tests.result }}"
           echo "capi-header: ${{ needs.capi-header.result }}"
           echo "glucose-tests: ${{ needs.glucose-tests.result }}"
           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 }}"
           echo "docs: ${{ needs.docs.result }}"
           echo "formatting: ${{ needs.formatting.result }}"
+          echo "code-spelling: ${{ needs.code-spelling.result }}"
       # Fail this required job if any of its dependent jobs have failed.
       #
       # Do not attempt to consolidate these steps into one step, it won't work.
@@ -71,6 +79,8 @@ jobs:
         run: exit 1
       - if: ${{ needs.cadical-tests.result != 'success' }}
         run: exit 1
+      - if: ${{ needs.cadical-test-all-features.result == 'failure' }}
+        run: exit 1
       - if: ${{ needs.capi-tests.result != 'success' }}
         run: exit 1
       - if: ${{ needs.capi-header.result != 'success' }}
@@ -79,8 +89,12 @@ jobs:
         run: exit 1
       - if: ${{ needs.kissat-tests.result != 'success' }}
         run: exit 1
+      - if: ${{ needs.kissat-test-all-features.result == 'failure' }}
+        run: exit 1
       - if: ${{ needs.minisat-tests.result != 'success' }}
         run: exit 1
+      - if: ${{ needs.pigeons-tests.result != 'success' }}
+        run: exit 1
       - if: ${{ needs.pyapi-tests.result != 'success' }}
         run: exit 1
       - if: ${{ needs.pyapi-stubs.result != 'success' }}
@@ -91,6 +105,8 @@ jobs:
         run: exit 1
       - if: ${{ needs.formatting.result != 'success' }}
         run: exit 1
+      - if: ${{ needs.code-spelling.result != 'success' }}
+        run: exit 1
 
   build-workspace:
     name: Build workspace
@@ -142,6 +158,17 @@ jobs:
       - name: Limit cmake parallelism
         if: matrix.os == 'macos-latest'
         run: echo "CMAKE_BUILD_PARALLEL_LEVEL=4" >> "$GITHUB_ENV"
+      - uses: actions/setup-python@v5
+        if: matrix.os == 'ubuntu-latest'
+        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 rustsat --verbose --features=all
       - name: CaDiCaL external solver
@@ -169,8 +196,6 @@ jobs:
       matrix:
         os: [ubuntu-latest, macos-latest, windows-latest]
     runs-on: ${{ matrix.os }}
-    needs:
-      - build-workspace
     steps:
       - uses: actions/checkout@v4
       - name: Determine Rust version
@@ -249,6 +274,29 @@ jobs:
       - name: Test suite
         run: cargo nextest run --profile ci -p rustsat-cadical --verbose
 
+  cadical-test-all-features:
+    name: CaDiCaL test all features
+    runs-on: ubuntu-latest
+    if: contains(github.event.pull_request.labels.*.name, 'solvers/cadical')
+    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: Test all features
+        run: scripts/check-all-features.sh -v -t -n -p rustsat-cadical
+
   capi-tests:
     name: C-API test suite
     strategy:
@@ -282,8 +330,6 @@ jobs:
   capi-header:
     name: Check C-API header
     runs-on: ubuntu-latest
-    needs:
-      - build-workspace
     steps:
       - uses: actions/checkout@v4
       - name: Determine Rust version
@@ -356,6 +402,29 @@ jobs:
       - name: Test suite
         run: cargo nextest run --profile ci -p rustsat-kissat --verbose
 
+  kissat-test-all-features:
+    name: Kissat test all features
+    runs-on: ubuntu-latest
+    if: contains(github.event.pull_request.labels.*.name, 'solvers/kissat')
+    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: Test all features
+        run: scripts/check-all-features.sh -v -t -n -p rustsat-kissat
+
   minisat-tests:
     name: MiniSat test suite
     strategy:
@@ -381,6 +450,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:
@@ -465,17 +570,17 @@ jobs:
         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: dtolnay/rust-toolchain@nightly
       - uses: Swatinem/rust-cache@v2
         with:
           shared-key: "toolchain-workspace"
           save-if: false
       - name: Cargo doc
-        run: cargo doc --workspace --verbose --no-deps --features=all
+        run: cargo +nightly doc -Zunstable-options -Zrustdoc-scrape-examples --workspace --no-deps --features=all,internals
+        env:
+          RUSTDOCFLAGS: "-Dwarnings --cfg docsrs"
       - name: Doc tests
-        run: cargo test --doc --workspace --verbose
+        run: cargo +nightly test --doc --workspace --verbose
       - uses: taiki-e/install-action@cargo-spellcheck
       - name: Spellcheck documentation
         run: cargo spellcheck --code 1
@@ -514,3 +619,10 @@ jobs:
       - uses: Swatinem/rust-cache@v2
       - name: Run cargo fmt
         run: cargo fmt --all -- --check
+
+  code-spelling:
+    name: Spell check with typos
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: crate-ci/[email protected]

.github/workflows/pages.yml

@@ -30,7 +30,7 @@ jobs:
       - name: Build rust docs
         run: |
           mkdir -p _site/
-          cargo +nightly doc -Zunstable-options -Zrustdoc-scrape-examples --workspace --no-deps
+          cargo +nightly doc -Zunstable-options -Zrustdoc-scrape-examples --workspace --no-deps --features=all,internals -- --cfg docsrs
           mv target/doc/ _site/main/
       - uses: actions/setup-python@v5
         with:

.github/workflows/semver-checks.yml

@@ -2,7 +2,7 @@ name: Semver checks
 
 on:
   pull_request:
-    branches: [ "main", "next-major" ]
+    branches: [ "main" ]
 
 env:
   CARGO_TERM_COLOR: always

CHANGELOG.md

@@ -327,12 +327,12 @@ guide](https://github.com/chrjabs/rustsat/blob/main/docs/0-5-0-migration-guide.m
 
 - Alternative totalizer implementation based on a totalizer database
 - Dynamic polynomial watchdog encoing
-- Changes to public API: changed some vectores to slices
+- Changes to public API: changed some vectors to slices
 - Changed internal variable/literal representation from `usize` to `u32`
 
 ## [0.2.x]
 
-Solver interfaces factored out into seperate crates.
+Solver interfaces factored out into separate crates.
 See detailed changes in [GitHub Releases](https://github.com/chrjabs/rustsat/releases).
 
 ## [0.1.2]