From 86ca9ea55a1a6d9b91b05ad380125fe809c37087 Mon Sep 17 00:00:00 2001 From: Mattia Matteini Date: Mon, 21 Aug 2023 12:21:51 +0200 Subject: [PATCH 1/2] feat: add fields to State, change xor symbol --- src/main/scala/satify/dsl/DSL.scala | 2 +- src/main/scala/satify/model/Problem.scala | 6 ++++++ src/main/scala/satify/model/State.scala | 19 ++++++++++--------- .../scala/satify/dsl/MathOperatorsTest.scala | 4 ++-- 4 files changed, 19 insertions(+), 12 deletions(-) create mode 100644 src/main/scala/satify/model/Problem.scala diff --git a/src/main/scala/satify/dsl/DSL.scala b/src/main/scala/satify/dsl/DSL.scala index bd6a3fc4..3a46bde6 100644 --- a/src/main/scala/satify/dsl/DSL.scala +++ b/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) diff --git a/src/main/scala/satify/model/Problem.scala b/src/main/scala/satify/model/Problem.scala new file mode 100644 index 00000000..b51ea624 --- /dev/null +++ b/src/main/scala/satify/model/Problem.scala @@ -0,0 +1,6 @@ +package satify.model + +enum Problem: + case NQueens(n: Int) + case NurseScheduling() + case ColoringGraph() diff --git a/src/main/scala/satify/model/State.scala b/src/main/scala/satify/model/State.scala index e9bff4d7..fa0dd8dd 100644 --- a/src/main/scala/satify/model/State.scala +++ b/src/main/scala/satify/model/State.scala @@ -4,24 +4,23 @@ 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. */ def apply(): State = StateImpl() @@ -31,12 +30,14 @@ object State: * @return a new State instance. */ def apply(exp: Expression, cnf: CNF): State = StateImpl(Some(exp), Some(cnf)) + 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 diff --git a/src/test/scala/satify/dsl/MathOperatorsTest.scala b/src/test/scala/satify/dsl/MathOperatorsTest.scala index f236ebf7..ea24bc6e 100644 --- a/src/test/scala/satify/dsl/MathOperatorsTest.scala +++ b/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") } From e791d4236c0ca56f07ddbbb8fd1f4510e868e3de Mon Sep 17 00:00:00 2001 From: Mattia Matteini Date: Mon, 21 Aug 2023 12:37:21 +0200 Subject: [PATCH 2/2] feat: define factories of State --- src/main/scala/satify/model/State.scala | 28 ++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/src/main/scala/satify/model/State.scala b/src/main/scala/satify/model/State.scala index fa0dd8dd..f97c5669 100644 --- a/src/main/scala/satify/model/State.scala +++ b/src/main/scala/satify/model/State.scala @@ -20,17 +20,35 @@ trait State: /** 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( override val expression: Option[Expression] = None, override val cnf: Option[CNF] = None,