Merge pull request #115 from Mala1180/feature/magic-string

Feature/magic-string

src/main/scala/satify/Main.scala

@@ -6,6 +6,7 @@ import satify.dsl.Reflection.startRepl
 import satify.view.Constants.windowSize
 import satify.view.GUI.*
 import satify.view.Reactions.*
+import satify.view.utils.Title.App
 import java.util.concurrent.Executors
 import scala.swing.event.ButtonClicked
 import scala.swing.{Dimension, FileChooser, MainFrame, Swing}
@@ -14,7 +15,7 @@ import scala.swing.{Dimension, FileChooser, MainFrame, Swing}
 object Main extends App with MVU:
   startRepl()
   new MainFrame:
-    title = "Satify SAT Solver"
+    title = App.title
 
     solveAllButton.reactions += { case ButtonClicked(_) =>
       Swing.onEDT(disableInteractions())

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

@@ -16,7 +16,6 @@ case class PartialAssignment(optVariables: List[OptionalVariable]):
   lazy val toAssignments: List[Assignment] = explodeAssignments(this)
 
   /** Cartesian product of all possible variable assignments to a partial assignment.
-    *
     * @param pa partial assignment
     * @return cartesian product of pa
     */
@@ -44,7 +43,6 @@ 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.
     */
@@ -60,7 +58,6 @@ object PartialAssignment:
     PartialAssignment(extractOptVars(cnf))
 
   /** Filters unconstrained variables from the partial model
-    *
     * @param partialAssignment partial model
     * @return filtered partial model
     */
@@ -70,7 +67,6 @@ object PartialAssignment:
         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
@@ -85,7 +81,6 @@ object PartialAssignment:
         })
 
   /** 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).
     */

src/main/scala/satify/model/errors/Error.scala

@@ -1,7 +1,8 @@
 package satify.model.errors
 
-enum Error:
-  case InvalidInput
-  case InvalidImport
-  case EmptySolution
-  case Unknown
+enum Error(val description: String):
+  case InvalidInput extends Error("Invalid input")
+  case InvalidImport extends Error("Import error, select a txt file containing a valid DIMACS CNF")
+  case InvalidExport extends Error("Export error, select a txt file to export the CNF")
+  case EmptySolution extends Error("Empty solution, no next assignment to show")
+  case Unknown extends Error("Unknown error occurred")

src/main/scala/satify/model/problems/Problem.scala

@@ -16,13 +16,3 @@ trait Problem:
   def exp: Expression = constraints.reduceLeft(And(_, _))
 
   def toString(assignment: Assignment): String
-
-//enum ProblemChoice:
-//  case GraphColoring
-//  case NQueens
-//  case NurseScheduling
-
-//enum Problem:
-//  case NQueens(n: Int)
-//  case NurseScheduling(edges: Int, nodes: Int, colors: Int)
-//  case GraphColoring(graph: Map[Int, Set[Int]], colors: Int)

src/main/scala/satify/update/Update.scala

@@ -59,7 +59,6 @@ object Update:
         if input.isEmpty then State(error) else State(input.get, error)
 
   /** Update function to react to the SolveAll message. This function will attempt to solve the input and return a state.
-    *
     * @param input input to solve
     * @return a state with the input, expression, and solution if no exception is thrown, otherwise a state with the input and the occurred error
     */
@@ -126,7 +125,6 @@ object Update:
     )
 
   /** Update function to react to the ConvertProblem message. This function will attempt to convert the selected problem and return a state.
-    *
     * @param problem problem to convert.
     * @return a state with the input, expression, and cnf if no exception is thrown, otherwise a state with the input and the occurred error
     */

src/main/scala/satify/update/converters/tseitin/TseitinTransformation.scala

@@ -2,6 +2,7 @@ package satify.update.converters.tseitin
 
 import satify.model.cnf.CNF
 import satify.model.expression.Expression
+import satify.model.expression.SymbolGeneration.tseitinVarPrefix
 
 import scala.annotation.tailrec
 
@@ -23,7 +24,6 @@ private[converters] object TseitinTransformation:
     concat(transformations)
 
   /** Substitute Symbols of nested subexpressions in all others expressions
-    *
     * @param exp the expression where to substitute Symbols
     * @return the decomposed expression in subexpressions with Symbols correctly substituted.
     */
@@ -58,7 +58,6 @@ private[converters] object TseitinTransformation:
   }
 
   /** Transform the Symbol and the corresponding expression to CNF form
-    *
     * @param exp a Symbol and the corresponding expression
     * @return a list of Symbol and expressions in CNF form for the given Symbol and expression
     * @throws IllegalArgumentException if the expression is not a subexpression
@@ -74,8 +73,7 @@ private[converters] object TseitinTransformation:
     def not(exp: Expression): Literal = exp match
       case Not(Symbol(v)) => CNFSymbol(v)
       case Symbol(v) => CNFNot(CNFSymbol(v))
-      case _ =>
-        throw new IllegalArgumentException("Expression is not a literal")
+      case _ => throw new IllegalArgumentException("Expression is not a literal")
 
     val (s, e) = exp
     val sym = symbol(s)
@@ -95,15 +93,14 @@ private[converters] object TseitinTransformation:
       case ssym @ Symbol(_) => List(symbol(ssym))
 
   /** Concat all subexpression in And to obtain a valid CNF expression.
-    *
     * @param subexpressions the subexpressions to concat.
     * @return the CNF expression.
     */
   def concat(subexpressions: List[CNF]): CNF =
     if subexpressions.size == 1 then subexpressions.head
     else
       var concatenated = subexpressions
-      concatenated = concatenated.prepended(CNFSymbol("TSTN0"))
+      concatenated = concatenated.prepended(CNFSymbol(tseitinVarPrefix + "0"))
       concatenated.reduceRight((s1, s2) =>
         CNFAnd(s1.asInstanceOf[CNFOr | Literal], s2.asInstanceOf[CNFAnd | CNFOr | Literal])
       )

src/main/scala/satify/update/converters/tseitin/Utils.scala

@@ -9,7 +9,6 @@ import satify.model.expression.SymbolGeneration.{SymbolGenerator, tseitinVarPref
 private[converters] object Utils:
 
   /** Zip the subexpressions found in the given expression with a Symbol.
-    *
     * @param exp the expression.
     * @return a list of the subexpressions found in the given expression zipped with the Symbol.
     */
@@ -19,7 +18,6 @@ private[converters] object Utils:
     zipWith(exp)(summon[SymbolGenerator].generate)
 
   /** Method to check if an expression is in CNF form and can be converted to CNF form.
-    *
     * @param expression The expression to check.
     * @return true if the expression could be converted to CNF form, false otherwise and in case of empty expression.
     */
@@ -39,7 +37,6 @@ private[converters] object Utils:
       case _ => false
 
   /** Method to check if an expression is in CNF form and can be converted to CNF form.
-    *
     * @param expression The expression to check.
     * @return true if the expression could be converted to CNF form, false otherwise and in case of empty expression.
     */

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

@@ -15,7 +15,6 @@ object DpllDecision:
 
   /** Make decisions based on the previous one selecting the most appropriate variable and assignment.
     * If no optimization can be applied, it makes a random decision.
-    *
     * @param d previous decision.
     * @return List of new Decisions
     */
@@ -31,7 +30,6 @@ object DpllDecision:
 
   /** Make random decisions based on the previous one given as parameter,
     * by choosing a random variable assigning a random value to it.
-    *
     * @param d previous decision
     * @return List of new decisions
     */
@@ -49,7 +47,6 @@ object DpllDecision:
       else Nil
 
   /** Make unit propagation decision based on the previous decision and the constraint provided.
-    *
     * @param d previous decision.
     * @param c constraint.
     * @return List of new decisions
@@ -64,7 +61,6 @@ object DpllDecision:
 
   /** Make pure literals elimination decisions based on the previous decision and the
     * constraint provided.
-    *
     * @param d previous decision.
     * @param c constraint.
     * @return List of new decisions

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

@@ -20,7 +20,6 @@ import scala.util.Random
 object DpllFinder:
 
   /** Save a run of DPLL algorithm.
-    *
     * @param dt decision tree
     * @param s  solution
     */

src/main/scala/satify/view/Constants.scala

@@ -17,14 +17,10 @@ object Constants:
   val solOutputDialogName = "solOutputDialog"
   val problemOutputDialogName = "problemOutputDialog"
   val nextBtnName = "nextButton"
-
-  // TO MOVE IN PROBLEMS OR PROBLEM UTILS
-  val nqQueens = "nQueens"
-
+  val nQueens = "nQueens"
   val gcNodes = "nodes"
   val gcEdges = "edges"
   val gcColors = "colors"
-
   val nsNurses = "nurses"
   val nsDays = "days"
   val nsShifts = "shifts"

src/main/scala/satify/view/GUI.scala

@@ -2,6 +2,7 @@ package satify.view
 
 import satify.view.utils.ComponentUtils.*
 import satify.view.Constants.*
+import satify.view.utils.Title.*
 
 import java.awt.{Color, Dimension}
 import javax.swing.filechooser.FileNameExtensionFilter
@@ -21,25 +22,25 @@ object GUI:
   val inputScrollPane = new ScrollPane(textPane)
   val problemComboBox: ComboBox[String] = createProblemComboBox()
 
-  val solveAllButton: Button = createButton("Solve all", 200, 40, Color(170, 30, 60))
-  val solveButton: Button = createButton("Solve", 100, 40, Color(170, 30, 60))
-  val solveProblemButton: Button = createButton("Solve", 100, 40, Color(170, 30, 60))
-  val cnfButton: Button = createButton("Convert to CNF", 170, 40, Color(50, 50, 150))
-  val cnfProblemButton: Button = createButton("Convert to CNF", 170, 40, Color(50, 50, 150))
+  val solveAllButton: Button = createButton(SolveAll.title, 200, 40, Color(170, 30, 60))
+  val solveButton: Button = createButton(Solve.title, 100, 40, Color(170, 30, 60))
+  val solveProblemButton: Button = createButton(Solve.title, 100, 40, Color(170, 30, 60))
+  val cnfButton: Button = createButton(Convert.title, 170, 40, Color(50, 50, 150))
+  val cnfProblemButton: Button = createButton(Convert.title, 170, 40, Color(50, 50, 150))
 
-  val solutionOutputDialog: Dialog = createOutputDialog("Solution")
-  val cnfOutputDialog: Dialog = createOutputDialog("Converted formula")
-  val problemOutputDialog: Dialog = createOutputDialog("Problem visualization")
+  val solutionOutputDialog: Dialog = createOutputDialog(SolutionDialog.title)
+  val cnfOutputDialog: Dialog = createOutputDialog(ConversionDialog.title)
+  val problemOutputDialog: Dialog = createOutputDialog(ProblemDialog.title)
   val helpDialog: Dialog = createHelpDialog()
-  val loadingLabel: Label = createLabel("Loading...", 16)
+  val loadingLabel: Label = createLabel(LoadingLabel.title, 16)
   loadingLabel.visible = false
 
   val importFileChooser: FileChooser = createImportFileChooser
   val exportFileChooser: FileChooser = createExportFileChooser
 
-  val helpMenuItem: MenuItem = new MenuItem("Help"):
+  val helpMenuItem: MenuItem = new MenuItem(Help.title):
     maximumSize = new Dimension(50, 200)
-  val importMenuItem: MenuItem = new MenuItem("Import"):
+  val importMenuItem: MenuItem = new MenuItem(Import.title):
     maximumSize = new Dimension(1000, 200)
 
   def inputTextPane: TextPane = inputScrollPane.contents
@@ -55,12 +56,12 @@ object GUI:
       contents += new BoxPanel(Orientation.Horizontal):
         contents += logoLabel
       contents += new TabbedPane:
-        pages += new Page("Input", createInputComponent())
-        pages += new Page("Problems", createProblemsComponent())
+        pages += new Page(InputTab.title, createInputComponent())
+        pages += new Page(ProblemTab.title, createProblemsComponent())
 
   private def createInputComponent(): Component =
     val borderPanel: BorderPanel = new BorderPanel():
-      val label = new Label("Input:")
+      val label = new Label(InputTab.title)
       label.border = Swing.EmptyBorder(0, 0, 2, 0)
       label.horizontalAlignment = Alignment.Left
       layout(label) = BorderPanel.Position.North
@@ -106,17 +107,16 @@ object GUI:
     * @return the file chooser
     */
   private def createImportFileChooser: FileChooser = new FileChooser:
-    title = "Import DIMACS formula"
+    title = ImportDialog.title
     fileSelectionMode = FileChooser.SelectionMode.FilesOnly
     fileFilter = new FileNameExtensionFilter("Text files", "txt")
     multiSelectionEnabled = false
 
   /** Creates a file chooser for the export item in CNF output dialog.
-    *
     * @return the file chooser
     */
   def createExportFileChooser: FileChooser = new FileChooser:
-    title = "Export DIMACS formula"
+    title = ExportDialog.title
     fileSelectionMode = FileChooser.SelectionMode.DirectoriesOnly
     multiSelectionEnabled = false
 

src/main/scala/satify/view/Reactions.scala

@@ -7,6 +7,12 @@ import satify.update.Update.update
 import satify.view.utils.ComponentUtils.createErrorDialog
 import satify.view.Constants.*
 import satify.view.GUI.*
+import satify.model.errors.Error.InvalidInput
+import satify.view.utils.ProblemTitle.{
+  NQueens as GUINQueens,
+  GraphColoring as GUIGraphColoring,
+  NurseScheduling as GUINurseScheduling
+}
 
 import java.io.File
 import scala.swing.{Component, Swing, TextArea}
@@ -88,7 +94,7 @@ object Reactions:
     var p: Problem = null
     def checkInt(input: String): Int =
       if !input.equals("") && input.forall(_.isDigit) && input.toInt > 0 then input.toInt
-      else throw new IllegalArgumentException("Parameter value is not valid")
+      else throw new IllegalArgumentException(InvalidInput.description)
     def getInput(name: String): TextArea = problemParameterPanel.contents
       .filter(c => c.isInstanceOf[TextArea] && c.name.equals(name))
       .head
@@ -98,14 +104,14 @@ object Reactions:
       input.split(",").map(_.trim).toList.map(_.split("-").map(_.trim).toList).map(l => (l.head, l.last))
     try
       p = problemComboBox.item match
-        case "N-Queens" => NQueens(checkInt(getInput(nqQueens).text))
-        case "Graph Coloring" =>
+        case GUINQueens.title => NQueens(checkInt(getInput(nQueens).text))
+        case GUIGraphColoring.title =>
           GraphColoring(
             checkEdges(getInput(gcEdges).text),
             checkNodes(getInput(gcNodes).text),
             checkInt(getInput(gcColors).text)
           )
-        case "Nurse Scheduling" =>
+        case GUINurseScheduling.title =>
           NurseScheduling(
             checkInt(getInput(nsNurses).text),
             checkInt(getInput(nsDays).text),
@@ -114,5 +120,5 @@ object Reactions:
     catch
       case e: Exception =>
         e.printStackTrace()
-        createErrorDialog("Input not valid").open()
+        createErrorDialog(InvalidInput.description).open()
     p