MaxSMT solver implementation

.github/workflows/maxsmt-tests-matrix.json

@@ -0,0 +1,46 @@
+[
+  {
+    "NAME": "QF_ABV-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_ABVFP-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_AUFBV",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_AUFBVLIA-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_AUFLIA",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_BV-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_FP",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_UF-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_UFBV-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_UFLIA-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  },
+  {
+    "NAME": "QF_UFLRA-light",
+    "TEST_DATA_REVISION": "0.0.0"
+  }
+]

.github/workflows/run-long-maxsat-tests.yml

@@ -0,0 +1,68 @@
+name: Build and run long ksmt MaxSAT tests
+
+on:
+  workflow_dispatch:
+    inputs:
+      smtSolver:
+        type: choice
+        description: Chosen SMT solver
+        options:
+          - Z3
+          - Bitwuzla
+          - Cvc5
+          - Yices
+
+env:
+  TEST_DATA_REVISION: 0.0.0
+
+jobs:
+  run-maxsat-tests:
+    runs-on: ubuntu-22.04
+
+    strategy:
+      matrix:
+        BENCHMARK_NUMBER: [ 1, 2, 3, 4, 5, 6 ]
+      fail-fast: false
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Prepare test data (cache)
+        id: test-data-cache
+        uses: actions/cache@v3
+        env:
+          cache-name: cache-maxsat-test-data
+        with:
+          key: maxsat-test-data-${{ env.TEST_DATA_REVISION }}-${{ matrix.os }}
+          path: ksmt-maxsmt-test/testData/data/*
+
+      - name: Set up JDK 1.8
+        uses: actions/setup-java@v3
+        with:
+          java-version: 8
+          distribution: 'zulu'
+          cache: gradle
+
+      - name: Prepare test data (download)
+        if: steps.test-data-cache.outputs.cache-hit != 'true'
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: |
+            :ksmt-maxsmt-test:maxsat-benchmark-${{ matrix.BENCHMARK_NUMBER }}
+            --no-daemon
+            -PtestDataRevision=${{ env.TEST_DATA_REVISION }}
+
+      - name: Run MaxSAT benchmark
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: |
+            :ksmt-maxsmt-test:test
+            --no-daemon
+            --tests "io.ksmt.solver.maxsmt.test.sat.KPrimalDualMaxResSATBenchmarkTest.maxSAT${{ inputs.smtSolver }}Test"
+
+      - name: Upload test report
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: ksmt-maxsat-test-report-${{ matrix.BENCHMARK_NUMBER }}
+          path: ksmt-maxsmt-test/build/reports/tests/test/*

.github/workflows/run-long-maxsmt-tests-pdmres.yml

@@ -0,0 +1,119 @@
+name: (PrimalDualMaxRes solver) Build and run long MaxSMT tests
+
+on:
+  workflow_dispatch:
+    inputs:
+      solver:
+        type: choice
+        description: Chosen MaxSMT solver
+        options:
+          - KPrimalDualMaxRes
+      smtSolver:
+        type: choice
+        description: Chosen SMT solver
+        options:
+          - Portfolio
+          - Z3
+          - Bitwuzla
+          - Cvc5
+          - Yices
+          - Z3Native
+      optimality:
+        type: boolean
+        description: Chosen optimal (otherwise suboptimal) configuration
+        default: false
+      strategy:
+        type: choice
+        description: Chosen MaxSMT solving strategy
+        options:
+          - Dual
+          - Primal
+      minimizeCores:
+        type: boolean
+        description: Core minimization option (only one of [minimizeCores, preferLargeWeightCores, getMultipleCores] can be true)
+        required: true
+        default: false
+      preferLargeWeightCores:
+        type: boolean
+        description: Prefer large weight constraints for cores (only one of [minimizeCores, preferLargeWeightCores, getMultipleCores] can be true)
+        required: true
+        default: true
+      getMultipleCores:
+        type: boolean
+        description: Get multiple cores (only one of [minimizeCores, preferLargeWeightCores, getMultipleCores] can be true)
+        required: true
+        default: false
+      commitSHA:
+        description: Commit SHA (latest commit is default)
+        required: false
+        type: string
+        default: ""
+
+jobs:
+  verify-inputs:
+    runs-on: ubuntu-22.04
+    steps:
+      - name: Verify inputs
+        # Check only one option of [minimizeCores, preferLargeWeightCores, getMultipleCores] is true
+        # (supported tests configurations)
+        run: |
+          if ([[ "${{ inputs.minimizeCores }}" == "true" ]] && [[ "${{ inputs.preferLargeWeightCores }}" == "true" ]]) || \
+            ([[ "${{ inputs.minimizeCores }}" == "true" ]] && [[ "${{ inputs.getMultipleCores }}" == "true" ]]) || \
+            ([[ "${{ inputs.preferLargeWeightCores }}" == "true" ]] && [[ "${{ inputs.getMultipleCores }}" == "true" ]])
+          then
+            echo "Only one option of [minimizeCores, preferLargeWeightCores, getMultipleCores] can be true"
+            exit 1
+          fi
+
+  construct-solver-name:
+    needs: verify-inputs
+    runs-on: ubuntu-22.04
+    outputs:
+      solver: ${{ steps.set-output.outputs.solver }}
+    steps:
+      - name: Construct solver name
+        run: |
+          if [[ "${{ inputs.minimizeCores }}" == false ]] && \
+            [[ "${{ inputs.preferLargeWeightCores }}" == false ]] && \
+            [[ "${{ inputs.getMultipleCores }}" == false ]]
+          then
+            export OPTION_TO_VALUE=""
+          elif [[ "${{ inputs.preferLargeWeightCores }}" == true ]]
+          then
+            export OPTION_TO_VALUE="2"
+          elif [[ "${{ inputs.minimizeCores }}" == true ]]
+          then
+            export OPTION_TO_VALUE="3"
+          elif [[ "${{ inputs.getMultipleCores }}" == true ]]
+          then
+            export OPTION_TO_VALUE="4"
+          fi
+
+          echo "OPTION_TO_VALUE=$OPTION_TO_VALUE" >> $GITHUB_ENV
+
+          if [[ "${{ inputs.optimality }}" == false ]]
+          then
+            export SUB_OPT="SubOpt"
+          fi
+
+          echo "SUB_OPT=$SUB_OPT" >> $GITHUB_ENV
+
+      - name: Set solver name to output
+        id: set-output
+        run: |
+          if [[ "${{ inputs.smtSolver }}" == "Z3Native" ]]
+          then
+            echo "solver=Z3Native" >> $GITHUB_OUTPUT
+          else
+            echo "solver=K${{ env.SUB_OPT }}${{ inputs.strategy }}MaxRes${{ env.OPTION_TO_VALUE }}" >> $GITHUB_OUTPUT
+          fi
+
+  run-long-maxsmt-tests:
+    needs: construct-solver-name
+    uses: ./.github/workflows/run-long-maxsmt-tests.yml
+    with:
+      solver: ${{ needs.construct-solver-name.outputs.solver }}
+      smtSolver: ${{ inputs.smtSolver }}
+      optimality: ${{ inputs.optimality }}
+      commitSHA: ${{ inputs.commitSHA }}
+    secrets: inherit

.github/workflows/run-long-maxsmt-tests-pmres.yml

@@ -0,0 +1,33 @@
+name: (PMRes solver) Build and run long MaxSMT tests
+
+on:
+  workflow_dispatch:
+    inputs:
+      solver:
+        type: choice
+        description: Chosen MaxSMT solver
+        options:
+          - KPMRes
+      smtSolver:
+        type: choice
+        description: Chosen SMT solver
+        options:
+          - Z3
+          - Bitwuzla
+          - Cvc5
+          - Yices
+      commitSHA:
+        description: Commit SHA (latest commit is default)
+        required: false
+        type: string
+        default: ""
+
+jobs:
+  run-long-maxsmt-tests:
+    uses: ./.github/workflows/run-long-maxsmt-tests.yml
+    with:
+      solver: ${{ inputs.solver }}
+      smtSolver: ${{ inputs.smtSolver }}
+      optimality: true
+      commitSHA: ${{ inputs.commitSHA }}
+    secrets: inherit