Additional constraints are handled by the PRL compiler now

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

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<PositionElementDO> = mutableListOf()

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<String>,
         cf: CspFactory
     ): SplitComputationDetail<ConsistencyDetail> {
-        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<String>,
-        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
     }
 

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<Pair<Formula, String>>()
         val invalidConstraints = mutableListOf<String>()
         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 {

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,50 +236,18 @@ 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
     }
 
     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<PrlConstraint>(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<DETAIL> {
         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

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)

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(

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)

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<Formula, Int>()
         val constraintMap = mutableMapOf<Formula, String>()
         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)
             }

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))
 

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

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