Feature/partial-assignment-test-refactor

src/main/scala/satify/model/dpll/PartialAssignment.scala

@@ -37,68 +37,3 @@ case class PartialAssignment(optVariables: List[OptionalVariable]):
                   .map { case Assignment(variables) => Assignment(v.toVariable +: variables) }
               else List(Assignment(List(v.toVariable)))
         case Nil => Nil
-
-object PartialAssignment:
-
-  import satify.model.dpll.OrderedList.given
-
-  /** Extract a partial assignment from an expression in CNF.
-    * @param cnf where to extract a Model
-    * @return correspondent partial assignment from CNF given as parameter.
-    */
-  def extractParAssignmentFromCnf(cnf: CNF): PartialAssignment =
-
-    def extractOptVars(cnf: CNF): List[OptionalVariable] = cnf match
-      case Symbol(name: String) => List(OptionalVariable(name))
-      case And(e1, e2) => extractOptVars(e1) ++ extractOptVars(e2)
-      case Or(e1, e2) => extractOptVars(e1) ++ extractOptVars(e2)
-      case Not(e) => extractOptVars(e)
-      case _ => Nil
-
-    PartialAssignment(list(extractOptVars(cnf): _*))
-
-  /** Filters unconstrained variables from the partial model
-    * @param partialAssignment partial model
-    * @return filtered partial model
-    */
-  def filterUnconstrVars(partialAssignment: PartialAssignment): List[OptionalVariable] =
-    partialAssignment match
-      case PartialAssignment(optVariables) =>
-        optVariables.filter { case OptionalVariable(_, o) => o.isEmpty }
-
-  /** Update a partial assignment given a constraint as parameter
-    * @param partialAssignment  partial model
-    * @param varConstr variable constraint
-    * @return updated partial assignment
-    */
-  def updatePartialAssignment(partialAssignment: PartialAssignment, varConstr: Constraint): PartialAssignment =
-    partialAssignment match
-      case PartialAssignment(optVariables) =>
-        PartialAssignment(optVariables.map {
-          case OptionalVariable(name, _) if name == varConstr.name =>
-            OptionalVariable(name, Some(varConstr.value))
-          case v => v
-        })
-
-  /** Get all SAT solutions, e.g. all Leaf nodes where the CNF has been simplified to Symbol(True).
-    * @param dt DecisionTree
-    * @return a set of PartialModel(s).
-    */
-  def extractParAssignments(dt: DecisionTree): List[PartialAssignment] =
-    dt match
-      case Leaf(Decision(PartialAssignment(optVars), cnf)) =>
-        cnf match
-          case Symbol(True) =>
-            List(
-              PartialAssignment(
-                optVars.filter(v =>
-                  v match
-                    case OptionalVariable(name, _)
-                        if name.startsWith(converterVarPrefix) || name.startsWith(encodingVarPrefix) =>
-                      false
-                    case _ => true
-                )
-              )
-            )
-          case _ => Nil
-      case Branch(_, left, right) => extractParAssignments(left) ++ extractParAssignments(right)

src/main/scala/satify/update/solver/dpll/DpllDecision.scala

@@ -2,10 +2,10 @@ package satify.update.solver.dpll
 
 import satify.model.cnf.Bool.False
 import satify.model.cnf.CNF.Symbol
-import satify.model.dpll.PartialAssignment.{filterUnconstrVars, updatePartialAssignment}
 import satify.model.dpll.{Constraint, Decision, OptionalVariable}
 import satify.update.solver.dpll.Optimizations.{pureLiteralIdentification, unitLiteralIdentification}
 import satify.update.solver.dpll.cnf.CNFSimplification.simplifyCnf
+import satify.update.solver.dpll.utils.PartialAssignmentUtils.{filterUnconstrVars, updatePartialAssignment}
 
 import scala.util.Random
 

src/main/scala/satify/update/solver/dpll/impl/DpllEnumerator.scala

@@ -4,12 +4,12 @@ import satify.model.Result.*
 import satify.model.Status.COMPLETED
 import satify.model.cnf.CNF
 import satify.model.dpll.DecisionTree.{Branch, Leaf}
-import satify.model.dpll.PartialAssignment.{extractParAssignmentFromCnf, extractParAssignments}
 import satify.model.dpll.{Constraint, Decision, DecisionTree, OptionalVariable}
 import satify.model.{Assignment, Solution}
 import satify.update.solver.dpll.DpllDecision.decide
 import satify.update.solver.dpll.cnf.CNFSat.{isSat, isUnsat}
 import satify.update.solver.dpll.cnf.CNFSimplification.simplifyCnf
+import satify.update.solver.dpll.utils.PartialAssignmentUtils.*
 
 import scala.annotation.tailrec
 import scala.util.Random

src/main/scala/satify/update/solver/dpll/impl/DpllFinder.scala

@@ -7,13 +7,14 @@ import satify.model.cnf.CNF
 import satify.model.cnf.CNF.*
 import satify.model.dpll.*
 import satify.model.dpll.DecisionTree.{Branch, Leaf}
-import satify.model.dpll.PartialAssignment.*
+import satify.model.dpll.PartialAssignment
 import satify.model.expression.SymbolGeneration.{encodingVarPrefix, converterVarPrefix}
 import satify.model.{Assignment, Result, Solution}
 import satify.update.solver.dpll.DpllDecision.decide
 import satify.update.solver.dpll.cnf.CNFSat.{isSat, isUnsat}
 import satify.update.solver.dpll.cnf.CNFSimplification.simplifyCnf
 import satify.update.solver.dpll.impl.DpllFinder.{findNext, resume}
+import satify.update.solver.dpll.utils.PartialAssignmentUtils.*
 
 import scala.util.Random
 

src/main/scala/satify/update/solver/dpll/utils/PartialAssignmentUtils.scala

@@ -0,0 +1,74 @@
+package satify.update.solver.dpll.utils
+
+import satify.model.cnf.Bool.True
+import satify.model.cnf.CNF
+import satify.model.cnf.CNF.{And, Not, Or, Symbol}
+import satify.model.dpll.DecisionTree.{Branch, Leaf}
+import satify.model.dpll.OrderedList.list
+import satify.model.dpll.{Constraint, Decision, DecisionTree, OptionalVariable, PartialAssignment}
+import satify.model.expression.SymbolGeneration.{converterVarPrefix, encodingVarPrefix}
+object PartialAssignmentUtils:
+
+  import satify.model.dpll.OrderedList.given
+
+  /** Get all SAT solutions, e.g. all Leaf nodes where the CNF has been simplified to Symbol(True).
+    *
+    * @param dt DecisionTree
+    * @return a set of PartialModel(s).
+    */
+  def extractParAssignments(dt: DecisionTree): List[PartialAssignment] =
+    dt match
+      case Leaf(Decision(PartialAssignment(optVars), cnf)) =>
+        cnf match
+          case Symbol(True) =>
+            List(
+              PartialAssignment(
+                optVars.filter(v =>
+                  v match
+                    case OptionalVariable(name, _)
+                        if name.startsWith(converterVarPrefix) || name.startsWith(encodingVarPrefix) =>
+                      false
+                    case _ => true
+                )
+              )
+            )
+          case _ => Nil
+      case Branch(_, left, right) => extractParAssignments(left) ++ extractParAssignments(right)
+
+  /** Extract a partial assignment from an expression in CNF.
+    * @param cnf where to extract a Model
+    * @return correspondent partial assignment from CNF given as parameter.
+    */
+  def extractParAssignmentFromCnf(cnf: CNF): PartialAssignment =
+
+    def extractOptVars(cnf: CNF): List[OptionalVariable] = cnf match
+      case Symbol(name: String) => List(OptionalVariable(name))
+      case And(e1, e2) => extractOptVars(e1) ++ extractOptVars(e2)
+      case Or(e1, e2) => extractOptVars(e1) ++ extractOptVars(e2)
+      case Not(e) => extractOptVars(e)
+      case _ => Nil
+
+    PartialAssignment(list(extractOptVars(cnf): _*))
+
+  /** Filters unconstrained variables from the partial model
+    * @param partialAssignment partial model
+    * @return filtered partial model
+    */
+  def filterUnconstrVars(partialAssignment: PartialAssignment): List[OptionalVariable] =
+    partialAssignment match
+      case PartialAssignment(optVariables) =>
+        optVariables.filter { case OptionalVariable(_, o) => o.isEmpty }
+
+  /** Update a partial assignment given a constraint as parameter
+    * @param partialAssignment  partial model
+    * @param varConstr variable constraint
+    * @return updated partial assignment
+    */
+  def updatePartialAssignment(partialAssignment: PartialAssignment, varConstr: Constraint): PartialAssignment =
+    partialAssignment match
+      case PartialAssignment(optVariables) =>
+        PartialAssignment(optVariables.map {
+          case OptionalVariable(name, _) if name == varConstr.name =>
+            OptionalVariable(name, Some(varConstr.value))
+          case v => v
+        })

src/test/scala/satify/model/dpll/PartialAssignmentTest.scala

@@ -7,103 +7,37 @@ import satify.model.cnf.CNF
 import satify.model.cnf.CNF.*
 import satify.model.dpll.DecisionTree.{Branch, Leaf}
 import satify.model.dpll.OrderedList.list
-import satify.model.dpll.PartialAssignment.*
+import satify.model.dpll.PartialAssignment
 import satify.model.dpll.{Constraint, Decision, OptionalVariable, PartialAssignment}
 import satify.model.{Assignment, Variable}
 
 class PartialAssignmentTest extends AnyFlatSpec with Matchers:
 
-  import satify.model.dpll.OrderedList.given
-
-  val varA: OptionalVariable = OptionalVariable("a")
-  val varB: OptionalVariable = OptionalVariable("b")
-
-  val cnf: CNF = And(Symbol("a"), Symbol("b"))
-
-  val dt: DecisionTree = Branch(
-    Decision(
-      PartialAssignment(List(varA, varB)),
-      And(Symbol("a"), Symbol("b"))
-    ),
-    Branch(
-      Decision(PartialAssignment(List(OptionalVariable("a", Some(true)), varB)), Symbol("b")),
-      Leaf(
-        Decision(
-          PartialAssignment(List(OptionalVariable("a", Some(true)), OptionalVariable("b", Some(true)))),
-          Symbol(True)
+  "A set of assignments" should
+    "be extracted from a partial assignment with unconstrained variables by exploding it" in {
+      val partialAssignment: PartialAssignment =
+        PartialAssignment(
+          OptionalVariable("a") ::
+            OptionalVariable("b") ::
+            OptionalVariable("c", Some(true)) :: Nil
         )
-      ),
-      Leaf(
-        Decision(
-          PartialAssignment(List(OptionalVariable("a", Some(true)), OptionalVariable("b", Some(false)))),
-          Symbol(False)
+      Set(partialAssignment.toAssignments: _*) shouldBe
+        Set(
+          Assignment(Variable("a", true) :: Variable("b", true) :: Variable("c", true) :: Nil),
+          Assignment(Variable("a", false) :: Variable("b", true) :: Variable("c", true) :: Nil),
+          Assignment(Variable("a", true) :: Variable("b", false) :: Variable("c", true) :: Nil),
+          Assignment(Variable("a", false) :: Variable("b", false) :: Variable("c", true) :: Nil)
         )
-      )
-    ),
-    Leaf(
-      Decision(PartialAssignment(List(OptionalVariable("a", Some(false)), varB)), Symbol(False))
-    )
-  )
-
-  "A partial assignment" should "be extractable from a CNF" in {
-    extractParAssignmentFromCnf(cnf) shouldBe PartialAssignment(list(varA, varB))
-    val allCnf: CNF =
-      And(Symbol("c"), And(Or(Symbol("d"), Not(Symbol("e"))), Symbol("f")))
-    extractParAssignmentFromCnf(allCnf) shouldBe
-      PartialAssignment(
-        list(
-          OptionalVariable("c"),
-          OptionalVariable("d"),
-          OptionalVariable("e"),
-          OptionalVariable("f")
+    }
+
+  "A unique assignment" should
+    "be extracted from a partial assignment with all variables constrained by exploding it" in {
+      val partialAssignment =
+        PartialAssignment(
+          OptionalVariable("a", Some(true)) ::
+            OptionalVariable("b", Some(true)) ::
+            OptionalVariable("c", Some(true)) :: Nil
         )
-      )
-  }
-
-  "Unconstrained variables" should "be filtered from a partial assignment" in {
-    val partialAssignment: PartialAssignment =
-      PartialAssignment(list(varA, OptionalVariable("c", Some(true)), varB, OptionalVariable("d", Some(false))))
-    filterUnconstrVars(partialAssignment) shouldBe list(varA, varB)
-  }
-
-  "A partial assignment" should "be updated after a constraint is applied" in {
-    val partialAssignment = extractParAssignmentFromCnf(cnf)
-    updatePartialAssignment(partialAssignment, Constraint("a", true)) shouldBe
-      PartialAssignment(
-        list(
-          OptionalVariable("a", Some(true)),
-          varB
-        )
-      )
-    updatePartialAssignment(partialAssignment, Constraint("b", false)) shouldBe
-      PartialAssignment(
-        list(
-          varA,
-          OptionalVariable("b", Some(false))
-        )
-      )
-  }
-
-  "Partial assignments" should "be extractable from a decision tree" in {
-    extractParAssignments(dt) shouldBe
-      PartialAssignment(list(OptionalVariable("a", Some(true)), OptionalVariable("b", Some(true)))) :: Nil
-  }
-
-  "All assignments" should "be extractable from a decision tree" in {
-    val allAssignments =
-      for partialAssignment <- extractParAssignments(dt)
-      yield partialAssignment.toAssignments
-    allAssignments.flatten shouldBe List(Assignment(Variable("a", true) :: Variable("b", true) :: Nil))
-  }
-
-  "All assignments" should "be extractable from a partial assignment" in {
-    val partialAssignment: PartialAssignment =
-      PartialAssignment(list(OptionalVariable("a"), OptionalVariable("b"), OptionalVariable("c", Some(true))))
-    partialAssignment.toAssignments shouldBe
-      List(
-        Assignment(Variable("a", true) :: Variable("b", true) :: Variable("c", true) :: Nil),
-        Assignment(Variable("a", false) :: Variable("b", true) :: Variable("c", true) :: Nil),
-        Assignment(Variable("a", true) :: Variable("b", false) :: Variable("c", true) :: Nil),
-        Assignment(Variable("a", false) :: Variable("b", false) :: Variable("c", true) :: Nil)
-      )
-  }
+      partialAssignment.toAssignments shouldBe
+        Assignment(Variable("a", true) :: Variable("b", true) :: Variable("c", true) :: Nil) :: Nil
+    }

src/test/scala/satify/update/solver/dpll/DpllDecisionTest.scala

@@ -5,7 +5,7 @@ import org.scalatest.matchers.should.Matchers
 import satify.model.cnf.CNF
 import satify.model.cnf.CNF.*
 import satify.model.dpll.{Decision, PartialAssignment, OptionalVariable}
-import satify.model.dpll.PartialAssignment.extractParAssignmentFromCnf
+import satify.update.solver.dpll.utils.PartialAssignmentUtils.extractParAssignmentFromCnf
 import satify.update.solver.dpll.DpllDecision.decide
 
 import scala.util.Random

src/test/scala/satify/update/solver/dpll/impl/DpllFinderTest.scala

@@ -8,10 +8,10 @@ import satify.model.cnf.Bool.{False, True}
 import satify.model.cnf.CNF
 import satify.model.cnf.CNF.{And, Not, Or, Symbol}
 import satify.model.dpll.DecisionTree.{Branch, Leaf}
-import satify.model.dpll.PartialAssignment.extractParAssignmentFromCnf
 import satify.model.dpll.{Decision, DecisionTree}
 import satify.model.{Assignment, Result, Solution, Variable}
 import satify.update.solver.dpll.impl.DpllFinder.{find, findNext, resume}
+import satify.update.solver.dpll.utils.PartialAssignmentUtils.extractParAssignmentFromCnf
 
 class DpllFinderTest extends AnyFlatSpec with Matchers: