From 9281a1dffcf91fb1000968eae5d513bb59c89571 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Thu, 30 May 2024 17:18:34 +0200 Subject: [PATCH] Additional constraints are handled by the PRL compiler now --- .../backbone/BackboneComputation.kt | 23 ++------- .../bomcheck/BomCheckComputation.kt | 2 +- .../consistency/ConsistencyComputation.kt | 18 +------ .../coverage/CoverageComputation.kt | 4 +- .../computations/generic/Computation.kt | 51 ++++--------------- .../minmaxconfig/MinMaxConfigComputation.kt | 2 +- .../modelcount/ModelCountComputation.kt | 7 +-- .../ModelEnumerationComputation.kt | 2 +- .../optimization/OptimizationComputation.kt | 10 ++-- .../BackboneOnlyEnumWithSlicesTest.kt | 3 +- .../computations/modelcount/ModelCountTest.kt | 5 +- .../modelenumeration/ModelEnumerationTest.kt | 5 +- 12 files changed, 33 insertions(+), 99 deletions(-) diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/backbone/BackboneComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/backbone/BackboneComputation.kt index 19e0675..44bc302 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/backbone/BackboneComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/backbone/BackboneComputation.kt @@ -80,27 +80,12 @@ internal object BackboneComputation : ListComputation< val result = BackboneInternalResult(slice, LinkedHashMap()) val relevantVars = computeRelevantVars(cf.formulaFactory(), info, request.features) - val solver = miniSat( - NON_PT_CONFIG, - request, - cf, - model, - info, - slice, - status - ).also { if (!status.successful()) return result } - + val solver = satSolver(NON_PT_CONFIG, cf, info, slice, status).also { if (!status.successful()) return result } val backbone = solver.backbone(relevantVars) if (backbone.isSat) { - backbone.positiveBackbone.forEach { - result.backbone[extractFeature(it, info)] = BackboneType.MANDATORY - } - backbone.negativeBackbone.forEach { - result.backbone[extractFeature(it, info)] = BackboneType.FORBIDDEN - } - backbone.optionalVariables.forEach { - result.backbone[extractFeature(it, info)] = BackboneType.OPTIONAL - } + backbone.positiveBackbone.forEach { result.backbone[extractFeature(it, info)] = BackboneType.MANDATORY } + backbone.negativeBackbone.forEach { result.backbone[extractFeature(it, info)] = BackboneType.FORBIDDEN } + backbone.optionalVariables.forEach { result.backbone[extractFeature(it, info)] = BackboneType.OPTIONAL } } else { relevantVars.forEach { result.backbone[extractFeature(it, info)] = BackboneType.FORBIDDEN diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckComputation.kt index 15a8d43..7107f05 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckComputation.kt @@ -76,7 +76,7 @@ internal object BomCheckComputation : cf: CspFactory, status: ComputationStatusBuilder, ): BomCheckInternalResult { - val solver = miniSat(NON_PT_CONFIG, request, cf, model, info, slice, status).also { + val solver = satSolver(NON_PT_CONFIG, cf, info, slice, status).also { if (!status.successful()) return BomCheckInternalResult(slice, mutableMapOf()) } val positionElements: MutableList = mutableListOf() 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 78dca12..0a6a6cd 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt @@ -7,9 +7,7 @@ import com.booleworks.boolerules.computations.ComputationType import com.booleworks.boolerules.computations.NoElement import com.booleworks.boolerules.computations.consistency.ConsistencyComputation.ConsistencyInternalResult import com.booleworks.boolerules.computations.generic.ApiDocs -import com.booleworks.boolerules.computations.generic.ComputationStatus import com.booleworks.boolerules.computations.generic.ComputationStatusBuilder -import com.booleworks.boolerules.computations.generic.ComputationVariant.SINGLE import com.booleworks.boolerules.computations.generic.FeatureModelDO import com.booleworks.boolerules.computations.generic.InternalResult import com.booleworks.boolerules.computations.generic.NON_CACHING_USE_FF @@ -73,7 +71,7 @@ internal object ConsistencyComputation : cf: CspFactory, status: ComputationStatusBuilder, ): ConsistencyInternalResult { - val solver = prepareSolver(cf, request.computeAllDetails, info, request.additionalConstraints, model, status) + val solver = prepareSolver(cf, request.computeAllDetails, info) if (!status.successful()) return ConsistencyInternalResult(slice, false, null, null) return solver.satCall().solve().use { satCall -> if (satCall.satResult == Tristate.TRUE) { @@ -103,7 +101,7 @@ internal object ConsistencyComputation : splitProperties: Set, cf: CspFactory ): SplitComputationDetail { - val solver = prepareSolver(cf, true, info, additionalConstraints, model, ComputationStatus("", "", SINGLE)) + val solver = prepareSolver(cf, true, info) 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(), cf) @@ -116,23 +114,11 @@ internal object ConsistencyComputation : cf: CspFactory, proofTracing: Boolean, info: TranslationInfo, - additionalConstraints: List, - model: PrlModel, - status: ComputationStatusBuilder ): SATSolver { val f = cf.formulaFactory() val solver = SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(proofTracing).build()).apply { addPropositions(info.propositions) } - if (solver.sat()) { - val additionalFormulas = - additionalConstraints.mapNotNull { constraint -> - processConstraint(cf, constraint, model, info, status) - } - if (!status.successful()) return solver - solver.addPropositions(additionalFormulas) - - } return solver } diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/coverage/CoverageComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/coverage/CoverageComputation.kt index fe189a4..d6c363f 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/coverage/CoverageComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/coverage/CoverageComputation.kt @@ -115,7 +115,7 @@ internal object CoverageComputation : ): CoverageInitialization? { val baseConstraints = translation.propositions.map { it.formula() }.toMutableList() baseConstraints += request.additionalConstraints.mapNotNull { - processConstraint(cf, it, model, translation, status)?.formula() + processConstraint(cf, it, model, translation, status) } val (invalidConstraints, constraintsToCover) = computeConstraintsToCover( cf, @@ -146,7 +146,7 @@ internal object CoverageComputation : val validConstraints = mutableListOf>() val invalidConstraints = mutableListOf() for (constraint in request.constraintsToCover) { - val formula = processConstraint(cf, constraint, model, info, status)?.formula() ?: return null + val formula = processConstraint(cf, constraint, model, info, status) ?: return null if (baseSolver.satCall().addFormulas(formula).sat() == Tristate.FALSE) { invalidConstraints.add(constraint) } else { 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 29fe729..eee5f7a 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/generic/Computation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/generic/Computation.kt @@ -5,6 +5,7 @@ package com.booleworks.boolerules.computations.generic import com.booleworks.boolerules.config.ComputationConfig import com.booleworks.logicng.csp.CspFactory +import com.booleworks.logicng.formulas.Formula import com.booleworks.logicng.formulas.FormulaFactory import com.booleworks.logicng.formulas.FormulaFactoryConfig import com.booleworks.logicng.formulas.FormulaFactoryConfig.FormulaMergeStrategy.IMPORT @@ -24,8 +25,6 @@ import com.booleworks.prl.parser.PrlFeature import com.booleworks.prl.parser.parseConstraint import com.booleworks.prl.transpiler.IntegerEncodingStore import com.booleworks.prl.transpiler.ModelTranslation -import com.booleworks.prl.transpiler.PrlProposition -import com.booleworks.prl.transpiler.RuleInformation import com.booleworks.prl.transpiler.SliceTranslation import com.booleworks.prl.transpiler.TranslationInfo import com.booleworks.prl.transpiler.mergeSlices @@ -122,7 +121,10 @@ sealed class Computation< val factory: FormulaFactory = FormulaFactory.caching() val cspFactory = CspFactory(factory) request.validateAndAugmentSliceSelection(model, allowedSliceTypes()) - val modelTranslation = transpileModel(cspFactory, model, request.modelSliceSelection()) + val modelTranslation = transpileModel( + cspFactory, model, request.modelSliceSelection(), + additionalConstraints = request.additionalConstraints + ) status.numberOfSlices = modelTranslation.allSlices.size status.sliceSets = computeProjectedSliceSets(modelTranslation.computations, request) val slice2Translation = modelTranslation.sliceMap() @@ -220,11 +222,9 @@ sealed class Computation< } } - internal fun miniSat( + internal fun satSolver( config: SATSolverConfig, - request: REQUEST, cf: CspFactory, - model: PrlModel, info: TranslationInfo, slice: Slice, status: ComputationStatusBuilder @@ -236,25 +236,6 @@ sealed class Computation< "Original rule set for the slice $slice is inconsistent. " + "Use the 'consistency' check to get an explanation, why." ) - return solver - } - val additionalFormulas = request.additionalConstraints.mapNotNull { constraint -> - processConstraint( - cf, - constraint, - model, - info, - status - ) - } - if (status.successful()) { - solver.addPropositions(additionalFormulas) - 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." - ) - } } return solver } @@ -262,24 +243,11 @@ sealed class Computation< internal fun maxSat( config: MaxSATConfig, algo: (FormulaFactory, MaxSATConfig) -> MaxSATSolver, - request: REQUEST, cf: CspFactory, - model: PrlModel, info: TranslationInfo, - status: ComputationStatusBuilder ): MaxSATSolver { val solver = algo(cf.formulaFactory(), config) info.propositions.forEach { solver.addHardFormula(it.formula()) } - val additionalFormulas = request.additionalConstraints.mapNotNull { constraint -> - processConstraint( - cf, - constraint, - model, - info, - status - ) - } - if (status.successful()) additionalFormulas.forEach { solver.addHardFormula(it.formula()) } return solver } @@ -289,13 +257,12 @@ sealed class Computation< model: PrlModel, info: TranslationInfo, status: ComputationStatusBuilder - ): PrlProposition? { + ): Formula? { val parsed = parseConstraint(constraint) val theoryMap = model.featureStore.theoryMap if (!checkTheoryMap(parsed, theoryMap, status)) return null val compiled = ConstraintCompiler().compileConstraint(parsed, theoryMap) - val formula = transpileConstraint(cf, compiled, info, IntegerEncodingStore.empty()) // TODO: integer store - return PrlProposition(RuleInformation.fromAdditionRestriction(compiled), formula) + return transpileConstraint(cf, compiled, info, IntegerEncodingStore.empty()) // TODO: integer store } private fun checkTheoryMap( @@ -348,7 +315,7 @@ abstract class SingleComputation< ): SplitComputationDetail { val f = FormulaFactory.caching() val cf = CspFactory(f) - val modelTranslation = transpileModel(cf, model, sliceSelection) + val modelTranslation = transpileModel(cf, model, sliceSelection, additionalConstraints = additionalConstraints) assert(modelTranslation.computations.size == 1) { "Expected to get exactly one slice" } val slice = modelTranslation.allSlices.first() val translation = modelTranslation.computations.first().info diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/minmaxconfig/MinMaxConfigComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/minmaxconfig/MinMaxConfigComputation.kt index 3271694..27d7ca8 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/minmaxconfig/MinMaxConfigComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/minmaxconfig/MinMaxConfigComputation.kt @@ -75,7 +75,7 @@ internal object MinMaxConfigComputation : ): MinMaxInternalResult { val f = cf.formulaFactory() val relevantVars = computeRelevantVars(f, info, request.features) - val solver = maxSat(MaxSATConfig.builder().build(), MaxSATSolver::oll, request, cf, model, info, status) + val solver = maxSat(MaxSATConfig.builder().build(), MaxSATSolver::oll, cf, info) relevantVars.forEach { solver.addSoftFormula(f.literal(it.name(), request.computationType == MAX), 1) } return if (solver.solve() == OPTIMUM) { val example = extractModel(solver.model().positiveVariables(), info) diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountComputation.kt index 4950d67..c965bd0 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountComputation.kt @@ -68,15 +68,10 @@ internal object ModelCountComputation : val f = cf.formulaFactory() val variables = info.knownVariables.toSortedSet() val formulas = info.propositions.map { it.formula() } - val additionalConstraints = - request.additionalConstraints.map { constraint -> processConstraint(cf, constraint, model, info, status) } if (!status.successful()) { return ModelCountInternalResult(slice, BigInteger.ZERO) } - return ModelCountInternalResult( - slice, - ModelCounter.count(f, formulas + additionalConstraints.map { it!!.formula() }, variables) - ) + return ModelCountInternalResult(slice, ModelCounter.count(f, formulas, variables)) } override fun computeDetailForSlice( 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 f2aa141..1c1b9df 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationComputation.kt @@ -85,7 +85,7 @@ internal object ModelEnumerationComputation : ListComputation< val f = cf.formulaFactory() val relevantVars = computeRelevantVars(f, info, request.features) - val solver = miniSat(NON_PT_CONFIG, request, cf, model, info, slice, status).also { + val solver = satSolver(NON_PT_CONFIG, cf, info, slice, status).also { if (!status.successful()) return ModelEnumerationInternalResult(slice, mutableMapOf()) } addTautologyClauses(solver, relevantVars) diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationComputation.kt index af97938..8f161c7 100644 --- a/src/main/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationComputation.kt +++ b/src/main/kotlin/com/booleworks/boolerules/computations/optimization/OptimizationComputation.kt @@ -76,7 +76,7 @@ internal object OptimizationComputation : cf: CspFactory, status: ComputationStatusBuilder, ): OptimizationInternalResult { - val solver = maxSat(MaxSATConfig.builder().build(), MaxSATSolver::oll, request, cf, model, info, status) + val solver = maxSat(MaxSATConfig.builder().build(), MaxSATSolver::oll, cf, info) val mapping = mutableMapOf() val constraintMap = mutableMapOf() request.weightings.forEach { wp -> @@ -88,12 +88,12 @@ internal object OptimizationComputation : if (request.computationType == MIN && wp.weight >= 0 || request.computationType == MAX && wp.weight < 0 ) { - constraint.formula().negate(cf.formulaFactory()) + constraint.negate(cf.formulaFactory()) } else { - constraint.formula() + constraint } - mapping[constraint.formula()] = wp.weight - constraintMap[constraint.formula()] = wp.constraint + mapping[constraint] = wp.weight + constraintMap[constraint] = wp.constraint val weight = wp.weight.absoluteValue solver.addSoftFormula(formula, weight) } diff --git a/src/test/kotlin/com/booleworks/boolerules/computations/backbone/BackboneOnlyEnumWithSlicesTest.kt b/src/test/kotlin/com/booleworks/boolerules/computations/backbone/BackboneOnlyEnumWithSlicesTest.kt index a3721fb..df188e5 100644 --- a/src/test/kotlin/com/booleworks/boolerules/computations/backbone/BackboneOnlyEnumWithSlicesTest.kt +++ b/src/test/kotlin/com/booleworks/boolerules/computations/backbone/BackboneOnlyEnumWithSlicesTest.kt @@ -289,8 +289,7 @@ internal class BackboneOnlyEnumWithSlicesTest : TestWithConfig() { ), PropertySelectionDO("version", PropertyTypeDO.INT, PropertyRangeDO(intValues = setOf(1)), SliceTypeDO.SPLIT) ) - val request = - BackboneRequest("any", sliceSelection, listOf("[c = \"c1\"]"), listOf("a", "b", "c")) + val request = BackboneRequest("any", sliceSelection, listOf("[c = \"c1\"]"), listOf("a", "b", "c")) val result = cut.computeForModel(request, model, ComputationStatusBuilder("fileId", "jobId", LIST)) diff --git a/src/test/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountTest.kt b/src/test/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountTest.kt index 7d931aa..1202c7e 100644 --- a/src/test/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountTest.kt +++ b/src/test/kotlin/com/booleworks/boolerules/computations/modelcount/ModelCountTest.kt @@ -73,9 +73,10 @@ internal class ModelCountTest : TestWithConfig() { fun testComputeForSliceWithAdditionalConstraints() { val f = FormulaFactory.nonCaching() val cf = CspFactory(f) - val modelTranslation = transpileModel(cf, model, listOf()) + val additionalConstraint = listOf("[c = \"c1\"]") + val modelTranslation = transpileModel(cf, model, listOf(), additionalConstraints = additionalConstraint) - val request = ModelCountRequest("any", mutableListOf(), listOf("[c = \"c1\"]")) + val request = ModelCountRequest("any", mutableListOf(), additionalConstraint) val info1 = modelTranslation[0].info val info2 = modelTranslation[1].info val info3 = modelTranslation[2].info diff --git a/src/test/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationTest.kt b/src/test/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationTest.kt index 474ecec..811f0f9 100644 --- a/src/test/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationTest.kt +++ b/src/test/kotlin/com/booleworks/boolerules/computations/modelenumeration/ModelEnumerationTest.kt @@ -125,9 +125,10 @@ internal class ModelEnumerationTest : TestWithConfig() { setUp(tc) val f = FormulaFactory.nonCaching() val cf = CspFactory(f) - val modelTranslation = transpileModel(cf, model, listOf()) + val additionalConstraints = listOf("[c = \"c1\"]") + val modelTranslation = transpileModel(cf, model, listOf(), additionalConstraints = additionalConstraints) - val request = ModelEnumerationRequest("any", mutableListOf(), listOf("[c = \"c1\"]"), listOf()) + val request = ModelEnumerationRequest("any", mutableListOf(), additionalConstraints, listOf()) val info1 = modelTranslation[0].info val info2 = modelTranslation[1].info val info3 = modelTranslation[2].info