diff --git a/doc/api/satify/model/cnf/CNF$.html b/doc/api/satify/model/cnf/CNF$.html index 3ea4e671..8d8809bd 100644 --- a/doc/api/satify/model/cnf/CNF$.html +++ b/doc/api/satify/model/cnf/CNF$.html @@ -196,20 +196,20 @@

Extensions

extension (cnf: CNF)(cnf: CNF) -
+
- def printAsDSL(flat: Boolean): String + def asDSL(flat: Boolean): String
-
+
- def printAsFormal(flat: Boolean): String + def asFormal(flat: Boolean): String
diff --git a/doc/api/satify/model/cnf/CNF.html b/doc/api/satify/model/cnf/CNF.html index b002eccb..9f910fd6 100644 --- a/doc/api/satify/model/cnf/CNF.html +++ b/doc/api/satify/model/cnf/CNF.html @@ -161,12 +161,12 @@

Value members

Concrete methods

-
+
- def printAsDSL(flat: Boolean): String + def asDSL(flat: Boolean): String
@@ -180,12 +180,12 @@

Concrete methods

-
+
- def printAsFormal(flat: Boolean): String + def asFormal(flat: Boolean): String
diff --git a/doc/api/satify/model/expression/Utils$.html b/doc/api/satify/model/expression/Utils$.html index 6fabf04a..e9d290d0 100644 --- a/doc/api/satify/model/expression/Utils$.html +++ b/doc/api/satify/model/expression/Utils$.html @@ -90,20 +90,20 @@

Extensions

extension (exp: Expression)(exp: Expression) -
+
- def printAsDSL(flat: Boolean): String + def asDSL(flat: Boolean): String
-
+
- def printAsFormal(flat: Boolean): String + def asFormal(flat: Boolean): String
diff --git a/doc/api/scripts/searchData.js b/doc/api/scripts/searchData.js index 5b518975..e49e0d54 100644 --- a/doc/api/scripts/searchData.js +++ b/doc/api/scripts/searchData.js @@ -77,8 +77,8 @@ pages = [{"l":"index.html#","e":false,"i":"","n":"satify","t":"satify","d":"","k {"l":"satify/model/cnf/CNF$$And.html#","e":false,"i":"","n":"And","t":"And(left: Or | Literal, right: And | Or | Literal)","d":"satify.model.cnf.CNF","k":"case","x":""}, {"l":"satify/model/cnf/CNF$$Or.html#","e":false,"i":"","n":"Or","t":"Or(left: Or | Literal, right: Or | Literal)","d":"satify.model.cnf.CNF","k":"case","x":""}, {"l":"satify/model/cnf/CNF$.html#","e":false,"i":"","n":"CNF","t":"CNF","d":"satify.model.cnf","k":"object","x":""}, -{"l":"satify/model/cnf/CNF$.html#printAsDSL-3da","e":false,"i":"extension (cnf: CNF)","n":"printAsDSL","t":"printAsDSL(flat: Boolean): String","d":"satify.model.cnf.CNF","k":"def","x":""}, -{"l":"satify/model/cnf/CNF$.html#printAsFormal-3da","e":false,"i":"extension (cnf: CNF)","n":"printAsFormal","t":"printAsFormal(flat: Boolean): String","d":"satify.model.cnf.CNF","k":"def","x":""}, +{"l":"satify/model/cnf/CNF$.html#asDSL-3da","e":false,"i":"extension (cnf: CNF)","n":"asDSL","t":"asDSL(flat: Boolean): String","d":"satify.model.cnf.CNF","k":"def","x":""}, +{"l":"satify/model/cnf/CNF$.html#asFormal-3da","e":false,"i":"extension (cnf: CNF)","n":"asFormal","t":"asFormal(flat: Boolean): String","d":"satify.model.cnf.CNF","k":"def","x":""}, {"l":"satify/model/errors.html#","e":false,"i":"","n":"satify.model.errors","t":"satify.model.errors","d":"","k":"package","x":""}, {"l":"satify/model/errors/Error.html#","e":false,"i":"","n":"Error","t":"Error(val description: String)","d":"satify.model.errors","k":"enum","x":""}, {"l":"satify/model/errors/Error$$InvalidInput.html#","e":false,"i":"","n":"InvalidInput","t":"InvalidInput() extends Error","d":"satify.model.errors.Error","k":"case","x":""}, @@ -128,8 +128,8 @@ pages = [{"l":"index.html#","e":false,"i":"","n":"satify","t":"satify","d":"","k {"l":"satify/model/expression/SymbolGeneration$$SymbolGenerator.html#prefix-0","e":false,"i":"","n":"prefix","t":"prefix: String","d":"satify.model.expression.SymbolGeneration.SymbolGenerator","k":"def","x":""}, {"l":"satify/model/expression/SymbolGeneration$$SymbolGenerator.html#reset-94c","e":false,"i":"","n":"reset","t":"reset(): Unit","d":"satify.model.expression.SymbolGeneration.SymbolGenerator","k":"def","x":""}, {"l":"satify/model/expression/Utils$.html#","e":false,"i":"","n":"Utils","t":"Utils","d":"satify.model.expression","k":"object","x":""}, -{"l":"satify/model/expression/Utils$.html#printAsDSL-d34","e":false,"i":"extension (exp: Expression)","n":"printAsDSL","t":"printAsDSL(flat: Boolean): String","d":"satify.model.expression.Utils","k":"def","x":""}, -{"l":"satify/model/expression/Utils$.html#printAsFormal-d34","e":false,"i":"extension (exp: Expression)","n":"printAsFormal","t":"printAsFormal(flat: Boolean): String","d":"satify.model.expression.Utils","k":"def","x":""}, +{"l":"satify/model/expression/Utils$.html#asDSL-d34","e":false,"i":"extension (exp: Expression)","n":"asDSL","t":"asDSL(flat: Boolean): String","d":"satify.model.expression.Utils","k":"def","x":""}, +{"l":"satify/model/expression/Utils$.html#asFormal-d34","e":false,"i":"extension (exp: Expression)","n":"asFormal","t":"asFormal(flat: Boolean): String","d":"satify.model.expression.Utils","k":"def","x":""}, {"l":"satify/model/problems.html#","e":false,"i":"","n":"satify.model.problems","t":"satify.model.problems","d":"","k":"package","x":""}, {"l":"satify/model/problems/GraphColoring.html#","e":false,"i":"","n":"GraphColoring","t":"GraphColoring(edges: List[(String, String)], nodes: List[String], colors: Int) extends Problem","d":"satify.model.problems","k":"class","x":""}, {"l":"satify/model/problems/GraphColoring.html#constraints-0","e":false,"i":"","n":"constraints","t":"constraints: Set[Expression]","d":"satify.model.problems.GraphColoring","k":"val","x":""}, diff --git a/doc/report/2-requirements.md b/doc/report/2-requirements.md index f6fab8b1..060fec9f 100644 --- a/doc/report/2-requirements.md +++ b/doc/report/2-requirements.md @@ -113,9 +113,10 @@ A problem is represented by a set of constraints which, composed together, form 3. ## Non-functional requirements 1. The system must be executable on the three main operating systems: Windows, Linux and MacOS. 2. The system has to be user-friendly, providing few and intuitive buttons, help section and flexible input. - 3. The system has to be secure, avoiding any kind of code injection through the input. - 4. // TODO: performance requirements and tests - 5. // TODO: questione estensibilità algoritmi + 3. The system has to be easily extensible with other algorithms for conversion and solving. + 4. The system has to be secure, avoiding any kind of code injection through the input. + 5. The system has to perform efficiently, completing satisfiability checks within acceptable + time limits and depending on the instance dimension conforming to the benchmarks. 4. ## Implementation requirements 1. The system must be implemented in Scala 3, using SBT as automation build tool and JDK 17. @@ -141,5 +142,7 @@ A problem is represented by a set of constraints which, composed together, form | [2.iii](#system-requirements) | [TseitinTest.scala](../../src/test/scala/satify/update/converters/tseitin/TseitinTest.scala) | | [2.iv](#system-requirements) | [DpllEnumerator.scala](../../src/test/scala/satify/update/solver/dpll/impl/DpllEnumeratorTest.scala)
[DpllFinder.scala](../../src/test/scala/satify/update/solver/dpll/impl/DpllFinderTest.scala) | | | | [2.ix](#system-requirements) | [problems package](../../src/test/scala/satify/problems) | +| [3.iv](#non-functional-requirements) | [DSL.feature](../../src/test/resources/features/DSL.feature) | +| [3.v](#non-functional-requirements) | [Tseitin Benchmarks](../../src/test/scala/satify/update/converters/tseitin/benchmark)
[DPLL Benchmarks](../../src/test/scala/satify/update/solver/dpll/benchmark) | [Previous](1-methodology.md) | [Next](3-architectural-design.md) diff --git a/doc/report/4-detailed-design.md b/doc/report/4-detailed-design.md index 7d4d9abc..7c75c2ea 100644 --- a/doc/report/4-detailed-design.md +++ b/doc/report/4-detailed-design.md @@ -4,13 +4,17 @@ ## Code organization +

+ packages diagram +

+ ## Architecture As described in the previous section, the architectural pattern used is the **Model-View-Update** (MVU). Moreover, the **Cake Pattern** has been introduced to improve the modeling of the dependencies. Some _trait_ has been designed to represent the components of the MVU pattern, which encapsulate within them some -_abstract type members_ related to Model, View and Update. +_abstract type members_ related to `Model`, `View` and `Update`.

Model-View-Update detailed diagram @@ -18,19 +22,18 @@ _abstract type members_ related to Model, View and Update. ## Model -Concretely, the **Model** will be a private implementation of the _trait_ **State**, which contains the following +Concretely, the **Model** is an implementation of the _trait_ **State**, which contains the following abstract types: ### Expression -Expression is represented through a simple _enumeration_ which contains all the possible types of expression: +Expression is represented through a _sum type_ which contains all the possible types of expression: -- **And**. It represents the logical And gate. Takes in input *left* and *right* parameters both of type Expression; -- **Or**. It represents the logical Or gate. Like the And Expression, it takes a *left* and *right* Expressions in - input; -- **Not**. It's the logical Not gate. In this case it takes in input another Expression; -- **Symbol**. It's the basic type of Expression, and can either represent an input variable by specifying its name or a - boolean constant by using a value of type **Bool**. +- `And`, it represents the logical And gate. It takes in input **left** and **right** parameters both of type + Expression. +- `Or`, it represents the logical Or gate. Like the `And`, it takes a **left** and **right** Expressions in input. +- `Not`, it's the logical Not gate. It takes in input another `Expression`. +- `Symbol`, represents an input variable by specifying its name, or a boolean constant by using boolean value. Because of its recursive structure, Expression is a tree data structure, where the inner nodes are either **And**, **Or** or **Not**, and each leaf is a **Symbol**. @@ -43,30 +46,31 @@ Because of its recursive structure, Expression is a tree data structure, where t

-The general Problem representation has been designed with a _trait_ **Problem**. +The general SAT problem representation has been designed with a _trait_ **Problem**. It is composed by: - A set of constraints that must be all satisfied in the solution. -- An expression, which is the reduction of the constraints through an And gate. +- An `Expression`, which is the reduction of the constraints using the `And` operator. -Each problem extends **Problem** using a __case class__, and adds the constraints needed to represent the specific +Each problem extends **Problem** using a _case class_, and adds the constraints needed to represent the specific problem. ### Solution ### CNF -CNF is a specific form of representing logical formulas as a *conjunction* of clauses, where each clause is a -*disjunction* -of literals (variables or their negations). For example: +`CNF` is the data structure representing logical formulas as a *conjunction* of clauses, +where each clause is a *disjunction* of literals (variables or their negations). + +For example: $$ (a \lor c) \land (a \lor \lnot d) $$ -CNF has been modeled a specific type of __Expression__ where: +It is a _sum type_ like `Expression`, but it has the following constraints: -- The **Or** gate cannot contain an **And** in either its *left* and *right* parameter; -- The **And** gate cannot contain an **And** in its *left* parameter; -- The **Not** gate can contain only a **Symbol** parameter; +- The `Or` gate cannot contain an `And` in either its **left** and **right** parameter. +- The `And` gate cannot contain an `And` in its **left** parameter. +- The `Not` gate can contain only a `Symbol` parameter. An _enumeration_ has been used for this type of entity. @@ -137,12 +141,11 @@ So, the best way to design it is decomposing the algorithm following the steps b connectives (AND, OR, NOT) following the transformations listed in the table below. | Operator | Circuit | Expression | Converted | - |----------|-------------------------|-----------------|-------------------------------------------------------------------------------| + |----------|-------------------------|-----------------|-------------------------------------------------------------------------------| | AND | ![](img/AndCircuit.svg) | $X = A \land B$ | $(\lnot A \lor \lnot B \lor X) \land (A \lor \lnot X) \land (B \lor \lnot X)$ | | OR | ![](img/OrCircuit.svg) | $X = A \lor B$ | $(A \lor B \lor \lnot X) \land (\lnot A \lor X) \land (\lnot B \lor X)$ | | NOT | ![](img/NotCircuit.svg) | $X = \lnot A$ | $(\lnot A \lor \lnot X) \land (A \lor X)$ | - 4. Combine the representations of the subformulas to obtain the CNF representation of the entire formula. The resulting formula is equi-satisfiable with the original formula, meaning they have the same set of satisfying diff --git a/doc/report/5-implementation.md b/doc/report/5-implementation.md index 3a4f9a7e..30cb25e6 100644 --- a/doc/report/5-implementation.md +++ b/doc/report/5-implementation.md @@ -124,22 +124,23 @@ Despite there aren't too many dependencies in MVU, I decided to use the Cake Pat flexibility. In particular, I made use of the _Self-Type Annotation_ and _Mixin_ mechanisms offered by Scala in order to -manage dependencies between pattern components at compile-time and to create an application instance in a simple and +manage dependencies between architecture components at compile-time and to create an application instance in a simple +and readable way. -`scala +```scala trait MVU extends ModelComponent with ViewComponent with UpdateComponent object Main extends App with MVU -` +``` ### Abstract Modelling -Initially I implemented the components making use of _Abstract Modelling_, +Initially, I implemented the components using _Abstract Modelling_, because at the start of the project I didn't know yet how `Model`, `View` and `Update` should have been concretely implemented. This approach permitted me to focus on high-level design, architecture testing -and to postpone the implementation details. +and to postpone implementation details. I adopted _Abstract Modelling_ approach also when I started to implement the `Model` entity. In fact, I knew that the latter had to be an immutable data structure, @@ -162,12 +163,6 @@ The use of the _extension methods_ allowed me to call methods and compose expres Using an Internal DSL, I obtained free and correct use of parenthesis and automatic error checking. -[//]: # (### Solver) - -[//]: # (One of the main entities is the `Solver`, it is implemented as a trait containing the `solve` method ) - -[//]: # (overloaded in order to perform also the conversion to CNF using the `Converter`, if the input is not in CNF.) - ## Alberto Paganelli Initially, I was involved in the analysis of the Tseitin transformation algorithm and its phases. diff --git a/doc/report/img/packages.svg b/doc/report/img/packages.svg new file mode 100644 index 00000000..2c2d2c86 --- /dev/null +++ b/doc/report/img/packages.svg @@ -0,0 +1,4 @@ + + + +
satify
satify
dsl
dsl
model
model
view
view
update
update
cnf
cnf
expression
expression
problems
problems
converters
converters
solver
solver
app
app
errors
errors
tseitin
tseitin
dpll
dpll
parser
parser
solver
solver
utils
utils
components
componentsText is not SVG - cannot display \ No newline at end of file diff --git a/doc/report/img/problem/problem.png b/doc/report/img/problem/problem.png deleted file mode 100644 index 9ba6d8c4..00000000 Binary files a/doc/report/img/problem/problem.png and /dev/null differ diff --git a/doc/report/img/problem/problem.svg b/doc/report/img/problem/problem.svg index b382b433..58e6f278 100644 --- a/doc/report/img/problem/problem.svg +++ b/doc/report/img/problem/problem.svg @@ -1,4 +1,4 @@ -<< trait >>Problemcontraints: Set[Expression]exp: ExpressiontoString(Assignment)<< case class >>GraphColoringvariables: Seq[Seq[Symbol]]nodeHasExactlyOneColor: ExpressionlinkedNodesHasDifferentColor: Expression<< case class >>NQueensvariables: Seq[Seq[Symbol]]atLeastOneQueen: ExpressionatMostOneQueen: ExpressiondiagConstr: Expression<< case class >>NurseSchedulingvariables: Seq[Seq[Seq[Symbol]]]oneNursePerShift: ExpressionatMostOneShiftPerDay: Expression minShiftsPerNurse: IntmaxShiftsPerNurse: IntminShiftsPerNurseConstraint: ExpressionmaxShiftsPerNurseConstraint: Expression \ No newline at end of file +<< trait >>Problemcontraints: Set[Expression]exp: ExpressiontoString(Assignment)<< case class >>GraphColoringvariables: Seq[Seq[Symbol]]nodeHasExactlyOneColor: ExpressionlinkedNodesHasDifferentColor: Expression<< case class >>NQueensvariables: Seq[Seq[Symbol]]atLeastOneQueenRowsColumns: ExpressionatMostOneQueenRowsColumns: ExpressionatMostOneQueenDiagonals: Expression<< case class >>NurseSchedulingvariables: Seq[Seq[Seq[Symbol]]]oneNursePerShift: ExpressionatMostOneShiftPerDay: ExpressionminShiftsPerNurseConstraint: ExpressionmaxShiftsPerNurseConstraint: Expression \ No newline at end of file diff --git a/src/main/scala/satify/model/cnf/CNF.scala b/src/main/scala/satify/model/cnf/CNF.scala index f41116c3..0bff0e1f 100644 --- a/src/main/scala/satify/model/cnf/CNF.scala +++ b/src/main/scala/satify/model/cnf/CNF.scala @@ -17,17 +17,17 @@ enum CNF: object CNF: extension (cnf: CNF) - def printAsDSL(flat: Boolean = false): String = + def asDSL(flat: Boolean = false): String = cnf match case Symbol(name) => name.toString case And(left, right) => - if flat then s"${left.printAsDSL(flat)} and ${right.printAsDSL(flat)}" - else s"${left.printAsDSL(flat)} and\n${right.printAsDSL(flat)}" - case Or(left, right) => s"${left.printAsDSL(flat)} or ${right.printAsDSL(flat)}" - case Not(branch) => s"not(${branch.printAsDSL(flat)})" + if flat then s"${left.asDSL(flat)} and ${right.asDSL(flat)}" + else s"${left.asDSL(flat)} and\n${right.asDSL(flat)}" + case Or(left, right) => s"${left.asDSL(flat)} or ${right.asDSL(flat)}" + case Not(branch) => s"not(${branch.asDSL(flat)})" - def printAsFormal(flat: Boolean = false): String = - var r = printAsDSL(flat) + def asFormal(flat: Boolean = false): String = + var r = asDSL(flat) .replace("and", "∧") .replace("or", "∨") .replace("not", "¬") diff --git a/src/main/scala/satify/model/expression/Utils.scala b/src/main/scala/satify/model/expression/Utils.scala index 87292b05..3f169aed 100644 --- a/src/main/scala/satify/model/expression/Utils.scala +++ b/src/main/scala/satify/model/expression/Utils.scala @@ -5,17 +5,17 @@ import satify.model.expression.Expression.{And, Not, Or, Symbol} object Utils: extension (exp: Expression) - def printAsDSL(flat: Boolean = false): String = + def asDSL(flat: Boolean = false): String = exp match case Symbol(value) => value case And(left, right) => - if flat then s"(${left.printAsDSL(flat)} and ${right.printAsDSL(flat)})" - else s"(${left.printAsDSL(flat)} and\n${right.printAsDSL(flat)})" - case Or(left, right) => s"(${left.printAsDSL(flat)} or ${right.printAsDSL(flat)})" - case Not(branch) => s"not(${branch.printAsDSL(flat)})" + if flat then s"(${left.asDSL(flat)} and ${right.asDSL(flat)})" + else s"(${left.asDSL(flat)} and\n${right.asDSL(flat)})" + case Or(left, right) => s"(${left.asDSL(flat)} or ${right.asDSL(flat)})" + case Not(branch) => s"not(${branch.asDSL(flat)})" - def printAsFormal(flat: Boolean = false): String = - var r = printAsDSL(flat) + def asFormal(flat: Boolean = false): String = + var r = asDSL(flat) .replace("and", "∧") .replace("or", "∨") .replace("not", "¬") diff --git a/src/main/scala/satify/model/problems/GraphColoring.scala b/src/main/scala/satify/model/problems/GraphColoring.scala index eb0f20ef..b2d88ef2 100644 --- a/src/main/scala/satify/model/problems/GraphColoring.scala +++ b/src/main/scala/satify/model/problems/GraphColoring.scala @@ -1,4 +1,5 @@ package satify.model.problems + import satify.model.Assignment import satify.model.expression.Expression import satify.model.expression.Expression.* diff --git a/src/main/scala/satify/model/problems/NQueens.scala b/src/main/scala/satify/model/problems/NQueens.scala index 6c1fd08f..9ace2cbe 100644 --- a/src/main/scala/satify/model/problems/NQueens.scala +++ b/src/main/scala/satify/model/problems/NQueens.scala @@ -21,21 +21,21 @@ case class NQueens(n: Int) extends Problem: yield Symbol(s"x_${i}_$j") /** At least one queen on each row and column */ - private val atLeastOneQueen: Expression = + private val atLeastOneQueenRowsColumns: Expression = val constraint = for i <- 0 until n yield And(atLeastOne(variables(i): _*), atLeastOne(variables.map(row => row(i)): _*)) constraint.reduceLeft(And(_, _)) /** At most one queen on each row and column */ - private val atMostOneQueen: Expression = + private val atMostOneQueenRowsColumns: Expression = val atMostConstraints = for i <- 0 until n yield And(atMostOne(variables(i): _*), atMostOne(variables.map(row => row(i)): _*)) atMostConstraints.reduceLeft(And(_, _)) /** At most one queen on each diagonal */ - private def diagConstr: Expression = + private def atMostOneQueenDiagonals: Expression = val clauses = for i <- 0 until (n - 1) yield @@ -57,8 +57,8 @@ case class NQueens(n: Int) extends Problem: clauses.reduceLeft(And(_, _)) override val constraints: Set[Expression] = - if n > 1 then Set(atLeastOneQueen, atMostOneQueen, diagConstr) - else Set(atLeastOneQueen, atMostOneQueen) + if n > 1 then Set(atLeastOneQueenRowsColumns, atMostOneQueenRowsColumns, atMostOneQueenDiagonals) + else Set(atLeastOneQueenRowsColumns, atMostOneQueenRowsColumns) override def toString(assignment: Assignment): String = @tailrec diff --git a/src/main/scala/satify/model/problems/NurseScheduling.scala b/src/main/scala/satify/model/problems/NurseScheduling.scala index 276dfb4d..5d99cc4a 100644 --- a/src/main/scala/satify/model/problems/NurseScheduling.scala +++ b/src/main/scala/satify/model/problems/NurseScheduling.scala @@ -1,4 +1,5 @@ package satify.model.problems + import satify.model.Assignment import satify.model.expression.Expression import satify.model.expression.Expression.* diff --git a/src/main/scala/satify/model/problems/Problem.scala b/src/main/scala/satify/model/problems/Problem.scala index 6bf2fd87..75e7c7c0 100644 --- a/src/main/scala/satify/model/problems/Problem.scala +++ b/src/main/scala/satify/model/problems/Problem.scala @@ -4,8 +4,6 @@ import satify.model.Assignment import satify.model.expression.Expression import satify.model.expression.Expression.And -import scala.swing.Component - /** Entity representing a SAT problem. */ trait Problem: diff --git a/src/main/scala/satify/update/Update.scala b/src/main/scala/satify/update/Update.scala index 2d5033ce..acaacc45 100644 --- a/src/main/scala/satify/update/Update.scala +++ b/src/main/scala/satify/update/Update.scala @@ -125,7 +125,7 @@ object Update: val lines = s.getLines.toSeq s.close() val cnf: CNF = parse(lines).getOrElse(Symbol("NO CNF")) - val input = cnf.printAsDSL() + val input = cnf.asDSL() State(input, cnf) safeUpdate(update) diff --git a/src/main/scala/satify/view/View.scala b/src/main/scala/satify/view/View.scala index 534f647b..12f16103 100644 --- a/src/main/scala/satify/view/View.scala +++ b/src/main/scala/satify/view/View.scala @@ -63,7 +63,7 @@ object View: } val fp: BoxPanel = new BoxPanel(Orientation.Vertical): name = cnfOutputDialogName - contents += new ScrollPane(createOutputTextArea(cnf.get.printAsFormal(), 30, 35)) + contents += new ScrollPane(createOutputTextArea(cnf.get.asFormal(), 30, 35)) contents += new FlowPanel(): contents += exportButton contents += new FlowPanel(): diff --git a/src/test/resources/features/DSL.feature b/src/test/resources/features/DSL.feature index 97307f49..49d40652 100644 --- a/src/test/resources/features/DSL.feature +++ b/src/test/resources/features/DSL.feature @@ -19,3 +19,8 @@ Feature: Inserting expression through DSL Given the input "and or not" When it is reflected to scala compiler Then I should obtain an IllegalArgumentException + + Scenario: I cannot make code injection + Given the input "a and b; println(\"hello\")" + When it is reflected to scala compiler + Then I should obtain an IllegalArgumentException diff --git a/src/test/scala/satify/features/ConversionSteps.scala b/src/test/scala/satify/features/ConversionSteps.scala index bdad4f35..732bf801 100644 --- a/src/test/scala/satify/features/ConversionSteps.scala +++ b/src/test/scala/satify/features/ConversionSteps.scala @@ -20,5 +20,5 @@ object ConversionSteps extends ScalaDsl with EN: } Then("I should obtain the CNF {string}") { (expected: String) => - cnf.get.printAsDSL(true) shouldBe expected + cnf.get.asDSL(true) shouldBe expected } diff --git a/src/test/scala/satify/features/DSLSteps.scala b/src/test/scala/satify/features/DSLSteps.scala index 811ae9c4..d802ee75 100644 --- a/src/test/scala/satify/features/DSLSteps.scala +++ b/src/test/scala/satify/features/DSLSteps.scala @@ -20,7 +20,7 @@ object DSLSteps extends ScalaDsl with EN: } Then("I should obtain the expression {string}") { (expected: String) => - expression.get.printAsDSL(true) shouldBe expected + expression.get.asDSL(true) shouldBe expected } Then("I should obtain an IllegalArgumentException") { error shouldBe a[IllegalArgumentException] diff --git a/src/test/scala/satify/model/cnf/CNFOutputTest.scala b/src/test/scala/satify/model/cnf/CNFOutputTest.scala index 1fa7f765..a7ce221e 100644 --- a/src/test/scala/satify/model/cnf/CNFOutputTest.scala +++ b/src/test/scala/satify/model/cnf/CNFOutputTest.scala @@ -8,23 +8,23 @@ class CNFOutputTest extends AnyFlatSpec with Matchers: import satify.model.cnf.CNF.* "The cnf symbol a" should "be printed as a in formal way" in { - Symbol("a").printAsFormal(true) shouldBe "a" - Symbol("a").printAsFormal() shouldBe "a" + Symbol("a").asFormal(true) shouldBe "a" + Symbol("a").asFormal() shouldBe "a" } "The cnf exp ((a ∨ ¬b) ∧ c)" should "be printed in the formal way and according to the output flat mode" in { val cnfExp: CNF = And(Or(Symbol("a"), Not(Symbol("b"))), Symbol("c")) - cnfExp.printAsFormal(true) shouldBe "a ∨ ¬(b) ∧ c" - cnfExp.printAsFormal() shouldBe "a ∨ ¬(b) ∧\nc" + cnfExp.asFormal(true) shouldBe "a ∨ ¬(b) ∧ c" + cnfExp.asFormal() shouldBe "a ∨ ¬(b) ∧\nc" } "The only symbol a" should "be printed as a in DSL" in { - Symbol("a").printAsDSL(true) shouldBe "a" - Symbol("a").printAsDSL() shouldBe "a" + Symbol("a").asDSL(true) shouldBe "a" + Symbol("a").asDSL() shouldBe "a" } "The exp ((a ∨ ¬b) ∧ c)" should "be printed in the DSL format according to the output flat mode" in { val exp: CNF = And(Or(Symbol("a"), Not(Symbol("b"))), Symbol("c")) - exp.printAsDSL(true) shouldBe "a or not(b) and c" - exp.printAsDSL() shouldBe "a or not(b) and\nc" + exp.asDSL(true) shouldBe "a or not(b) and c" + exp.asDSL() shouldBe "a or not(b) and\nc" } diff --git a/src/test/scala/satify/model/expression/ExpressionOutputTest.scala b/src/test/scala/satify/model/expression/ExpressionOutputTest.scala index 9676802f..884637c7 100644 --- a/src/test/scala/satify/model/expression/ExpressionOutputTest.scala +++ b/src/test/scala/satify/model/expression/ExpressionOutputTest.scala @@ -9,8 +9,8 @@ class ExpressionOutputTest extends AnyFlatSpec with Matchers: "The only symbol a" should "be printed as a in formal way" in { val exp: Expression = Symbol("a") - val fRes: String = exp.printAsFormal(true) - val nfRes: String = exp.printAsFormal(false) + val fRes: String = exp.asFormal(true) + val nfRes: String = exp.asFormal(false) val expected = "a" List(fRes, nfRes) shouldBe List(expected, expected) } @@ -18,17 +18,17 @@ class ExpressionOutputTest extends AnyFlatSpec with Matchers: "The exp ((a ∧ ¬b) ∨ c)" should "be printed in the formal way according to the output flat mode" in { val exp: Expression = Or(And(Symbol("a"), Not(Symbol("b"))), Symbol("c")) - val fRes: String = exp.printAsFormal(true) + val fRes: String = exp.asFormal(true) val fExp = "((a ∧ ¬(b)) ∨ c)" - val nfRes: String = exp.printAsFormal(false) + val nfRes: String = exp.asFormal(false) val nfExp = "((a ∧\n¬(b)) ∨ c)" List(fRes, nfRes) shouldBe List(fExp, nfExp) } "The only symbol a" should "be printed as a in DSL" in { val exp: Expression = Symbol("a") - val fRes: String = exp.printAsDSL(true) - val nfRes: String = exp.printAsDSL(false) + val fRes: String = exp.asDSL(true) + val nfRes: String = exp.asDSL(false) val expected = "a" List(fRes, nfRes) shouldBe List(expected, expected) } @@ -36,9 +36,9 @@ class ExpressionOutputTest extends AnyFlatSpec with Matchers: "The exp ((a ∧ ¬b) ∨ c)" should "be printed in the DSL format according to the output flat mode" in { val exp: Expression = Or(And(Symbol("a"), Not(Symbol("b"))), Symbol("c")) - val fRes: String = exp.printAsDSL(true) + val fRes: String = exp.asDSL(true) val fExp = "((a and not(b)) or c)" - val nfRes: String = exp.printAsDSL(false) + val nfRes: String = exp.asDSL(false) val nfExp = "((a and\nnot(b)) or c)" List(fRes, nfRes) shouldBe List(fExp, nfExp) } diff --git a/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionMemoryBenchmark.scala b/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionMemoryBenchmark.scala index 433e01a0..b8ce89e7 100644 --- a/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionMemoryBenchmark.scala +++ b/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionMemoryBenchmark.scala @@ -1,18 +1,20 @@ package satify.update.converters.tseitin.benchmark import org.scalameter.api.* -import satify.model.problems.{NQueens, GraphColoring, NurseScheduling} +import satify.model.problems.{GraphColoring, NQueens, NurseScheduling} import satify.update.converters.Converter -import satify.update.converters.ConverterType.Tseitin object ConversionMemoryBenchmark extends Bench.OfflineReport: + + import satify.update.converters.ConverterType.Tseitin + override def measurer = new Measurer.MemoryFootprint performance of "N-Queens conversion memory" in { val sizes: Gen[Int] = Gen.range("size")(2, 10, 1) measure method "N-Queens Conversion" in { using(sizes) in { size => - val cnf = Converter(Tseitin).convert(NQueens(size).exp, false) + Converter(Tseitin).convert(NQueens(size).exp, false) } } } @@ -24,7 +26,7 @@ object ConversionMemoryBenchmark extends Bench.OfflineReport: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Graph-Coloring Conversion" in { using(sizes) in { size => - val cnf = Converter(Tseitin).convert(GraphColoring(edges, nodes, colors).exp, false) + Converter(Tseitin).convert(GraphColoring(edges, nodes, colors).exp, false) } } } @@ -36,7 +38,7 @@ object ConversionMemoryBenchmark extends Bench.OfflineReport: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Nurse-Scheduling Conversion" in { using(sizes) in { size => - val cnf = Converter(Tseitin).convert(NurseScheduling(nurses, days, shifts).exp, false) + Converter(Tseitin).convert(NurseScheduling(nurses, days, shifts).exp, false) } } } diff --git a/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionProblemBenchmark.scala b/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionProblemBenchmark.scala index bc0f0f30..96e9cc7b 100644 --- a/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionProblemBenchmark.scala +++ b/src/test/scala/satify/update/converters/tseitin/benchmark/ConversionProblemBenchmark.scala @@ -3,16 +3,17 @@ package satify.update.converters.tseitin.benchmark import org.scalameter.api.* import satify.model.problems.{GraphColoring, NQueens, NurseScheduling} import satify.update.converters.Converter -import satify.update.converters.ConverterType.Tseitin object ConversionProblemBenchmark extends Bench.OfflineReport: + import satify.update.converters.ConverterType.Tseitin performance of "N-Queens conversion time" in { val sizes: Gen[Int] = Gen.range("size")(1, 10, 1) measure method "N-Queens Conversion" in { using(sizes) in { size => - val cnf = Converter(Tseitin).convert(NQueens(size).exp, false) + println(reports.resultDir) + Converter(Tseitin).convert(NQueens(size).exp, false) } } } @@ -24,7 +25,7 @@ object ConversionProblemBenchmark extends Bench.OfflineReport: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Graph-Coloring Conversion" in { using(sizes) in { size => - val cnf = Converter(Tseitin).convert(GraphColoring(edges, nodes, colors).exp, false) + Converter(Tseitin).convert(GraphColoring(edges, nodes, colors).exp, false) } } } @@ -36,7 +37,7 @@ object ConversionProblemBenchmark extends Bench.OfflineReport: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Nurse-Scheduling Conversion" in { using(sizes) in { size => - val cnf = Converter(Tseitin).convert(NurseScheduling(nurses, days, shifts).exp, false) + Converter(Tseitin).convert(NurseScheduling(nurses, days, shifts).exp, false) } } } diff --git a/src/test/scala/satify/update/solver/dpll/benchmark/SolvingMemoryBenchmark.scala b/src/test/scala/satify/update/solver/dpll/benchmark/SolvingMemoryBenchmark.scala index 83f43a6c..997c1b66 100644 --- a/src/test/scala/satify/update/solver/dpll/benchmark/SolvingMemoryBenchmark.scala +++ b/src/test/scala/satify/update/solver/dpll/benchmark/SolvingMemoryBenchmark.scala @@ -1,19 +1,21 @@ package satify.update.solver.dpll.benchmark import org.scalameter.api.* -import satify.model.problems.{NQueens, NurseScheduling, GraphColoring} +import satify.model.problems.{GraphColoring, NQueens, NurseScheduling} import satify.update.solver.Solver -import satify.update.solver.SolverType.* -import satify.update.converters.ConverterType.Tseitin object SolvingMemoryBenchmark extends Bench.OfflineReport: + + import satify.update.converters.ConverterType.Tseitin + import satify.update.solver.SolverType.DPLL + override def measurer = new Measurer.MemoryFootprint performance of "N-Queens solving memory" in { val sizes: Gen[Int] = Gen.range("size")(2, 5, 1) measure method "N-Queens Solving" in { using(sizes) in { size => - val s = Solver(DPLL, Tseitin).solveAll(NQueens(size).exp, false) + Solver(DPLL, Tseitin).solveAll(NQueens(size).exp, false) } } } @@ -25,7 +27,7 @@ object SolvingMemoryBenchmark extends Bench.OfflineReport: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Graph-Coloring Solving" in { using(sizes) in { size => - val s = Solver(DPLL, Tseitin).solveAll(GraphColoring(edges, nodes, colors).exp, false) + Solver(DPLL, Tseitin).solveAll(GraphColoring(edges, nodes, colors).exp, false) } } } @@ -37,7 +39,7 @@ object SolvingMemoryBenchmark extends Bench.OfflineReport: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Nurse-Scheduling Solving" in { using(sizes) in { size => - val s = Solver(DPLL, Tseitin).solveAll(NurseScheduling(nurses, days, shifts).exp, false) + Solver(DPLL, Tseitin).solveAll(NurseScheduling(nurses, days, shifts).exp, false) } } } diff --git a/src/test/scala/satify/update/solver/dpll/benchmark/SolvingProblemBenchmark.scala b/src/test/scala/satify/update/solver/dpll/benchmark/SolvingProblemBenchmark.scala index 0aab76e8..8118777c 100644 --- a/src/test/scala/satify/update/solver/dpll/benchmark/SolvingProblemBenchmark.scala +++ b/src/test/scala/satify/update/solver/dpll/benchmark/SolvingProblemBenchmark.scala @@ -3,16 +3,17 @@ package satify.update.solver.dpll.benchmark import org.scalameter.api.* import satify.model.problems.{GraphColoring, NQueens, NurseScheduling} import satify.update.solver.Solver -import satify.update.solver.SolverType.* object SolvingProblemBenchmark extends Bench.LocalTime: + import satify.update.converters.ConverterType.Tseitin + import satify.update.solver.SolverType.DPLL performance of "N-Queens solving time" in { val sizes: Gen[Int] = Gen.range("size")(2, 5, 1) measure method "N-Queens Solving" in { using(sizes) in { size => - val s = Solver(DPLL, Tseitin).solveAll(NQueens(size).exp, false) + Solver(DPLL, Tseitin).solveAll(NQueens(size).exp, false) } } } @@ -24,7 +25,7 @@ object SolvingProblemBenchmark extends Bench.LocalTime: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Graph-Coloring Solving" in { using(sizes) in { size => - val s = Solver(DPLL, Tseitin).solveAll(GraphColoring(edges, nodes, colors).exp, false) + Solver(DPLL, Tseitin).solveAll(GraphColoring(edges, nodes, colors).exp, false) } } } @@ -36,7 +37,7 @@ object SolvingProblemBenchmark extends Bench.LocalTime: val sizes: Gen[Int] = Gen.range("size")(0, 1, 1) measure method "Nurse-Scheduling Solving" in { using(sizes) in { size => - val s = Solver(DPLL, Tseitin).solveAll(NurseScheduling(nurses, days, shifts).exp, false) + Solver(DPLL, Tseitin).solveAll(NurseScheduling(nurses, days, shifts).exp, false) } } }