Adjustements for latest 0.0.2

booleworks · Jun 2, 2024 · 2660988 · 2660988
1 parent 9fdea71
commit 2660988
Show file tree

Hide file tree

Showing 19 changed files with 230 additions and 407 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
@@ -23,7 +23,7 @@ import com.booleworks.boolerules.computations.generic.extractFeature
 import com.booleworks.logicng.csp.CspFactory
 import com.booleworks.prl.model.PrlModel
 import com.booleworks.prl.model.slices.Slice
-import com.booleworks.prl.transpiler.TranslationInfo
+import com.booleworks.prl.transpiler.TranspilationInfo
 
 val BACKBONE =
     object : ComputationType<
@@ -72,15 +72,16 @@ internal object BackboneComputation : ListComputation<
     override fun computeForSlice(
         request: BackboneRequest,
         slice: Slice,
-        info: TranslationInfo,
+        info: TranspilationInfo,
         model: PrlModel,
         cf: CspFactory,
         status: ComputationStatusBuilder,
     ): BackboneInternalResult {
+        val f = cf.formulaFactory()
         val result = BackboneInternalResult(slice, LinkedHashMap())
-        val relevantVars = computeRelevantVars(cf.formulaFactory(), info, request.features)
+        val relevantVars = computeRelevantVars(f, info, request.features)
 
-        val solver = satSolver(NON_PT_CONFIG, cf, info, slice, status).also { if (!status.successful()) return result }
+        val solver = satSolver(NON_PT_CONFIG, f, 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 }

diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckApi.kt b/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckApi.kt
diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/bomcheck/BomCheckComputation.kt
diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt b/src/main/kotlin/com/booleworks/boolerules/computations/consistency/ConsistencyComputation.kt
@@ -24,7 +24,7 @@ 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
+import com.booleworks.prl.transpiler.TranspilationInfo
 
 val CONSISTENCY = object : ComputationType<
         ConsistencyRequest,
@@ -66,7 +66,7 @@ internal object ConsistencyComputation :
     override fun computeForSlice(
         request: ConsistencyRequest,
         slice: Slice,
-        info: TranslationInfo,
+        info: TranspilationInfo,
         model: PrlModel,
         cf: CspFactory,
         status: ComputationStatusBuilder,
@@ -96,15 +96,15 @@ internal object ConsistencyComputation :
     override fun computeDetailForSlice(
         slice: Slice,
         model: PrlModel,
-        info: TranslationInfo,
+        info: TranspilationInfo,
         additionalConstraints: List<String>,
         splitProperties: Set<String>,
         cf: CspFactory
     ): SplitComputationDetail<ConsistencyDetail> {
         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)
+            val explanation = computeExplanation(satCall, model.propertyStore.allDefinitions(), info.cf)
             val result = ConsistencyInternalResult(slice, false, null, explanation)
             SplitComputationDetail(result, splitProperties)
         }
@@ -113,7 +113,7 @@ internal object ConsistencyComputation :
     private fun prepareSolver(
         cf: CspFactory,
         proofTracing: Boolean,
-        info: TranslationInfo,
+        info: TranspilationInfo,
     ): SATSolver {
         val f = cf.formulaFactory()
         val solver = SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(proofTracing).build()).apply {

diff --git a/src/main/kotlin/com/booleworks/boolerules/computations/coverage/CoverageApi.kt b/src/main/kotlin/com/booleworks/boolerules/computations/coverage/CoverageApi.kt
@@ -31,7 +31,9 @@ data class CoverageRequest(
                 "must be covered. So for constraints A, B, and C, the combinations A+B, A+C, and B+C must be covered."
     )
     val pairwiseCover: Boolean = false
-) : ComputationRequest
+) : ComputationRequest {
+    override fun considerConstraints() = constraintsToCover
+}
 
 @Schema(description = "The details for a coverage computation")
 data class CoverageDetail(