diff --git a/.github/workflows/maxsmt-tests-matrix.json b/.github/workflows/maxsmt-tests-matrix.json new file mode 100644 index 000000000..8e5812a27 --- /dev/null +++ b/.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" + } +] diff --git a/.github/workflows/run-long-maxsat-tests.yml b/.github/workflows/run-long-maxsat-tests.yml new file mode 100644 index 000000000..db4969ddc --- /dev/null +++ b/.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/* diff --git a/.github/workflows/run-long-maxsmt-tests-pdmres.yml b/.github/workflows/run-long-maxsmt-tests-pdmres.yml new file mode 100644 index 000000000..dd273ca23 --- /dev/null +++ b/.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 diff --git a/.github/workflows/run-long-maxsmt-tests-pmres.yml b/.github/workflows/run-long-maxsmt-tests-pmres.yml new file mode 100644 index 000000000..1daa28655 --- /dev/null +++ b/.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 diff --git a/.github/workflows/run-long-maxsmt-tests.yml b/.github/workflows/run-long-maxsmt-tests.yml new file mode 100644 index 000000000..7e349f31c --- /dev/null +++ b/.github/workflows/run-long-maxsmt-tests.yml @@ -0,0 +1,177 @@ +name: Build and run long MaxSMT tests + +on: + workflow_call: + inputs: + solver: + type: string + description: Chosen MaxSMT solver configuration + required: true + smtSolver: + type: string + description: Chosen SMT solver + required: true + optimality: + type: boolean + description: Chosen optimal (otherwise suboptimal) configuration + required: true + commitSHA: + description: Commit SHA (latest commit is default) + required: false + type: string + default: "" + +env: + TEST_DATA_REVISION: 0.0.0 + PUSHGATEWAY_HOSTNAME: monitoring.utbot.org + +jobs: + prepare-matrix: + runs-on: ubuntu-22.04 + outputs: + logics-matrix: ${{ steps.set-matrix.outputs.maxsmt-tests-matrix }} + steps: + - name: Print environment variables + run: printenv + + - name: Checkout repository (or SHA) + uses: actions/checkout@v4 + with: + ref: ${{ inputs.commitSHA }} + + - id: set-matrix + name: Create and print MaxSMT logics matrix + # Exclude LIA, LRA tests for Bitwuzla solver + # Exclude FP tests for Yices solver + run: | + if ${{ inputs.smtSolver == 'Bitwuzla' }} + then + MAXSMT_TESTS=$(echo $(cat .github/workflows/maxsmt-tests-matrix.json | jq '{ "logics": [ .[] | select(.NAME | contains("LIA") or contains("LRA") | not) ] }')) + elif ${{ inputs.smtSolver == 'Yices' }} + then + MAXSMT_TESTS=$(echo $(cat .github/workflows/maxsmt-tests-matrix.json | jq '{ "logics": [ .[] | select(.NAME | contains("FP") | not) ] }')) + else + MAXSMT_TESTS=$(echo $(cat .github/workflows/maxsmt-tests-matrix.json | jq '{ "logics": [ .[] ] }')) + fi + + echo "maxsmt-tests-matrix=$MAXSMT_TESTS" >> $GITHUB_OUTPUT + echo $MAXSMT_TESTS + + run-maxsmt-tests: + needs: prepare-matrix + continue-on-error: true + runs-on: ubuntu-22.04 + strategy: + matrix: ${{ fromJSON(needs.prepare-matrix.outputs.logics-matrix) }} + + name: Run ${{ matrix.logics.NAME }} tests + + steps: + - name: Checkout repository (or SHA) + uses: actions/checkout@v4 + with: + ref: ${{ inputs.commitSHA }} + + - name: Set up JDK 1.8 + uses: actions/setup-java@v3 + with: + java-version: 8 + distribution: 'zulu' + + - name: Run monitoring + # secret uploaded using base64 encoding to have one-line output: + # cat file | base64 -w 0 + continue-on-error: true + run: | + chmod +x ./scripts/monitoring.sh + ./scripts/monitoring.sh "${PUSHGATEWAY_HOSTNAME}" "${{ secrets.PUSHGATEWAY_USER }}" "${{ secrets.PUSHGATEWAY_PASSWORD }}" + echo "Please visit Grafana to check metrics: https://${PUSHGATEWAY_HOSTNAME}/d/rYdddlPWk/node-exporter-full?orgId=1&from=now-1h&to=now&var-service=github&var-instance=${GITHUB_RUN_ID}-${HOSTNAME}&refresh=1m" + + - name: Download ${{ matrix.logics.NAME }} tests + uses: gradle/gradle-build-action@v2 + with: + arguments: | + :ksmt-maxsmt-test:maxSmtBenchmark-${{ matrix.logics.NAME }} + --no-daemon + -PtestDataRevision=${{ env.TEST_DATA_REVISION }} + + - name: Run ${{ matrix.logics.NAME }} tests + uses: gradle/gradle-build-action@v2 + with: + arguments: | + :ksmt-maxsmt-test:test + --no-daemon + --tests "io.ksmt.solver.maxsmt.test.configurations.${{ inputs.solver }}SMTBenchmarkTest.maxSMT${{ inputs.smtSolver }}Test" + + - name: Add logic name to test run statistics + if: ${{ always() }} + # Create an object with the field 'logics' from the JSON list + run: | + cat <<< $(jq -S '. += { "NAME": "${{ matrix.logics.NAME }}" }' ksmt-maxsmt-test/src/test/resources/maxsmt-statistics-*.json) > ksmt-maxsmt-test/src/test/resources/maxsmt-statistics-*.json + + - name: Upload ${{ matrix.logics.NAME }} test statistics + if: ${{ always() }} + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.logics.NAME }}_${{ inputs.solver }}_${{ inputs.smtSolver }}_test_statistics + path: ksmt-maxsmt-test/src/test/resources/maxsmt-statistics-*.json + + - name: Upload ${{ matrix.logics.NAME }} test report + if: ${{ always() }} + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.logics.NAME }}_${{ inputs.solver }}_${{ inputs.smtSolver }}_test_report + path: ksmt-maxsmt-test/build/reports/tests/test/* + + - name: Upload ${{ matrix.logics.NAME }} test logs + if: ${{ always() }} + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.logics.NAME }}_${{ inputs.solver }}_${{ inputs.smtSolver }}_test_logs + path: ksmt-maxsmt-test/logs/* + + merge-and-analyze-maxsmt-statistics: + needs: run-maxsmt-tests + runs-on: ubuntu-22.04 + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Download test statistics + uses: actions/download-artifact@v4 + id: download + with: + path: downloads + + - name: Add merged test run statistics and analyzed statistics paths to environment variables + run: | + export MERGED_STATISTICS_PATH=${{steps.download.outputs.download-path}}/${{ inputs.solver }}_${{ inputs.smtSolver }}_test_statistics.json + echo "MERGED_STATISTICS_PATH=$MERGED_STATISTICS_PATH" >> $GITHUB_ENV + + export ANALYZED_STATISTICS_PATH=${{steps.download.outputs.download-path}}/${{ inputs.solver }}_${{ inputs.smtSolver }}_analyzed_test_statistics.json + echo "ANALYZED_STATISTICS_PATH=$ANALYZED_STATISTICS_PATH" >> $GITHUB_ENV + + - name: Merge test run statistics + # 1. Merge all test run statistics files into a single file: + # - merge all test run statistics files (${{steps.download.outputs.download-path}}/*_test_statistics/*.json) for different theories + # - save merged files into a single JSON file (${{ env.MERGED_STATISTICS_PATH }}_temp) + # + # 2. Create an object with the field 'logics' from the JSON list + run: | + jq -s '.' ${{steps.download.outputs.download-path}}/*_test_statistics/*.json > ${{ env.MERGED_STATISTICS_PATH }}_temp + cat ${{ env.MERGED_STATISTICS_PATH }}_temp | jq '{ "logics": . }' > ${{ env.MERGED_STATISTICS_PATH }} + + - name: Upload test run statistics + uses: actions/upload-artifact@v4 + with: + name: ${{ inputs.solver }}_${{ inputs.smtSolver }}_test_statistics + path: ${{ env.MERGED_STATISTICS_PATH }} + + - name: Analyze test run statistics + run: python ./scripts/analyze_maxsmt_statistics.py ${{ env.MERGED_STATISTICS_PATH }} ${{ env.ANALYZED_STATISTICS_PATH }} + + - name: Upload analyzed test run statistics + uses: actions/upload-artifact@v4 + with: + name: ${{ inputs.solver }}_${{ inputs.smtSolver }}_analyzed_test_statistics + path: ${{ env.ANALYZED_STATISTICS_PATH }} diff --git a/.gitignore b/.gitignore index 7dc56f914..ba0cbcdbb 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,19 @@ build # ignore ksmt test data ksmt-test/testData + +# ignore maxsat test data +ksmt-maxsmt-test/testData + +# ignore maxsmt test data +ksmt-maxsmt-test/src/test/resources/maxSmtBenchmark + +# ignore maxsmt statistics +ksmt-maxsmt-test/src/test/resources/maxsmt-statistics-*.json + +**/logs/ + +ksmt-maxsmt-test/src/test/resources/ + +ksmt-maxsmt-test/*.log + diff --git a/buildSrc/src/main/kotlin/BenchmarkUtil.kt b/buildSrc/src/main/kotlin/BenchmarkUtil.kt new file mode 100644 index 000000000..70bcb4970 --- /dev/null +++ b/buildSrc/src/main/kotlin/BenchmarkUtil.kt @@ -0,0 +1,57 @@ +import org.gradle.api.Project +import org.gradle.api.Task +import org.gradle.api.file.DuplicatesStrategy +import org.gradle.api.plugins.ExtensionAware +import org.gradle.api.tasks.SourceSetContainer +import org.gradle.api.tasks.TaskProvider +import org.gradle.kotlin.dsl.get +import java.io.File + +fun Project.downloadPreparedBenchmarkTestData( + downloadPath: File, + testDataPath: File, + benchmarkName: String, + benchmarkUrl: String, +): TaskProvider = + tasks.register("downloadPrepared${benchmarkName}BenchmarkTestData") { + doLast { + download(benchmarkUrl, downloadPath) + + copy { + from(zipTree(downloadPath)) + into(testDataPath) + duplicatesStrategy = DuplicatesStrategy.EXCLUDE + } + } + } + +fun Project.usePreparedBenchmarkTestData(path: File, benchmarkName: String): TaskProvider = + tasks.register("${benchmarkName}Benchmark-data-use") { + doLast { + check(path.exists()) { "No test data provided" } + val testResources = testResourceDir() ?: error("No resource directory found for benchmarks") + val testData = testResources.resolve("testData") + + testData.executeIfNotReady("test-data-ready") { + copy { + from(path) + into(testData) + duplicatesStrategy = DuplicatesStrategy.EXCLUDE + } + } + } + } + +fun Project.testResourceDir(): File? { + val sourceSets = (this as ExtensionAware).extensions.getByName("sourceSets") as SourceSetContainer + return sourceSets["test"]?.output?.resourcesDir +} + +inline fun File.executeIfNotReady(markerName: String, body: () -> Unit) { + val marker = this.resolve(markerName) + if (marker.exists()) return + + body() + + marker.createNewFile() +} diff --git a/buildSrc/src/main/kotlin/MaxSMTBenchmarkUtil.kt b/buildSrc/src/main/kotlin/MaxSMTBenchmarkUtil.kt new file mode 100644 index 000000000..319519ecc --- /dev/null +++ b/buildSrc/src/main/kotlin/MaxSMTBenchmarkUtil.kt @@ -0,0 +1,41 @@ +import org.gradle.api.Project +import org.gradle.api.file.DuplicatesStrategy +import org.gradle.kotlin.dsl.support.unzipTo + +fun Project.maxSmtBenchmarkTestData(name: String, testDataRevision: String) = tasks.register("maxSmtBenchmark-$name") { + doLast { + downloadBenchmarkTestData(name, testDataRevision) + } +} + +fun Project.maxSatBenchmarkTestData(name: String, testDataRevision: String) = tasks.register(name) { + doLast { + downloadBenchmarkTestData(name, testDataRevision) + unzipMaxSATBenchmarkTestFiles() + } +} + +fun Project.downloadBenchmarkTestData(name: String, testDataRevision: String) { + val path = testResourcesDir().resolve("maxSmtBenchmark/$name") + val downloadTarget = path.resolve("$name.zip") + val url = "$BENCHMARKS_REPO_URL/releases/download/$testDataRevision/$name.zip" + + download(url, downloadTarget) + + path.executeIfNotReady("unpack-complete") { + copy { + from(zipTree(downloadTarget)) + into(path) + duplicatesStrategy = DuplicatesStrategy.EXCLUDE + } + } +} + +fun Project.unzipMaxSATBenchmarkTestFiles() { + val testData = testResourcesDir().resolve("maxSmtBenchmark") + testData.walk().forEach { if (it.isFile && it.extension == "zip") unzipTo(it.parentFile, it) } +} + +private fun Project.testResourcesDir() = projectDir.resolve("src/test/resources") + +private const val BENCHMARKS_REPO_URL = "https://github.com/victoriafomina/ksmt" diff --git a/buildSrc/src/main/kotlin/Publications.kt b/buildSrc/src/main/kotlin/Publications.kt index 246a852fa..26c625b3d 100644 --- a/buildSrc/src/main/kotlin/Publications.kt +++ b/buildSrc/src/main/kotlin/Publications.kt @@ -1,5 +1,5 @@ -import gradle.kotlin.dsl.accessors._87b80c14bf1c4d505c7a71d7741e0994.publishing -import gradle.kotlin.dsl.accessors._87b80c14bf1c4d505c7a71d7741e0994.signing +import gradle.kotlin.dsl.accessors._0942c15ed799f01c8e4bd02858158e54.publishing +import gradle.kotlin.dsl.accessors._0942c15ed799f01c8e4bd02858158e54.signing import groovy.util.Node import org.gradle.api.Project import org.gradle.api.artifacts.Dependency diff --git a/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt b/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt index 42696d6a4..534c2b2d6 100644 --- a/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt +++ b/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt @@ -1,15 +1,12 @@ import org.gradle.api.Project import org.gradle.api.file.DuplicatesStrategy -import org.gradle.api.plugins.ExtensionAware -import org.gradle.api.tasks.SourceSetContainer -import org.gradle.kotlin.dsl.get import java.io.File fun Project.mkSmtLibBenchmarkTestData(name: String) = tasks.register("smtLibBenchmark-$name") { doLast { val path = buildDir.resolve("smtLibBenchmark/$name") val downloadTarget = path.resolve("$name.zip") - val url = "$BENCHMARK_REPO_URL/zip/$name.zip" + val url = "$MK_SMTLIB_BENCHMARK_REPO_URL/zip/$name.zip" download(url, downloadTarget) @@ -36,49 +33,19 @@ fun Project.mkSmtLibBenchmarkTestData(name: String) = tasks.register("smtLibBenc } } -fun Project.usePreparedSmtLibBenchmarkTestData(path: File) = tasks.register("smtLibBenchmark-data-use") { - doLast { - check(path.exists()) { "No test data provided" } - val testResources = testResourceDir() ?: error("No resource directory found for benchmarks") - val testData = testResources.resolve("testData") +fun Project.usePreparedSmtLibBenchmarkTestData(path: File) = + usePreparedBenchmarkTestData(path, SMTLIB_BENCHMARK_NAME_L) - testData.executeIfNotReady("test-data-ready") { - copy { - from(path) - into(testData) - duplicatesStrategy = DuplicatesStrategy.EXCLUDE - } - } - } -} +fun Project.downloadPreparedSmtLibBenchmarkTestData(downloadPath: File, testDataPath: File, testDataRevision: String) = + downloadPreparedBenchmarkTestData( + downloadPath, + testDataPath, + SMTLIB_BENCHMARK_NAME_U, + "https://github.com/UnitTestBot/ksmt/releases/download/$testDataRevision/benchmarks.zip", + ) -fun Project.downloadPreparedSmtLibBenchmarkTestData(downloadPath: File, testDataPath: File, version: String) = - tasks.register("downloadPreparedSmtLibBenchmarkTestData") { - doLast { - val benchmarksUrl = "https://github.com/UnitTestBot/ksmt/releases/download/$version/benchmarks.zip" +private const val MK_SMTLIB_BENCHMARK_REPO_URL = "http://smt-lib.loria.fr" - download(benchmarksUrl, downloadPath) +private const val SMTLIB_BENCHMARK_NAME_U = "SmtLib" - copy { - from(zipTree(downloadPath)) - into(testDataPath) - duplicatesStrategy = DuplicatesStrategy.EXCLUDE - } - } - } - -private fun Project.testResourceDir(): File? { - val sourceSets = (this as ExtensionAware).extensions.getByName("sourceSets") as SourceSetContainer - return sourceSets["test"]?.output?.resourcesDir -} - -private const val BENCHMARK_REPO_URL = "http://smt-lib.loria.fr" - -private inline fun File.executeIfNotReady(markerName: String, body: () -> Unit) { - val marker = this.resolve(markerName) - if (marker.exists()) return - - body() - - marker.createNewFile() -} +private const val SMTLIB_BENCHMARK_NAME_L = "smtLib" diff --git a/ksmt-maxsmt-test/build.gradle.kts b/ksmt-maxsmt-test/build.gradle.kts new file mode 100644 index 000000000..728218844 --- /dev/null +++ b/ksmt-maxsmt-test/build.gradle.kts @@ -0,0 +1,98 @@ +import org.jetbrains.kotlin.konan.properties.loadProperties + +plugins { + id("io.ksmt.ksmt-base") +} + +repositories { + mavenCentral() +} + +val versions = loadProperties(projectDir.parentFile.resolve("version.properties").absolutePath) + +dependencies { + implementation(project(":ksmt-core")) + implementation(project(":ksmt-maxsmt")) + + testImplementation("org.junit.jupiter:junit-jupiter-api:${versions["junit-jupiter"]}") + testImplementation("org.junit.jupiter:junit-jupiter-params:${versions["junit-jupiter"]}") + + testImplementation(project(":ksmt-z3")) + testImplementation(project(":ksmt-bitwuzla")) + testImplementation(project(":ksmt-cvc5")) + testImplementation(project(":ksmt-yices")) + testImplementation(project(":ksmt-symfpu")) + + testImplementation(project(":ksmt-test")) + testImplementation(project(":ksmt-runner")) + + testImplementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:${versions["kotlinx-coroutines"]}") + + testImplementation("io.github.oshai:kotlin-logging-jvm:${versions["kotlin-logging-jvm"]}") + testImplementation("org.slf4j:slf4j-log4j12:${versions["slf4j-log4j12"]}") + + testImplementation("com.google.code.gson:gson:${versions["gson"]}") +} + +val maxSmtBenchmarks = listOfNotNull( + "QF_ABV-light", // 2.56M + "QF_ABVFP-light", // 650K + "QF_AUFBV", // 233K + "QF_AUFBVLIA-light", // 3.8M + "QF_AUFLIA", // 244K + "QF_BV-light", // 8.55M + "QF_FP", // 250K + "QF_UF-light", // 3.79M + "QF_UFBV-light", // 6.27M + "QF_UFLIA-light", // 488K + "QF_UFLRA-light", // 2.23M +) + +val maxSatBenchmarks = listOfNotNull( + "maxsat-benchmark-1", // 48.6M + "maxsat-benchmark-2", // 34.1M + "maxsat-benchmark-3", // 56.8M + "maxsat-benchmark-4", // 17.2M + "maxsat-benchmark-5", // 90.4M + "maxsat-benchmark-6", // 37.9M +) + +val runMaxSmtBenchmarkTests = project.booleanProperty("runMaxSmtBenchmarkTests") ?: false +val runMaxSatBenchmarkTests = project.booleanProperty("runMaxSatBenchmarkTests") ?: false + +// Use benchmarks from maxSmtBenchmark directory (test resources) instead of downloading +val usePreparedBenchmarks = project.booleanProperty("usePreparedBenchmarks") ?: true + +val testDataRevision = project.stringProperty("testDataRevision") ?: "0.0.0" + +val downloadPreparedMaxSmtBenchmarkTestData = + maxSmtBenchmarks.map { maxSmtBenchmarkTestData(it, testDataRevision) } + +val prepareMaxSmtTestData by tasks.registering { + tasks.withType().forEach { it.enabled = false } + if (!usePreparedBenchmarks) { + dependsOn.addAll(downloadPreparedMaxSmtBenchmarkTestData) + } +} + +tasks.withType { + if (runMaxSmtBenchmarkTests) { + dependsOn.add(prepareMaxSmtTestData) + } +} + +val downloadPreparedMaxSatBenchmarkTestData = + maxSatBenchmarks.map { maxSatBenchmarkTestData(it, testDataRevision) } + +val prepareMaxSatTestData by tasks.registering { + tasks.withType().forEach { it.enabled = false } + if (!usePreparedBenchmarks) { + dependsOn.addAll(downloadPreparedMaxSatBenchmarkTestData) + } +} + +tasks.withType { + if (runMaxSatBenchmarkTests) { + dependsOn.add(prepareMaxSatTestData) + } +} diff --git a/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/CurrentLineState.kt b/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/CurrentLineState.kt new file mode 100644 index 000000000..3dea1d4ab --- /dev/null +++ b/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/CurrentLineState.kt @@ -0,0 +1,8 @@ +package io.ksmt.solver.maxsmt.test + +enum class CurrentLineState { + COMMENT, + HARD_CONSTRAINT, + SOFT_CONSTRAINT, + ERROR, +} diff --git a/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/MaxSMTTestInfo.kt b/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/MaxSMTTestInfo.kt new file mode 100644 index 000000000..ad6bfee68 --- /dev/null +++ b/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/MaxSMTTestInfo.kt @@ -0,0 +1,7 @@ +package io.ksmt.solver.maxsmt.test + +data class MaxSMTTestInfo( + val softConstraintsWeights: List, + val softConstraintsWeightsSum: ULong, + val satSoftConstraintsWeightsSum: ULong +) diff --git a/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/TestParser.kt b/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/TestParser.kt new file mode 100644 index 000000000..e803284f0 --- /dev/null +++ b/ksmt-maxsmt-test/src/main/kotlin/io/ksmt/solver/maxsmt/test/TestParser.kt @@ -0,0 +1,112 @@ +package io.ksmt.solver.maxsmt.test + +import io.ksmt.KContext +import io.ksmt.solver.maxsmt.constraints.Constraint +import io.ksmt.solver.maxsmt.constraints.HardConstraint +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.utils.mkConst +import java.io.File +import java.nio.file.Path +import kotlin.io.path.extension +import kotlin.io.path.notExists + +fun parseMaxSMTTestInfo(path: Path): MaxSMTTestInfo { + if (path.notExists()) { + error("Path [$path] does not exist") + } + + require(path.extension == "maxsmt") { + "File extension cannot be '${path.extension}' as it must be 'maxsmt'" + } + + var softConstraintsWeights = listOf() + var softConstraintsWeightsSum = 0uL + var satSoftConstraintsWeightsSum = 0uL + + File(path.toUri()).forEachLine { str -> + when { + str.startsWith("soft_constraints_weights: ") -> { + softConstraintsWeights = str + .removePrefix("soft_constraints_weights: ") + .split(" ") + .map { it.toUInt() } + } + + str.startsWith("soft_constraints_weights_sum: ") -> { + softConstraintsWeightsSum = str.removePrefix("soft_constraints_weights_sum: ").toULong() + } + + str.startsWith("sat_soft_constraints_weights_sum: ") -> { + satSoftConstraintsWeightsSum = str.removePrefix("sat_soft_constraints_weights_sum: ").toULong() + } + } + } + + return MaxSMTTestInfo(softConstraintsWeights, softConstraintsWeightsSum, satSoftConstraintsWeightsSum) +} + +fun parseMaxSATTest(path: Path, ctx: KContext): List { + if (path.notExists()) { + error("Path [$path] does not exist") + } + + require(path.extension == "wcnf") { + "File extension cannot be '${path.extension}' as it must be 'wcnf'" + } + + var currentState: CurrentLineState + + val constraints = mutableListOf() + + File(path.toUri()).forEachLine { wcnfStr -> + currentState = when { + wcnfStr.startsWith("c") -> CurrentLineState.COMMENT + wcnfStr.startsWith("h ") -> CurrentLineState.HARD_CONSTRAINT + wcnfStr.substringBefore(" ").toUIntOrNull() != null -> CurrentLineState.SOFT_CONSTRAINT + else -> CurrentLineState.ERROR + } + + if (currentState == CurrentLineState.ERROR) { + error("Unexpected string:\n\"$wcnfStr\"") + } + + if (currentState == CurrentLineState.HARD_CONSTRAINT || currentState == CurrentLineState.SOFT_CONSTRAINT) { + val constraintBeginIndex = getConstraintBeginIndex(currentState, wcnfStr) + val constraintEndIndex = wcnfStr.lastIndex - 1 + + // We do not take the last element in the string as this is a zero indicating the constraint end. + val constraintStr = wcnfStr.substring(constraintBeginIndex, constraintEndIndex) + val constraintStrSplit = constraintStr.split(" ").filterNot { it.isEmpty() } + val constraintIntVars = constraintStrSplit.map { x -> x.toInt() } + + with(ctx) { + val constraintVars = constraintIntVars.map { + if (it < 0) { + !ctx.boolSort.mkConst("${-it}") + } else if (it > 0) { + ctx.boolSort.mkConst("$it") + } else { + error("Map element should not be 0!") + } + } + + val constraint = constraintVars.reduce { x, y -> x or y } + + if (currentState == CurrentLineState.HARD_CONSTRAINT) { + constraints.add(HardConstraint(constraint)) + } else { + val weight = wcnfStr.substringBefore(" ").toUInt() + constraints.add(SoftConstraint(constraint, weight)) + } + } + } + } + + return constraints +} + +private fun getConstraintBeginIndex(currentState: CurrentLineState, str: String): Int = when (currentState) { + CurrentLineState.HARD_CONSTRAINT -> 2 + CurrentLineState.SOFT_CONSTRAINT -> str.substringBefore(" ").length + 1 + else -> error("Unexpected value: [$currentState]") +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/KMaxSMTBenchmarkBasedTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/KMaxSMTBenchmarkBasedTest.kt new file mode 100644 index 000000000..ffe519734 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/KMaxSMTBenchmarkBasedTest.kt @@ -0,0 +1,48 @@ +package io.ksmt.solver.maxsmt.test + +import org.junit.jupiter.params.provider.Arguments +import java.nio.file.Path +import java.nio.file.Paths + +interface KMaxSMTBenchmarkBasedTest { + data class BenchmarkTestArguments( + val name: String, + val samplePath: Path, + ) : Arguments { + override fun get() = arrayOf(name, samplePath) + } + + companion object { + private fun testDataLocation(): Path = + this::class.java.classLoader.getResource("maxSmtBenchmark")?.toURI() + ?.let { Paths.get(it) } + ?: error("No test data") + + private fun prepareTestData(extension: String): List { + val testDataLocation = testDataLocation() + return testDataLocation.toFile().walkTopDown() + .filter { f -> f.isFile && (f.extension == extension) }.toList() + .sorted() + .map { + BenchmarkTestArguments( + it.relativeTo(testDataLocation.toFile()).toString(), + it.toPath(), + ) + } + } + + private val maxSmtTestData by lazy { + prepareTestData("smt2") + } + + @JvmStatic + fun maxSMTTestData() = maxSmtTestData + + private val maxSatTestData by lazy { + prepareTestData("wcnf") + } + + @JvmStatic + fun maxSATTestData() = maxSatTestData + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes2SMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes2SMTBenchmarkTest.kt new file mode 100644 index 000000000..eb3b5cbf6 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes2SMTBenchmarkTest.kt @@ -0,0 +1,27 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.subopt.KSubOptMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KDualMaxRes2SMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(preferLargeWeightConstraintsForCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} + +class KSubOptDualMaxRes2SMTBenchmarkTest : KSubOptMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(preferLargeWeightConstraintsForCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes3SMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes3SMTBenchmarkTest.kt new file mode 100644 index 000000000..ba96c94a4 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes3SMTBenchmarkTest.kt @@ -0,0 +1,27 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.subopt.KSubOptMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KDualMaxRes3SMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(minimizeCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} + +class KSubOptDualMaxRes3SMTBenchmarkTest : KSubOptMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(minimizeCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes4SMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes4SMTBenchmarkTest.kt new file mode 100644 index 000000000..dff5c4953 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxRes4SMTBenchmarkTest.kt @@ -0,0 +1,27 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.subopt.KSubOptMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KDualMaxRes4SMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(getMultipleCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} + +class KSubOptDualMaxRes4SMTBenchmarkTest : KSubOptMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(getMultipleCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxResSMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxResSMTBenchmarkTest.kt new file mode 100644 index 000000000..8daccf61e --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KDualMaxResSMTBenchmarkTest.kt @@ -0,0 +1,17 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KDualMaxResSMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext() + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPMResSMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPMResSMTBenchmarkTest.kt new file mode 100644 index 000000000..5bd24d53f --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPMResSMTBenchmarkTest.kt @@ -0,0 +1,18 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KPMResSMTBenchmarkTest : KMaxSMTBenchmarkTest() { + // TODO: in fact for KPMRes we don't need MaxSMTContext. + override val maxSmtCtx = KMaxSMTContext() + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PMRES, smtSolver) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes2SMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes2SMTBenchmarkTest.kt new file mode 100644 index 000000000..48d49a22e --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes2SMTBenchmarkTest.kt @@ -0,0 +1,34 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalMaxRes +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.subopt.KSubOptMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KPrimalMaxRes2SMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext( + strategy = PrimalMaxRes, + preferLargeWeightConstraintsForCores = true, + ) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} + +class KSubOptPrimalMaxRes2SMTBenchmarkTest : KSubOptMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext( + strategy = PrimalMaxRes, + preferLargeWeightConstraintsForCores = true, + ) + + override fun getSolver(solver: Solver): KMaxSMTSolverInterface { + val smtSolver = getSmtSolver(solver) + return getMaxSmtSolver(MaxSmtSolver.PRIMAL_DUAL_MAXRES, smtSolver) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes3SMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes3SMTBenchmarkTest.kt new file mode 100644 index 000000000..ac8cced78 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes3SMTBenchmarkTest.kt @@ -0,0 +1,18 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalMaxRes +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KPrimalMaxRes3SMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(strategy = PrimalMaxRes, minimizeCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverBase = with(ctx) { + val smtSolver = getSmtSolver(solver) + return KPrimalDualMaxResSolver(this, smtSolver, maxSmtCtx) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes4SMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes4SMTBenchmarkTest.kt new file mode 100644 index 000000000..150af5018 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxRes4SMTBenchmarkTest.kt @@ -0,0 +1,18 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalMaxRes +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KPrimalMaxRes4SMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(strategy = PrimalMaxRes, getMultipleCores = true) + + override fun getSolver(solver: Solver): KMaxSMTSolverBase = with(ctx) { + val smtSolver = getSmtSolver(solver) + return KPrimalDualMaxResSolver(this, smtSolver, maxSmtCtx) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxResSMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxResSMTBenchmarkTest.kt new file mode 100644 index 000000000..1f002eff1 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/KPrimalMaxResSMTBenchmarkTest.kt @@ -0,0 +1,18 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalMaxRes +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.maxsmt.test.smt.KMaxSMTBenchmarkTest +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KPrimalMaxResSMTBenchmarkTest : KMaxSMTBenchmarkTest() { + override val maxSmtCtx = KMaxSMTContext(strategy = PrimalMaxRes) + + override fun getSolver(solver: Solver): KMaxSMTSolverBase = with(ctx) { + val smtSolver = getSmtSolver(solver) + return KPrimalDualMaxResSolver(this, smtSolver, KMaxSMTContext(strategy = PrimalMaxRes)) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/Z3NativeSMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/Z3NativeSMTBenchmarkTest.kt new file mode 100644 index 000000000..bd3c5010c --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/configurations/Z3NativeSMTBenchmarkTest.kt @@ -0,0 +1,5 @@ +package io.ksmt.solver.maxsmt.test.configurations + +import io.ksmt.solver.maxsmt.test.z3.KZ3NativeMaxSMTBenchmarkTest + +class Z3NativeSMTBenchmarkTest : KZ3NativeMaxSMTBenchmarkTest() \ No newline at end of file diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KMaxSATBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KMaxSATBenchmarkTest.kt new file mode 100644 index 000000000..32bc88226 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KMaxSATBenchmarkTest.kt @@ -0,0 +1,487 @@ +package io.ksmt.solver.maxsmt.test.sat + +import io.ksmt.KContext +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus.SAT +import io.ksmt.solver.bitwuzla.KBitwuzlaSolver +import io.ksmt.solver.cvc5.KCvc5Solver +import io.ksmt.solver.maxsmt.constraints.HardConstraint +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.test.KMaxSMTBenchmarkBasedTest +import io.ksmt.solver.maxsmt.test.parseMaxSATTest +import io.ksmt.solver.maxsmt.test.utils.Solver +import io.ksmt.solver.yices.KYicesSolver +import io.ksmt.solver.z3.KZ3Solver +import org.junit.jupiter.api.AfterEach +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.MethodSource +import java.nio.file.Path +import kotlin.io.path.name +import kotlin.test.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +abstract class KMaxSATBenchmarkTest : KMaxSMTBenchmarkBasedTest { + protected fun getSmtSolver(solver: Solver): KSolver = with(ctx) { + return when (solver) { + Solver.Z3 -> KZ3Solver(this) + Solver.BITWUZLA -> KBitwuzlaSolver(this) + Solver.CVC5 -> KCvc5Solver(this) + Solver.YICES -> KYicesSolver(this) + Solver.PORTFOLIO -> + throw NotImplementedError("Portfolio solver for MaxSAT is not supported in tests") + + Solver.Z3_NATIVE -> error("Unexpected solver type: Z3_NATIVE") + } + } + + abstract fun getSolver(solver: Solver): KMaxSMTSolverBase + + protected val ctx: KContext = KContext() + private lateinit var maxSATSolver: KMaxSMTSolverBase + + private fun initSolver(solver: Solver) { + maxSATSolver = getSolver(solver) + } + + @AfterEach + fun closeSolver() = maxSATSolver.close() + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSATTestData") + fun maxSATZ3Test(name: String, samplePath: Path) { + testMaxSATSolver(name, samplePath, Solver.Z3) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSATTestData") + fun maxSATBitwuzlaTest(name: String, samplePath: Path) { + testMaxSATSolver(name, samplePath, Solver.BITWUZLA) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSATTestData") + fun maxSATCvc5Test(name: String, samplePath: Path) { + testMaxSATSolver(name, samplePath, Solver.CVC5) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSATTestData") + fun maxSATYicesTest(name: String, samplePath: Path) { + testMaxSATSolver(name, samplePath, Solver.YICES) + } + + private fun testMaxSATSolver(name: String, samplePath: Path, solver: Solver) = with(ctx) { + val testData = maxSATTestNameToExpectedResult.find { it.first == samplePath.name } + require(testData != null) { "Test [$name] expected result must be specified" } + + val constraints = parseMaxSATTest(samplePath, this) + + var sumOfSoftConstraintsWeights = 0uL + + initSolver(solver) + + constraints.forEach { + if (it is HardConstraint) { + maxSATSolver.assert(it.expression) + } else { + maxSATSolver.assertSoft(it.expression, (it as SoftConstraint).weight) + sumOfSoftConstraintsWeights += it.weight + } + } + + val maxSATResult = maxSATSolver.checkMaxSMT(420.seconds) + val satConstraintsScore = maxSATResult.satSoftConstraints.sumOf { it.weight.toULong() } + val expectedSatConstraintsScore = + sumOfSoftConstraintsWeights - maxSATTestNameToExpectedResult.first { it.first == samplePath.name }.second + + assertEquals(SAT, maxSATResult.hardConstraintsSatStatus, "Hard constraints must be SAT") + assertTrue( + !maxSATResult.timeoutExceededOrUnknown, "Timeout exceeded, solver returned UNKNOWN" + + "or something else happened [$name]" + ) + assertTrue(maxSATResult.satSoftConstraints.isNotEmpty(), "Soft constraints size should not be 0") + assertEquals( + expectedSatConstraintsScore, + satConstraintsScore, + "Soft constraints score was [$satConstraintsScore], " + + "but must be [$expectedSatConstraintsScore]", + ) + } + + // Elements are pairs of test name and expected test result (cost equal to the excluded soft constraints sum). + private val maxSATTestNameToExpectedResult = hashSetOf( + "ae_5_20_ibmq-casablanca_7.wcnf" to 15uL, + "af-synthesis_stb_50_20_8.wcnf" to 120uL, + "af-synthesis_stb_50_40_0.wcnf" to 111uL, + "af-synthesis_stb_50_40_8.wcnf" to 117uL, + "af-synthesis_stb_50_60_3.wcnf" to 115uL, + "af-synthesis_stb_50_80_7.wcnf" to 115uL, + "af-synthesis_stb_50_80_8.wcnf" to 116uL, + "af-synthesis_stb_50_100_3.wcnf" to 104uL, + "af-synthesis_stb_50_120_3.wcnf" to 100uL, + "af-synthesis_stb_50_140_1.wcnf" to 127uL, + "af-synthesis_stb_50_140_3.wcnf" to 96uL, + "af-synthesis_stb_50_140_8.wcnf" to 113uL, + "af-synthesis_stb_50_160_5.wcnf" to 113uL, + "af-synthesis_stb_50_180_1.wcnf" to 130uL, + "af-synthesis_stb_50_200_4.wcnf" to 105uL, + "af-synthesis_stb_50_200_5.wcnf" to 102uL, + "af-synthesis_stb_50_200_6.wcnf" to 111uL, + "amazon.dimacs.wcnf" to 113575uL, + "ar-3.wcnf" to 43814uL, + "archlinux.dimacs.wcnf" to 11744uL, + "auc.cat_paths_60_100_0006.txt.wcnf" to 70929uL, + "auc.cat_paths_60_150_0007.txt.wcnf" to 100364uL, + "auc.cat_paths_60_170_0007.txt.wcnf" to 94165uL, + "auc.cat_paths_60_200_0009.txt.wcnf" to 157873uL, + "auc.cat_reg_60_110_0004.txt.wcnf" to 75602uL, + "auc.cat_reg_60_130_0001.txt.wcnf" to 104032uL, + "auc.cat_reg_60_160_0002.txt.wcnf" to 164897uL, + "auc.cat_sched_60_80_0005.txt.wcnf" to 34950uL, + "auc.cat_sched_60_90_0001.txt.wcnf" to 82847uL, + "auc.cat_sched_60_100_0003.txt.wcnf" to 34771uL, + "auc.cat_sched_60_120_0004.txt.wcnf" to 82385uL, + "auc.cat_sched_60_150_0001.txt.wcnf" to 155865uL, + "auc.cat_sched_60_150_0005.txt.wcnf" to 72866uL, + "auc.cat_sched_60_150_0009.txt.wcnf" to 58699uL, + "auc.cat_sched_60_160_0003.txt.wcnf" to 118883uL, + "auc.cat_sched_60_200_0005.txt.wcnf" to 172768uL, + "cap71.wcsp.wcnf" to 9326144uL, + "cap72.wcsp.wcnf" to 9777981uL, + "cap91.wcsp.wcnf" to 7966472uL, + "cap92.wcsp.wcnf" to 8547029uL, + "cap131.wcsp.wcnf" to 7934385uL, + "cap132.wcsp.wcnf" to 8514942uL, + "car.formula_0.8_2021_atleast_15_max-3_reduced_incomplete_adaboost_2.wcnf" to 232uL, + "causal_Meta_7_528.wcnf" to 55120uL, + "causal_n5_i5_N1000_uai13_log_int.wcnf" to 46030289uL, + "causal_n6_i1_N10000_uai14_log_int.wcnf" to 1510725680uL, + "causal_n6_i6_N1000_uai14_log_int.wcnf" to 126257527700uL, + "causal_n7_i8_N10000_uai14_log_int.wcnf" to 11486104693uL, + "causal_n7_i10_N1000_uai14_log_int.wcnf" to 3246397504uL, + "causal_Pigs_6_10000.wcnf" to 25539892uL, + "causal_Statlog_7_752.wcnf" to 380356uL, + "causal_Voting_7_435.wcnf" to 930263uL, + "causal_Water_7_380.wcnf" to 414473uL, + "comp04.wcnf" to 35uL, + "comp06.wcnf" to 27uL, + "CSG40-40-95.wcnf" to 8847uL, + "CSG60-60-88.wcnf" to 7714uL, + "CSGNaive60-60-53.wcnf" to 9829uL, + "CSGNaive70-70-91.wcnf" to 11177uL, + "dblp.dimacs.wcnf" to 25014uL, + "dim.brock800_3.clq.wcnf" to 1079uL, + "dim.c-fat200-1.clq.wcnf" to 14uL, + "dim.c-fat500-1.clq.wcnf" to 10uL, + "dim.san400_0.7_3.clq.wcnf" to 1201uL, + "dir.5.wcsp.dir.wcnf" to 261uL, + "dir.28.wcsp.dir.wcnf" to 270105uL, + "dir.54.wcsp.dir.wcnf" to 37uL, + "dir.404.wcsp.dir.wcnf" to 114uL, + "dir.408.wcsp.dir.wcnf" to 6228uL, + "dir.507.wcsp.dir.wcnf" to 27390uL, + "dir.509.wcsp.dir.wcnf" to 36446uL, + "dir.1403.wcsp.dir.wcnf" to 459246uL, + "dir.1502.wcsp.dir.wcnf" to 28042uL, + "dir.1506.wcsp.dir.wcnf" to 354517uL, + "drmx-am12-outof-40-ecardn-w.wcnf" to 28uL, + "drmx-am12-outof-40-esortn-w.wcnf" to 28uL, + "drmx-am16-outof-45-emtot-w.wcnf" to 29uL, + "drmx-am16-outof-45-eseqc-w.wcnf" to 29uL, + "drmx-am20-outof-50-ekmtot-w.wcnf" to 30uL, + "drmx-am20-outof-50-emtot-w.wcnf" to 30uL, + "drmx-am20-outof-50-eseqc-w.wcnf" to 30uL, + "drmx-am24-outof-55-emtot-w.wcnf" to 31uL, + "drmx-am24-outof-55-etot-w.wcnf" to 31uL, + "drmx-am28-outof-60-emtot-w.wcnf" to 32uL, + "drmx-am28-outof-60-eseqc-w.wcnf" to 32uL, + "drmx-am28-outof-60-etot-w.wcnf" to 32uL, + "drmx-am32-outof-70-ecardn-w.wcnf" to 38uL, + "drmx-am32-outof-70-ekmtot-w.wcnf" to 38uL, + "drmx-am32-outof-70-emtot-w.wcnf" to 38uL, + "drmx-am32-outof-70-etot-w.wcnf" to 38uL, + "eas.310-15.wcnf" to 30501uL, + "eas.310-28.wcnf" to 33151uL, + "eas.310-29.wcnf" to 34431uL, + "eas.310-33.wcnf" to 35463uL, + "eas.310-43.wcnf" to 33138uL, + "eas.310-44.wcnf" to 50871uL, + "eas.310-55.wcnf" to 21952uL, + "eas.310-74.wcnf" to 21867uL, + "eas.310-91.wcnf" to 37183uL, + "eas.310-93.wcnf" to 19146uL, + "eas.310-94.wcnf" to 26160uL, + "eas.310-95.wcnf" to 25854uL, + "eas.310-97.wcnf" to 35249uL, + "ebay.dimacs.wcnf" to 123941uL, + "f1-DataDisplay_0_order4.seq-A-2-1-EDCBAir.wcnf" to 6223203uL, + "f1-DataDisplay_0_order4.seq-A-2-2-abcdeir.wcnf" to 481429uL, + "f1-DataDisplay_0_order4.seq-A-2-2-irabcde.wcnf" to 2220415uL, + "f1-DataDisplay_0_order4.seq-A-3-1-EDCBAir.wcnf" to 6240245uL, + "f1-DataDisplay_0_order4.seq-A-3-1-irabcde.wcnf" to 5960556uL, + "f1-DataDisplay_0_order4.seq-A-3-2-irabcde.wcnf" to 5955300uL, + "f1-DataDisplay_0_order4.seq-B-2-2-abcdeir.wcnf" to 53533uL, + "f1-DataDisplay_0_order4.seq-B-2-2-irEDCBA.wcnf" to 2273346uL, + "f49-DC_TotalLoss.seq-A-2-1-abcdeir.wcnf" to 27698412327uL, + "f49-DC_TotalLoss.seq-A-2-1-irEDCBA.wcnf" to 14779649425uL, + "f49-DC_TotalLoss.seq-A-2-combined-irabcde.wcnf" to 14735114187uL, + "f49-DC_TotalLoss.seq-A-3-2-irEDCBA.wcnf" to 87222797189uL, + "f49-DC_TotalLoss.seq-B-2-2-abcdeir.wcnf" to 44321234uL, + "f49-DC_TotalLoss.seq-B-2-combined-EDCBAir.wcnf" to 83838199998uL, + "f49-DC_TotalLoss.seq-B-3-combined-EDCBAir.wcnf" to 117355113043uL, + "f49-DC_TotalLoss.seq-B-3-combined-irabcde.wcnf" to 87177360578uL, + "facebook1.dimacs.wcnf" to 45581uL, + "github.dimacs.wcnf" to 187405uL, + "graphstate_6_6_rigetti-agave_8.wcnf" to 6uL, + "grover-noancilla_4_52_rigetti-agave_8.wcnf" to 42uL, + "grover-v-chain_4_52_ibmq-casablanca_7.wcnf" to 27uL, + "guardian.dimacs.wcnf" to 160777uL, + "inst2.lp.sm-extracted.wcnf" to 97uL, + "inst10.lp.sm-extracted.wcnf" to 105uL, + "inst22.lp.sm-extracted.wcnf" to 180uL, + "instance1.wcnf" to 607uL, + "instance2.wcnf" to 828uL, + "ItalyInstance1.xml.wcnf" to 12uL, + "k50-18-30.rna.pre.wcnf" to 462uL, + "k50-21-38.rna.pre.wcnf" to 497uL, + "k100-14-38.rna.pre.wcnf" to 1953uL, + "k100-20-63.rna.pre.wcnf" to 2030uL, + "k100-38-60.rna.pre.wcnf" to 1878uL, + "k100-40-52.rna.pre.wcnf" to 1861uL, + "k100-73-76.rna.pre.wcnf" to 2008uL, + "k100-78-85.rna.pre.wcnf" to 1744uL, + "lisbon-wedding-1-18.wcnf" to 961uL, + "lisbon-wedding-2-18.wcnf" to 1137uL, + "lisbon-wedding-3-17.wcnf" to 1035uL, + "lisbon-wedding-4-18.wcnf" to 803uL, + "lisbon-wedding-5-17.wcnf" to 802uL, + "lisbon-wedding-9-17.wcnf" to 394uL, + "lisbon-wedding-10-17.wcnf" to 377uL, + "log.8.wcsp.log.wcnf" to 2uL, + "log.28.wcsp.log.wcnf" to 270105uL, + "log.408.wcsp.log.wcnf" to 6228uL, + "log.505.wcsp.log.wcnf" to 21253uL, + "log.1401.wcsp.log.wcnf" to 459106uL, + "londonist.dimacs.wcnf" to 70703uL, + "metro_8_8_5_20_10_6_500_1_0.lp.sm-extracted.wcnf" to 82uL, + "metro_8_8_5_20_10_6_500_1_7.lp.sm-extracted.wcnf" to 89uL, + "metro_8_8_5_20_10_6_500_1_9.lp.sm-extracted.wcnf" to 105uL, + "metro_9_8_7_22_10_6_500_1_1.lp.sm-extracted.wcnf" to 52uL, + "metro_9_8_7_22_10_6_500_1_2.lp.sm-extracted.wcnf" to 60uL, + "metro_9_8_7_22_10_6_500_1_3.lp.sm-extracted.wcnf" to 44uL, + "metro_9_8_7_30_10_6_500_1_5.lp.sm-extracted.wcnf" to 47uL, + "metro_9_8_7_30_10_6_500_1_6.lp.sm-extracted.wcnf" to 31uL, + "metro_9_8_7_30_10_6_500_1_7.lp.sm-extracted.wcnf" to 47uL, + "metro_9_8_7_30_10_6_500_1_8.lp.sm-extracted.wcnf" to 55uL, + "metro_9_9_10_35_13_7_500_2_7.lp.sm-extracted.wcnf" to 37uL, + "MinWidthCB_milan_100_12_1k_1s_2t_3.wcnf" to 109520uL, + "MinWidthCB_milan_200_12_1k_4s_1t_4.wcnf" to 108863uL, + "MinWidthCB_mitdbsample_100_43_1k_2s_2t_2.wcnf" to 38570uL, + "MinWidthCB_mitdbsample_100_64_1k_2s_1t_2.wcnf" to 66045uL, + "MinWidthCB_mitdbsample_200_43_1k_2s_2t_2.wcnf" to 50615uL, + "MinWidthCB_mitdbsample_200_64_1k_2s_1t_2.wcnf" to 78400uL, + "MinWidthCB_mitdbsample_200_64_1k_2s_3t_2.wcnf" to 73730uL, + "MinWidthCB_mitdbsample_300_26_1k_3s_2t_3.wcnf" to 32420uL, + "MLI.ilpd_train_0_DNF_5_5.wcnf" to 700uL, + "mul.role_smallcomp_multiple_0.3_6.wcnf" to 139251uL, + "mul.role_smallcomp_multiple_1.0_6.wcnf" to 295598uL, + "openstreetmap.dimacs.wcnf" to 65915uL, + "pac.80cfe9a6-9b1b-11df-965e-00163e46d37a_l1.wcnf" to 1924238uL, + "pac.fa3d0fb2-db9e-11df-a0ec-00163e3d3b7c_l1.wcnf" to 4569599uL, + "pac.rand179_l1.wcnf" to 493118uL, + "pac.rand892_l1.wcnf" to 224702uL, + "pac.rand984_l1.wcnf" to 345082uL, + "ped2.B.recomb1-0.01-2.wcnf" to 7uL, + "ped2.B.recomb1-0.10-7.wcnf" to 588uL, + "ped3.D.recomb10-0.20-12.wcnf" to 349uL, + "ped3.D.recomb10-0.20-14.wcnf" to 7uL, + "portfoliovqe_4_18_rigetti-agave_8.wcnf" to 33uL, + "power-distribution_1_2.wcnf" to 3uL, + "power-distribution_1_4.wcnf" to 3uL, + "power-distribution_1_6.wcnf" to 3uL, + "power-distribution_1_8.wcnf" to 3uL, + "power-distribution_2_2.wcnf" to 10uL, + "power-distribution_2_8.wcnf" to 10uL, + "power-distribution_3_4.wcnf" to 1uL, + "power-distribution_7_6.wcnf" to 18uL, + "power-distribution_8_4.wcnf" to 40uL, + "power-distribution_8_7.wcnf" to 40uL, + "power-distribution_9_2.wcnf" to 18uL, + "power-distribution_11_6.wcnf" to 126uL, + "power-distribution_12_2.wcnf" to 216uL, + "power-distribution_12_5.wcnf" to 216uL, + "qaoa_4_16_ibmq-casablanca_7.wcnf" to 12uL, + "qft_5_26_ibmq-casablanca_7.wcnf" to 15uL, + "qftentangled_4_21_ibmq-casablanca_7.wcnf" to 15uL, + "qftentangled_4_39_rigetti-agave_8.wcnf" to 18uL, + "qftentangled_5_30_ibmq-london_5.wcnf" to 27uL, + "qftentangled_5_48_rigetti-agave_8.wcnf" to 24uL, + "qgan_6_15_ibmq-casablanca_7.wcnf" to 24uL, + "qpeexact_5_26_ibmq-casablanca_7.wcnf" to 15uL, + "qwalk-v-chain_3_30_ibmq-casablanca_7.wcnf" to 30uL, + "qwalk-v-chain_5_102_ibmq-london_5.wcnf" to 81uL, + "rail507.wcnf" to 174uL, + "rail516.wcnf" to 182uL, + "rail582.wcnf" to 211uL, + "ran.max_cut_60_420_2.asc.wcnf" to 703uL, + "ran.max_cut_60_420_5.asc.wcnf" to 715uL, + "ran.max_cut_60_420_9.asc.wcnf" to 674uL, + "ran.max_cut_60_500_2.asc.wcnf" to 900uL, + "ran.max_cut_60_560_3.asc.wcnf" to 1054uL, + "ran.max_cut_60_560_7.asc.wcnf" to 1053uL, + "ran.max_cut_60_600_1.asc.wcnf" to 1156uL, + "ran.max_cut_60_600_9.asc.wcnf" to 1149uL, + "random-dif-2.rna.pre.wcnf" to 929uL, + "random-dif-9.rna.pre.wcnf" to 456uL, + "random-dif-16.rna.pre.wcnf" to 768uL, + "random-dif-25.rna.pre.wcnf" to 512uL, + "random-net-20-5_network-4.net.wcnf" to 19602uL, + "random-net-30-3_network-2.net.wcnf" to 27606uL, + "random-net-30-4_network-3.net.wcnf" to 24925uL, + "random-net-40-2_network-8.net.wcnf" to 38289uL, + "random-net-40-2_network-9.net.wcnf" to 35951uL, + "random-net-40-3_network-5.net.wcnf" to 35488uL, + "random-net-40-4_network-2.net.wcnf" to 36427uL, + "random-net-50-3_network-5.net.wcnf" to 41356uL, + "random-net-50-4_network-8.net.wcnf" to 43243uL, + "random-net-60-3_network-3.net" to 50929uL, + "random-net-100-1_network-3.net.wcnf" to 91570uL, + "random-net-120-1_network-5.net.wcnf" to 117198uL, + "random-net-220-1_network-7.net.wcnf" to 203783uL, + "random-net-240-1_network-7.net.wcnf" to 219252uL, + "random-net-260-1_network-4.net.wcnf" to 238131uL, + "random-same-5.rna.pre.wcnf" to 456uL, + "random-same-12.rna.pre.wcnf" to 597uL, + "random-same-19.rna.pre.wcnf" to 337uL, + "random-same-25.rna.pre.wcnf" to 224uL, + "ran-scp.scp41_weighted.wcnf" to 429uL, + "ran-scp.scp48_weighted.wcnf" to 492uL, + "ran-scp.scp49_weighted.wcnf" to 641uL, + "ran-scp.scp51_weighted.wcnf" to 253uL, + "ran-scp.scp54_weighted.wcnf" to 242uL, + "ran-scp.scp56_weighted.wcnf" to 213uL, + "ran-scp.scp58_weighted.wcnf" to 288uL, + "ran-scp.scp65_weighted.wcnf" to 161uL, + "ran-scp.scp410_weighted.wcnf" to 514uL, + "ran-scp.scpnre5_weighted.wcnf" to 28uL, + "ran-scp.scpnrf1_weighted.wcnf" to 14uL, + "ran-scp.scpnrf4_weighted.wcnf" to 14uL, + "ran-scp.scpnrf5_weighted.wcnf" to 13uL, + "realamprandom_4_72_rigetti-agave_8.wcnf" to 36uL, + "role_smallcomp_0.7_11.wcnf" to 333834uL, + "role_smallcomp_0.75_8.wcnf" to 348219uL, + "role_smallcomp_0.85_4.wcnf" to 369639uL, + "role_smallcomp_0.85_7.wcnf" to 369639uL, + "Rounded_BTWBNSL_asia_100_1_3.scores_TWBound_2.wcnf" to 24564427uL, + "Rounded_BTWBNSL_asia_100_1_3.scores_TWBound_3.wcnf" to 24564427uL, + "Rounded_BTWBNSL_asia_10000_1_3.scores_TWBound_2.wcnf" to 2247208255uL, + "Rounded_BTWBNSL_hailfinder_100_1_3.scores_TWBound_2.wcnf" to 602126938uL, + "Rounded_BTWBNSL_hailfinder_100_1_3.scores_TWBound_3.wcnf" to 601946991uL, + "Rounded_BTWBNSL_Heart.BIC_TWBound_2.wcnf" to 239742296uL, + "Rounded_BTWBNSL_insurance_100_1_3.scores_TWBound_2.wcnf" to 170760179uL, + "Rounded_BTWBNSL_insurance_1000_1_3.scores_TWBound_2.wcnf" to 1389279780uL, + "Rounded_BTWBNSL_insurance_1000_1_3.scores_TWBound_3.wcnf" to 1388734978uL, + "Rounded_BTWBNSL_insurance_1000_1_3.scores_TWBound_4.wcnf" to 1388734978uL, + "Rounded_BTWBNSL_Water_1000_1_2.scores_TWBound_4.wcnf" to 1326306453uL, + "Rounded_CorrelationClustering_Ionosphere_BINARY_N200_D0.200.wcnf" to 4604640uL, + "Rounded_CorrelationClustering_Orl_BINARY_N320_D0.200.wcnf" to 4429109uL, + "Rounded_CorrelationClustering_Protein1_BINARY_N360.wcnf" to 27536228uL, + "Rounded_CorrelationClustering_Protein2_BINARY_N220.wcnf" to 13727551uL, + "Rounded_CorrelationClustering_Protein2_UNARY_N100.wcnf" to 3913145uL, + "simNo_1-s_15-m_50-n_50-fp_0.0001-fn_0.20.wcnf" to 11501657324586uL, + "simNo_2-s_5-m_100-n_100-fp_0.0001-fn_0.05.wcnf" to 99635408482313uL, + "simNo_3-s_5-m_50-n_50-fp_0.0001-fn_0.05.wcnf" to 18938961942919uL, + "simNo_5-s_15-m_100-n_100-fp_0.0001-fn_0.20.wcnf" to 113321765415159uL, + "simNo_6-s_5-m_100-n_50-fp_0.01-fn_0.05.wcnf" to 90981027155327uL, + "simNo_6-s_15-m_100-n_50-fp_0.01-fn_0.05.wcnf" to 60142712649443uL, + "simNo_8-s_5-m_100-n_100-fp_0.0001-fn_0.05.wcnf" to 74156301822200uL, + "simNo_8-s_5-m_100-n_100-fp_0.0001-fn_0.20.wcnf" to 131749300472480uL, + "simNo_9-s_5-m_100-n_100-fp_0.0001-fn_0.05.wcnf" to 131749300472480uL, + "simNo_10-s_15-m_100-n_50-fp_0.01-fn_0.20.wcnf" to 84803002848794uL, + "simNo_10-s_15-m_100-n_100-fp_0.0001-fn_0.20.wcnf" to 82981983123459uL, + "su2random_4_18_ibmq-casablanca_7.wcnf" to 24uL, + "su2random_5_30_ibmq-london_5.wcnf" to 51uL, + "tcp_students_91_it_2.wcnf" to 3024uL, + "tcp_students_91_it_3.wcnf" to 2430uL, + "tcp_students_91_it_6.wcnf" to 2877uL, + "tcp_students_91_it_7.wcnf" to 2505uL, + "tcp_students_91_it_13.wcnf" to 2730uL, + "tcp_students_98_it_8.wcnf" to 2727uL, + "tcp_students_98_it_9.wcnf" to 2469uL, + "tcp_students_98_it_12.wcnf" to 2994uL, + "tcp_students_105_it_7.wcnf" to 3024uL, + "tcp_students_105_it_13.wcnf" to 3360uL, + "tcp_students_105_it_15.wcnf" to 3258uL, + "tcp_students_112_it_1.wcnf" to 3513uL, + "tcp_students_112_it_3.wcnf" to 2916uL, + "tcp_students_112_it_5.wcnf" to 3366uL, + "tcp_students_112_it_7.wcnf" to 3513uL, + "tcp_students_112_it_15.wcnf" to 3585uL, + "test1--n-5000.wcnf" to 20uL, + "test2.wcnf" to 16uL, + "test2--n-5000.wcnf" to 3uL, + "test5--n-5000.wcnf" to 2uL, + "test9--n-5000.wcnf" to 2uL, + "test18--n-5000.wcnf" to 22uL, + "test25--n-10000.wcnf" to 4uL, + "test34--n-10000.wcnf" to 3uL, + "test41--n-15000.wcnf" to 5uL, + "test42--n-15000.wcnf" to 2uL, + "test53--n-15000.wcnf" to 10uL, + "test54--n-15000.wcnf" to 45uL, + "test66--n-20000.wcnf" to 1uL, + "test67--n-20000.wcnf" to 1uL, + "test70--n-20000.wcnf" to 5uL, + "test75--n-20000.wcnf" to 5uL, + "up-.mancoosi-test-i10d0u98-11.wcnf" to 1780771uL, + "up-.mancoosi-test-i10d0u98-16.wcnf" to 1780806uL, + "up-.mancoosi-test-i20d0u98-9.wcnf" to 1780788uL, + "up-.mancoosi-test-i30d0u98-3.wcnf" to 1780860uL, + "up-.mancoosi-test-i40d0u98-7.wcnf" to 1780807uL, + "up-.mancoosi-test-i40d0u98-17.wcnf" to 1780852uL, + "vio.role_smallcomp_violations_0.3_3.wcnf" to 185080uL, + "vio.role_smallcomp_violations_0.45_8.wcnf" to 244141uL, + "vqe_4_12_ibmq-casablanca_7.wcnf" to 15uL, + "vqe_5_20_ibmq-london_5.wcnf" to 33uL, + "warehouse0.wcsp.wcnf" to 328uL, + "warehouse1.wcsp.wcnf" to 730567uL, + "wcn.adult_train_3_DNF_1_5.wcnf" to 24254uL, + "wcn.ilpd_test_8_CNF_4_20.wcnf" to 287uL, + "wcn.ionosphere_train_5_DNF_2_10.wcnf" to 47uL, + "wcn.parkinsons_test_5_CNF_2_10.wcnf" to 58uL, + "wcn.pima_test_3_CNF_1_5.wcnf" to 125uL, + "wcn.tictactoe_test_8_CNF_2_20.wcnf" to 346uL, + "wcn.titanic_test_7_CNF_5_20.wcnf" to 557uL, + "wcn.titanic_test_8_DNF_1_20.wcnf" to 449uL, + "wcn.titanic_train_7_CNF_5_15.wcnf" to 3262uL, + "wcn.titanic_train_8_CNF_5_10.wcnf" to 2201uL, + "wcn.transfusion_test_7_DNF_3_5.wcnf" to 96uL, + "wcn.transfusion_train_2_CNF_5_10.wcnf" to 1600uL, + "wcn.transfusion_train_3_CNF_3_15.wcnf" to 2400uL, + "WCNF_pathways_p01.wcnf" to 2uL, + "WCNF_pathways_p03.wcnf" to 30uL, + "WCNF_pathways_p05.wcnf" to 60uL, + "WCNF_pathways_p06.wcnf" to 64uL, + "WCNF_pathways_p08.wcnf" to 182uL, + "WCNF_pathways_p09.wcnf" to 157uL, + "WCNF_pathways_p10.wcnf" to 129uL, + "WCNF_pathways_p12.wcnf" to 188uL, + "WCNF_pathways_p14.wcnf" to 207uL, + "WCNF_pathways_p16.wcnf" to 257uL, + "WCNF_storage_p02.wcnf" to 5uL, + "WCNF_storage_p06.wcnf" to 173uL, + "wei.SingleDay_3_weighted.wcnf" to 35439uL, + "wei.Subnetwork_7_weighted.wcnf" to 43213uL, + "wei.Subnetwork_9_weighted.wcnf" to 82813uL, + "wikipedia.dimacs.wcnf" to 42676uL, + "wpm.mancoosi-test-i1000d0u98-15.wcnf" to 92031744uL, + "wpm.mancoosi-test-i2000d0u98-25.wcnf" to 332548069uL, + "wpm.mancoosi-test-i3000d0u98-50.wcnf" to 422725765uL, + "wpm.mancoosi-test-i3000d0u98-70.wcnf" to 512958012uL, + "wpm.mancoosi-test-i4000d0u98-76.wcnf" to 738411504uL, + "youtube.dimacs.wcnf" to 227167uL, + ) +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KPMResSATBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KPMResSATBenchmarkTest.kt new file mode 100644 index 000000000..90277789d --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KPMResSATBenchmarkTest.kt @@ -0,0 +1,13 @@ +package io.ksmt.solver.maxsmt.test.sat + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPMResSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KPMResSATBenchmarkTest : KMaxSATBenchmarkTest() { + override fun getSolver(solver: Solver): KMaxSMTSolverBase = with(ctx) { + val smtSolver = getSmtSolver(solver) + return KPMResSolver(this, smtSolver) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KPrimalDualMaxResSATBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KPrimalDualMaxResSATBenchmarkTest.kt new file mode 100644 index 000000000..4358d7eaa --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/sat/KPrimalDualMaxResSATBenchmarkTest.kt @@ -0,0 +1,17 @@ +package io.ksmt.solver.maxsmt.test.sat + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.maxsmt.test.utils.Solver + +class KPrimalDualMaxResSATBenchmarkTest : KMaxSATBenchmarkTest() { + override fun getSolver(solver: Solver): KMaxSMTSolverBase = with(ctx) { + val smtSolver = getSmtSolver(solver) + return KPrimalDualMaxResSolver( + this, smtSolver, + KMaxSMTContext(preferLargeWeightConstraintsForCores = true) + ) + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/smt/KMaxSMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/smt/KMaxSMTBenchmarkTest.kt new file mode 100644 index 000000000..b658a1576 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/smt/KMaxSMTBenchmarkTest.kt @@ -0,0 +1,337 @@ +package io.ksmt.solver.maxsmt.test.smt + +import io.github.oshai.kotlinlogging.KotlinLogging +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.runner.core.KsmtWorkerArgs +import io.ksmt.runner.core.KsmtWorkerFactory +import io.ksmt.runner.core.KsmtWorkerPool +import io.ksmt.runner.core.RdServer +import io.ksmt.runner.core.WorkerInitializationFailedException +import io.ksmt.runner.generated.models.TestProtocolModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus.SAT +import io.ksmt.solver.bitwuzla.KBitwuzlaSolver +import io.ksmt.solver.cvc5.KCvc5Solver +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.solvers.KPMResSolver +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.maxsmt.test.KMaxSMTBenchmarkBasedTest +import io.ksmt.solver.maxsmt.test.parseMaxSMTTestInfo +import io.ksmt.solver.maxsmt.test.statistics.JsonStatisticsHelper +import io.ksmt.solver.maxsmt.test.statistics.MaxSMTTestStatistics +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver +import io.ksmt.solver.maxsmt.test.utils.Solver.BITWUZLA +import io.ksmt.solver.maxsmt.test.utils.Solver.CVC5 +import io.ksmt.solver.maxsmt.test.utils.Solver.PORTFOLIO +import io.ksmt.solver.maxsmt.test.utils.Solver.YICES +import io.ksmt.solver.maxsmt.test.utils.Solver.Z3 +import io.ksmt.solver.maxsmt.test.utils.Solver.Z3_NATIVE +import io.ksmt.solver.maxsmt.test.utils.getRandomString +import io.ksmt.solver.portfolio.KPortfolioSolver +import io.ksmt.solver.portfolio.KPortfolioSolverManager +import io.ksmt.solver.yices.KYicesSolver +import io.ksmt.solver.z3.KZ3Solver +import io.ksmt.sort.KBoolSort +import io.ksmt.test.TestRunner +import io.ksmt.test.TestWorker +import io.ksmt.test.TestWorkerProcess +import kotlinx.coroutines.TimeoutCancellationException +import kotlinx.coroutines.runBlocking +import org.junit.jupiter.api.AfterAll +import org.junit.jupiter.api.AfterEach +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.MethodSource +import java.io.File +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.io.path.extension +import kotlin.system.measureTimeMillis +import kotlin.test.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.minutes +import kotlin.time.Duration.Companion.seconds + +abstract class KMaxSMTBenchmarkTest : KMaxSMTBenchmarkBasedTest { + protected fun getMaxSmtSolver( + maxSmtSolver: MaxSmtSolver, + solver: KSolver + ): KMaxSMTSolverInterface { + when (maxSmtSolver) { + MaxSmtSolver.PMRES -> return KPMResSolver(ctx, solver) + MaxSmtSolver.PRIMAL_DUAL_MAXRES -> { + // Thus, MaxSMT algorithm will be executed in the backend process. + if (solver is KPortfolioSolver) { + return solver + } + return KPrimalDualMaxResSolver(ctx, solver, maxSmtCtx) + } + } + } + + protected fun getSmtSolver(solver: Solver): KSolver = with(ctx) { + return when (solver) { + Z3 -> KZ3Solver(this) + BITWUZLA -> KBitwuzlaSolver(this) + CVC5 -> KCvc5Solver(this) + YICES -> KYicesSolver(this) + PORTFOLIO -> { + solverManager.createPortfolioSolver(this) + } + + Z3_NATIVE -> error("Unexpected solver type: Z3_NATIVE") + } + } + + abstract fun getSolver(solver: Solver): KMaxSMTSolverInterface + + protected val ctx: KContext = KContext() + protected abstract val maxSmtCtx: KMaxSMTContext + private lateinit var maxSMTSolver: KMaxSMTSolverInterface + private val logger = KotlinLogging.logger {} + + private fun initSolver(solver: Solver) { + maxSMTSolver = getSolver(solver) + } + + @AfterEach + fun close() { + maxSMTSolver.close() + ctx.close() + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTZ3Test(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, Z3) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTBitwuzlaTest(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, BITWUZLA) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTCvc5Test(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, CVC5) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTYicesTest(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, YICES) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTPortfolioTest(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, PORTFOLIO) + } + + private fun testMaxSMTSolver( + name: String, + samplePath: Path, + solver: Solver = Z3, + ) { + initSolver(solver) + + val extension = "smt2" + require(samplePath.extension == extension) { + "File extension cannot be '${samplePath.extension}' as it must be $extension" + } + + logger.info { "Test name: [$name]" } + + lateinit var convertedAssertions: List> + val testStatistics = MaxSMTTestStatistics(name, solver) + + try { + testWorkers.withWorker(ctx) { worker -> + val assertions = worker.parseFile(samplePath) + convertedAssertions = worker.convertAssertions(assertions) + } + } catch (ex: IgnoreTestException) { + testStatistics.ignoredTest = true + testStatistics.exceptionMessage = ex.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { ex.message + System.lineSeparator() } + throw ex + } catch (ex: Exception) { + testStatistics.failedOnParsingOrConvertingExpressions = true + testStatistics.exceptionMessage = ex.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { ex.message + System.lineSeparator() } + throw ex + } + + val maxSmtTestPath = File(samplePath.toString().removeSuffix(extension) + "maxsmt").toPath() + val maxSmtTestInfo = parseMaxSMTTestInfo(maxSmtTestPath) + + val softConstraintsSize = maxSmtTestInfo.softConstraintsWeights.size + + val softExpressions = + convertedAssertions.subList(convertedAssertions.size - softConstraintsSize, convertedAssertions.size) + val hardExpressions = convertedAssertions.subList(0, convertedAssertions.size - softConstraintsSize) + + hardExpressions.forEach { + maxSMTSolver.assert(it) + } + + maxSmtTestInfo.softConstraintsWeights + .zip(softExpressions) + .forEach { (weight, expr) -> + maxSMTSolver.assertSoft(expr, weight) + } + + lateinit var maxSMTResult: KMaxSMTResult + val elapsedTime = measureTimeMillis { + try { + maxSMTResult = maxSMTSolver.checkMaxSMT(60.seconds, true) + } catch (ex: Exception) { + testStatistics.maxSMTCallStatistics = maxSMTSolver.collectMaxSMTStatistics() + testStatistics.exceptionMessage = ex.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { ex.message + System.lineSeparator() } + throw ex + } + } + testStatistics.elapsedTimeMs = elapsedTime + + testStatistics.maxSMTCallStatistics = maxSMTSolver.collectMaxSMTStatistics() + testStatistics.timeoutExceededOrUnknown = maxSMTResult.timeoutExceededOrUnknown + + logger.info { "Elapsed time: $elapsedTime ms --- MaxSMT call${System.lineSeparator()}" } + + try { + assertTrue( + !maxSMTResult.timeoutExceededOrUnknown, "MaxSMT was not successful [$name] as timeout" + + "has exceeded, solver was interrupted or returned UNKNOWN" + ) + assertEquals(SAT, maxSMTResult.hardConstraintsSatStatus, "Hard constraints must be SAT") + + val satSoftConstraintsWeightsSum = maxSMTResult.satSoftConstraints.sumOf { it.weight } + if (maxSmtTestInfo.satSoftConstraintsWeightsSum != satSoftConstraintsWeightsSum.toULong()) { + testStatistics.checkedSoftConstraintsSumIsWrong = true + } + assertEquals( + maxSmtTestInfo.satSoftConstraintsWeightsSum, + satSoftConstraintsWeightsSum.toULong(), + "Soft constraints weights sum was [$satSoftConstraintsWeightsSum], " + + "but must be [${maxSmtTestInfo.satSoftConstraintsWeightsSum}]", + ) + testStatistics.passed = true + } catch (ex: Exception) { + logger.error { ex.message + System.lineSeparator() } + } finally { + jsonHelper.appendTestStatisticsToFile(testStatistics) + } + } + + private fun KsmtWorkerPool.withWorker( + ctx: KContext, + body: suspend (TestRunner) -> Unit, + ) = runBlocking { + val worker = try { + getOrCreateFreeWorker() + } catch (ex: WorkerInitializationFailedException) { + logger.error { ex.message + System.lineSeparator() } + ignoreTest { "worker initialization failed -- ${ex.message}" } + } + worker.astSerializationCtx.initCtx(ctx) + worker.lifetime.onTermination { + worker.astSerializationCtx.resetCtx() + } + try { + TestRunner(ctx, TEST_WORKER_SINGLE_OPERATION_TIMEOUT, worker).let { + try { + it.init() + body(it) + } finally { + it.delete() + } + } + } catch (ex: TimeoutCancellationException) { + logger.error { ex.message + System.lineSeparator() } + ignoreTest { "worker timeout -- ${ex.message}" } + } finally { + worker.release() + } + } + + // See [handleIgnoredTests] + private inline fun ignoreTest(message: () -> String?): Nothing { + throw IgnoreTestException(message()) + } + + class IgnoreTestException(message: String?) : Exception(message) + + companion object { + val TEST_WORKER_SINGLE_OPERATION_TIMEOUT = 45.seconds + + internal lateinit var testWorkers: KsmtWorkerPool + private lateinit var jsonHelper: JsonStatisticsHelper + private lateinit var solverManager: KPortfolioSolverManager + + @BeforeAll + @JvmStatic + fun initWorkerPools() { + testWorkers = KsmtWorkerPool( + maxWorkerPoolSize = 1, + workerProcessIdleTimeout = 10.minutes, + workerFactory = object : KsmtWorkerFactory { + override val childProcessEntrypoint = TestWorkerProcess::class + override fun updateArgs(args: KsmtWorkerArgs): KsmtWorkerArgs = args + override fun mkWorker(id: Int, process: RdServer) = TestWorker(id, process) + }, + ) + } + + @AfterAll + @JvmStatic + fun closeWorkerPools() { + testWorkers.terminate() + } + + @BeforeAll + @JvmStatic + fun initSolverManager() { + solverManager = KPortfolioSolverManager( + listOf( + KZ3Solver::class, KBitwuzlaSolver::class, KYicesSolver::class + ) + ) + } + + @AfterAll + @JvmStatic + fun closeSolverManager() { + solverManager.close() + } + + @BeforeAll + @JvmStatic + fun initJsonHelper() { + jsonHelper = + JsonStatisticsHelper( + File( + "${ + Paths.get("").toAbsolutePath() + }/src/test/resources/maxsmt-statistics-${getRandomString(16)}.json", + ), + ) + } + + @AfterAll + @JvmStatic + fun closeJsonHelper() { + jsonHelper.markLastTestStatisticsAsProcessed() + } + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/statistics/JsonStatisticsHelper.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/statistics/JsonStatisticsHelper.kt new file mode 100644 index 000000000..56f2db22e --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/statistics/JsonStatisticsHelper.kt @@ -0,0 +1,37 @@ +package io.ksmt.solver.maxsmt.test.statistics + +import com.google.gson.Gson +import java.io.File + +internal class JsonStatisticsHelper(private val jsonFile: File) { + private var firstMet = false + private var lastMet = false + private val gson = Gson().newBuilder().setPrettyPrinting().create() + + init { + if (!jsonFile.exists()) { + jsonFile.createNewFile() + } + } + + fun appendTestStatisticsToFile(statistics: MaxSMTTestStatistics) { + processBeforeAppending() + jsonFile.appendText(gson.toJson(statistics)) + } + + fun markLastTestStatisticsAsProcessed() { + lastMet = true + jsonFile.appendText("\n]\n}") + } + + private fun processBeforeAppending() { + require(!lastMet) { "It's not allowed to append statistics when the last test is processed" } + + if (firstMet) { + jsonFile.appendText(",") + } else { + jsonFile.appendText("{\n\"TESTS\": [\n") + firstMet = true + } + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/statistics/MaxSMTTestStatistics.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/statistics/MaxSMTTestStatistics.kt new file mode 100644 index 000000000..2b6711f71 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/statistics/MaxSMTTestStatistics.kt @@ -0,0 +1,24 @@ +package io.ksmt.solver.maxsmt.test.statistics + +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics +import io.ksmt.solver.maxsmt.test.utils.Solver + +internal data class MaxSMTTestStatistics(val name: String, var smtSolver: Solver) { + var maxSMTCallStatistics: KMaxSMTStatistics? = null + var passed = false + var ignoredTest = false + var failedOnParsingOrConvertingExpressions = false + var exceptionMessage: String? = null + var elapsedTimeMs: Long = 0 + /** + * It's false when a sum is more than optimal in case of SubOpt + * or is different from expected in case of Opt. + */ + var checkedSoftConstraintsSumIsWrong = false + var optimalWeight: ULong = 0U + var foundSoFarWeight: ULong = 0U + /** + * Shows whether timeout has been exceeded, solver was terminated or returned UNKNOWN. + */ + var timeoutExceededOrUnknown: Boolean = true +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/subopt/KSubOptMaxSMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/subopt/KSubOptMaxSMTBenchmarkTest.kt new file mode 100644 index 000000000..0618467ec --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/subopt/KSubOptMaxSMTBenchmarkTest.kt @@ -0,0 +1,340 @@ +package io.ksmt.solver.maxsmt.test.subopt + +import io.github.oshai.kotlinlogging.KotlinLogging +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.runner.core.KsmtWorkerArgs +import io.ksmt.runner.core.KsmtWorkerFactory +import io.ksmt.runner.core.KsmtWorkerPool +import io.ksmt.runner.core.RdServer +import io.ksmt.runner.core.WorkerInitializationFailedException +import io.ksmt.runner.generated.models.TestProtocolModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus.SAT +import io.ksmt.solver.bitwuzla.KBitwuzlaSolver +import io.ksmt.solver.cvc5.KCvc5Solver +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.solvers.KPMResSolver +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.maxsmt.test.KMaxSMTBenchmarkBasedTest +import io.ksmt.solver.maxsmt.test.parseMaxSMTTestInfo +import io.ksmt.solver.maxsmt.test.statistics.JsonStatisticsHelper +import io.ksmt.solver.maxsmt.test.statistics.MaxSMTTestStatistics +import io.ksmt.solver.maxsmt.test.utils.MaxSmtSolver +import io.ksmt.solver.maxsmt.test.utils.Solver +import io.ksmt.solver.maxsmt.test.utils.Solver.BITWUZLA +import io.ksmt.solver.maxsmt.test.utils.Solver.CVC5 +import io.ksmt.solver.maxsmt.test.utils.Solver.PORTFOLIO +import io.ksmt.solver.maxsmt.test.utils.Solver.YICES +import io.ksmt.solver.maxsmt.test.utils.Solver.Z3 +import io.ksmt.solver.maxsmt.test.utils.Solver.Z3_NATIVE +import io.ksmt.solver.maxsmt.test.utils.getRandomString +import io.ksmt.solver.portfolio.KPortfolioSolver +import io.ksmt.solver.portfolio.KPortfolioSolverManager +import io.ksmt.solver.yices.KYicesSolver +import io.ksmt.solver.z3.KZ3Solver +import io.ksmt.sort.KBoolSort +import io.ksmt.test.TestRunner +import io.ksmt.test.TestWorker +import io.ksmt.test.TestWorkerProcess +import kotlinx.coroutines.TimeoutCancellationException +import kotlinx.coroutines.runBlocking +import org.junit.jupiter.api.AfterAll +import org.junit.jupiter.api.AfterEach +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.MethodSource +import java.io.File +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.io.path.extension +import kotlin.system.measureTimeMillis +import kotlin.test.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.milliseconds +import kotlin.time.Duration.Companion.minutes +import kotlin.time.Duration.Companion.seconds + +abstract class KSubOptMaxSMTBenchmarkTest : KMaxSMTBenchmarkBasedTest { + protected fun getMaxSmtSolver( + maxSmtSolver: MaxSmtSolver, + solver: KSolver + ): KMaxSMTSolverInterface { + when (maxSmtSolver) { + MaxSmtSolver.PMRES -> return KPMResSolver(ctx, solver) + MaxSmtSolver.PRIMAL_DUAL_MAXRES -> { + // Thus, MaxSMT algorithm will be executed in the backend process. + if (solver is KPortfolioSolver) { + return solver + } + return KPrimalDualMaxResSolver(ctx, solver, maxSmtCtx) + } + } + } + + protected fun getSmtSolver(solver: Solver): KSolver = with(ctx) { + return when (solver) { + Z3 -> KZ3Solver(this) + BITWUZLA -> KBitwuzlaSolver(this) + CVC5 -> KCvc5Solver(this) + YICES -> KYicesSolver(this) + PORTFOLIO -> { + solverManager.createPortfolioSolver(this) + } + + Z3_NATIVE -> error("Unexpected solver type: Z3_NATIVE") + } + } + + abstract fun getSolver(solver: Solver): KMaxSMTSolverInterface + + private val ctx: KContext = KContext() + protected abstract val maxSmtCtx: KMaxSMTContext + private lateinit var maxSMTSolver: KMaxSMTSolverInterface + + private val logger = KotlinLogging.logger {} + + private fun initSolver(solver: Solver) { + maxSMTSolver = getSolver(solver) + } + + @AfterEach + fun close() { + maxSMTSolver.close() + ctx.close() + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTZ3Test(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, Z3) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTBitwuzlaTest(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, BITWUZLA) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTCvc5Test(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, CVC5) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTYicesTest(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, YICES) + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTPortfolioTest(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath, PORTFOLIO) + } + + private fun testMaxSMTSolver( + name: String, + samplePath: Path, + solver: Solver = Z3, + ) { + initSolver(solver) + + val extension = "smt2" + require(samplePath.extension == extension) { + "File extension cannot be '${samplePath.extension}' as it must be $extension" + } + + logger.info { "Test name: [$name]" } + + lateinit var convertedAssertions: List> + val testStatistics = MaxSMTTestStatistics(name, solver) + + try { + testWorkers.withWorker(ctx) { worker -> + val assertions = worker.parseFile(samplePath) + convertedAssertions = worker.convertAssertions(assertions) + } + } catch (ex: IgnoreTestException) { + testStatistics.ignoredTest = true + testStatistics.exceptionMessage = ex.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { ex.message + System.lineSeparator() } + throw ex + } catch (ex: Exception) { + testStatistics.failedOnParsingOrConvertingExpressions = true + testStatistics.exceptionMessage = ex.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { ex.message + System.lineSeparator() } + throw ex + } + + val maxSmtTestPath = File(samplePath.toString().removeSuffix(extension) + "maxsmt").toPath() + val maxSmtTestInfo = parseMaxSMTTestInfo(maxSmtTestPath) + + val optimalWeight = maxSmtTestInfo.satSoftConstraintsWeightsSum + testStatistics.optimalWeight = optimalWeight + + val softConstraintsSize = maxSmtTestInfo.softConstraintsWeights.size + + val softExpressions = + convertedAssertions.subList(convertedAssertions.size - softConstraintsSize, convertedAssertions.size) + val hardExpressions = convertedAssertions.subList(0, convertedAssertions.size - softConstraintsSize) + + hardExpressions.forEach { + maxSMTSolver.assert(it) + } + + maxSmtTestInfo.softConstraintsWeights + .zip(softExpressions) + .forEach { (weight, expr) -> + maxSMTSolver.assertSoft(expr, weight) + } + + lateinit var maxSMTResult: KMaxSMTResult + val elapsedTime = measureTimeMillis { + try { + maxSMTResult = maxSMTSolver.checkMaxSMT(500.milliseconds, true) + } catch (ex: Exception) { + testStatistics.maxSMTCallStatistics = maxSMTSolver.collectMaxSMTStatistics() + testStatistics.exceptionMessage = ex.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { ex.message + System.lineSeparator() } + throw ex + } + } + testStatistics.elapsedTimeMs = elapsedTime + testStatistics.timeoutExceededOrUnknown = maxSMTResult.timeoutExceededOrUnknown + + val foundSoFarWeight = maxSMTResult.satSoftConstraints.sumOf { it.weight.toULong() } + testStatistics.foundSoFarWeight = foundSoFarWeight + + testStatistics.maxSMTCallStatistics = maxSMTSolver.collectMaxSMTStatistics() + + logger.info { "Elapsed time: $elapsedTime ms --- SubOpt MaxSMT call${System.lineSeparator()}" } + + try { + assertEquals(SAT, maxSMTResult.hardConstraintsSatStatus, "Hard constraints must be SAT") + + if (foundSoFarWeight > optimalWeight) { + testStatistics.checkedSoftConstraintsSumIsWrong = true + } + assertTrue( + optimalWeight >= foundSoFarWeight, + "Soft constraints weights sum was [$foundSoFarWeight], " + + "but must be no more than [${optimalWeight}]", + ) + + testStatistics.passed = true + } catch (ex: Exception) { + logger.error { ex.message + System.lineSeparator() } + } finally { + jsonHelper.appendTestStatisticsToFile(testStatistics) + } + } + + private fun KsmtWorkerPool.withWorker( + ctx: KContext, + body: suspend (TestRunner) -> Unit, + ) = runBlocking { + val worker = try { + getOrCreateFreeWorker() + } catch (ex: WorkerInitializationFailedException) { + logger.error { ex.message + System.lineSeparator() } + ignoreTest { "worker initialization failed -- ${ex.message}" } + } + worker.astSerializationCtx.initCtx(ctx) + worker.lifetime.onTermination { + worker.astSerializationCtx.resetCtx() + } + try { + TestRunner(ctx, TEST_WORKER_SINGLE_OPERATION_TIMEOUT, worker).let { + try { + it.init() + body(it) + } finally { + it.delete() + } + } + } catch (ex: TimeoutCancellationException) { + logger.error { ex.message + System.lineSeparator() } + ignoreTest { "worker timeout -- ${ex.message}" } + } finally { + worker.release() + } + } + + // See [handleIgnoredTests] + private inline fun ignoreTest(message: () -> String?): Nothing { + throw IgnoreTestException(message()) + } + + class IgnoreTestException(message: String?) : Exception(message) + + companion object { + val TEST_WORKER_SINGLE_OPERATION_TIMEOUT = 45.seconds + + internal lateinit var testWorkers: KsmtWorkerPool + private lateinit var jsonHelper: JsonStatisticsHelper + private lateinit var solverManager: KPortfolioSolverManager + + @BeforeAll + @JvmStatic + fun initWorkerPools() { + testWorkers = KsmtWorkerPool( + maxWorkerPoolSize = 1, + workerProcessIdleTimeout = 10.minutes, + workerFactory = object : KsmtWorkerFactory { + override val childProcessEntrypoint = TestWorkerProcess::class + override fun updateArgs(args: KsmtWorkerArgs): KsmtWorkerArgs = args + override fun mkWorker(id: Int, process: RdServer) = TestWorker(id, process) + }, + ) + } + + @AfterAll + @JvmStatic + fun closeWorkerPools() { + testWorkers.terminate() + } + + @BeforeAll + @JvmStatic + fun initSolverManager() { + solverManager = KPortfolioSolverManager( + listOf( + KZ3Solver::class, KBitwuzlaSolver::class, KYicesSolver::class + ), 2 + ) + } + + @AfterAll + @JvmStatic + fun closeSolverManager() { + solverManager.close() + } + + @BeforeAll + @JvmStatic + fun initJsonHelper() { + jsonHelper = + JsonStatisticsHelper( + File( + "${ + Paths.get("").toAbsolutePath() + }/src/test/resources/maxsmt-statistics-${getRandomString(16)}.json", + ), + ) + } + + @AfterAll + @JvmStatic + fun closeJsonHelper() { + jsonHelper.markLastTestStatisticsAsProcessed() + } + } +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/utils/SolverUtil.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/utils/SolverUtil.kt new file mode 100644 index 000000000..64aefdbf1 --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/utils/SolverUtil.kt @@ -0,0 +1,9 @@ +package io.ksmt.solver.maxsmt.test.utils + +enum class Solver { + Z3, BITWUZLA, CVC5, YICES, PORTFOLIO, Z3_NATIVE +} + +enum class MaxSmtSolver { + PMRES, PRIMAL_DUAL_MAXRES +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/utils/StringUtil.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/utils/StringUtil.kt new file mode 100644 index 000000000..879645f5e --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/utils/StringUtil.kt @@ -0,0 +1,8 @@ +package io.ksmt.solver.maxsmt.test.utils + +fun getRandomString(length: Int): String { + val charset = ('a'..'z') + ('0'..'9') + + return List(length) { charset.random() } + .joinToString("") +} diff --git a/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/z3/KZ3NativeMaxSMTBenchmarkTest.kt b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/z3/KZ3NativeMaxSMTBenchmarkTest.kt new file mode 100644 index 000000000..b3a62829b --- /dev/null +++ b/ksmt-maxsmt-test/src/test/kotlin/io/ksmt/solver/maxsmt/test/z3/KZ3NativeMaxSMTBenchmarkTest.kt @@ -0,0 +1,203 @@ +package io.ksmt.solver.maxsmt.test.z3 + +import com.microsoft.z3.BoolExpr +import com.microsoft.z3.Context +import com.microsoft.z3.Optimize +import com.microsoft.z3.Status +import io.github.oshai.kotlinlogging.KotlinLogging +import io.ksmt.KContext +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics +import io.ksmt.solver.maxsmt.test.KMaxSMTBenchmarkBasedTest +import io.ksmt.solver.maxsmt.test.parseMaxSMTTestInfo +import io.ksmt.solver.maxsmt.test.statistics.JsonStatisticsHelper +import io.ksmt.solver.maxsmt.test.statistics.MaxSMTTestStatistics +import io.ksmt.solver.maxsmt.test.utils.Solver.Z3_NATIVE +import io.ksmt.solver.maxsmt.test.utils.getRandomString +import io.ksmt.solver.z3.KZ3Solver +import org.junit.jupiter.api.AfterAll +import org.junit.jupiter.api.AfterEach +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.MethodSource +import java.io.File +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.io.path.extension +import kotlin.system.measureTimeMillis +import kotlin.test.assertEquals + +abstract class KZ3NativeMaxSMTBenchmarkTest : KMaxSMTBenchmarkBasedTest { + private lateinit var z3Ctx: Context + private lateinit var maxSMTSolver: Optimize + private val logger = KotlinLogging.logger {} + + @BeforeEach + fun initSolver() { + z3Ctx = Context() + maxSMTSolver = z3Ctx.mkOptimize() + } + + @AfterEach + fun close() { + z3Ctx.close() + } + + @ParameterizedTest(name = "{0}") + @MethodSource("maxSMTTestData") + fun maxSMTZ3NativeTest(name: String, samplePath: Path) { + testMaxSMTSolver(name, samplePath) + } + + private fun testMaxSMTSolver(name: String, samplePath: Path) { + val extension = "smt2" + require(samplePath.extension == extension) { + "File extension cannot be '${samplePath.extension}' as it must be $extension" + } + + logger.info { "Test name: [$name]" } + + val testStatistics = MaxSMTTestStatistics(name, Z3_NATIVE) + lateinit var expressions: List + + try { + expressions = z3Ctx.parseSMTLIB2File( + samplePath.toString(), + emptyArray(), + emptyArray(), + emptyArray(), + emptyArray(), + ).toList() + } catch (t: Throwable) { + testStatistics.failedOnParsingOrConvertingExpressions = true + testStatistics.exceptionMessage = t.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { t.message + System.lineSeparator() } + throw t + } + + val maxSmtTestIntoPath = samplePath.toString().removeSuffix(".smt2") + ".maxsmt" + val maxSmtTestInfo = parseMaxSMTTestInfo(File(maxSmtTestIntoPath).toPath()) + + val softConstraintsSize = maxSmtTestInfo.softConstraintsWeights.size + + val softExpressions = + expressions.subList( + expressions.lastIndex + 1 - softConstraintsSize, + expressions.lastIndex + 1, + ) + val hardExpressions = + expressions.subList(0, expressions.lastIndex + 1 - softConstraintsSize) + + hardExpressions.forEach { + maxSMTSolver.Assert(it) + } + + var softConstraintsWeightsSum = 0u + + maxSmtTestInfo.softConstraintsWeights + .zip(softExpressions) + .forEach { (weight, expr) -> + maxSMTSolver.AssertSoft(expr, weight.toInt(), "s") + softConstraintsWeightsSum += weight + } + + // Solver tries to find an optimal solution by default and suboptimal if timeout is set. + // Cores are non-minimized by default. + val params = z3Ctx.mkParams() + // Setting parameters (timeout). + val timeoutMs = 500 + params.add("timeout", timeoutMs) + // Choose an algorithm. + params.add("maxsat_engine", "pd-maxres") + // Prefer larger cores. + params.add("maxres.hill_climb", true) + params.add("maxres.max_core_size", 3) + maxSMTSolver.setParameters(params) + + val maxSmtCallStatistics = KMaxSMTStatistics( + KMaxSMTContext( + KMaxSMTContext.Strategy.PrimalDualMaxRes, + preferLargeWeightConstraintsForCores = true + ) + ).apply { + this.timeoutMs = timeoutMs.toLong() + } + + testStatistics.maxSMTCallStatistics = maxSmtCallStatistics + + var maxSMTResult: Status? + val elapsedTimeMs: Long + + try { + elapsedTimeMs = measureTimeMillis { + maxSMTResult = maxSMTSolver.Check() + } + } catch (ex: Exception) { + testStatistics.exceptionMessage = ex.message.toString() + jsonHelper.appendTestStatisticsToFile(testStatistics) + logger.error { ex.message + System.lineSeparator() } + throw ex + } + + logger.info { "Elapsed time: $elapsedTimeMs ms --- MaxSMT call${System.lineSeparator()}" } + testStatistics.elapsedTimeMs = elapsedTimeMs + testStatistics.timeoutExceededOrUnknown = (maxSMTResult == Status.UNKNOWN) + + val actualSatSoftConstraintsWeightsSum = maxSmtTestInfo.softConstraintsWeights + .zip(softExpressions) + .fold(0uL) { acc, expr -> + acc + if (maxSMTSolver.model.eval(expr.second, true).isTrue) expr.first.toULong() else 0uL + } + + if (maxSMTResult == null || maxSMTResult == Status.UNKNOWN) { + // TODO: ... + } + + try { + testStatistics.passed = true + testStatistics.optimalWeight = maxSmtTestInfo.satSoftConstraintsWeightsSum + testStatistics.foundSoFarWeight = actualSatSoftConstraintsWeightsSum + + // assertEquals(Status.SATISFIABLE, maxSMTResult, "MaxSMT returned $maxSMTResult status") + assertEquals( + maxSmtTestInfo.satSoftConstraintsWeightsSum, + actualSatSoftConstraintsWeightsSum, + "Soft constraints weights sum was [$actualSatSoftConstraintsWeightsSum], " + + "but must be [${maxSmtTestInfo.satSoftConstraintsWeightsSum}]", + ) + } catch (ex: Exception) { + logger.error { ex.message + System.lineSeparator() } + } finally { + jsonHelper.appendTestStatisticsToFile(testStatistics) + } + } + + companion object { + init { + KZ3Solver(KContext()).close() + } + + private lateinit var jsonHelper: JsonStatisticsHelper + + @BeforeAll + @JvmStatic + fun initJsonHelper() { + jsonHelper = + JsonStatisticsHelper( + File( + "${ + Paths.get("").toAbsolutePath() + }/src/test/resources/maxsmt-statistics-${getRandomString(16)}.json", + ), + ) + } + + @AfterAll + @JvmStatic + fun closeJsonHelper() { + jsonHelper.markLastTestStatisticsAsProcessed() + } + } +} diff --git a/ksmt-maxsmt/build.gradle.kts b/ksmt-maxsmt/build.gradle.kts new file mode 100644 index 000000000..30bd28d1d --- /dev/null +++ b/ksmt-maxsmt/build.gradle.kts @@ -0,0 +1,22 @@ +import org.jetbrains.kotlin.konan.properties.loadProperties + +plugins { + id("io.ksmt.ksmt-base") +} + +repositories { + mavenCentral() +} + +val versions = loadProperties(projectDir.parentFile.resolve("version.properties").absolutePath) + +dependencies { + implementation(project(":ksmt-core")) + implementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:${versions["kotlinx-coroutines"]}") + + implementation("io.github.oshai:kotlin-logging-jvm:${versions["kotlin-logging-jvm"]}") + implementation("org.slf4j:slf4j-log4j12:${versions["slf4j-log4j12"]}") + + testImplementation("org.junit.jupiter:junit-jupiter-api:${versions["junit-jupiter"]}") + testImplementation(project(":ksmt-z3")) +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/KMaxSMTContext.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/KMaxSMTContext.kt new file mode 100644 index 000000000..8336efef7 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/KMaxSMTContext.kt @@ -0,0 +1,16 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalDualMaxRes + +class KMaxSMTContext( + val strategy: Strategy = PrimalDualMaxRes, + val preferLargeWeightConstraintsForCores: Boolean = false, + val minimizeCores: Boolean = false, + val getMultipleCores: Boolean = false, +) { + + enum class Strategy { + PrimalMaxRes, + PrimalDualMaxRes, + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/KMaxSMTResult.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/KMaxSMTResult.kt new file mode 100644 index 000000000..52d09f3d6 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/KMaxSMTResult.kt @@ -0,0 +1,24 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.maxsmt.constraints.SoftConstraint + +/** + * @property satSoftConstraints + * Contains soft constraints algorithm considered as the best solution found by the moment. + * + * @property hardConstraintsSatStatus + * Shows satisfiability status of hardly asserted constraints' conjunction. + * + * @property timeoutExceededOrUnknown + * Shows whether timeout has exceeded, solver was interrupted or returned UNKNOWN (can happen when timeout has exceeded + * or by some other reason). + * + * It may end without success in case of exceeding the timeout or in case solver started returning UNKNOWN during + * MaxSAT calculation. + */ +class KMaxSMTResult( + val satSoftConstraints: List, + val hardConstraintsSatStatus: KSolverStatus, + val timeoutExceededOrUnknown: Boolean +) diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/Constraint.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/Constraint.kt new file mode 100644 index 000000000..b5f959557 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/Constraint.kt @@ -0,0 +1,8 @@ +package io.ksmt.solver.maxsmt.constraints + +import io.ksmt.expr.KExpr +import io.ksmt.sort.KBoolSort + +interface Constraint { + val expression: KExpr +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/HardConstraint.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/HardConstraint.kt new file mode 100644 index 000000000..a73fb709d --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/HardConstraint.kt @@ -0,0 +1,6 @@ +package io.ksmt.solver.maxsmt.constraints + +import io.ksmt.expr.KExpr +import io.ksmt.sort.KBoolSort + +class HardConstraint(override val expression: KExpr) : Constraint diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/SoftConstraint.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/SoftConstraint.kt new file mode 100644 index 000000000..c19168773 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/constraints/SoftConstraint.kt @@ -0,0 +1,6 @@ +package io.ksmt.solver.maxsmt.constraints + +import io.ksmt.expr.KExpr +import io.ksmt.sort.KBoolSort + +class SoftConstraint(override val expression: KExpr, val weight: UInt) : Constraint diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/scope/MaxSMTScope.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/scope/MaxSMTScope.kt new file mode 100644 index 000000000..b0c82189d --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/scope/MaxSMTScope.kt @@ -0,0 +1,3 @@ +package io.ksmt.solver.maxsmt.scope + +internal class MaxSMTScope(val scopeAddedSoftConstraints: Int) diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/scope/MaxSMTScopeManager.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/scope/MaxSMTScopeManager.kt new file mode 100644 index 000000000..19df85201 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/scope/MaxSMTScopeManager.kt @@ -0,0 +1,64 @@ +package io.ksmt.solver.maxsmt.scope + +import io.ksmt.solver.maxsmt.constraints.SoftConstraint + +internal class MaxSMTScopeManager { + private var currentScope = 0u + + private val prevScopes = mutableListOf() + + private var scopeAddedSoftConstraints = 0 + + /** + * Increment scope added soft constraints number. + */ + fun incrementSoft() { + if (currentScope != 0u) { + scopeAddedSoftConstraints++ + } + } + + /** + * Push a new scope level. + * + * @see pop + */ + fun push() { + if (currentScope != 0u) { + prevScopes.add(MaxSMTScope(scopeAddedSoftConstraints)) + scopeAddedSoftConstraints = 0 + } + + currentScope++ + } + + /** + * Pop scope levels with removing soft constraints added in these scope levels. + * + * @see push + */ + fun pop(n: UInt = 1u, softConstraints: MutableList): MutableList { + require(n <= currentScope) { + "Can not pop $n scope levels because current scope level is $currentScope" + } + if (n == 0u) { + return softConstraints + } + + repeat(n.toInt()) { + val size = softConstraints.size + softConstraints.subList(size - scopeAddedSoftConstraints, size).clear() + + if (prevScopes.isNotEmpty()) { + scopeAddedSoftConstraints = prevScopes.last().scopeAddedSoftConstraints + prevScopes.removeLast() + } else { + scopeAddedSoftConstraints = 0 + } + } + + currentScope -= n + + return softConstraints + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxResSolverBase.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxResSolverBase.kt new file mode 100644 index 000000000..71abcb990 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxResSolverBase.kt @@ -0,0 +1,36 @@ +package io.ksmt.solver.maxsmt.solvers + +import io.ksmt.KContext +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.solver.maxsmt.utils.CoreUtils + +abstract class KMaxResSolverBase( + ctx: KContext, + solver: KSolver, +) : KMaxSMTSolverBase(ctx, solver) where T : KSolverConfiguration { + protected fun removeCoreAssumptions(core: List, assumptions: MutableList) { + assumptions.removeAll(core) + } + + protected fun splitCore( + core: List, + assumptions: MutableList, + ): Pair> { + val splitCore = mutableListOf() + + val minWeight = CoreUtils.getCoreWeight(core) + // Add fresh soft clauses for weights that are above w. + for (constraint in core) { + if (constraint.weight > minWeight) { + assumptions.add(SoftConstraint(constraint.expression, constraint.weight - minWeight)) + splitCore.add(SoftConstraint(constraint.expression, minWeight)) + } else { + splitCore.add(SoftConstraint(constraint.expression, constraint.weight)) + } + } + + return Pair(minWeight, splitCore) + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxSMTSolverBase.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxSMTSolverBase.kt new file mode 100644 index 000000000..fca97536c --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxSMTSolverBase.kt @@ -0,0 +1,124 @@ +package io.ksmt.solver.maxsmt.solvers + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.solver.maxsmt.scope.MaxSMTScopeManager +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics +import io.ksmt.sort.KBoolSort +import kotlin.time.Duration + +/** + * This class implements a logic general for any MaxSMT solver. + */ +abstract class KMaxSMTSolverBase( + private val ctx: KContext, + private val solver: KSolver, +) : KMaxSMTSolverInterface where T : KSolverConfiguration { + private val scopeManager = MaxSMTScopeManager() + protected var softConstraints = mutableListOf() + protected lateinit var maxSMTStatistics: KMaxSMTStatistics + protected var isInterrupted = false + + /** + * Softly assert an expression with weight (aka soft constraint) into solver. + * + * @see checkMaxSMT + * */ + override fun assertSoft(expr: KExpr, weight: UInt) { + require(weight > 0u) { "Soft constraint weight cannot be equal to $weight as it must be greater than 0" } + + val softConstraint = SoftConstraint(expr, weight) + softConstraints.add(softConstraint) + scopeManager.incrementSoft() + } + + /** + * Solve maximum satisfiability modulo theories problem. + */ + fun checkMaxSMT(timeout: Duration): KMaxSMTResult = + checkMaxSMT(timeout, collectStatistics = false) + + /** + * Solve maximum satisfiability modulo theories problem. + * + * @param collectStatistics specifies whether statistics (elapsed time to execute method etc.) should be collected or not. + */ + abstract override fun checkMaxSMT(timeout: Duration, collectStatistics: Boolean): KMaxSMTResult + + /** + * Get last MaxSMT launch statistics (number of queries to solver, MaxSMT timeout etc.). + */ + override fun collectMaxSMTStatistics(): KMaxSMTStatistics { + require(this::maxSMTStatistics.isInitialized) { + "MaxSMT statistics is only available after MaxSMT launches with statistics collection enabled" + } + + return maxSMTStatistics + } + + protected fun getSatSoftConstraintsByModel(model: KModel): List { + return softConstraints.filter { + model.eval(it.expression, true) == ctx.trueExpr || model.eval( + it.expression, + true, + ) != ctx.falseExpr + }.also { model.close() } + } + + override fun configure(configurator: T.() -> Unit) { + solver.configure(configurator) + } + + override fun assert(expr: KExpr) { + solver.assert(expr) + } + + override fun assertAndTrack(expr: KExpr) { + solver.assertAndTrack(expr) + } + + override fun push() { + solver.push() + scopeManager.push() + } + + override fun pop(n: UInt) { + solver.pop(n) + softConstraints = scopeManager.pop(n, softConstraints) + } + + override fun check(timeout: Duration): KSolverStatus { + return solver.check(timeout) + } + + override fun checkWithAssumptions(assumptions: List>, timeout: Duration): KSolverStatus { + return solver.checkWithAssumptions(assumptions, timeout) + } + + override fun model(): KModel { + return solver.model() + } + + override fun unsatCore(): List> { + return solver.unsatCore() + } + + override fun reasonOfUnknown(): String { + return solver.reasonOfUnknown() + } + + override fun interrupt() { + isInterrupted = true + solver.interrupt() + } + + override fun close() { + solver.close() + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxSMTSolverInterface.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxSMTSolverInterface.kt new file mode 100644 index 000000000..a3813d189 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KMaxSMTSolverInterface.kt @@ -0,0 +1,17 @@ +package io.ksmt.solver.maxsmt.solvers + +import io.ksmt.expr.KExpr +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics +import io.ksmt.sort.KBoolSort +import kotlin.time.Duration + +interface KMaxSMTSolverInterface : KSolver where C : KSolverConfiguration { + fun assertSoft(expr: KExpr, weight: UInt) + + fun checkMaxSMT(timeout: Duration = Duration.INFINITE, collectStatistics: Boolean = false): KMaxSMTResult + + fun collectMaxSMTStatistics(): KMaxSMTStatistics +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KPMResSolver.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KPMResSolver.kt new file mode 100644 index 000000000..702a4cb76 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KPMResSolver.kt @@ -0,0 +1,236 @@ +package io.ksmt.solver.maxsmt.solvers + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KSolverStatus.SAT +import io.ksmt.solver.KSolverStatus.UNKNOWN +import io.ksmt.solver.KSolverStatus.UNSAT +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalMaxRes +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics +import io.ksmt.solver.maxsmt.utils.CoreUtils +import io.ksmt.solver.maxsmt.utils.TimerUtils +import io.ksmt.sort.KBoolSort +import io.ksmt.utils.mkConst +import kotlin.time.Duration +import kotlin.time.TimeSource.Monotonic.markNow + +class KPMResSolver(private val ctx: KContext, solver: KSolver) : + KMaxResSolverBase(ctx, solver) { + private var collectStatistics = false + private val maxSmtCtx = KMaxSMTContext( + strategy = PrimalMaxRes, + preferLargeWeightConstraintsForCores = false, + minimizeCores = false, + getMultipleCores = false, + ) + + override fun checkMaxSMT(timeout: Duration, collectStatistics: Boolean): KMaxSMTResult { + val markCheckMaxSMTStart = markNow() + + if (TimerUtils.timeoutExceeded(timeout)) { + error("Timeout must be positive but was [${timeout.inWholeSeconds} s]") + } + + this.collectStatistics = collectStatistics + + if (this.collectStatistics) { + maxSMTStatistics = KMaxSMTStatistics(maxSmtCtx) + maxSMTStatistics.timeoutMs = timeout.inWholeMilliseconds + } + + val maxSMTResult = runMaxSMTLogic(timeout) + + if (this.collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + + return maxSMTResult + } + + private fun runMaxSMTLogic(timeout: Duration): KMaxSMTResult { + val markHardConstraintsCheckStart = markNow() + val hardConstraintsStatus = check(timeout) + + if (collectStatistics) { + maxSMTStatistics.queriesToSolverNumber++ + maxSMTStatistics.timeInSolverQueriesMs += markHardConstraintsCheckStart.elapsedNow().inWholeMilliseconds + } + + if (softConstraints.isEmpty()) { + return KMaxSMTResult( + listOf(), + hardConstraintsStatus, + hardConstraintsStatus == UNKNOWN, + ) + } + + if (hardConstraintsStatus == UNSAT) { + return KMaxSMTResult( + listOf(), hardConstraintsStatus, + timeoutExceededOrUnknown = false, + ) + } else if (hardConstraintsStatus == UNKNOWN) { + return KMaxSMTResult( + listOf(), hardConstraintsStatus, + timeoutExceededOrUnknown = true, + ) + } + + push() + + var i = 0 + var formula = softConstraints.toMutableList() + + while (true) { + val checkRemainingTime = TimerUtils.computeRemainingTime(timeout, markHardConstraintsCheckStart) + + if (TimerUtils.timeoutExceeded(checkRemainingTime) || isInterrupted) { + pop() + return KMaxSMTResult( + listOf(), hardConstraintsStatus, + timeoutExceededOrUnknown = true, + ) + } + + val markCheckSatStart = markNow() + val (solverStatus, unsatCore, model) = + checkSat(formula, checkRemainingTime) + + if (collectStatistics) { + maxSMTStatistics.queriesToSolverNumber++ + maxSMTStatistics.timeInSolverQueriesMs += markCheckSatStart.elapsedNow().inWholeMilliseconds + } + + if (solverStatus == SAT) { + pop() + return processSat(model!!) + } else if (solverStatus == UNKNOWN) { + pop() + return KMaxSMTResult(emptyList(), SAT, timeoutExceededOrUnknown = true) + } + + val (weight, splitUnsatCore) = splitUnsatCore(formula, unsatCore) + + val (formulaReified, reificationLiterals) = + reifyUnsatCore(formula, splitUnsatCore, i, weight) + + unionReificationLiterals(reificationLiterals) + + formula = applyMaxRes(formulaReified, reificationLiterals, i, weight) + + i++ + } + } + + /** + * Split all soft constraints from the unsat core into two groups: + * - constraints with the weight equal to the minimum of the unsat core soft constraint weights + * - constraints with the weight equal to old weight - minimum weight + * + * @return a pair of minimum weight and a list of unsat core soft constraints with minimum weight. + */ + private fun splitUnsatCore( + formula: MutableList, + unsatCore: List>, + ): Pair> { + val unsatCoreSoftConstraints = CoreUtils.coreToSoftConstraints(unsatCore, formula) + removeCoreAssumptions(unsatCoreSoftConstraints, formula) + return splitCore(unsatCoreSoftConstraints, formula) + } + + /** + * Reify unsat core soft constraints with literals. + */ + private fun reifyUnsatCore( + formula: MutableList, + unsatCore: List, + iter: Int, + weight: UInt, + ): Pair, List>> = with(ctx) { + val literalsToReify = mutableListOf>() + + unsatCore.forEachIndexed { index, coreElement -> + if (coreElement.weight == weight) { + formula.remove(coreElement) + + val coreElementExpr = coreElement.expression + val literalToReify = coreElementExpr.sort.mkConst("*$iter:$index") + val constraintToReify = coreElementExpr eq !literalToReify + + assert(constraintToReify) + + literalsToReify.add(literalToReify) + } + } + + return Pair(formula, literalsToReify) + } + + private fun unionReificationLiterals(reificationLiterals: List>) = with(ctx) { + when (reificationLiterals.size) { + 1 -> assert(reificationLiterals.first()) + 2 -> assert(reificationLiterals[0] or reificationLiterals[1]) + else -> assert(reificationLiterals.reduce { x, y -> x or y }) + } + } + + /** + * Apply MaxRes rule. + */ + private fun applyMaxRes( + formula: MutableList, + literalsToReify: List>, + iter: Int, + weight: UInt, + ): MutableList = + with(ctx) { + literalsToReify.forEachIndexed { index, literal -> + val indexLast = literalsToReify.lastIndex + + if (index < indexLast) { + val sort = literal.sort + val currentLiteralToReifyDisjunction = sort.mkConst("#$iter:$index") + val nextLiteralToReifyDisjunction = sort.mkConst("#$iter:${index + 1}") + + val disjunction = + when (indexLast - index) { + // The second element is omitted as it is an empty disjunction. + 1 -> literalsToReify[index + 1] + else -> literalsToReify[index + 1] or nextLiteralToReifyDisjunction + } + + assert(currentLiteralToReifyDisjunction eq disjunction) + + formula.add(SoftConstraint(!currentLiteralToReifyDisjunction or !literal, weight)) + } + } + + return formula + } + + private fun processSat(model: KModel): KMaxSMTResult { + val satSoftConstraints = getSatSoftConstraintsByModel(model) + return KMaxSMTResult(satSoftConstraints, SAT, timeoutExceededOrUnknown = false) + } + + /** + * Check on satisfiability hard constraints with assumed soft constraints. + * + * @return a triple of solver status, unsat core (if exists, empty list otherwise) and model + * (if exists, null otherwise). + */ + private fun checkSat(assumptions: List, timeout: Duration): + Triple>, KModel?> = + when (val status = checkWithAssumptions(assumptions.map { x -> x.expression }, timeout)) { + SAT -> Triple(status, listOf(), model()) + UNSAT -> Triple(status, unsatCore(), null) + UNKNOWN -> Triple(status, listOf(), null) + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KPrimalDualMaxResSolver.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KPrimalDualMaxResSolver.kt new file mode 100644 index 000000000..645a6d1e3 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/KPrimalDualMaxResSolver.kt @@ -0,0 +1,620 @@ +package io.ksmt.solver.maxsmt.solvers + +import io.github.oshai.kotlinlogging.KotlinLogging +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KSolverStatus.SAT +import io.ksmt.solver.KSolverStatus.UNKNOWN +import io.ksmt.solver.KSolverStatus.UNSAT +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalDualMaxRes +import io.ksmt.solver.maxsmt.KMaxSMTContext.Strategy.PrimalMaxRes +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.solver.maxsmt.solvers.utils.MinimalUnsatCore +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics +import io.ksmt.solver.maxsmt.utils.CoreUtils +import io.ksmt.solver.maxsmt.utils.ModelUtils +import io.ksmt.solver.maxsmt.utils.TimerUtils +import io.ksmt.sort.KBoolSort +import kotlin.time.Duration +import kotlin.time.TimeSource.Monotonic.markNow + +class KPrimalDualMaxResSolver( + private val ctx: KContext, + solver: KSolver, + private val maxSmtCtx: KMaxSMTContext, +) : KMaxResSolverBase(ctx, solver) { + private var _lower: ULong = 0uL // Current lower frontier + private var _upper: ULong = 0uL // Current upper frontier + private var _maxUpper = 0uL // Max possible upper frontier + private var _correctionSetSize: Int = 0 // Current corrections set size + private val _maxCoreSize = 3 + private var _correctionSetModel: KModel? = null + private var _model: KModel? = null + private var _minimalUnsatCore = MinimalUnsatCore(ctx, solver) + private var collectStatistics = false + private var _iteration = 0 + private val logger = KotlinLogging.logger {} + private var markLoggingPoint = markNow() + + private data class WeightedCore(val expressions: List>, val weight: UInt) + + override fun checkMaxSMT(timeout: Duration, collectStatistics: Boolean): KMaxSMTResult { + val markCheckMaxSMTStart = markNow() + markLoggingPoint = markCheckMaxSMTStart + + if (TimerUtils.timeoutExceeded(timeout)) { + error("Timeout must be positive but was [${timeout.inWholeSeconds} s]") + } + + this.collectStatistics = collectStatistics + + if (this.collectStatistics) { + maxSMTStatistics = KMaxSMTStatistics(maxSmtCtx) + maxSMTStatistics.timeoutMs = timeout.inWholeMilliseconds + } + + val markHardConstraintsCheckStart = markNow() + val hardConstraintsStatus = check(timeout) + if (this.collectStatistics) { + maxSMTStatistics.queriesToSolverNumber++ + maxSMTStatistics.timeInSolverQueriesMs += markHardConstraintsCheckStart.elapsedNow().inWholeMilliseconds + } + + if (hardConstraintsStatus == UNSAT || softConstraints.isEmpty()) { + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + return KMaxSMTResult( + listOf(), hardConstraintsStatus, + timeoutExceededOrUnknown = false, + ) + } else if (hardConstraintsStatus == UNKNOWN) { + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + return KMaxSMTResult( + listOf(), hardConstraintsStatus, + timeoutExceededOrUnknown = true, + ) + } + + push() + initMaxSMT() + + val assumptions = softConstraints.toMutableList() + + while (_lower < _upper) { + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] Iteration number: $_iteration" + } + markLoggingPoint = markNow() + + val softConstraintsCheckRemainingTime = TimerUtils.computeRemainingTime(timeout, markCheckMaxSMTStart) + if (TimerUtils.timeoutExceeded(softConstraintsCheckRemainingTime) || isInterrupted) { + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] --- returning SubOpt MaxSMT result" + } + return getSubOptMaxSMTResult() + } + + val status = checkSatHillClimb(assumptions, timeout) + + when (status) { + SAT -> { + when (maxSmtCtx.strategy) { + PrimalMaxRes -> _upper = _lower + + PrimalDualMaxRes -> { + val correctionSet = getCorrectionSet(model(), assumptions) + if (correctionSet.isEmpty()) { + if (_model != null) { + // Feasible optimum is found by the moment. + _lower = _upper + } + } else { + processSat(correctionSet, assumptions) + } + } + } + } + + UNSAT -> { + val remainingTime = TimerUtils.computeRemainingTime(timeout, markCheckMaxSMTStart) + if (TimerUtils.timeoutExceeded(remainingTime) || isInterrupted) { + pop() + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] --- returning SubOpt MaxSMT result" + } + return getSubOptMaxSMTResult() + } + + val processUnsatStatus = processUnsat(assumptions, remainingTime) + if (processUnsatStatus == UNSAT) { + _lower = _upper + // TODO: process this case as it can happen when timeout exceeded??? + pop() + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + // TODO: is it Ok? + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] --- returning SubOpt MaxSMT result" + } + // Something went wrong, so timeout has exceeded, solver was interrupted or returned UNKNOWN. + return getSubOptMaxSMTResult() + } else if (processUnsatStatus == UNKNOWN) { + pop() + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] --- returning SubOpt MaxSMT result" + } + return getSubOptMaxSMTResult() + } + } + + UNKNOWN -> { + pop() + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] --- returning SubOpt MaxSMT result" + } + return getSubOptMaxSMTResult() + } + } + + ++_iteration + } + + _lower = _upper + + val result = KMaxSMTResult( + if (_model != null) getSatSoftConstraintsByModel(_model!!) else listOf(), SAT, + timeoutExceededOrUnknown = false, + ) + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] --- returning SubOpt MaxSMT result" + } + + pop() + + if (collectStatistics) { + maxSMTStatistics.elapsedTimeMs = markCheckMaxSMTStart.elapsedNow().inWholeMilliseconds + } + return result + } + + private fun processSat(correctionSet: List, assumptions: MutableList) { + removeCoreAssumptions(correctionSet, assumptions) + val (minWeight, _) = splitCore(correctionSet, assumptions) + correctionSetMaxResolve(correctionSet, assumptions, minWeight) + + _correctionSetModel = null + _correctionSetSize = 0 + } + + private fun processUnsat(assumptions: MutableList, timeout: Duration): KSolverStatus { + // We can't get UNSAT from it. + val (status, cores) = getCores(assumptions, timeout) + + if (status != SAT) { + return status + } + + // Timeout has exceeded or some core was empty (how???). + if (cores.isEmpty()) { + return UNSAT + } + + for (core in cores) { + processUnsatCore(core, assumptions) + } + + return SAT + } + + private fun processUnsatCore(weightedCore: WeightedCore, assumptions: MutableList) = with(ctx) { + logger.info { "processing unsat core --- started" } + + val core = weightedCore.expressions + + require(core.isNotEmpty()) { "Core should not be empty here" } + + maxResolve(weightedCore, assumptions) + + val fml = !(core.reduce { x, y -> x and y }) + assert(fml) + + _lower += weightedCore.weight + logger.info { "Unsat core weight: ${weightedCore.weight}" } + + if (maxSmtCtx.strategy == PrimalDualMaxRes) { + _lower = minOf(_lower, _upper) + logger.info { "(lower bound: $_lower, upper bound: $_upper) --- lower bound is updated" } + } + + if (_correctionSetModel != null && _correctionSetSize > 0) { + // This estimate can overshoot for weighted soft constraints. + --_correctionSetSize + } + + // Here we also prefer a smaller correction set to core. + if (_correctionSetModel != null && _correctionSetSize < core.size) { + val correctionSet = getCorrectionSet(_correctionSetModel!!, assumptions) + if (correctionSet.size >= core.size) { + logger.info { "processing unsat core --- ended" } + return + } + + var weight = 0u + for (asm in assumptions) { + val weight1 = asm.weight + if (weight != 0u && weight1 != weight) { + logger.info { "processing unsat core --- ended" } + return + } + + weight = weight1 + } + + processSat(correctionSet, assumptions) + } + + logger.info { "processing unsat core --- ended" } + } + + /** + * Status is UNKNOWN when timeout has exceeded or solver returned UNKNOWN. + */ + private fun getCores( + assumptions: MutableList, + timeout: Duration, + ): Pair> { + val markStart = markNow() + + val cores = mutableListOf() + var status = UNSAT + + while (status == UNSAT) { + var unsatCore: List + + if (maxSmtCtx.minimizeCores) { + val minimizeCoreRemainingTime = TimerUtils.computeRemainingTime(timeout, markStart) + if (TimerUtils.timeoutExceeded(minimizeCoreRemainingTime) || isInterrupted) { + return Pair(SAT, cores) // TODO: is this status Ok? + } + + unsatCore = minimizeCore(assumptions, minimizeCoreRemainingTime) + updateMinimalUnsatCoreModel(assumptions) + } else { + unsatCore = CoreUtils.coreToSoftConstraints(unsatCore(), assumptions) + } + + // TODO: when can we reach it? + if (unsatCore.isEmpty()) { + cores.clear() + _lower = _upper + return Pair(SAT, cores) + } + + // 1. remove all core literals from assumptions + // 2. re-add literals of higher weight than min-weight. + // 3. 'core' stores the core literals that are re-encoded as assumptions afterward + cores.add(WeightedCore(unsatCore.map { it.expression }, CoreUtils.getCoreWeight(unsatCore))) + + removeCoreAssumptions(unsatCore, assumptions) + splitCore(unsatCore, assumptions) + + if (unsatCore.size >= _maxCoreSize || !maxSmtCtx.getMultipleCores) { + return Pair(SAT, cores) + } + + val checkSatRemainingTime = TimerUtils.computeRemainingTime(timeout, markStart) + if (TimerUtils.timeoutExceeded(checkSatRemainingTime) || isInterrupted) { + return Pair(SAT, cores) // TODO: is this status Ok? + } + + status = checkSatHillClimb(assumptions, checkSatRemainingTime) + } + + // TODO: for the future, we can improve this processing UNKNOWN case. + // Okay, it's UNKNOWN, but if timeout has not exceeded and we have a core then it's Okay, we can do something. + return Pair(status, cores) + } + + private fun minimizeCore(assumptions: List, timeout: Duration): List { + val minimalUnsatCore = _minimalUnsatCore.tryGetMinimalUnsatCore(assumptions, timeout, collectStatistics) + if (collectStatistics) { + val minimalCoreStatistics = _minimalUnsatCore.collectStatistics() + maxSMTStatistics.queriesToSolverNumber += minimalCoreStatistics.queriesToSolverNumber + maxSMTStatistics.timeInSolverQueriesMs += minimalCoreStatistics.timeInSolverQueriesMs + } + + return minimalUnsatCore + } + + private fun updateMinimalUnsatCoreModel(assumptions: List) { + val (model, weight) = _minimalUnsatCore.getBestModel() + + if (model != null && _upper > weight) { + updateAssignment(model, assumptions) + } + } + + private fun updateAssignment(model: KModel, assumptions: List) { + var correctionSetSize = 0 + for (constr in assumptions) { + if (ModelUtils.expressionIsNotTrue(ctx, model, constr.expression)) { + ++correctionSetSize + } + } + + if (_correctionSetModel == null || correctionSetSize < _correctionSetSize) { + _correctionSetModel = model + _correctionSetSize = correctionSetSize + } + + val upper = ModelUtils.getModelCost(ctx, model, softConstraints) + + if (_model != null && upper >= _upper) { + logger.info { "Found model has less or equal weight --- model is not updated" } + return + } + + _model?.close() + _model = model + _upper = upper + + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] (lower bound: $_lower, upper bound: $_upper) --- model is updated" + } + markLoggingPoint = markNow() + } + + private fun maxResolve(weightedCore: WeightedCore, assumptions: MutableList) = with(ctx) { + val core = weightedCore.expressions + + require(core.isNotEmpty()) { "Core should not be empty here" } + + // d_0 := true + // d_i := b_{i-1} and d_{i-1} for i = 1...sz-1 + // soft (b_i or !d_i) + // == (b_i or !(!b_{i-1} or d_{i-1})) + // == (b_i or b_0 & b_1 & ... & b_{i-1}) + // + // Soft constraint is satisfied if the previous soft constraint + // holds or if it is the first soft constraint to fail. + // + // The Soundness of this rule can be established using MaxRes. + + lateinit var d: KExpr + var dd: KExpr + var fml: KExpr + + for (index in 1..core.lastIndex) { + val b_i = core[index - 1] + val b_i1 = core[index] + + when (index) { + 1 -> { + d = b_i + } + + 2 -> { + d = b_i and d + } + + else -> { + dd = mkFreshConst("d", this.boolSort) + fml = mkImplies(dd, d) + assert(fml) + fml = mkImplies(dd, b_i) + assert(fml) + fml = d and b_i + // TODO: process!!! + // update_model(dd, fml); + // I use the string below instead!!! + assert(dd eq fml) + d = dd + } + } + + val asm = mkFreshConst("a", this.boolSort) + val cls = b_i1 or d + fml = mkImplies(asm, cls) + assumptions.add(SoftConstraint(asm, weightedCore.weight)) + // TODO: process!!! + // update_model(asm, cls); + // I use the string below instead!!! + assert(asm eq cls) + assert(fml) + } + } + + private fun correctionSetMaxResolve( + correctionSet: List, + assumptions: MutableList, + weight: UInt, + ) = with(ctx) { + if (correctionSet.isEmpty()) { + return + } + + var d: KExpr = falseExpr + var fml: KExpr + var asm: KExpr + // + // d_0 := false + // d_i := b_{i-1} or d_{i-1} for i = 1...sz-1 + // soft (b_i and d_i) + // == (b_i and (b_0 or b_1 or ... or b_{i-1})) + // + // asm => b_i + // asm => d_{i-1} or b_{i-1} + // d_i => d_{i-1} or b_{i-1} + // + for (i in 1..correctionSet.lastIndex) { + val b_i = correctionSet[i - 1].expression + val b_i1 = correctionSet[i].expression + val cls = b_i or d + + if (i > 2) { + d = mkFreshConst("d", this.boolSort) + fml = mkImplies(d, cls) + + // TODO: process!!! + // update_model(d, cls); + // I use the string below instead: + assert(d eq cls) + + assert(fml) + } else { + d = cls + } + + asm = mkFreshConst("a", this.boolSort) + fml = mkImplies(asm, b_i1) + assert(fml) + fml = mkImplies(asm, cls) + assert(fml) + assumptions.add(SoftConstraint(asm, weight)) + + fml = b_i1 and cls + // TODO: process!!! update_model(asm, fml); + // I use the string below instead: + assert(asm eq fml) + } + + fml = correctionSet + .map { it.expression } + .reduce { x, y -> x or y } + assert(fml) + } + + private fun initMaxSMT() { + isInterrupted = false + + _lower = 0u + _upper = softConstraints.sumOf { it.weight.toULong() } + + _maxUpper = _upper + _correctionSetSize = 0 + + _iteration = 0 + + logger.info { + "[${markLoggingPoint.elapsedNow().inWholeMicroseconds} mcs] (lower bound: $_lower, upper bound: $_upper)" + " --- model is initialized with null" + } + markLoggingPoint = markNow() + + _model = null + _correctionSetModel = null + _minimalUnsatCore.reset() + } + + private fun getCorrectionSet(model: KModel, assumptions: List): List { + updateAssignment(model, assumptions) + + return ModelUtils.getCorrectionSet(ctx, model, assumptions) + } + + private fun checkSatHillClimb(assumptions: MutableList, timeout: Duration): KSolverStatus { + logger.info { "checking formula on satisfiability --- started" } + + var status = SAT + + if (maxSmtCtx.preferLargeWeightConstraintsForCores && assumptions.isNotEmpty()) { + val markStart = markNow() + + // Give preference to cores that have large minimal values. + assumptions.sortByDescending { it.weight } + + var lastIndex = 0 + var index = 0 + + while (index < assumptions.size && status == SAT) { + while (assumptions.size > 20 * (index - lastIndex) && index < assumptions.size) { + index = getNextIndex(assumptions, index) + } + lastIndex = index + + val assumptionsToCheck = assumptions.subList(0, index) + + val remainingTime = TimerUtils.computeRemainingTime(timeout, markStart) + if (TimerUtils.timeoutExceeded(remainingTime) || isInterrupted) { + logger.info { + "checking formula on satisfiability --- ended --- solver returned UNKNOWN" + + "or operation was interrupted" + } + return UNKNOWN + } + + val markCheckAssumptionsStart = markNow() + status = checkSat(assumptionsToCheck, remainingTime) + if (collectStatistics) { + maxSMTStatistics.queriesToSolverNumber++ + maxSMTStatistics.timeInSolverQueriesMs += markCheckAssumptionsStart.elapsedNow().inWholeMilliseconds + } + } + } else { + val markCheckStart = markNow() + status = checkSat(assumptions, timeout) + if (collectStatistics) { + maxSMTStatistics.queriesToSolverNumber++ + maxSMTStatistics.timeInSolverQueriesMs += markCheckStart.elapsedNow().inWholeMilliseconds + } + } + + logger.info { "checking formula on satisfiability --- ended" } + return status + } + + private fun getNextIndex(assumptions: List, index: Int): Int { + var currentIndex = index + + if (currentIndex < assumptions.size) { + val weight = assumptions[currentIndex].weight + ++currentIndex + while (currentIndex < assumptions.size && weight == assumptions[currentIndex].weight) { + ++currentIndex + } + } + return currentIndex + } + + private fun checkSat( + assumptions: List, + timeout: Duration, + ): KSolverStatus { + val status = checkWithAssumptions(assumptions.map { it.expression }, timeout) + + if (status == SAT) { + updateAssignment(model().detach(), assumptions) + } + + return status + } + + private fun getSubOptMaxSMTResult(): KMaxSMTResult = + KMaxSMTResult( + if (_model != null) getSatSoftConstraintsByModel(_model!!) else listOf(), + SAT, + true + ) +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/utils/MinimalCoreStatistics.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/utils/MinimalCoreStatistics.kt new file mode 100644 index 000000000..98bc53c56 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/utils/MinimalCoreStatistics.kt @@ -0,0 +1,6 @@ +package io.ksmt.solver.maxsmt.solvers.utils + +internal class MinimalCoreStatistics { + var queriesToSolverNumber = 0 + var timeInSolverQueriesMs: Long = 0 +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/utils/MinimalUnsatCore.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/utils/MinimalUnsatCore.kt new file mode 100644 index 000000000..48630ba7f --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/solvers/utils/MinimalUnsatCore.kt @@ -0,0 +1,161 @@ +package io.ksmt.solver.maxsmt.solvers.utils + +import io.github.oshai.kotlinlogging.KotlinLogging +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus.SAT +import io.ksmt.solver.KSolverStatus.UNKNOWN +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.solver.maxsmt.utils.CoreUtils +import io.ksmt.solver.maxsmt.utils.ModelUtils +import io.ksmt.solver.maxsmt.utils.TimerUtils +import io.ksmt.sort.KBoolSort +import kotlin.time.Duration +import kotlin.time.TimeSource.Monotonic.markNow + +internal class MinimalUnsatCore( + private val ctx: KContext, + private val solver: KSolver, +) { + private val _minimalUnsatCoreModel = MinimalUnsatCoreModel(ctx, solver) + private lateinit var coreStatistics: MinimalCoreStatistics + private val logger = KotlinLogging.logger {} + + fun getBestModel(): Pair = _minimalUnsatCoreModel.getBestModel() + + // If solver starts returning unknown or exceeds the timeout, non-minimized unsat core is returned. + fun tryGetMinimalUnsatCore( + assumptions: List, + timeout: Duration = Duration.INFINITE, + collectStatistics: Boolean = false, + ): List = with(ctx) { + logger.info { "core minimization --- started" } + + val markStart = markNow() + + if (collectStatistics) { + coreStatistics = MinimalCoreStatistics() + } + + val unsatCore = solver.unsatCore() + + if (unsatCore.isEmpty()) { + logger.info { "core minimization ended --- unsat core is empty" } + return emptyList() + } + + val minimalUnsatCore = mutableListOf>() + + val unknown = unsatCore.toMutableList() + + while (unknown.isNotEmpty()) { + val remainingTime = TimerUtils.computeRemainingTime(timeout, markStart) + if (TimerUtils.timeoutExceeded(remainingTime)) { + logger.info { "core minimization ended --- timeout exceeded" } + return CoreUtils.coreToSoftConstraints(unsatCore, assumptions) + } + + val expr = unknown.removeLast() + + val notExpr = !expr + + val markCheckStart = markNow() + val status = solver.checkWithAssumptions(minimalUnsatCore + notExpr + unknown, remainingTime) + if (collectStatistics) { + coreStatistics.queriesToSolverNumber++ + coreStatistics.timeInSolverQueriesMs += (markNow() - markCheckStart).inWholeMilliseconds + } + + when (status) { + UNKNOWN -> { + logger.info { "core minimization ended --- solver returned UNKNOWN" } + return CoreUtils.coreToSoftConstraints(unsatCore, assumptions) + } + + SAT -> { + minimalUnsatCore.add(expr) + _minimalUnsatCoreModel.updateModel(assumptions) + } + + else -> processUnsat(notExpr, unknown, minimalUnsatCore) + } + } + + logger.info { "core minimization ended --- core is minimized" } + return CoreUtils.coreToSoftConstraints(minimalUnsatCore, assumptions) + } + + /** + * Get last core minimization statistics (number of queries to solver, time in solver queries (ms) etc.). + */ + fun collectStatistics(): MinimalCoreStatistics { + require(this::coreStatistics.isInitialized) { + "Minimal core construction statistics is only available after core minimization launches with statistics collection enabled" + } + + return coreStatistics + } + + fun reset() = _minimalUnsatCoreModel.reset() + + private fun processUnsat( + notExpr: KExpr, + unknown: MutableList>, + minimalUnsatCore: List>, + ) { + val core = solver.unsatCore() + + if (!core.contains(notExpr)) { + // unknown := core \ mus + unknown.clear() + + for (e in core) { + if (!minimalUnsatCore.contains(e)) { + unknown.add(e) + } + } + } + } + + private class MinimalUnsatCoreModel( + private val ctx: KContext, + private val solver: KSolver, + ) { + private var _model: KModel? = null + private var _weight = 0u + + fun getBestModel(): Pair { + return Pair(_model, _weight) + } + + fun updateModel(assumptions: List) { + reset() + + if (assumptions.isEmpty()) { + return + } + + val model = solver.model().detach() + var weight = 0u + + for (asm in assumptions) { + if (ModelUtils.expressionIsNotTrue(ctx, model, asm.expression)) { + weight += asm.weight + } + } + + if (_model == null || weight < _weight) { + _model = model + _weight = weight + } + } + + fun reset() { + _model = null + _weight = 0u + } + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/statistics/KMaxSMTStatistics.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/statistics/KMaxSMTStatistics.kt new file mode 100644 index 000000000..a6252bd3c --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/statistics/KMaxSMTStatistics.kt @@ -0,0 +1,10 @@ +package io.ksmt.solver.maxsmt.statistics + +import io.ksmt.solver.maxsmt.KMaxSMTContext + +data class KMaxSMTStatistics(val maxSmtCtx: KMaxSMTContext) { + var timeoutMs: Long = 0 + var elapsedTimeMs: Long = 0 + var timeInSolverQueriesMs: Long = 0 + var queriesToSolverNumber = 0 +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/CoreUtils.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/CoreUtils.kt new file mode 100644 index 000000000..136951d5a --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/CoreUtils.kt @@ -0,0 +1,31 @@ +package io.ksmt.solver.maxsmt.utils + +import io.ksmt.expr.KExpr +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.sort.KBoolSort + +internal object CoreUtils { + fun coreToSoftConstraints(core: List>, assumptions: List): List { + val softs = mutableListOf() + + val potentialSofts = assumptions.filter { core.contains(it.expression) }.toMutableList() + + for (element in core) { + val softIndex = potentialSofts.indexOfFirst { it.expression == element } + val softElement = potentialSofts[softIndex] + + potentialSofts.removeAt(softIndex) + softs.add(softElement) + } + + return softs + } + + fun getCoreWeight(core: List): UInt { + if (core.isEmpty()) { + return 0u + } + + return core.minOf { it.weight } + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/ModelUtils.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/ModelUtils.kt new file mode 100644 index 000000000..ea1ac38f1 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/ModelUtils.kt @@ -0,0 +1,36 @@ +package io.ksmt.solver.maxsmt.utils + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.sort.KBoolSort + +internal object ModelUtils { + fun expressionIsNotTrue(ctx: KContext, model: KModel, expression: KExpr) = + model.eval(expression, true) != ctx.trueExpr + + fun getModelCost(ctx: KContext, model: KModel, softConstraints: List): ULong { + var upper = 0uL + + for (soft in softConstraints) { + if (expressionIsNotTrue(ctx, model, soft.expression)) { + upper += soft.weight + } + } + + return upper + } + + fun getCorrectionSet(ctx: KContext, model: KModel, softConstraints: List): List { + val correctionSet = mutableListOf() + + for (constr in softConstraints) { + if (expressionIsNotTrue(ctx, model, constr.expression)) { + correctionSet.add(constr) + } + } + + return correctionSet + } +} diff --git a/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/TimerUtils.kt b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/TimerUtils.kt new file mode 100644 index 000000000..6b1885de7 --- /dev/null +++ b/ksmt-maxsmt/src/main/kotlin/io/ksmt/solver/maxsmt/utils/TimerUtils.kt @@ -0,0 +1,13 @@ +package io.ksmt.solver.maxsmt.utils + +import kotlin.time.Duration +import kotlin.time.TimeSource.Monotonic.ValueTimeMark + +internal object TimerUtils { + fun computeRemainingTime(timeout: Duration, markStart: ValueTimeMark): Duration { + return timeout - markStart.elapsedNow() + } + + fun timeoutExceeded(timeout: Duration): Boolean = + timeout.isNegative() || timeout == Duration.ZERO +} diff --git a/ksmt-maxsmt/src/main/resources/log4j.xml b/ksmt-maxsmt/src/main/resources/log4j.xml new file mode 100644 index 000000000..80ab56d31 --- /dev/null +++ b/ksmt-maxsmt/src/main/resources/log4j.xml @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KMaxSMTSolverTest.kt b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KMaxSMTSolverTest.kt new file mode 100644 index 000000000..d80bf1b25 --- /dev/null +++ b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KMaxSMTSolverTest.kt @@ -0,0 +1,413 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.KContext +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus.SAT +import io.ksmt.solver.KSolverStatus.UNSAT +import io.ksmt.solver.maxsmt.constraints.SoftConstraint +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.utils.getValue +import org.junit.jupiter.api.AfterEach +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test + +abstract class KMaxSMTSolverTest { + abstract fun getSolver(): KMaxSMTSolverBase + + protected val ctx: KContext = KContext() + private lateinit var maxSMTSolver: KMaxSMTSolverBase + + @BeforeEach + fun initSolver() { + maxSMTSolver = getSolver() + } + + @AfterEach + fun closeSolver() = maxSMTSolver.close() + + @Test + fun hardConstraintsUnsatTest() = with(ctx) { + val a by boolSort + val b by boolSort + maxSMTSolver.assert(a) + maxSMTSolver.assert(b) + maxSMTSolver.assert(!a) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + assertTrue(maxSMTResult.hardConstraintsSatStatus == UNSAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.isEmpty()) + } + + @Test + fun hardConstraintsUnsatNoSoftTest() = with(ctx) { + val a by boolSort + val b by boolSort + maxSMTSolver.assert(a) + maxSMTSolver.assert(b) + maxSMTSolver.assert(!a) + + maxSMTSolver.assertSoft(a and !b, 3u) + maxSMTSolver.assertSoft(!a, 5u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == UNSAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.isEmpty()) + } + + @Test + fun noSoftConstraintsTest() = with(ctx) { + val a by boolSort + val b by boolSort + val c by boolSort + maxSMTSolver.assert(a) + maxSMTSolver.assert(b) + maxSMTSolver.assert(c) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.isEmpty()) + } + + @Test + fun noSoftConstraintsSatTest() = with(ctx) { + val a by boolSort + val b by boolSort + val c by boolSort + maxSMTSolver.assert(a) + maxSMTSolver.assert(b) + maxSMTSolver.assert(c) + maxSMTSolver.assertSoft(a and !c, 3u) + maxSMTSolver.assertSoft(!a, 5u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.isEmpty()) + } + + @Test + fun oneOfTwoSoftConstraintsSatTest() = with(ctx) { + val a by boolSort + val b by boolSort + + maxSMTSolver.assert(a or b) + maxSMTSolver.assert(!a or b) + + maxSMTSolver.assertSoft(a or !b, 2u) + maxSMTSolver.assertSoft(!a or !b, 3u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 1) + assertSoftConstraintsSat(listOf(SoftConstraint(!a or !b, 3u)), maxSMTResult.satSoftConstraints) + } + + @Test + fun twoOfFourSoftConstraintsSatTest() = with(ctx) { + val a by boolSort + val b by boolSort + val c by boolSort + val d by boolSort + + maxSMTSolver.assert(a or b) + maxSMTSolver.assert(c or d) + maxSMTSolver.assert(!a or b) + maxSMTSolver.assert(!c or d) + + maxSMTSolver.assertSoft(a or !b, 2u) + maxSMTSolver.assertSoft(c or !d, 2u) + maxSMTSolver.assertSoft(!a or !b, 3u) + maxSMTSolver.assertSoft(!c or !d, 3u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 2) + assertSoftConstraintsSat( + listOf(SoftConstraint(!a or !b, 3u), SoftConstraint(!c or !d, 3u)), + maxSMTResult.satSoftConstraints, + ) + } + + @Test + fun sixOfEightSoftConstraintsSatTest() = with(ctx) { + val a by boolSort + val b by boolSort + val c by boolSort + val d by boolSort + + maxSMTSolver.assertSoft(a or b, 9u) + maxSMTSolver.assertSoft(c or d, 9u) + maxSMTSolver.assertSoft(!a or b, 9u) + maxSMTSolver.assertSoft(!c or d, 9u) + maxSMTSolver.assertSoft(a or !b, 2u) + maxSMTSolver.assertSoft(c or !d, 2u) + maxSMTSolver.assertSoft(!a or !b, 3u) + maxSMTSolver.assertSoft(!c or !d, 3u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 6) + assertEquals(42u, maxSMTResult.satSoftConstraints.sumOf { it.weight }) + } + + @Test + fun twoOfThreeSoftConstraintsSatTest() = with(ctx) { + val a by boolSort + val b by boolSort + + maxSMTSolver.assert(a or b) + + maxSMTSolver.assertSoft(!a or b, 4u) + maxSMTSolver.assertSoft(a or !b, 6u) + maxSMTSolver.assertSoft(!a or !b, 2u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 2) + val softConstraintsToAssertSAT = + listOf(SoftConstraint(!a or b, 4u), SoftConstraint(a or !b, 6u)) + assertSoftConstraintsSat(softConstraintsToAssertSAT, maxSMTResult.satSoftConstraints) + } + + @Test + fun sameExpressionSoftConstraintsSatTest() = with(ctx) { + val x by boolSort + val y by boolSort + + maxSMTSolver.assert(x or y) + + maxSMTSolver.assertSoft(!x or y, 7u) + maxSMTSolver.assertSoft(x or !y, 6u) + maxSMTSolver.assertSoft(!x or !y, 3u) + maxSMTSolver.assertSoft(!x or !y, 4u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 3) + assertSoftConstraintsSat( + listOf( + SoftConstraint(!x or y, 7u), + SoftConstraint(!x or !y, 3u), + SoftConstraint(!x or !y, 4u), + ), + maxSMTResult.satSoftConstraints, + ) + } + + @Test + fun sameExpressionSoftConstraintsUnsatTest() = with(ctx) { + val x by boolSort + val y by boolSort + + maxSMTSolver.assert(x or y) + + maxSMTSolver.assertSoft(!x or y, 6u) + maxSMTSolver.assertSoft(x or !y, 6u) + maxSMTSolver.assertSoft(!x or !y, 3u) + maxSMTSolver.assertSoft(!x or !y, 2u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 2) + assertSoftConstraintsSat( + listOf(SoftConstraint(!x or y, 6u), SoftConstraint(x or !y, 6u)), + maxSMTResult.satSoftConstraints, + ) + } + + @Test + fun chooseOneConstraintByWeightTest() = with(ctx) { + val z by boolSort + val a by boolSort + val b by boolSort + + maxSMTSolver.assert(z) + maxSMTSolver.assertSoft(a and b, 1u) + maxSMTSolver.assertSoft(!a and !b, 5u) + maxSMTSolver.assertSoft(a and b and z, 2u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 1) + assertSoftConstraintsSat(listOf(SoftConstraint(!a and !b, 5u)), maxSMTResult.satSoftConstraints) + } + + @Test + fun equalWeightsTest() = with(ctx) { + val a by boolSort + val b by boolSort + + maxSMTSolver.assert(a or b) + maxSMTSolver.assert(!a or b) + + maxSMTSolver.assertSoft(a or !b, 2u) + maxSMTSolver.assertSoft(!a or !b, 2u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(maxSMTResult.satSoftConstraints.size == 1) + } + + @Test + fun similarExpressionsTest(): Unit = with(ctx) { + val a by boolSort + val b by boolSort + + maxSMTSolver.assertSoft(a or b, 1u) + maxSMTSolver.assertSoft(!a or b, 1u) + maxSMTSolver.assertSoft(a or !b, 1u) + maxSMTSolver.assertSoft(!a or !b, 1u) + maxSMTSolver.assertSoft(!a or !b or !b, 1u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(maxSMTResult.satSoftConstraints.size == 4) + assertTrue(maxSMTResult.satSoftConstraints.any { it.expression == !a or !b }) + assertTrue(maxSMTResult.satSoftConstraints.any { it.expression == !a or !b or !b }) + } + + @Test + fun inequalitiesTest() = with(ctx) { + val x by intSort + val y by intSort + + val a1 = x gt 0.expr + val a2 = x lt y + val a3 = x + y le 0.expr + + maxSMTSolver.assert(a3 eq a1) + maxSMTSolver.assert(a3 or a2) + + maxSMTSolver.assertSoft(a3, 3u) + maxSMTSolver.assertSoft(!a3, 5u) + maxSMTSolver.assertSoft(!a1, 10u) + maxSMTSolver.assertSoft(!a2, 3u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResult.satSoftConstraints.size == 2) + assertSoftConstraintsSat( + listOf(SoftConstraint(!a3, 5u), SoftConstraint(!a1, 10u)), + maxSMTResult.satSoftConstraints, + ) + } + + @Test + fun threeExpressionsAreInconsistentTest() = with(ctx) { + val x by boolSort + val y by boolSort + + maxSMTSolver.assertSoft(x, 671u) + maxSMTSolver.assertSoft(y, 783u) + maxSMTSolver.assertSoft(!x and !y or !x or !y, 859u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertSoftConstraintsSat( + listOf(SoftConstraint(y, 783u), SoftConstraint(!x and !y or !x or !y, 859u)), + maxSMTResult.satSoftConstraints, + ) + } + + @Test + fun oneScopePushPopTest() = with(ctx) { + val a by boolSort + val b by boolSort + + maxSMTSolver.assert(a or b) + + maxSMTSolver.assertSoft(!a or b, 1u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + assertSoftConstraintsSat(listOf(SoftConstraint(!a or b, 1u)), maxSMTResult.satSoftConstraints) + + maxSMTSolver.push() + + maxSMTSolver.assertSoft(a or !b, 1u) + maxSMTSolver.assertSoft(!a or !b, 1u) + + val maxSMTResultScoped = maxSMTSolver.checkMaxSMT() + + assertTrue(maxSMTResult.hardConstraintsSatStatus == SAT) + assertTrue(!maxSMTResult.timeoutExceededOrUnknown) + assertTrue(maxSMTResultScoped.satSoftConstraints.size == 2) + + maxSMTSolver.pop() + + assertSoftConstraintsSat(listOf(SoftConstraint(!a or b, 1u)), maxSMTResult.satSoftConstraints) + } + + @Test + fun threeScopesPushPopTest() = with(ctx) { + val a by boolSort + val b by boolSort + val c by boolSort + + maxSMTSolver.assert(a) + + maxSMTSolver.push() + maxSMTSolver.assertSoft(a or b, 1u) + maxSMTSolver.assertSoft(c or b, 1u) + + val maxSMTResult = maxSMTSolver.checkMaxSMT() + assertTrue(maxSMTResult.satSoftConstraints.size == 2) + + maxSMTSolver.push() + maxSMTSolver.assertSoft(!b and !c, 2u) + val maxSMTResult2 = maxSMTSolver.checkMaxSMT() + assertTrue(maxSMTResult2.satSoftConstraints.size == 2) + + maxSMTSolver.push() + maxSMTSolver.assertSoft(a or c, 1u) + val maxSMTResult3 = maxSMTSolver.checkMaxSMT() + assertTrue(maxSMTResult3.satSoftConstraints.size == 3) + + maxSMTSolver.pop(2u) + val maxSMTResult4 = maxSMTSolver.checkMaxSMT() + assertTrue(maxSMTResult4.satSoftConstraints.size == 2) + + maxSMTSolver.pop() + val maxSMTResult5 = maxSMTSolver.checkMaxSMT() + assertTrue(maxSMTResult5.satSoftConstraints.isEmpty()) + } + + private fun assertSoftConstraintsSat( + constraintsToAssert: List, + satConstraints: List, + ) { + for (constraint in constraintsToAssert) { + assertTrue( + satConstraints.any { + constraint.expression == it.expression && constraint.weight == it.weight + }, + ) + } + } +} diff --git a/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPMResSolverTest.kt b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPMResSolverTest.kt new file mode 100644 index 000000000..77e2b040a --- /dev/null +++ b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPMResSolverTest.kt @@ -0,0 +1,13 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPMResSolver +import io.ksmt.solver.z3.KZ3Solver + +class KPMResSolverTest : KMaxSMTSolverTest() { + override fun getSolver(): KMaxSMTSolverBase = with(ctx) { + val z3Solver = KZ3Solver(this) + return KPMResSolver(this, z3Solver) + } +} diff --git a/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver2Test.kt b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver2Test.kt new file mode 100644 index 000000000..e42617af6 --- /dev/null +++ b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver2Test.kt @@ -0,0 +1,13 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.z3.KZ3Solver + +class KPrimalDualMaxResSolver2Test : KMaxSMTSolverTest() { + override fun getSolver(): KMaxSMTSolverBase = with(ctx) { + val z3Solver = KZ3Solver(this) + return KPrimalDualMaxResSolver(this, z3Solver, KMaxSMTContext(preferLargeWeightConstraintsForCores = true)) + } +} diff --git a/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver3Test.kt b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver3Test.kt new file mode 100644 index 000000000..486d24e98 --- /dev/null +++ b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver3Test.kt @@ -0,0 +1,13 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.z3.KZ3Solver + +class KPrimalDualMaxResSolver3Test : KMaxSMTSolverTest() { + override fun getSolver(): KMaxSMTSolverBase = with(ctx) { + val z3Solver = KZ3Solver(this) + return KPrimalDualMaxResSolver(this, z3Solver, KMaxSMTContext(minimizeCores = true)) + } +} diff --git a/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver4Test.kt b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver4Test.kt new file mode 100644 index 000000000..dee45f28f --- /dev/null +++ b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolver4Test.kt @@ -0,0 +1,13 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.z3.KZ3Solver + +class KPrimalDualMaxResSolver4Test : KMaxSMTSolverTest() { + override fun getSolver(): KMaxSMTSolverBase = with(ctx) { + val z3Solver = KZ3Solver(this) + return KPrimalDualMaxResSolver(this, z3Solver, KMaxSMTContext(getMultipleCores = true)) + } +} diff --git a/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolverTest.kt b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolverTest.kt new file mode 100644 index 000000000..53dd34da2 --- /dev/null +++ b/ksmt-maxsmt/src/test/kotlin/io/ksmt/solver/maxsmt/KPrimalDualMaxResSolverTest.kt @@ -0,0 +1,13 @@ +package io.ksmt.solver.maxsmt + +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver +import io.ksmt.solver.z3.KZ3Solver + +class KPrimalDualMaxResSolverTest : KMaxSMTSolverTest() { + override fun getSolver(): KMaxSMTSolverBase = with(ctx) { + val z3Solver = KZ3Solver(this) + return KPrimalDualMaxResSolver(this, z3Solver, KMaxSMTContext()) + } +} diff --git a/ksmt-runner/build.gradle.kts b/ksmt-runner/build.gradle.kts index ef9b2c790..1459611bc 100644 --- a/ksmt-runner/build.gradle.kts +++ b/ksmt-runner/build.gradle.kts @@ -23,6 +23,7 @@ kotlin { dependencies { implementation(project(":ksmt-core")) + implementation(project(":ksmt-maxsmt")) implementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:1.6.4") diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt index 89b598d49..105fd6412 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt @@ -22,12 +22,15 @@ class SolverProtocolModel private constructor( private val _deleteSolver: RdCall, private val _configure: RdCall, Unit>, private val _assert: RdCall, + private val _assertSoft: RdCall, private val _bulkAssert: RdCall, private val _assertAndTrack: RdCall, private val _bulkAssertAndTrack: RdCall, private val _push: RdCall, private val _pop: RdCall, private val _check: RdCall, + private val _checkMaxSMT: RdCall, + private val _collectMaxSMTStatistics: RdCall, private val _checkWithAssumptions: RdCall, private val _model: RdCall, private val _unsatCore: RdCall, @@ -41,12 +44,16 @@ class SolverProtocolModel private constructor( override fun registerSerializersCore(serializers: ISerializers) { serializers.register(CreateSolverParams) serializers.register(SolverConfigurationParam) + serializers.register(SoftConstraint) serializers.register(AssertParams) serializers.register(BulkAssertParams) serializers.register(PopParams) serializers.register(CheckParams) serializers.register(CheckResult) + serializers.register(CheckMaxSMTParams) + serializers.register(CheckMaxSMTResult) serializers.register(CheckWithAssumptionsParams) + serializers.register(CollectMaxSMTStatisticsResult) serializers.register(UnsatCoreResult) serializers.register(ReasonUnknownResult) serializers.register(ModelFuncInterpEntry) @@ -80,7 +87,7 @@ class SolverProtocolModel private constructor( private val __SolverConfigurationParamListSerializer = SolverConfigurationParam.list() - const val serializationHash = 6588187342629653927L + const val serializationHash = -1861632144359942979L } override val serializersOwner: ISerializersOwner get() = SolverProtocolModel @@ -108,6 +115,11 @@ class SolverProtocolModel private constructor( */ val assert: RdCall get() = _assert + /** + * Assert expression softly + */ + val assertSoft: RdCall get() = _assertSoft + /** * Assert multiple expressions */ @@ -138,6 +150,16 @@ class SolverProtocolModel private constructor( */ val check: RdCall get() = _check + /** + * Check MaxSMT + */ + val checkMaxSMT: RdCall get() = _checkMaxSMT + + /** + * Collect MaxSMT statistics + */ + val collectMaxSMTStatistics: RdCall get() = _collectMaxSMTStatistics + /** * Check SAT with assumptions */ @@ -169,12 +191,15 @@ class SolverProtocolModel private constructor( _deleteSolver.async = true _configure.async = true _assert.async = true + _assertSoft.async = true _bulkAssert.async = true _assertAndTrack.async = true _bulkAssertAndTrack.async = true _push.async = true _pop.async = true _check.async = true + _checkMaxSMT.async = true + _collectMaxSMTStatistics.async = true _checkWithAssumptions.async = true _model.async = true _unsatCore.async = true @@ -187,12 +212,15 @@ class SolverProtocolModel private constructor( bindableChildren.add("deleteSolver" to _deleteSolver) bindableChildren.add("configure" to _configure) bindableChildren.add("assert" to _assert) + bindableChildren.add("assertSoft" to _assertSoft) bindableChildren.add("bulkAssert" to _bulkAssert) bindableChildren.add("assertAndTrack" to _assertAndTrack) bindableChildren.add("bulkAssertAndTrack" to _bulkAssertAndTrack) bindableChildren.add("push" to _push) bindableChildren.add("pop" to _pop) bindableChildren.add("check" to _check) + bindableChildren.add("checkMaxSMT" to _checkMaxSMT) + bindableChildren.add("collectMaxSMTStatistics" to _collectMaxSMTStatistics) bindableChildren.add("checkWithAssumptions" to _checkWithAssumptions) bindableChildren.add("model" to _model) bindableChildren.add("unsatCore" to _unsatCore) @@ -207,12 +235,15 @@ class SolverProtocolModel private constructor( RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void), RdCall, Unit>(__SolverConfigurationParamListSerializer, FrameworkMarshallers.Void), RdCall(AssertParams, FrameworkMarshallers.Void), + RdCall(SoftConstraint, FrameworkMarshallers.Void), RdCall(BulkAssertParams, FrameworkMarshallers.Void), RdCall(AssertParams, FrameworkMarshallers.Void), RdCall(BulkAssertParams, FrameworkMarshallers.Void), RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void), RdCall(PopParams, FrameworkMarshallers.Void), RdCall(CheckParams, CheckResult), + RdCall(CheckMaxSMTParams, CheckMaxSMTResult), + RdCall(FrameworkMarshallers.Void, CollectMaxSMTStatisticsResult), RdCall(CheckWithAssumptionsParams, CheckResult), RdCall(FrameworkMarshallers.Void, ModelResult), RdCall(FrameworkMarshallers.Void, UnsatCoreResult), @@ -230,12 +261,15 @@ class SolverProtocolModel private constructor( print("deleteSolver = "); _deleteSolver.print(printer); println() print("configure = "); _configure.print(printer); println() print("assert = "); _assert.print(printer); println() + print("assertSoft = "); _assertSoft.print(printer); println() print("bulkAssert = "); _bulkAssert.print(printer); println() print("assertAndTrack = "); _assertAndTrack.print(printer); println() print("bulkAssertAndTrack = "); _bulkAssertAndTrack.print(printer); println() print("push = "); _push.print(printer); println() print("pop = "); _pop.print(printer); println() print("check = "); _check.print(printer); println() + print("checkMaxSMT = "); _checkMaxSMT.print(printer); println() + print("collectMaxSMTStatistics = "); _collectMaxSMTStatistics.print(printer); println() print("checkWithAssumptions = "); _checkWithAssumptions.print(printer); println() print("model = "); _model.print(printer); println() print("unsatCore = "); _unsatCore.print(printer); println() @@ -251,12 +285,15 @@ class SolverProtocolModel private constructor( _deleteSolver.deepClonePolymorphic(), _configure.deepClonePolymorphic(), _assert.deepClonePolymorphic(), + _assertSoft.deepClonePolymorphic(), _bulkAssert.deepClonePolymorphic(), _assertAndTrack.deepClonePolymorphic(), _bulkAssertAndTrack.deepClonePolymorphic(), _push.deepClonePolymorphic(), _pop.deepClonePolymorphic(), _check.deepClonePolymorphic(), + _checkMaxSMT.deepClonePolymorphic(), + _collectMaxSMTStatistics.deepClonePolymorphic(), _checkWithAssumptions.deepClonePolymorphic(), _model.deepClonePolymorphic(), _unsatCore.deepClonePolymorphic(), @@ -271,7 +308,7 @@ val IProtocol.solverProtocolModel get() = getOrCreateExtension(SolverProtocolMod /** - * #### Generated from [SolverProtocolModel.kt:47] + * #### Generated from [SolverProtocolModel.kt:52] */ data class AssertParams ( val expression: io.ksmt.KAst @@ -328,7 +365,7 @@ data class AssertParams ( /** - * #### Generated from [SolverProtocolModel.kt:51] + * #### Generated from [SolverProtocolModel.kt:56] */ data class BulkAssertParams ( val expressions: List @@ -385,7 +422,145 @@ data class BulkAssertParams ( /** - * #### Generated from [SolverProtocolModel.kt:59] + * #### Generated from [SolverProtocolModel.kt:72] + */ +data class CheckMaxSMTParams ( + val timeout: Long, + val collectStatistics: Boolean +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = CheckMaxSMTParams::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): CheckMaxSMTParams { + val timeout = buffer.readLong() + val collectStatistics = buffer.readBool() + return CheckMaxSMTParams(timeout, collectStatistics) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: CheckMaxSMTParams) { + buffer.writeLong(value.timeout) + buffer.writeBool(value.collectStatistics) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as CheckMaxSMTParams + + if (timeout != other.timeout) return false + if (collectStatistics != other.collectStatistics) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + timeout.hashCode() + __r = __r*31 + collectStatistics.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("CheckMaxSMTParams (") + printer.indent { + print("timeout = "); timeout.print(printer); println() + print("collectStatistics = "); collectStatistics.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + +/** + * #### Generated from [SolverProtocolModel.kt:77] + */ +data class CheckMaxSMTResult ( + val satSoftConstraintExprs: List, + val satSoftConstraintWeights: List, + val hardConstraintsSatStatus: io.ksmt.solver.KSolverStatus, + val timeoutExceededOrUnknown: Boolean +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = CheckMaxSMTResult::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): CheckMaxSMTResult { + val satSoftConstraintExprs = buffer.readList { (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).read(ctx, buffer) } + val satSoftConstraintWeights = buffer.readList { buffer.readUInt() } + val hardConstraintsSatStatus = buffer.readEnum() + val timeoutExceededOrUnknown = buffer.readBool() + return CheckMaxSMTResult(satSoftConstraintExprs, satSoftConstraintWeights, hardConstraintsSatStatus, timeoutExceededOrUnknown) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: CheckMaxSMTResult) { + buffer.writeList(value.satSoftConstraintExprs) { v -> (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).write(ctx,buffer, v) } + buffer.writeList(value.satSoftConstraintWeights) { v -> buffer.writeUInt(v) } + buffer.writeEnum(value.hardConstraintsSatStatus) + buffer.writeBool(value.timeoutExceededOrUnknown) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as CheckMaxSMTResult + + if (satSoftConstraintExprs != other.satSoftConstraintExprs) return false + if (satSoftConstraintWeights != other.satSoftConstraintWeights) return false + if (hardConstraintsSatStatus != other.hardConstraintsSatStatus) return false + if (timeoutExceededOrUnknown != other.timeoutExceededOrUnknown) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + satSoftConstraintExprs.hashCode() + __r = __r*31 + satSoftConstraintWeights.hashCode() + __r = __r*31 + hardConstraintsSatStatus.hashCode() + __r = __r*31 + timeoutExceededOrUnknown.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("CheckMaxSMTResult (") + printer.indent { + print("satSoftConstraintExprs = "); satSoftConstraintExprs.print(printer); println() + print("satSoftConstraintWeights = "); satSoftConstraintWeights.print(printer); println() + print("hardConstraintsSatStatus = "); hardConstraintsSatStatus.print(printer); println() + print("timeoutExceededOrUnknown = "); timeoutExceededOrUnknown.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + +/** + * #### Generated from [SolverProtocolModel.kt:64] */ data class CheckParams ( val timeout: Long @@ -442,7 +617,7 @@ data class CheckParams ( /** - * #### Generated from [SolverProtocolModel.kt:63] + * #### Generated from [SolverProtocolModel.kt:68] */ data class CheckResult ( val status: io.ksmt.solver.KSolverStatus @@ -499,7 +674,7 @@ data class CheckResult ( /** - * #### Generated from [SolverProtocolModel.kt:67] + * #### Generated from [SolverProtocolModel.kt:84] */ data class CheckWithAssumptionsParams ( val assumptions: List, @@ -561,6 +736,81 @@ data class CheckWithAssumptionsParams ( } +/** + * #### Generated from [SolverProtocolModel.kt:89] + */ +data class CollectMaxSMTStatisticsResult ( + val timeoutMs: Long, + val elapsedTimeMs: Long, + val timeInSolverQueriesMs: Long, + val queriesToSolverNumber: Int +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = CollectMaxSMTStatisticsResult::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): CollectMaxSMTStatisticsResult { + val timeoutMs = buffer.readLong() + val elapsedTimeMs = buffer.readLong() + val timeInSolverQueriesMs = buffer.readLong() + val queriesToSolverNumber = buffer.readInt() + return CollectMaxSMTStatisticsResult(timeoutMs, elapsedTimeMs, timeInSolverQueriesMs, queriesToSolverNumber) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: CollectMaxSMTStatisticsResult) { + buffer.writeLong(value.timeoutMs) + buffer.writeLong(value.elapsedTimeMs) + buffer.writeLong(value.timeInSolverQueriesMs) + buffer.writeInt(value.queriesToSolverNumber) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as CollectMaxSMTStatisticsResult + + if (timeoutMs != other.timeoutMs) return false + if (elapsedTimeMs != other.elapsedTimeMs) return false + if (timeInSolverQueriesMs != other.timeInSolverQueriesMs) return false + if (queriesToSolverNumber != other.queriesToSolverNumber) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + timeoutMs.hashCode() + __r = __r*31 + elapsedTimeMs.hashCode() + __r = __r*31 + timeInSolverQueriesMs.hashCode() + __r = __r*31 + queriesToSolverNumber.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("CollectMaxSMTStatisticsResult (") + printer.indent { + print("timeoutMs = "); timeoutMs.print(printer); println() + print("elapsedTimeMs = "); elapsedTimeMs.print(printer); println() + print("timeInSolverQueriesMs = "); timeInSolverQueriesMs.print(printer); println() + print("queriesToSolverNumber = "); queriesToSolverNumber.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + /** * #### Generated from [SolverProtocolModel.kt:37] */ @@ -667,7 +917,7 @@ data class CreateSolverParams ( /** - * #### Generated from [SolverProtocolModel.kt:86] + * #### Generated from [SolverProtocolModel.kt:110] */ data class ModelEntry ( val decl: io.ksmt.KAst, @@ -742,7 +992,7 @@ data class ModelEntry ( /** - * #### Generated from [SolverProtocolModel.kt:80] + * #### Generated from [SolverProtocolModel.kt:104] */ data class ModelFuncInterpEntry ( val hasVars: Boolean, @@ -811,7 +1061,7 @@ data class ModelFuncInterpEntry ( /** - * #### Generated from [SolverProtocolModel.kt:98] + * #### Generated from [SolverProtocolModel.kt:122] */ data class ModelResult ( val declarations: List, @@ -880,7 +1130,7 @@ data class ModelResult ( /** - * #### Generated from [SolverProtocolModel.kt:93] + * #### Generated from [SolverProtocolModel.kt:117] */ data class ModelUninterpretedSortUniverse ( val sort: io.ksmt.KAst, @@ -943,7 +1193,7 @@ data class ModelUninterpretedSortUniverse ( /** - * #### Generated from [SolverProtocolModel.kt:55] + * #### Generated from [SolverProtocolModel.kt:60] */ data class PopParams ( val levels: UInt @@ -1000,7 +1250,7 @@ data class PopParams ( /** - * #### Generated from [SolverProtocolModel.kt:76] + * #### Generated from [SolverProtocolModel.kt:100] */ data class ReasonUnknownResult ( val reasonUnknown: String @@ -1056,6 +1306,69 @@ data class ReasonUnknownResult ( } +/** + * #### Generated from [SolverProtocolModel.kt:47] + */ +data class SoftConstraint ( + val expression: io.ksmt.KAst, + val weight: UInt +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = SoftConstraint::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): SoftConstraint { + val expression = (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).read(ctx, buffer) + val weight = buffer.readUInt() + return SoftConstraint(expression, weight) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: SoftConstraint) { + (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).write(ctx,buffer, value.expression) + buffer.writeUInt(value.weight) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as SoftConstraint + + if (expression != other.expression) return false + if (weight != other.weight) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + expression.hashCode() + __r = __r*31 + weight.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("SoftConstraint (") + printer.indent { + print("expression = "); expression.print(printer); println() + print("weight = "); weight.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + /** * #### Generated from [SolverProtocolModel.kt:36] */ @@ -1143,7 +1456,7 @@ enum class SolverType { /** - * #### Generated from [SolverProtocolModel.kt:72] + * #### Generated from [SolverProtocolModel.kt:96] */ data class UnsatCoreResult ( val core: List diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/TestProtocolModel.Generated.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/TestProtocolModel.Generated.kt index 1e8a3cc8d..ef980a754 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/TestProtocolModel.Generated.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/TestProtocolModel.Generated.kt @@ -27,7 +27,10 @@ class TestProtocolModel private constructor( private val _internalizeAndConvertCvc5: RdCall, private val _createSolver: RdCall, private val _assert: RdCall, + private val _assertSoft: RdCall, private val _check: RdCall, + private val _checkMaxSMT: RdCall, + private val _collectMaxSMTStatistics: RdCall, private val _exprToString: RdCall, private val _getReasonUnknown: RdCall, private val _addEqualityCheck: RdCall, @@ -41,10 +44,14 @@ class TestProtocolModel private constructor( companion object : ISerializersOwner { override fun registerSerializersCore(serializers: ISerializers) { + serializers.register(TestSoftConstraint) serializers.register(EqualityCheckParams) serializers.register(EqualityCheckAssumptionsParams) serializers.register(TestAssertParams) serializers.register(TestCheckResult) + serializers.register(TestCheckMaxSMTParams) + serializers.register(TestCheckMaxSMTResult) + serializers.register(TestCollectMaxSMTStatisticsResult) serializers.register(TestConversionResult) serializers.register(TestInternalizeAndConvertParams) } @@ -72,7 +79,7 @@ class TestProtocolModel private constructor( private val __LongListSerializer = FrameworkMarshallers.Long.list() private val __IntNullableSerializer = FrameworkMarshallers.Int.nullable() - const val serializationHash = -2815464060158594303L + const val serializationHash = 1052422932439377909L } override val serializersOwner: ISerializersOwner get() = TestProtocolModel @@ -125,11 +132,26 @@ class TestProtocolModel private constructor( */ val assert: RdCall get() = _assert + /** + * Assert expression softly + */ + val assertSoft: RdCall get() = _assertSoft + /** * Check-sat */ val check: RdCall get() = _check + /** + * Check MaxSMT + */ + val checkMaxSMT: RdCall get() = _checkMaxSMT + + /** + * Collect MaxSMT statistics + */ + val collectMaxSMTStatistics: RdCall get() = _collectMaxSMTStatistics + /** * Expression to string */ @@ -176,7 +198,10 @@ class TestProtocolModel private constructor( _internalizeAndConvertCvc5.async = true _createSolver.async = true _assert.async = true + _assertSoft.async = true _check.async = true + _checkMaxSMT.async = true + _collectMaxSMTStatistics.async = true _exprToString.async = true _getReasonUnknown.async = true _addEqualityCheck.async = true @@ -196,7 +221,10 @@ class TestProtocolModel private constructor( bindableChildren.add("internalizeAndConvertCvc5" to _internalizeAndConvertCvc5) bindableChildren.add("createSolver" to _createSolver) bindableChildren.add("assert" to _assert) + bindableChildren.add("assertSoft" to _assertSoft) bindableChildren.add("check" to _check) + bindableChildren.add("checkMaxSMT" to _checkMaxSMT) + bindableChildren.add("collectMaxSMTStatistics" to _collectMaxSMTStatistics) bindableChildren.add("exprToString" to _exprToString) bindableChildren.add("getReasonUnknown" to _getReasonUnknown) bindableChildren.add("addEqualityCheck" to _addEqualityCheck) @@ -218,7 +246,10 @@ class TestProtocolModel private constructor( RdCall(TestInternalizeAndConvertParams, TestConversionResult), RdCall(FrameworkMarshallers.Int, FrameworkMarshallers.Int), RdCall(TestAssertParams, FrameworkMarshallers.Void), + RdCall(TestSoftConstraint, FrameworkMarshallers.Void), RdCall(FrameworkMarshallers.Int, TestCheckResult), + RdCall(TestCheckMaxSMTParams, TestCheckMaxSMTResult), + RdCall(FrameworkMarshallers.Void, TestCollectMaxSMTStatisticsResult), RdCall(FrameworkMarshallers.Long, FrameworkMarshallers.String), RdCall(FrameworkMarshallers.Int, FrameworkMarshallers.String), RdCall(EqualityCheckParams, FrameworkMarshallers.Void), @@ -243,7 +274,10 @@ class TestProtocolModel private constructor( print("internalizeAndConvertCvc5 = "); _internalizeAndConvertCvc5.print(printer); println() print("createSolver = "); _createSolver.print(printer); println() print("assert = "); _assert.print(printer); println() + print("assertSoft = "); _assertSoft.print(printer); println() print("check = "); _check.print(printer); println() + print("checkMaxSMT = "); _checkMaxSMT.print(printer); println() + print("collectMaxSMTStatistics = "); _collectMaxSMTStatistics.print(printer); println() print("exprToString = "); _exprToString.print(printer); println() print("getReasonUnknown = "); _getReasonUnknown.print(printer); println() print("addEqualityCheck = "); _addEqualityCheck.print(printer); println() @@ -266,7 +300,10 @@ class TestProtocolModel private constructor( _internalizeAndConvertCvc5.deepClonePolymorphic(), _createSolver.deepClonePolymorphic(), _assert.deepClonePolymorphic(), + _assertSoft.deepClonePolymorphic(), _check.deepClonePolymorphic(), + _checkMaxSMT.deepClonePolymorphic(), + _collectMaxSMTStatistics.deepClonePolymorphic(), _exprToString.deepClonePolymorphic(), _getReasonUnknown.deepClonePolymorphic(), _addEqualityCheck.deepClonePolymorphic(), @@ -283,7 +320,7 @@ val IProtocol.testProtocolModel get() = getOrCreateExtension(TestProtocolModel:: /** - * #### Generated from [TestProtocolModel.kt:25] + * #### Generated from [TestProtocolModel.kt:30] */ data class EqualityCheckAssumptionsParams ( val solver: Int, @@ -346,7 +383,7 @@ data class EqualityCheckAssumptionsParams ( /** - * #### Generated from [TestProtocolModel.kt:19] + * #### Generated from [TestProtocolModel.kt:24] */ data class EqualityCheckParams ( val solver: Int, @@ -415,7 +452,7 @@ data class EqualityCheckParams ( /** - * #### Generated from [TestProtocolModel.kt:30] + * #### Generated from [TestProtocolModel.kt:35] */ data class TestAssertParams ( val solver: Int, @@ -478,7 +515,145 @@ data class TestAssertParams ( /** - * #### Generated from [TestProtocolModel.kt:35] + * #### Generated from [TestProtocolModel.kt:44] + */ +data class TestCheckMaxSMTParams ( + val timeout: Long, + val collectStatistics: Boolean +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = TestCheckMaxSMTParams::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): TestCheckMaxSMTParams { + val timeout = buffer.readLong() + val collectStatistics = buffer.readBool() + return TestCheckMaxSMTParams(timeout, collectStatistics) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: TestCheckMaxSMTParams) { + buffer.writeLong(value.timeout) + buffer.writeBool(value.collectStatistics) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as TestCheckMaxSMTParams + + if (timeout != other.timeout) return false + if (collectStatistics != other.collectStatistics) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + timeout.hashCode() + __r = __r*31 + collectStatistics.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("TestCheckMaxSMTParams (") + printer.indent { + print("timeout = "); timeout.print(printer); println() + print("collectStatistics = "); collectStatistics.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + +/** + * #### Generated from [TestProtocolModel.kt:49] + */ +data class TestCheckMaxSMTResult ( + val satSoftConstraintExprs: List, + val satSoftConstraintWeights: List, + val hardConstraintsSatStatus: io.ksmt.solver.KSolverStatus, + val timeoutExceededOrUnknown: Boolean +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = TestCheckMaxSMTResult::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): TestCheckMaxSMTResult { + val satSoftConstraintExprs = buffer.readList { (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).read(ctx, buffer) } + val satSoftConstraintWeights = buffer.readList { buffer.readUInt() } + val hardConstraintsSatStatus = buffer.readEnum() + val timeoutExceededOrUnknown = buffer.readBool() + return TestCheckMaxSMTResult(satSoftConstraintExprs, satSoftConstraintWeights, hardConstraintsSatStatus, timeoutExceededOrUnknown) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: TestCheckMaxSMTResult) { + buffer.writeList(value.satSoftConstraintExprs) { v -> (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).write(ctx,buffer, v) } + buffer.writeList(value.satSoftConstraintWeights) { v -> buffer.writeUInt(v) } + buffer.writeEnum(value.hardConstraintsSatStatus) + buffer.writeBool(value.timeoutExceededOrUnknown) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as TestCheckMaxSMTResult + + if (satSoftConstraintExprs != other.satSoftConstraintExprs) return false + if (satSoftConstraintWeights != other.satSoftConstraintWeights) return false + if (hardConstraintsSatStatus != other.hardConstraintsSatStatus) return false + if (timeoutExceededOrUnknown != other.timeoutExceededOrUnknown) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + satSoftConstraintExprs.hashCode() + __r = __r*31 + satSoftConstraintWeights.hashCode() + __r = __r*31 + hardConstraintsSatStatus.hashCode() + __r = __r*31 + timeoutExceededOrUnknown.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("TestCheckMaxSMTResult (") + printer.indent { + print("satSoftConstraintExprs = "); satSoftConstraintExprs.print(printer); println() + print("satSoftConstraintWeights = "); satSoftConstraintWeights.print(printer); println() + print("hardConstraintsSatStatus = "); hardConstraintsSatStatus.print(printer); println() + print("timeoutExceededOrUnknown = "); timeoutExceededOrUnknown.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + +/** + * #### Generated from [TestProtocolModel.kt:40] */ data class TestCheckResult ( val status: io.ksmt.solver.KSolverStatus @@ -535,7 +710,82 @@ data class TestCheckResult ( /** - * #### Generated from [TestProtocolModel.kt:39] + * #### Generated from [TestProtocolModel.kt:56] + */ +data class TestCollectMaxSMTStatisticsResult ( + val timeoutMs: Long, + val elapsedTimeMs: Long, + val timeInSolverQueriesMs: Long, + val queriesToSolverNumber: Int +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = TestCollectMaxSMTStatisticsResult::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): TestCollectMaxSMTStatisticsResult { + val timeoutMs = buffer.readLong() + val elapsedTimeMs = buffer.readLong() + val timeInSolverQueriesMs = buffer.readLong() + val queriesToSolverNumber = buffer.readInt() + return TestCollectMaxSMTStatisticsResult(timeoutMs, elapsedTimeMs, timeInSolverQueriesMs, queriesToSolverNumber) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: TestCollectMaxSMTStatisticsResult) { + buffer.writeLong(value.timeoutMs) + buffer.writeLong(value.elapsedTimeMs) + buffer.writeLong(value.timeInSolverQueriesMs) + buffer.writeInt(value.queriesToSolverNumber) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as TestCollectMaxSMTStatisticsResult + + if (timeoutMs != other.timeoutMs) return false + if (elapsedTimeMs != other.elapsedTimeMs) return false + if (timeInSolverQueriesMs != other.timeInSolverQueriesMs) return false + if (queriesToSolverNumber != other.queriesToSolverNumber) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + timeoutMs.hashCode() + __r = __r*31 + elapsedTimeMs.hashCode() + __r = __r*31 + timeInSolverQueriesMs.hashCode() + __r = __r*31 + queriesToSolverNumber.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("TestCollectMaxSMTStatisticsResult (") + printer.indent { + print("timeoutMs = "); timeoutMs.print(printer); println() + print("elapsedTimeMs = "); elapsedTimeMs.print(printer); println() + print("timeInSolverQueriesMs = "); timeInSolverQueriesMs.print(printer); println() + print("queriesToSolverNumber = "); queriesToSolverNumber.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + +/** + * #### Generated from [TestProtocolModel.kt:63] */ data class TestConversionResult ( val expressions: List @@ -592,7 +842,7 @@ data class TestConversionResult ( /** - * #### Generated from [TestProtocolModel.kt:43] + * #### Generated from [TestProtocolModel.kt:67] */ data class TestInternalizeAndConvertParams ( val expressions: List @@ -646,3 +896,66 @@ data class TestInternalizeAndConvertParams ( //deepClone //contexts } + + +/** + * #### Generated from [TestProtocolModel.kt:19] + */ +data class TestSoftConstraint ( + val expression: io.ksmt.KAst, + val weight: UInt +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = TestSoftConstraint::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): TestSoftConstraint { + val expression = (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).read(ctx, buffer) + val weight = buffer.readUInt() + return TestSoftConstraint(expression, weight) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: TestSoftConstraint) { + (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).write(ctx,buffer, value.expression) + buffer.writeUInt(value.weight) + } + + + } + //fields + //methods + //initializer + //secondary constructor + //equals trait + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other::class != this::class) return false + + other as TestSoftConstraint + + if (expression != other.expression) return false + if (weight != other.weight) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + expression.hashCode() + __r = __r*31 + weight.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("TestSoftConstraint (") + printer.indent { + print("expression = "); expression.print(printer); println() + print("weight = "); weight.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt index 161a5b1ef..583bcdb37 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt @@ -2,15 +2,6 @@ package io.ksmt.solver.portfolio import com.jetbrains.rd.util.AtomicInteger import com.jetbrains.rd.util.AtomicReference -import kotlinx.coroutines.CompletableDeferred -import kotlinx.coroutines.CoroutineExceptionHandler -import kotlinx.coroutines.CoroutineScope -import kotlinx.coroutines.DelicateCoroutinesApi -import kotlinx.coroutines.Job -import kotlinx.coroutines.joinAll -import kotlinx.coroutines.launch -import kotlinx.coroutines.newSingleThreadContext -import kotlinx.coroutines.runBlocking import io.ksmt.expr.KExpr import io.ksmt.solver.KModel import io.ksmt.solver.KSolver @@ -18,8 +9,20 @@ import io.ksmt.solver.KSolverConfiguration import io.ksmt.solver.KSolverException import io.ksmt.solver.KSolverStatus import io.ksmt.solver.async.KAsyncSolver +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverInterface +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics import io.ksmt.solver.runner.KSolverRunner import io.ksmt.sort.KBoolSort +import kotlinx.coroutines.CompletableDeferred +import kotlinx.coroutines.CoroutineExceptionHandler +import kotlinx.coroutines.CoroutineScope +import kotlinx.coroutines.DelicateCoroutinesApi +import kotlinx.coroutines.Job +import kotlinx.coroutines.joinAll +import kotlinx.coroutines.launch +import kotlinx.coroutines.newSingleThreadContext +import kotlinx.coroutines.runBlocking import java.util.concurrent.ConcurrentLinkedQueue import java.util.concurrent.atomic.AtomicBoolean import java.util.concurrent.atomic.AtomicReferenceArray @@ -28,7 +31,7 @@ import kotlin.time.Duration class KPortfolioSolver( solverRunners: List>, KSolverRunner<*>>> -) : KAsyncSolver { +) : KAsyncSolver, KMaxSMTSolverInterface { private val lastSuccessfulSolver = AtomicReference?>(null) private val pendingTermination = ConcurrentLinkedQueue>() @@ -61,7 +64,7 @@ class KPortfolioSolver( } } - class SolverStatistic(val solver: KClass>) { + private class SolverStatistic(val solver: KClass>) { private val numberOfBestQueries = AtomicInteger(0) private val solverIsActive = AtomicBoolean(true) @@ -71,11 +74,11 @@ class KPortfolioSolver( val isActive: Boolean get() = solverIsActive.get() - internal fun logSolverQueryBest() { + fun logSolverQueryBest() { numberOfBestQueries.incrementAndGet() } - internal fun logSolverRemovedFromPortfolio() { + fun logSolverRemovedFromPortfolio() { solverIsActive.set(false) } @@ -96,7 +99,7 @@ class KPortfolioSolver( /** * Gather current statistic on the solvers in the portfolio. * */ - fun solverPortfolioStats(): List = solverStats.toList() + private fun solverPortfolioStats(): List = solverStats.toList() override fun configure(configurator: KSolverConfiguration.() -> Unit) = runBlocking { configureAsync(configurator) @@ -110,6 +113,12 @@ class KPortfolioSolver( assertAsync(exprs) } + override fun assertSoft(expr: KExpr, weight: UInt) = runBlocking { + solverOperation { + assertSoft(expr, weight) + } + } + override fun assertAndTrack(expr: KExpr) = runBlocking { assertAndTrackAsync(expr) } @@ -130,6 +139,29 @@ class KPortfolioSolver( checkAsync(timeout) } + override fun checkMaxSMT(timeout: Duration, collectStatistics: Boolean): KMaxSMTResult = runBlocking { + solverMaxSmtQueryAsync( + { checkSubOptMaxSMT(timeout, collectStatistics) }, + solverPredicate = { !this.timeoutExceededOrUnknown }, + onFailure = { results -> + results.results + .mapNotNull { it.getOrNull() } + .maxByOrNull { it.result.satSoftConstraints.sumOf { constr -> constr.weight } }!! + } + ) + } + + override fun collectMaxSMTStatistics(): KMaxSMTStatistics = runBlocking { + val solverAwaitResult = solverOperationWithResult( + { this.collectMaxSMTStatistics() } + ) + + when (solverAwaitResult) { + is SolverAwaitSuccess -> return@runBlocking solverAwaitResult.result.result + is SolverAwaitFailure -> throw KSolverException("MaxSMT portfolio solver failed") + } + } + override fun checkWithAssumptions( assumptions: List>, timeout: Duration @@ -181,16 +213,19 @@ class KPortfolioSolver( popAsync(n) } - override suspend fun checkAsync(timeout: Duration): KSolverStatus = solverQuery { - checkAsync(timeout) - } + override suspend fun checkAsync(timeout: Duration): KSolverStatus = solverQuery( + { checkAsync(timeout) }, + { this != KSolverStatus.UNKNOWN } + ) override suspend fun checkWithAssumptionsAsync( assumptions: List>, timeout: Duration - ): KSolverStatus = solverQuery { - checkWithAssumptionsAsync(assumptions, timeout) - } + ): KSolverStatus = solverQuery( + { checkWithAssumptionsAsync(assumptions, timeout) }, + { this != KSolverStatus.UNKNOWN } + + ) override suspend fun modelAsync(): KModel = lastSuccessfulSolver.get()?.modelAsync() @@ -233,15 +268,68 @@ class KPortfolioSolver( } } - private suspend inline fun solverQuery( - crossinline block: suspend KSolverRunner<*>.() -> KSolverStatus - ): KSolverStatus { + private suspend inline fun solverOperationWithResult( + crossinline block: suspend KSolverRunner<*>.() -> T, + crossinline predicate: (T) -> Boolean = { true } + ): SolverAwaitResult { + val result = awaitFirstSolver(block, predicate) + if (result is SolverAwaitFailure<*>) { + // throw exception if all solvers in portfolio failed with exception + result.findSuccessOrThrow() + } + + return result + } + + private suspend inline fun solverMaxSmtQueryAsync( + crossinline block: suspend KSolverRunner<*>.() -> T, + crossinline solverPredicate: T.() -> Boolean, + crossinline onFailure: (SolverAwaitFailure) -> SolverOperationResult = { it.findSuccessOrThrow() } + ): T { + terminateIfNeeded() + + lastSuccessfulSolver.getAndSet(null) + + val awaitResult = awaitFirstSolver(block) { + solverPredicate(it) + } + + val result = when (awaitResult) { + is SolverAwaitSuccess -> awaitResult.result.also { + solverStats[awaitResult.result.solverId].logSolverQueryBest() + } + /** + * All solvers finished with Unknown or failed with exception. + * If some solver ends up with Unknown we can treat this result as successful. + * */ + is SolverAwaitFailure -> onFailure(awaitResult) + } + + lastSuccessfulSolver.getAndSet(result.solver) + + activeSolvers.forEach { _, solverOperationState -> + if (solverOperationState.solver != result.solver) { + val failedSolver = solverOperationState.solver + solverOperationState.operationScope.launch { + failedSolver.interruptAsync() + } + pendingTermination.offer(failedSolver) + } + } + + return result.result + } + + private suspend inline fun solverQuery( + crossinline block: suspend KSolverRunner<*>.() -> T, + crossinline solverPredicate: T.() -> Boolean + ): T { terminateIfNeeded() lastSuccessfulSolver.getAndSet(null) val awaitResult = awaitFirstSolver(block) { - it != KSolverStatus.UNKNOWN + solverPredicate(it) } val result = when (awaitResult) { diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolverManager.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolverManager.kt index 87d5b3c89..db099264d 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolverManager.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolverManager.kt @@ -3,13 +3,14 @@ package io.ksmt.solver.portfolio import io.ksmt.KContext import io.ksmt.solver.KSolver import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext import io.ksmt.solver.runner.KSolverRunnerManager import io.ksmt.utils.uncheckedCast import kotlin.reflect.KClass import kotlin.time.Duration import kotlin.time.Duration.Companion.seconds -class KPortfolioSolverManager( +open class KPortfolioSolverManager( private val solvers: List>>, portfolioPoolSize: Int = DEFAULT_PORTFOLIO_POOL_SIZE, hardTimeout: Duration = DEFAULT_HARD_TIMEOUT, @@ -23,10 +24,13 @@ class KPortfolioSolverManager( require(solvers.isNotEmpty()) { "Empty solver portfolio" } } - fun createPortfolioSolver(ctx: KContext): KPortfolioSolver { + fun createPortfolioSolver( + ctx: KContext, + maxsmtCtx: KMaxSMTContext = KMaxSMTContext(preferLargeWeightConstraintsForCores = true) + ): KPortfolioSolver { val solverInstances = solvers.map { val solverType: KClass> = it.uncheckedCast() - it to createSolver(ctx, solverType) + it to createSolver(ctx, maxsmtCtx, solverType) } return KPortfolioSolver(solverInstances) } diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt index e77ee03f7..a14111ac8 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt @@ -2,7 +2,6 @@ package io.ksmt.solver.runner import com.jetbrains.rd.util.AtomicReference import com.jetbrains.rd.util.threading.SpinWait -import kotlinx.coroutines.sync.Mutex import io.ksmt.KContext import io.ksmt.expr.KExpr import io.ksmt.runner.generated.ConfigurationBuilder @@ -13,8 +12,12 @@ import io.ksmt.solver.KSolverConfiguration import io.ksmt.solver.KSolverException import io.ksmt.solver.KSolverStatus import io.ksmt.solver.async.KAsyncSolver +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics import io.ksmt.solver.runner.KSolverRunnerManager.CustomSolverInfo import io.ksmt.sort.KBoolSort +import kotlinx.coroutines.sync.Mutex import java.util.concurrent.atomic.AtomicBoolean import kotlin.time.Duration @@ -27,6 +30,7 @@ import kotlin.time.Duration class KSolverRunner( private val manager: KSolverRunnerManager, private val ctx: KContext, + private val maxSmtCtx: KMaxSMTContext = KMaxSMTContext(), private val configurationBuilder: ConfigurationBuilder, private val solverType: SolverType, private val customSolverInfo: CustomSolverInfo? = null, @@ -115,6 +119,14 @@ class KSolverRunner( } } + suspend fun assertSoft(expr: KExpr, weight: UInt) { + ctx.ensureContextMatch(expr) + + ensureInitializedAndExecuteAsync(onException = {}) { + assertSoft(expr, weight) + } + } + private inline fun bulkAssert( exprs: List>, execute: (List>) -> Unit @@ -232,6 +244,16 @@ class KSolverRunner( checkSync(timeout) } + suspend fun checkMaxSMT(timeout: Duration, collectStatistics: Boolean): KMaxSMTResult = + handleCheckAnyMaxSMTExceptionAsNotSucceededAsync { + checkMaxSMT(timeout, collectStatistics) + } + + suspend fun collectMaxSMTStatistics(): KMaxSMTStatistics = + handleCollectStatisticsAsync { + collectMaxSMTStatistics() + } + override suspend fun checkWithAssumptionsAsync( assumptions: List>, timeout: Duration @@ -425,6 +447,30 @@ class KSolverRunner( ) } + private suspend inline fun handleCheckAnyMaxSMTExceptionAsNotSucceededAsync( + crossinline body: suspend KSolverRunnerExecutor.() -> KMaxSMTResult + ): KMaxSMTResult { + return ensureInitializedAndExecuteAsync( + body = body, + onException = { + KMaxSMTResult( + emptyList(), + KSolverStatus.UNKNOWN, + timeoutExceededOrUnknown = true + ) + } + ) + } + + private suspend inline fun handleCollectStatisticsAsync( + crossinline body: suspend KSolverRunnerExecutor.() -> KMaxSMTStatistics + ): KMaxSMTStatistics { + return ensureInitializedAndExecuteAsync( + body = body, + onException = { KMaxSMTStatistics(maxSmtCtx) } + ) + } + private inline fun handleCheckSatExceptionAsUnknown( execute: ((KSolverExecutorException) -> KSolverStatus) -> KSolverStatus ): KSolverStatus { diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt index 328cc9cbf..0ddd254f6 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt @@ -8,8 +8,6 @@ import com.jetbrains.rd.util.TimeoutException import com.jetbrains.rd.util.lifetime.Lifetime import com.jetbrains.rd.util.reactive.RdFault import com.jetbrains.rd.util.threading.SynchronousScheduler -import kotlinx.coroutines.TimeoutCancellationException -import kotlinx.coroutines.withTimeout import io.ksmt.KContext import io.ksmt.decl.KDecl import io.ksmt.expr.KExpr @@ -17,45 +15,55 @@ import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.runner.core.KsmtWorkerSession import io.ksmt.runner.generated.models.AssertParams import io.ksmt.runner.generated.models.BulkAssertParams +import io.ksmt.runner.generated.models.CheckMaxSMTParams +import io.ksmt.runner.generated.models.CheckMaxSMTResult import io.ksmt.runner.generated.models.CheckParams import io.ksmt.runner.generated.models.CheckResult import io.ksmt.runner.generated.models.CheckWithAssumptionsParams import io.ksmt.runner.generated.models.ContextSimplificationMode import io.ksmt.runner.generated.models.CreateSolverParams -import io.ksmt.runner.generated.models.ModelResult import io.ksmt.runner.generated.models.ModelEntry import io.ksmt.runner.generated.models.ModelFuncInterpEntry +import io.ksmt.runner.generated.models.ModelResult import io.ksmt.runner.generated.models.PopParams import io.ksmt.runner.generated.models.ReasonUnknownResult +import io.ksmt.runner.generated.models.SoftConstraint import io.ksmt.runner.generated.models.SolverConfigurationParam import io.ksmt.runner.generated.models.SolverProtocolModel import io.ksmt.runner.generated.models.SolverType import io.ksmt.runner.generated.models.UnsatCoreResult +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolverException +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KSolverUnsupportedFeatureException +import io.ksmt.solver.KSolverUnsupportedParameterException +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.KMaxSMTResult +import io.ksmt.solver.maxsmt.statistics.KMaxSMTStatistics import io.ksmt.solver.model.KFuncInterp import io.ksmt.solver.model.KFuncInterpEntry import io.ksmt.solver.model.KFuncInterpEntryVarsFree import io.ksmt.solver.model.KFuncInterpEntryWithVars import io.ksmt.solver.model.KFuncInterpVarsFree import io.ksmt.solver.model.KFuncInterpWithVars -import io.ksmt.solver.KModel -import io.ksmt.solver.KSolverException -import io.ksmt.solver.KSolverStatus -import io.ksmt.solver.KSolverUnsupportedFeatureException -import io.ksmt.solver.KSolverUnsupportedParameterException import io.ksmt.solver.model.KModelImpl import io.ksmt.solver.runner.KSolverRunnerManager.CustomSolverInfo import io.ksmt.sort.KBoolSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort +import io.ksmt.utils.uncheckedCast +import kotlinx.coroutines.TimeoutCancellationException +import kotlinx.coroutines.withTimeout import java.util.concurrent.CompletableFuture import java.util.concurrent.TimeUnit -import io.ksmt.utils.uncheckedCast import kotlin.time.Duration class KSolverRunnerExecutor( private val hardTimeout: Duration, private val worker: KsmtWorkerSession, ) { + private val maxSmtCtx = KMaxSMTContext(preferLargeWeightConstraintsForCores = true) + fun configureSync(config: List) = configure(config) { cfg -> queryWithTimeoutAndExceptionHandlingSync { configure.querySync(cfg) @@ -88,11 +96,22 @@ class KSolverRunnerExecutor( } } + suspend fun assertSoft(expr: KExpr, weight: UInt) = assertSoft(expr, weight) { params -> + queryWithTimeoutAndExceptionHandlingAsync { + assertSoft.queryAsync(params) + } + } + private inline fun assert(expr: KExpr, query: (AssertParams) -> Unit) { ensureActive() query(AssertParams(expr)) } + private inline fun assertSoft(expr: KExpr, weight: UInt, query: (SoftConstraint) -> Unit) { + ensureActive() + query(SoftConstraint(expr, weight)) + } + fun bulkAssertSync(exprs: List>) = bulkAssert(exprs) { params -> queryWithTimeoutAndExceptionHandlingSync { bulkAssert.querySync(params) @@ -206,6 +225,53 @@ class KSolverRunnerExecutor( return result.status } + suspend fun checkMaxSMT(timeout: Duration, collectStatistics: Boolean): KMaxSMTResult = + checkAnyMaxSMT(timeout, collectStatistics) { params -> + queryWithTimeoutAndExceptionHandlingAsync { + checkMaxSMT.queryAsync(params) + } + } + + /** + * Can be used with both optimal and suboptimal versions. + */ + private inline fun checkAnyMaxSMT( + timeout: Duration, + collectStatistics: Boolean, + query: (CheckMaxSMTParams) -> CheckMaxSMTResult + ): KMaxSMTResult { + ensureActive() + + val params = CheckMaxSMTParams(timeout.inWholeMilliseconds, collectStatistics) + val result = query(params) + @Suppress("UNCHECKED_CAST") + val satSoftConstraints = (result.satSoftConstraintExprs as List>) + .zip(result.satSoftConstraintWeights) + .map { io.ksmt.solver.maxsmt.constraints.SoftConstraint(it.first, it.second) } + + return KMaxSMTResult( + satSoftConstraints, + result.hardConstraintsSatStatus, + result.timeoutExceededOrUnknown + ) + } + + suspend fun collectMaxSMTStatistics(): KMaxSMTStatistics { + ensureActive() + + val result = queryWithTimeoutAndExceptionHandlingAsync { + collectMaxSMTStatistics.queryAsync(Unit) + } + + val maxSMTStatistics = KMaxSMTStatistics(maxSmtCtx).apply { + timeoutMs = result.timeoutMs + elapsedTimeMs = result.elapsedTimeMs + queriesToSolverNumber = result.queriesToSolverNumber + result.timeInSolverQueriesMs + } + return maxSMTStatistics + } + fun checkWithAssumptionsSync( assumptions: List>, timeout: Duration diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerManager.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerManager.kt index e4deea228..90557bb5c 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerManager.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerManager.kt @@ -1,7 +1,6 @@ package io.ksmt.solver.runner import com.jetbrains.rd.util.lifetime.isNotAlive -import kotlinx.coroutines.runBlocking import io.ksmt.KContext import io.ksmt.runner.core.KsmtWorkerArgs import io.ksmt.runner.core.KsmtWorkerFactory @@ -18,6 +17,8 @@ import io.ksmt.runner.generated.solverType import io.ksmt.solver.KSolver import io.ksmt.solver.KSolverConfiguration import io.ksmt.solver.KSolverException +import io.ksmt.solver.maxsmt.KMaxSMTContext +import kotlinx.coroutines.runBlocking import kotlin.reflect.KClass import kotlin.time.Duration import kotlin.time.Duration.Companion.seconds @@ -47,6 +48,7 @@ open class KSolverRunnerManager( fun createSolver( ctx: KContext, + maxsmtCtx: KMaxSMTContext = KMaxSMTContext(), solver: KClass> ): KSolverRunner { if (workers.lifetime.isNotAlive) { @@ -54,7 +56,7 @@ open class KSolverRunnerManager( } val solverType = solver.solverType if (solverType != SolverType.Custom) { - return KSolverRunner(this, ctx, solverType.createConfigurationBuilder(), solverType) + return KSolverRunner(this, ctx, maxsmtCtx, solverType.createConfigurationBuilder(), solverType) } return createCustomSolver(ctx, solver) diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt index 48ff7c29b..ba062941e 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt @@ -8,23 +8,31 @@ import io.ksmt.runner.core.ChildProcessBase import io.ksmt.runner.core.KsmtWorkerArgs import io.ksmt.runner.generated.createInstance import io.ksmt.runner.generated.createSolverConstructor +import io.ksmt.runner.generated.models.CheckMaxSMTResult import io.ksmt.runner.generated.models.CheckResult +import io.ksmt.runner.generated.models.CollectMaxSMTStatisticsResult import io.ksmt.runner.generated.models.ContextSimplificationMode import io.ksmt.runner.generated.models.ModelEntry import io.ksmt.runner.generated.models.ModelFuncInterpEntry import io.ksmt.runner.generated.models.ModelResult import io.ksmt.runner.generated.models.ModelUninterpretedSortUniverse import io.ksmt.runner.generated.models.ReasonUnknownResult +import io.ksmt.runner.generated.models.SoftConstraint import io.ksmt.runner.generated.models.SolverProtocolModel import io.ksmt.runner.generated.models.SolverType import io.ksmt.runner.generated.models.UnsatCoreResult import io.ksmt.runner.generated.models.solverProtocolModel import io.ksmt.runner.serializer.AstSerializationCtx +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.maxsmt.KMaxSMTContext +import io.ksmt.solver.maxsmt.solvers.KMaxSMTSolverBase +import io.ksmt.solver.maxsmt.solvers.KPrimalDualMaxResSolver import io.ksmt.solver.model.KFuncInterp import io.ksmt.solver.model.KFuncInterpEntry import io.ksmt.solver.model.KFuncInterpEntryWithVars -import io.ksmt.solver.KSolver import io.ksmt.solver.model.KFuncInterpWithVars +import io.ksmt.solver.model.KNativeSolverModel import io.ksmt.sort.KBoolSort import kotlin.time.Duration.Companion.milliseconds @@ -32,6 +40,15 @@ class KSolverWorkerProcess : ChildProcessBase() { private var workerCtx: KContext? = null private var workerSolver: KSolver<*>? = null private val customSolverCreators = hashMapOf KSolver<*>>() + private var _maxSmtSolver: KMaxSMTSolverBase? = null + private val maxSmtSolver: KMaxSMTSolverBase + get() { + if (_maxSmtSolver == null) { + _maxSmtSolver = KPrimalDualMaxResSolver(ctx, solver, KMaxSMTContext(preferLargeWeightConstraintsForCores = true)) + return _maxSmtSolver!! + } + return _maxSmtSolver!! + } private val ctx: KContext get() = workerCtx ?: error("Solver is not initialized") @@ -71,54 +88,82 @@ class KSolverWorkerProcess : ChildProcessBase() { } } deleteSolver.measureExecutionForTermination { - solver.close() + maxSmtSolver.close() ctx.close() astSerializationCtx.resetCtx() workerSolver = null workerCtx = null + _maxSmtSolver = null } configure.measureExecutionForTermination { config -> - solver.configure { + maxSmtSolver.configure { config.forEach { addUniversalParam(it) } } } assert.measureExecutionForTermination { params -> @Suppress("UNCHECKED_CAST") - solver.assert(params.expression as KExpr) + maxSmtSolver.assert(params.expression as KExpr) + } + assertSoft.measureExecutionForTermination { params -> + @Suppress("UNCHECKED_CAST") + maxSmtSolver.assertSoft(params.expression as KExpr, params.weight) } bulkAssert.measureExecutionForTermination { params -> @Suppress("UNCHECKED_CAST") - solver.assert(params.expressions as List>) + maxSmtSolver.assert(params.expressions as List>) } assertAndTrack.measureExecutionForTermination { params -> @Suppress("UNCHECKED_CAST") - solver.assertAndTrack(params.expression as KExpr) + maxSmtSolver.assertAndTrack(params.expression as KExpr) } bulkAssertAndTrack.measureExecutionForTermination { params -> @Suppress("UNCHECKED_CAST") - solver.assertAndTrack(params.expressions as List>) + maxSmtSolver.assertAndTrack(params.expressions as List>) } push.measureExecutionForTermination { - solver.push() + maxSmtSolver.push() } pop.measureExecutionForTermination { params -> - solver.pop(params.levels) + maxSmtSolver.pop(params.levels) } check.measureExecutionForTermination { params -> val timeout = params.timeout.milliseconds - val status = solver.check(timeout) + val status = maxSmtSolver.check(timeout) CheckResult(status) } checkWithAssumptions.measureExecutionForTermination { params -> val timeout = params.timeout.milliseconds @Suppress("UNCHECKED_CAST") - val status = solver.checkWithAssumptions(params.assumptions as List>, timeout) + val status = maxSmtSolver.checkWithAssumptions(params.assumptions as List>, timeout) CheckResult(status) } + checkMaxSMT.measureExecutionForTermination { params -> + val timeout = params.timeout.milliseconds + val collectStatistics = params.collectStatistics + + val result = maxSmtSolver.checkMaxSMT(timeout, collectStatistics) + + CheckMaxSMTResult( + result.satSoftConstraints.map { it.expression }, + result.satSoftConstraints.map { it.weight }, + result.hardConstraintsSatStatus, + result.timeoutExceededOrUnknown + ) + } + collectMaxSMTStatistics.measureExecutionForTermination { + val statistics = maxSmtSolver.collectMaxSMTStatistics() + + CollectMaxSMTStatisticsResult( + statistics.timeoutMs, + statistics.elapsedTimeMs, + statistics.timeInSolverQueriesMs, + statistics.queriesToSolverNumber + ) + } model.measureExecutionForTermination { - val model = solver.model().detach() + val model = maxSmtSolver.model().detach() val declarations = model.declarations.toList() val interpretations = declarations.map { val interp = model.interpretation(it) ?: error("No interpretation for model declaration $it") @@ -132,15 +177,15 @@ class KSolverWorkerProcess : ChildProcessBase() { ModelResult(declarations, interpretations, uninterpretedSortUniverse) } unsatCore.measureExecutionForTermination { - val core = solver.unsatCore() + val core = maxSmtSolver.unsatCore() UnsatCoreResult(core) } reasonOfUnknown.measureExecutionForTermination { - val reason = solver.reasonOfUnknown() + val reason = maxSmtSolver.reasonOfUnknown() ReasonUnknownResult(reason) } interrupt.measureExecutionForTermination { - solver.interrupt() + maxSmtSolver.interrupt() } lifetime.onTermination { workerSolver?.close() diff --git a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt index f6c1dfa79..86338a2a5 100644 --- a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt +++ b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt @@ -44,6 +44,11 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { field("value", PredefinedType.string) } + private val softConstraint = structdef { + field("expression", kastType) + field("weight", PredefinedType.uint) + } + private val assertParams = structdef { field("expression", kastType) } @@ -64,11 +69,30 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { field("status", statusType) } + private val checkMaxSMTParams = structdef { + field("timeout", PredefinedType.long) + field("collectStatistics", PredefinedType.bool) + } + + private val checkMaxSMTResult = structdef { + field("satSoftConstraintExprs", immutableList(kastType)) + field("satSoftConstraintWeights", immutableList(PredefinedType.uint)) + field("hardConstraintsSatStatus", statusType) + field("timeoutExceededOrUnknown", PredefinedType.bool) + } + private val checkWithAssumptionsParams = structdef { field("assumptions", immutableList(kastType)) field("timeout", PredefinedType.long) } + private val collectMaxSMTStatisticsResult = structdef { + field("timeoutMs", PredefinedType.long) + field("elapsedTimeMs", PredefinedType.long) + field("timeInSolverQueriesMs", PredefinedType.long) + field("queriesToSolverNumber", PredefinedType.int) + } + private val unsatCoreResult = structdef { field("core", immutableList(kastType)) } @@ -118,6 +142,10 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { async documentation = "Assert expression" } + call("assertSoft", softConstraint, PredefinedType.void).apply { + async + documentation = "Assert expression softly" + } call("bulkAssert", bulkAssertParams, PredefinedType.void).apply { async documentation = "Assert multiple expressions" @@ -142,6 +170,14 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { async documentation = "Check SAT" } + call("checkMaxSMT", checkMaxSMTParams, checkMaxSMTResult).apply { + async + documentation = "Check MaxSMT" + } + call("collectMaxSMTStatistics", PredefinedType.void, collectMaxSMTStatisticsResult).apply { + async + documentation = "Collect MaxSMT statistics" + } call("checkWithAssumptions", checkWithAssumptionsParams, checkResult).apply { async documentation = "Check SAT with assumptions" diff --git a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/TestProtocolModel.kt b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/TestProtocolModel.kt index 5c3088bb7..9c661dfa7 100644 --- a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/TestProtocolModel.kt +++ b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/TestProtocolModel.kt @@ -16,6 +16,11 @@ object TestProtocolModel : Ext(TestProtocolRoot) { private val kastType = kastType() private val statusType = solverStatusType() + private val testSoftConstraint = structdef { + field("expression", kastType) + field("weight", PredefinedType.uint) + } + private val equalityCheckParams = structdef { field("solver", PredefinedType.int) field("actual", kastType) @@ -36,6 +41,25 @@ object TestProtocolModel : Ext(TestProtocolRoot) { field("status", statusType) } + private val testCheckMaxSMTParams = structdef { + field("timeout", PredefinedType.long) + field("collectStatistics", PredefinedType.bool) + } + + private val testCheckMaxSMTResult = structdef { + field("satSoftConstraintExprs", immutableList(kastType)) + field("satSoftConstraintWeights", immutableList(PredefinedType.uint)) + field("hardConstraintsSatStatus", statusType) + field("timeoutExceededOrUnknown", PredefinedType.bool) + } + + private val testCollectMaxSMTStatisticsResult = structdef { + field("timeoutMs", PredefinedType.long) + field("elapsedTimeMs", PredefinedType.long) + field("timeInSolverQueriesMs", PredefinedType.long) + field("queriesToSolverNumber", PredefinedType.int) + } + private val testConversionResult = structdef { field("expressions", immutableList(kastType)) } @@ -81,10 +105,22 @@ object TestProtocolModel : Ext(TestProtocolRoot) { async documentation = "Assert expr" } + call("assertSoft", testSoftConstraint, PredefinedType.void).apply { + async + documentation = "Assert expression softly" + } call("check", PredefinedType.int, testCheckResult).apply { async documentation = "Check-sat" } + call("checkMaxSMT", testCheckMaxSMTParams, testCheckMaxSMTResult).apply { + async + documentation = "Check MaxSMT" + } + call("collectMaxSMTStatistics", PredefinedType.void, testCollectMaxSMTStatisticsResult).apply { + async + documentation = "Collect MaxSMT statistics" + } call("exprToString", PredefinedType.long, PredefinedType.string).apply { async documentation = "Expression to string" diff --git a/ksmt-test/build.gradle.kts b/ksmt-test/build.gradle.kts index 7fabeb0d3..137f17c1a 100644 --- a/ksmt-test/build.gradle.kts +++ b/ksmt-test/build.gradle.kts @@ -103,7 +103,7 @@ val testDataRevision = project.stringProperty("testDataRevision") ?: "no-revisio val downloadPreparedBenchmarksTestData = downloadPreparedSmtLibBenchmarkTestData( downloadPath = downloadedTestData, testDataPath = unpackedTestDataDir, - version = testDataRevision + testDataRevision = testDataRevision ) tasks.withType { diff --git a/scripts/analyze_maxsmt_statistics.py b/scripts/analyze_maxsmt_statistics.py new file mode 100644 index 000000000..a7744b81b --- /dev/null +++ b/scripts/analyze_maxsmt_statistics.py @@ -0,0 +1,372 @@ +import json +import operator +from functools import reduce +from pathlib import Path +from sys import argv + + +def main(args): + analyze_maxsmt_statistics(Path(args[1]), Path(args[2])) + + +def analyze_maxsmt_statistics(stat_file, analyzed_stat_file_to_save): + if not stat_file.exists() or not stat_file.is_file(): + raise FileExistsError(f"File with statistics [{str(stat_file)}] does not exist") + + with open(stat_file, "r", encoding="utf-8") as f: + stat = json.load(f) + + logics_size = len(stat["logics"]) + logics_statistics = [] + + def obj_dict(obj): + return obj.__dict__ + + for i in range(0, logics_size): + logic_stat = create_logic_statistics((stat["logics"])[i]) + logics_statistics.append(logic_stat) + logic_stat_str = json.dumps(logic_stat, default=obj_dict, indent=2, separators=(',', ': ')) + print(logic_stat_str + "\n") + + all_tests_stat = create_all_tests_statistics(logics_statistics) + logics_statistics.append(all_tests_stat) + all_tests_stat_str = json.dumps(all_tests_stat, default=obj_dict, indent=2, separators=(',', ': ')) + print(all_tests_stat_str + "\n") + + with open(analyzed_stat_file_to_save, "w", encoding="utf-8") as f: + json.dump(logics_statistics, f, default=obj_dict, indent=2, separators=(',', ': ')) + + +def create_tests_size_statistics(tests): + tests_size = len(tests) + tests_executed_maxsmt_size = len(list(filter(lambda x: x.get("maxSMTCallStatistics") is not None, tests))) + tests_executed_maxsmt_passed_size = len(list(filter(lambda x: x["passed"], tests))) + tests_executed_maxsmt_passed_tests_percent = 0 if tests_executed_maxsmt_size == 0 \ + else tests_executed_maxsmt_passed_size / tests_executed_maxsmt_size * 100 + failed_or_ignored_tests_size = len(list(filter(lambda x: not x["passed"], tests))) + failed_tests_wrong_soft_constr_sum_size = len(list(filter(lambda x: x["checkedSoftConstraintsSumIsWrong"], tests))) + ignored_tests_size = len(list(filter(lambda x: x["ignoredTest"], tests))) + failed_on_parsing_or_converting_expressions_size = len( + list(filter(lambda x: x["failedOnParsingOrConvertingExpressions"], tests))) + + def get_unique_exception_messages(collection): + # Set is converted to list in order to dump statistics to JSON (otherwise, the script fails + # with such error: 'AttributeError: 'set' object has no attribute '__dict__'.'). + return list( + set(map(lambda x: None if x.get("exceptionMessage") is None else x["exceptionMessage"], collection))) + + failed_on_parsing_or_converting_expressions_exception_messages = get_unique_exception_messages( + list(filter(lambda x: x["failedOnParsingOrConvertingExpressions"], tests))) + + return TestsSizeStatistics(tests_size, tests_executed_maxsmt_size, + tests_executed_maxsmt_passed_size, + tests_executed_maxsmt_passed_tests_percent, + failed_or_ignored_tests_size, ignored_tests_size, + failed_on_parsing_or_converting_expressions_size, + failed_on_parsing_or_converting_expressions_exception_messages, + failed_tests_wrong_soft_constr_sum_size) + + +def create_tests_queries_to_solver_statistics(tests): + def max_smt_stat(test): + return test["maxSMTCallStatistics"] + + def queries_to_solver_number(test): + if isinstance(test, int): + return test + return max_smt_stat(test)["queriesToSolverNumber"] + + def time_in_solver_queries_ms(test): + if isinstance(test, int): + return test + return max_smt_stat(test)["timeInSolverQueriesMs"] + + def elapsed_time_ms(test): + return test["elapsedTimeMs"] + + tests_executed_maxsmt = list(filter(lambda x: x.get("maxSMTCallStatistics") is not None, tests)) + tests_executed_maxsmt_size = len(tests_executed_maxsmt) + + tests_executed_maxsmt_passed = list(filter(lambda x: x["passed"], tests_executed_maxsmt)) + tests_executed_maxsmt_passed_size = len(tests_executed_maxsmt_passed) + + tests_executed_maxsmt_failed = list(filter(lambda x: not x["passed"], tests_executed_maxsmt)) + tests_executed_maxsmt_failed_size = len(tests_executed_maxsmt_failed) + + avg_queries_to_solver_number = 0 if tests_executed_maxsmt_size == 0 else reduce( + lambda x, y: queries_to_solver_number(x) + queries_to_solver_number(y), + tests_executed_maxsmt, 0) / tests_executed_maxsmt_size + + avg_queries_to_solver_passed_tests_number = 0 if tests_executed_maxsmt_passed_size == 0 else reduce( + lambda x, y: queries_to_solver_number(x) + queries_to_solver_number(y), + tests_executed_maxsmt_passed, 0) / tests_executed_maxsmt_passed_size + + avg_queries_to_solver_failed_tests_number = 0 if tests_executed_maxsmt_failed_size == 0 else reduce( + lambda x, y: queries_to_solver_number(x) + queries_to_solver_number(y), + tests_executed_maxsmt_failed, 0) / tests_executed_maxsmt_failed_size + + def is_zero(value): + return abs(value) < 0.00000001 + + def avg_time_per_solver_queries_percent_list(bunch_of_tests): + return map(lambda x: time_in_solver_queries_ms(x) / elapsed_time_ms(x) * 100 if not is_zero( + elapsed_time_ms(x)) else elapsed_time_ms(x), bunch_of_tests) + + avg_time_per_solver_queries_percent = \ + 0 if tests_executed_maxsmt_size == 0 else reduce(operator.add, avg_time_per_solver_queries_percent_list( + tests_executed_maxsmt), + 0) / tests_executed_maxsmt_size + avg_time_per_solver_queries_passed_tests_percent = \ + 0 if tests_executed_maxsmt_passed_size == 0 else reduce(operator.add, avg_time_per_solver_queries_percent_list( + tests_executed_maxsmt_passed), + 0) / tests_executed_maxsmt_passed_size + + avg_time_per_solver_queries_failed_tests_percent = \ + 0 if tests_executed_maxsmt_failed_size == 0 else reduce(operator.add, avg_time_per_solver_queries_percent_list( + tests_executed_maxsmt_failed), + 0) / tests_executed_maxsmt_failed_size + + return TestsQueriesToSolverStatistics(avg_queries_to_solver_number, avg_queries_to_solver_passed_tests_number, + avg_queries_to_solver_failed_tests_number, + avg_time_per_solver_queries_percent, + avg_time_per_solver_queries_passed_tests_percent, + avg_time_per_solver_queries_failed_tests_percent) + + +def create_tests_elapsed_time_statistics(tests): + def max_smt_stat(test): + return test["maxSMTCallStatistics"] + + def elapsed_time_ms(test): + if isinstance(test, int): + return test + return test["elapsedTimeMs"] + + tests_executed_maxsmt = list(filter(lambda x: x.get("maxSMTCallStatistics") is not None, tests)) + tests_executed_maxsmt_size = len(tests_executed_maxsmt) + + avg_elapsed_time_ms = 0 if tests_executed_maxsmt_size == 0 else reduce( + lambda x, y: elapsed_time_ms(x) + elapsed_time_ms(y), tests_executed_maxsmt, + 0) / tests_executed_maxsmt_size + + passed_tests = list(filter(lambda x: x["passed"], tests_executed_maxsmt)) + avg_elapsed_passed_tests_time_ms = 0 if tests_executed_maxsmt_size == 0 else reduce( + lambda x, y: elapsed_time_ms(x) + elapsed_time_ms(y), passed_tests, + 0) / tests_executed_maxsmt_size + + failed_tests = list(filter(lambda x: not x["passed"], tests_executed_maxsmt)) + avg_elapsed_failed_tests_time_ms = 0 if tests_executed_maxsmt_size == 0 else reduce( + lambda x, y: elapsed_time_ms(x) + elapsed_time_ms(y), failed_tests, + 0) / tests_executed_maxsmt_size + + return TestsElapsedTimeStatistics(avg_elapsed_time_ms, avg_elapsed_passed_tests_time_ms, + avg_elapsed_failed_tests_time_ms) + + +def create_tests_score_statistics(tests): + tests_executed_maxsmt = list(filter(lambda x: x.get("maxSMTCallStatistics") is not None, tests)) + + passed_tests = list(filter(lambda x: x["passed"], tests_executed_maxsmt)) + passed_tests_size = len(passed_tests) + + def score(x): + if isinstance(x, int) or isinstance(x, float): + return x + found_so_far_weight = x["foundSoFarWeight"] + optimal_weight = x["optimalWeight"] + + if optimal_weight == 0: + if found_so_far_weight == 0: + return 1 + else: + return 0 + else: + return found_so_far_weight / optimal_weight + + avg_score_passed_tests = reduce( + lambda x, y: score(x) + score(y), passed_tests, 0) / passed_tests_size + + return TestsScoreStatistics(avg_score_passed_tests) + + +class MaxSMTContext: + def __int__(self, strategy, prefer_large_weight_constraints_for_cores, minimize_cores, get_multiple_cores): + self.strategy = strategy + self.prefer_large_weight_constraints_for_cores = prefer_large_weight_constraints_for_cores + self.minimize_cores = minimize_cores + self.get_multiple_cores = get_multiple_cores + + +class TestsSizeStatistics: + def __init__(self, tests_size, tests_executed_maxsmt_size, + tests_executed_maxsmt_passed_size, + tests_executed_maxsmt_passed_tests_percent, + failed_tests_size, + ignored_tests_size, + failed_on_parsing_or_converting_expressions_size, + failed_on_parsing_or_converting_expressions_exception_messages, + failed_tests_wrong_soft_constr_sum_size): + self.tests_size = tests_size + self.tests_executed_maxsmt_size = tests_executed_maxsmt_size + self.tests_executed_maxsmt_passed_size = tests_executed_maxsmt_passed_size + self.tests_executed_maxsmt_passed_tests_percent = tests_executed_maxsmt_passed_tests_percent, + self.failed_tests_size = failed_tests_size + self.ignored_tests_size = ignored_tests_size + self.failed_on_parsing_or_converting_expressions_size = failed_on_parsing_or_converting_expressions_size + self.failed_on_parsing_or_converting_expressions_exception_messages = ( + failed_on_parsing_or_converting_expressions_exception_messages) + self.failed_tests_wrong_soft_constr_sum_size = failed_tests_wrong_soft_constr_sum_size + + +class TestsScoreStatistics: + def __init__(self, avg_score_passed_tests): + self.avg_score_passed_tests = avg_score_passed_tests + + +class TestsQueriesToSolverStatistics: + def __init__(self, avg_queries_to_solver_number, avg_queries_to_solver_passed_tests_number, + avg_queries_to_solver_failed_tests_number, avg_time_per_solver_queries_percent, + avg_time_per_solver_queries_passed_tests_percent, avg_time_per_solver_queries_failed_tests_percent): + self.avg_queries_to_solver_number = avg_queries_to_solver_number + self.avg_queries_to_solver_passed_tests_number = avg_queries_to_solver_passed_tests_number + self.avg_queries_to_solver_failed_tests_number = avg_queries_to_solver_failed_tests_number + self.avg_time_per_solver_queries_percent = avg_time_per_solver_queries_percent + self.avg_time_per_solver_queries_passed_tests_percent = avg_time_per_solver_queries_passed_tests_percent + self.avg_time_per_solver_queries_failed_tests_percent = avg_time_per_solver_queries_failed_tests_percent + + +class TestsElapsedTimeStatistics: + def __init__(self, avg_elapsed_time_ms, avg_elapsed_passed_tests_time_ms, + avg_elapsed_failed_tests_time_ms): + self.avg_elapsed_time_ms = avg_elapsed_time_ms + self.avg_elapsed_passed_tests_time_ms = avg_elapsed_passed_tests_time_ms + self.avg_elapsed_failed_tests_time_ms = avg_elapsed_failed_tests_time_ms + + +class LogicTestsStatistics: + def __init__(self, smt_solver, name, timeout_ms, max_smt_ctx, tests_size_stat: TestsSizeStatistics, + tests_score_stat: TestsScoreStatistics, + tests_queries_to_solver_stat: TestsQueriesToSolverStatistics, + tests_elapsed_time_stat: TestsElapsedTimeStatistics): + self.smt_solver = smt_solver + self.name = name + self.timeout_ms = timeout_ms + self.max_smt_ctx = max_smt_ctx + self.tests_size_stat = tests_size_stat + self.tests_score_stat = tests_score_stat + self.tests_queries_to_solver_stat = tests_queries_to_solver_stat + self.tests_elapsed_time_stat = tests_elapsed_time_stat + + +class AllTestsStatistics: + def __init__(self, timeout_ms, max_smt_ctx, tests_size_stat: TestsSizeStatistics, + tests_score_stat: TestsScoreStatistics, tests_elapsed_time_stat: TestsElapsedTimeStatistics): + self.timeout_ms = timeout_ms + self.max_smt_ctx = max_smt_ctx + self.tests_size_stat = tests_size_stat + self.tests_score_stat = tests_score_stat + self.tests_elapsed_time_stat = tests_elapsed_time_stat + + +def create_all_tests_statistics(logics_statistics): + first_logic: LogicTestsStatistics = logics_statistics[0] + + timeout_ms = first_logic.timeout_ms + max_smt_ctx = first_logic.max_smt_ctx + + # For test size statistics. + tests_size = 0 + tests_executed_maxsmt_size = 0 + tests_executed_maxsmt_passed_size = 0 + failed_tests_size = 0 + ignored_tests_size = 0 + failed_on_parsing_or_converting_expressions_size = 0 + failed_on_parsing_or_converting_expressions_exception_messages = [] + failed_tests_wrong_soft_constr_sum_size = 0 + + # For test score statistics. + avg_score_passed_tests = 0.0 + + # For elapsed time statistics. + avg_elapsed_time_ms = 0.0 + avg_elapsed_passed_tests_time_ms = 0.0 + avg_elapsed_failed_tests_time_ms = 0.0 + + for logic in logics_statistics: + size_statistics = logic.tests_size_stat + score_statistics = logic.tests_score_stat + elapsed_time_statistics = logic.tests_elapsed_time_stat + + tests_size += size_statistics.tests_size + tests_executed_maxsmt_size += size_statistics.tests_executed_maxsmt_size + tests_executed_maxsmt_passed_size += size_statistics.tests_executed_maxsmt_passed_size + failed_tests_size += size_statistics.failed_tests_size + ignored_tests_size += size_statistics.ignored_tests_size + failed_on_parsing_or_converting_expressions_size += ( + size_statistics.failed_on_parsing_or_converting_expressions_size) + failed_on_parsing_or_converting_expressions_exception_messages += ( + size_statistics.failed_on_parsing_or_converting_expressions_exception_messages) + failed_tests_wrong_soft_constr_sum_size += size_statistics.failed_tests_wrong_soft_constr_sum_size + + avg_score_passed_tests += (score_statistics.avg_score_passed_tests * + size_statistics.tests_executed_maxsmt_passed_size) + + avg_elapsed_time_ms += (elapsed_time_statistics.avg_elapsed_time_ms * + size_statistics.tests_executed_maxsmt_size) + avg_elapsed_passed_tests_time_ms += ( + elapsed_time_statistics.avg_elapsed_passed_tests_time_ms * + size_statistics.tests_executed_maxsmt_passed_size) + avg_elapsed_failed_tests_time_ms += elapsed_time_statistics.avg_elapsed_failed_tests_time_ms * ( + size_statistics.tests_executed_maxsmt_size - size_statistics.tests_executed_maxsmt_passed_size) + + if tests_executed_maxsmt_passed_size != 0: + avg_score_passed_tests /= tests_executed_maxsmt_passed_size + else: + avg_score_passed_tests = "No tests" + + if tests_executed_maxsmt_size != 0: + avg_elapsed_time_ms /= tests_executed_maxsmt_size + else: + avg_elapsed_time_ms = "No tests" + + if tests_executed_maxsmt_passed_size != 0: + avg_elapsed_passed_tests_time_ms /= tests_executed_maxsmt_passed_size + else: + avg_elapsed_passed_tests_time_ms = "No tests" + + if (tests_executed_maxsmt_size - tests_executed_maxsmt_passed_size) != 0: + avg_elapsed_failed_tests_time_ms /= (tests_executed_maxsmt_size - tests_executed_maxsmt_passed_size) + else: + avg_elapsed_failed_tests_time_ms = "No tests" + + return AllTestsStatistics(timeout_ms, max_smt_ctx, + TestsSizeStatistics(tests_size, tests_executed_maxsmt_size, + tests_executed_maxsmt_passed_size, + tests_executed_maxsmt_passed_size / tests_executed_maxsmt_size, + failed_tests_size, ignored_tests_size, + failed_on_parsing_or_converting_expressions_size, + failed_on_parsing_or_converting_expressions_exception_messages, + failed_tests_wrong_soft_constr_sum_size + ), + TestsScoreStatistics(avg_score_passed_tests), + TestsElapsedTimeStatistics(avg_elapsed_time_ms, + avg_elapsed_passed_tests_time_ms, + avg_elapsed_failed_tests_time_ms) + ) + + +def create_logic_statistics(logic): + tests = logic["TESTS"] + first_test = tests[0] + test_executed_maxsmt = filter(lambda x: x.get("maxSMTCallStatistics") is not None, tests) + first_max_smt_call_stat = None if test_executed_maxsmt is None else (list(test_executed_maxsmt)[0])[ + "maxSMTCallStatistics"] + return LogicTestsStatistics(first_test["smtSolver"], logic["NAME"], first_max_smt_call_stat["timeoutMs"], + first_max_smt_call_stat["maxSmtCtx"], create_tests_size_statistics(tests), + create_tests_score_statistics(tests), + create_tests_queries_to_solver_statistics(tests), + create_tests_elapsed_time_statistics(tests)) + + +if __name__ == "__main__": + main(argv) diff --git a/scripts/monitoring.sh b/scripts/monitoring.sh new file mode 100644 index 000000000..bf9508c63 --- /dev/null +++ b/scripts/monitoring.sh @@ -0,0 +1,29 @@ +#!/bin/bash + +PUSHGATEWAY_HOSTNAME=${1} +PUSHGATEWAY_USER=${2} +PUSHGATEWAY_PASSWORD=${3} +PUSHGATEWAY_ADDITIONAL_PATH=/pushgateway + +PROM_ADDITIONAL_LABELS=/service/ksmt +SLEEP_TIME_SECONDS=15 +VERSION_CADVISOR=v0.36.0 +VERSION_CURL=7.84.0 +VERSION_NODE_EXPORTER=v1.3.1 +PORT_CADVISOR=9280 +PORT_NODE_EXPORTER=9100 + +# base linux system metrics +if ! netstat -tulpn | grep -q ${PORT_NODE_EXPORTER} ; then + docker run -d --name node_exporter \ + --net="host" \ + --pid="host" \ + --volume="/:/host:ro,rslave" \ + quay.io/prometheus/node-exporter:${VERSION_NODE_EXPORTER} \ + --path.rootfs=/host + docker run -d --name curl-node \ + --net="host" \ + --entrypoint=/bin/sh \ + curlimages/curl:${VERSION_CURL} \ + "-c" "while true; do curl localhost:9100/metrics | curl -u ${PUSHGATEWAY_USER}:${PUSHGATEWAY_PASSWORD} --data-binary @- https://${PUSHGATEWAY_HOSTNAME}${PUSHGATEWAY_ADDITIONAL_PATH}/metrics/job/pushgateway/instance/${GITHUB_RUN_ID}-${HOSTNAME}${PROM_ADDITIONAL_LABELS} ; sleep ${SLEEP_TIME_SECONDS}; done" +fi diff --git a/settings.gradle.kts b/settings.gradle.kts index 887d3798c..6a28d286c 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -23,6 +23,9 @@ include("ksmt-runner:solver-generator") include("ksmt-test") include("ksmt-symfpu") +include("ksmt-maxsmt") +include("ksmt-maxsmt-test") + pluginManagement { resolutionStrategy { eachPlugin { diff --git a/version.properties b/version.properties index 5b9aeb949..fb43dda9b 100644 --- a/version.properties +++ b/version.properties @@ -1,2 +1,13 @@ -kotlin=1.7.20 +kotlin=1.9.0 detekt=1.20.0 + +junit-jupiter=5.8.2 + +kotlinx-coroutines=1.7.2 + +# Logging +kotlin-logging-jvm=6.0.3 +slf4j-log4j12=2.0.11 + +# Google GSON for JSON +gson=2.10.1