adjustments for latest LNG3 snapshot

pom.xml

@@ -53,6 +53,12 @@
     </resources>
 
     <plugins>
+      <plugin>
+        <groupId>org.apache.maven.plugins</groupId>
+        <artifactId>maven-compiler-plugin</artifactId>
+        <version>${version.maven-compiler}</version>
+      </plugin>
+
       <plugin>
         <groupId>org.jetbrains.kotlin</groupId>
         <artifactId>kotlin-maven-plugin</artifactId>
@@ -62,6 +68,9 @@
             <goals>
               <goal>compile</goal>
             </goals>
+            <configuration>
+              <args>-opt-in=kotlin.time.ExperimentalTime</args>
+            </configuration>
           </execution>
           <execution>
             <id>test-compile</id>
@@ -274,7 +283,7 @@
       <scope>test</scope>
     </dependency>
   </dependencies>
-  
+
   <repositories>
     <repository>
       <id>maven-snapshots</id>

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<ConsistencyDetail> {
         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<String>,
         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)

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."

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

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<AnySlicingPropertyDefinition>): List<RuleDO> {
-    assert(solver.sat() == Tristate.FALSE)
-    val mus = MUSGeneration().computeMUS(solver.factory(), solver.unsatCore().propositions())
+internal fun computeExplanation(satCall: SATCall, allDefinitions: List<AnySlicingPropertyDefinition>, f: FormulaFactory): List<RuleDO> {
+    assert(satCall.satResult == Tristate.FALSE)
+    val mus = MUSGeneration().computeMUS(f, satCall.unsatCore().propositions())
     return mus.propositions().filterIsInstance<PrlProposition>().map { p ->
         when (p.backpack().ruleType) {
             RuleType.ORIGINAL_RULE -> RuleDO.fromRulesetRule(p.backpack().rule!!, allDefinitions.map { it.name })

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<Variable>) {
+    private fun addTautologyClauses(solver: SATSolver, variables: SortedSet<Variable>) {
         val f = solver.factory()
         val selTautology = f.variable(SEL_TAUTOLOGY)
         variables.forEach { solver.add(f.or(selTautology, it)) }

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

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)

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