From 247374f72bd9805e997b3fc2e3a400dbe1d22ef4 Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Mon, 13 May 2024 14:23:28 +0200 Subject: [PATCH] adjustments for latest LNG3 snapshot --- pom.xml | 11 +++- .../consistency/ConsistencyComputation.kt | 52 ++++++++++--------- .../computations/generic/Computation.kt | 19 ++++--- .../computations/generic/ComputationApi.kt | 2 +- .../computations/generic/Explanation.kt | 9 ++-- .../ModelEnumerationComputation.kt | 4 +- .../generic/ComputationRequestTest.kt | 1 + .../OptimizationOnlyBooleanNoSlicesTest.kt | 2 +- .../OptimizationOnlyEnumWithSlicesTest.kt | 4 +- 9 files changed, 59 insertions(+), 45 deletions(-) diff --git a/pom.xml b/pom.xml index 84c9b02..c2f2b36 100644 --- a/pom.xml +++ b/pom.xml @@ -53,6 +53,12 @@ + + org.apache.maven.plugins + maven-compiler-plugin + ${version.maven-compiler} + + org.jetbrains.kotlin kotlin-maven-plugin @@ -62,6 +68,9 @@ compile + + -opt-in=kotlin.time.ExperimentalTime + test-compile @@ -274,7 +283,7 @@ test - + maven-snapshots diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt index d290b15..0584bad 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt @@ -22,8 +22,8 @@ import com.booleworks.boolerules.computations.generic.computeExplanation import com.booleworks.boolerules.computations.generic.extractModel import com.booleworks.logicng.datastructures.Tristate import com.booleworks.logicng.formulas.FormulaFactory -import com.booleworks.logicng.solvers.MiniSat -import com.booleworks.logicng.solvers.sat.MiniSatConfig +import com.booleworks.logicng.solvers.SATSolver +import com.booleworks.logicng.solvers.sat.SATSolverConfig import com.booleworks.prl.model.PrlModel import com.booleworks.prl.model.slices.Slice import com.booleworks.prl.transpiler.TranslationInfo @@ -75,20 +75,23 @@ internal object ConsistencyComputation : ): ConsistencyInternalResult { val solver = prepareSolver(f, request.computeAllDetails, info, request.additionalConstraints, model, status) if (!status.successful()) return ConsistencyInternalResult(slice, false, null, null) - return if (solver.sat() == Tristate.TRUE) { - val example = extractModel(solver.model(info.knownVariables).positiveVariables(), info) - ConsistencyInternalResult(slice, true, example, null) - } else { - //TODO beautify explanation - ConsistencyInternalResult( - slice, - false, - null, - if (request.computeAllDetails) computeExplanation( - solver, - model.propertyStore.allDefinitions() - ) else null - ) + return solver.satCall().solve().use { satCall -> + if (satCall.satResult == Tristate.TRUE) { + val example = extractModel(satCall.model(info.knownVariables).positiveVariables(), info) + ConsistencyInternalResult(slice, true, example, null) + } else { + //TODO beautify explanation + ConsistencyInternalResult( + slice, + false, + null, + if (request.computeAllDetails) computeExplanation( + satCall, + model.propertyStore.allDefinitions(), + f + ) else null + ) + } } } @@ -101,11 +104,12 @@ internal object ConsistencyComputation : f: FormulaFactory ): SplitComputationDetail { val solver = prepareSolver(f, true, info, additionalConstraints, model, ComputationStatus("", "", SINGLE)) - val sat = solver.sat() - assert(sat == Tristate.FALSE) { "Detail computation should only be called for inconsistent slices" } - val explanation = computeExplanation(solver, model.propertyStore.allDefinitions()) - val result = ConsistencyInternalResult(slice, false, null, explanation) - return SplitComputationDetail(result, splitProperties) + return solver.satCall().solve().use { satCall -> + assert(satCall.satResult == Tristate.FALSE) { "Detail computation should only be called for inconsistent slices" } + val explanation = computeExplanation(satCall, model.propertyStore.allDefinitions(), f) + val result = ConsistencyInternalResult(slice, false, null, explanation) + SplitComputationDetail(result, splitProperties) + } } private fun prepareSolver( @@ -115,11 +119,11 @@ internal object ConsistencyComputation : additionalConstraints: List, model: PrlModel, status: ComputationStatusBuilder - ): MiniSat { - val solver = MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(proofTracing).build()).apply { + ): SATSolver { + val solver = SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(proofTracing).build()).apply { addPropositions(info.propositions) } - if (solver.sat() == Tristate.TRUE) { + if (solver.sat()) { val additionalFormulas = additionalConstraints.mapNotNull { constraint -> processConstraint(f, constraint, model, info, status) diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/generic/Computation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/generic/Computation.kt index 0710388..9c44ba6 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/generic/Computation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/generic/Computation.kt @@ -4,15 +4,14 @@ package com.booleworks.boolerules.computations.generic import com.booleworks.boolerules.config.ComputationConfig -import com.booleworks.logicng.datastructures.Tristate import com.booleworks.logicng.formulas.FormulaFactory import com.booleworks.logicng.formulas.FormulaFactoryConfig import com.booleworks.logicng.formulas.FormulaFactoryConfig.FormulaMergeStrategy.IMPORT import com.booleworks.logicng.formulas.FormulaFactoryConfig.FormulaMergeStrategy.USE_BUT_NO_IMPORT import com.booleworks.logicng.solvers.MaxSATSolver -import com.booleworks.logicng.solvers.MiniSat +import com.booleworks.logicng.solvers.SATSolver import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig -import com.booleworks.logicng.solvers.sat.MiniSatConfig +import com.booleworks.logicng.solvers.sat.SATSolverConfig import com.booleworks.prl.compiler.ConstraintCompiler import com.booleworks.prl.compiler.FeatureStore import com.booleworks.prl.model.AnyFeatureDef @@ -47,8 +46,8 @@ val NON_CACHING_USE_FF: () -> FormulaFactory = val CACHING_IMPORT_FF: () -> FormulaFactory = { FormulaFactory.caching(FormulaFactoryConfig.builder().formulaMergeStrategy(IMPORT).build()) } -val PT_CONFIG: MiniSatConfig = MiniSatConfig.builder().proofGeneration(true).build() -val NON_PT_CONFIG: MiniSatConfig = MiniSatConfig.builder().proofGeneration(false).build() +val PT_CONFIG: SATSolverConfig = SATSolverConfig.builder().proofGeneration(true).build() +val NON_PT_CONFIG: SATSolverConfig = SATSolverConfig.builder().proofGeneration(false).build() /** * Super class for all internal computations. @@ -221,17 +220,17 @@ sealed class Computation< } internal fun miniSat( - config: MiniSatConfig, + config: SATSolverConfig, request: REQUEST, f: FormulaFactory, model: PrlModel, info: TranslationInfo, slice: Slice, status: ComputationStatusBuilder - ): MiniSat { - val solver = MiniSat.miniSat(f, config) + ): SATSolver { + val solver = SATSolver.newSolver(f, config) solver.addPropositions(info.propositions) - if (solver.sat() == Tristate.FALSE) { + if (!solver.sat()) { status.addWarning( "Original rule set for the slice $slice is inconsistent. " + "Use the 'consistency' check to get an explanation, why." @@ -249,7 +248,7 @@ sealed class Computation< } if (status.successful()) { solver.addPropositions(additionalFormulas) - if (solver.sat() == Tristate.FALSE) { + if (!solver.sat()) { status.addWarning( "The additional constraints turned the rule set for for the slice $slice inconsistent. " + "Use the 'consistency' check to get an explanation, why." diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/generic/ComputationApi.kt b/src/main/kotlin/com/booleworks/boolerules/computations/generic/ComputationApi.kt index b0332b7..f124c64 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/generic/ComputationApi.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/generic/ComputationApi.kt @@ -342,7 +342,7 @@ data class ComputationStatus( @field:Schema(description = "A flag whether the computation was successful or not") val success: Boolean, - @field:Schema(description = "The Job ID whithin the kjobs framework") + @field:Schema(description = "The Job ID within the kjobs framework") val jobId: String, @field:Schema(description = "The Rule file ID used for this computation") diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/generic/Explanation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/generic/Explanation.kt index 2e9790c..bea641e 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/generic/Explanation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/generic/Explanation.kt @@ -5,7 +5,8 @@ package com.booleworks.boolerules.computations.generic import com.booleworks.logicng.datastructures.Tristate import com.booleworks.logicng.explanations.mus.MUSGeneration -import com.booleworks.logicng.solvers.SATSolver +import com.booleworks.logicng.formulas.FormulaFactory +import com.booleworks.logicng.solvers.sat.SATCall import com.booleworks.prl.model.AnySlicingPropertyDefinition import com.booleworks.prl.model.rules.ConstraintRule import com.booleworks.prl.transpiler.PrlProposition @@ -15,9 +16,9 @@ import com.booleworks.prl.transpiler.RuleType * Computes an explanation for an unsatisfiable SAT solver state and returns * a list of original rules of the rule file involved in the conflict. */ -internal fun computeExplanation(solver: SATSolver, allDefinitions: List): List { - assert(solver.sat() == Tristate.FALSE) - val mus = MUSGeneration().computeMUS(solver.factory(), solver.unsatCore().propositions()) +internal fun computeExplanation(satCall: SATCall, allDefinitions: List, f: FormulaFactory): List { + assert(satCall.satResult == Tristate.FALSE) + val mus = MUSGeneration().computeMUS(f, satCall.unsatCore().propositions()) return mus.propositions().filterIsInstance().map { p -> when (p.backpack().ruleType) { RuleType.ORIGINAL_RULE -> RuleDO.fromRulesetRule(p.backpack().rule!!, allDefinitions.map { it.name }) diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationComputation.kt index 63775fb..750dde9 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationComputation.kt @@ -21,7 +21,7 @@ import com.booleworks.boolerules.computations.modelenumeration.ModelEnumerationC import com.booleworks.boolerules.computations.modelenumeration.ModelEnumerationComputation.ModelEnumerationInternalResult import com.booleworks.logicng.formulas.FormulaFactory import com.booleworks.logicng.formulas.Variable -import com.booleworks.logicng.solvers.MiniSat +import com.booleworks.logicng.solvers.SATSolver import com.booleworks.prl.model.PrlModel import com.booleworks.prl.model.slices.Slice import com.booleworks.prl.transpiler.TranslationInfo @@ -95,7 +95,7 @@ internal object ModelEnumerationComputation : ListComputation< return ModelEnumerationInternalResult(slice, models.associateWith { slice }.toMutableMap()) } - private fun addTautologyClauses(solver: MiniSat, variables: SortedSet) { + private fun addTautologyClauses(solver: SATSolver, variables: SortedSet) { val f = solver.factory() val selTautology = f.variable(SEL_TAUTOLOGY) variables.forEach { solver.add(f.or(selTautology, it)) } diff --git a/src/test/kotlin/com/booleworks/boolerules/computations/generic/ComputationRequestTest.kt b/src/test/kotlin/com/booleworks/boolerules/computations/generic/ComputationRequestTest.kt index 5373b8a..0001e8a 100644 --- a/src/test/kotlin/com/booleworks/boolerules/computations/generic/ComputationRequestTest.kt +++ b/src/test/kotlin/com/booleworks/boolerules/computations/generic/ComputationRequestTest.kt @@ -10,6 +10,7 @@ import org.assertj.core.api.Assertions.assertThatThrownBy import org.junit.jupiter.api.Test import java.time.LocalDate +@OptIn(ExperimentalStdlibApi::class) class ComputationRequestTest { private val compiler = PrlCompiler() diff --git a/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyBooleanNoSlicesTest.kt b/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyBooleanNoSlicesTest.kt index cda7974..9be5233 100644 --- a/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyBooleanNoSlicesTest.kt +++ b/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyBooleanNoSlicesTest.kt @@ -66,7 +66,7 @@ internal class OptimizationOnlyBooleanNoSlicesTest : TestWithConfig() { assertThat(responseMin.detailMap[1]).hasSize(1) assertThat(responseMin.detailMap[1]!![0].slice).isEqualTo(SliceDO(listOf())) - assertThat(responseMin.detailMap[1]!![0].detail.exampleConfiguration!!.features.size).isEqualTo(12) + assertThat(responseMin.detailMap[1]!![0].detail.exampleConfiguration!!.features.size).isEqualTo(13) assertThat(responseMax.merge).hasSize(1) assertThat(responseMax.merge[0].result).isEqualTo(134) diff --git a/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyEnumWithSlicesTest.kt b/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyEnumWithSlicesTest.kt index 32127e4..1e5e99e 100644 --- a/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyEnumWithSlicesTest.kt +++ b/src/test/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationOnlyEnumWithSlicesTest.kt @@ -156,7 +156,7 @@ internal class OptimizationOnlyEnumWithSlicesTest : TestWithConfig() { ) details = detailsForSlice(slice4, result.detailMap[4]) assertThat(details.detail.exampleConfiguration!!.size).isEqualTo(5) - assertThat(details.detail.exampleConfiguration!!.toString()).isEqualTo("a=a2, b=b2, c=c1, p=p2, q=q2") + assertThat(details.detail.exampleConfiguration!!.toString()).isEqualTo("a=a2, b=b2, c=c1, p=p2, q=q1") } @ParameterizedTest @@ -273,7 +273,7 @@ internal class OptimizationOnlyEnumWithSlicesTest : TestWithConfig() { ) details = detailsForSlice(slice4, result.detailMap[4]) assertThat(details.detail.exampleConfiguration!!.size).isEqualTo(5) - assertThat(details.detail.exampleConfiguration!!.toString()).isEqualTo("a=a2, b=b2, c=c3, p=p2, q=q2") + assertThat(details.detail.exampleConfiguration!!.toString()).isEqualTo("a=a2, b=b2, c=c3, p=p2, q=q1") } @ParameterizedTest