Feature/complete-model

src/main/scala/satify/dsl/DSL.scala

@@ -25,4 +25,4 @@ object DSL:
     @targetName("notSymbol")
     def unary_! : Expression = not
     @targetName("xorSymbol")
-    def ⊕(exp2: Expression): Expression = xor(exp2)
+    def ^(exp2: Expression): Expression = xor(exp2)

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

@@ -0,0 +1,6 @@
+package satify.model
+
+enum Problem:
+  case NQueens(n: Int)
+  case NurseScheduling()
+  case ColoringGraph()

src/main/scala/satify/model/State.scala

@@ -4,39 +4,58 @@ package satify.model
 trait State:
   /** A general expression of boolean logic, it is the user input */
   type Expression
-//  val expression: Option[Expression] = None
+  val expression: Option[Expression]
 
   /** The input expression converted to Conjunctive Normal Form (CNF) */
   type CNF
-//  val cnf: Option[CNF] = None
+  val cnf: Option[CNF]
 
   /** An entity containing the solution of the problem (SAT or UNSAT, optional Assignment), it is the output of DPLL */
   type Solution
-//  val solution: Option[Solution] = None
+  val solution: Option[Solution]
 
   /** An entity representing the problem to solve */
   type Problem
-//  val problem: Option[Problem] = None
+  val problem: Option[Problem]
 
 /** Factory for [[satify.model.State]] instances. */
 object State:
-  /** Creates a new application state.
-    *
-    * @return a new State instance.
+  /** Creates a new empty application state.
+    * @return a new [[State]] instance.
     */
   def apply(): State = StateImpl()
 
-  /** Creates a new application state with the given CNF.
-    * @param cnf the CNF to set
-    * @return a new State instance.
+  /** Creates a new application state with input expression and its CNF.
+    * @param exp the input [[Expression]]
+    * @param cnf the [[CNF]]
+    * @return a new [[State]] instance.
     */
   def apply(exp: Expression, cnf: CNF): State = StateImpl(Some(exp), Some(cnf))
+
+  /** Creates a new application state with the input expression, its CNF and the solution.
+    * @param exp the input [[Expression]]
+    * @param cnf the [[CNF]]
+    * @param sol the [[Solution]]
+    * @return a new [[State]] instance.
+    */
+  def apply(exp: Expression, cnf: CNF, sol: Solution): State = StateImpl(Some(exp), Some(cnf), Some(sol))
+
+  /** Creates a new application state with an input problem, its CNF, and its solution.
+    * @param cnf the [[CNF]]
+    * @param sol the [[Solution]]
+    * @param problem the [[Problem]] selected
+    * @return a new [[State]] instance.
+    */
+  def apply(cnf: CNF, sol: Solution, problem: Problem): State =
+    StateImpl(None, Some(cnf), Some(sol), Some(problem))
+
   private case class StateImpl(
-      expression: Option[Expression] = None,
-      cnf: Option[CNF] = None,
-      solution: Option[Solution] = None
+      override val expression: Option[Expression] = None,
+      override val cnf: Option[CNF] = None,
+      override val solution: Option[Solution] = None,
+      override val problem: Option[Problem] = None
   ) extends State:
     override type Expression = satify.model.Expression
     override type CNF = satify.model.CNF
     override type Solution = satify.model.Solution
-//    type Problem = satify.model.Problem
+    override type Problem = satify.model.Problem

src/test/scala/satify/dsl/MathOperatorsTest.scala

@@ -19,6 +19,6 @@ class MathOperatorsTest extends AnyFlatSpec:
     !"A" shouldBe not("A")
   }
 
-  """ "A" ⊕ "B" """ should """ be equal to "A" xor "B" """ in {
-    "A" ⊕ "B" shouldBe ("A" xor "B")
+  """ "A" ^ "B" """ should """ be equal to "A" xor "B" """ in {
+    "A" ^ "B" shouldBe ("A" xor "B")
   }