Merge pull request #145 from Mala1180/feature/doc-benchmark-and-update

Feature/doc-benchmark-and-update

doc/api/satify/model/cnf/CNF$.html

@@ -196,20 +196,20 @@ <h4 class="groupHeader h200">Extensions</h4>
         </div>
         <div>
          <span class="groupHeader"><span t="k">extension </span>(cnf: <a href="CNF.html" t="t">CNF</a>)(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">cnf</span>: <a href="CNF.html" t="t">CNF</a>)</span>
-         <div class="documentableElement" id="printAsDSL-3da">
+         <div class="documentableElement" id="asDSL-3da">
           <div class="documentableElement-expander">
            <div class="header monospace mono-medium">
             <div class="signature">
-             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#printAsDSL-3da" t="n" class="documentableName ">printAsDSL</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
+             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#asDSL-3da" t="n" class="documentableName ">asDSL</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
             </div>
            </div>
           </div>
          </div>
-         <div class="documentableElement" id="printAsFormal-3da">
+         <div class="documentableElement" id="asFormal-3da">
           <div class="documentableElement-expander">
            <div class="header monospace mono-medium">
             <div class="signature">
-             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#printAsFormal-3da" t="n" class="documentableName ">printAsFormal</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
+             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#asFormal-3da" t="n" class="documentableName ">asFormal</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
             </div>
            </div>
           </div>

doc/api/satify/model/cnf/CNF.html

@@ -161,12 +161,12 @@ <h3 data-togglable="Value members" class="h400">Value members</h3>
          <button class="icon-button show-content expand"></button>
          <h4 class="groupHeader h200">Concrete methods</h4>
         </div>
-        <div class="documentableElement" id="printAsDSL-3da" data-f-extension="from CNF">
+        <div class="documentableElement" id="asDSL-3da" data-f-extension="from CNF">
          <div class="documentableElement-expander">
           <button class="icon-button ar show-content"></button>
           <div class="header monospace mono-medium">
            <div class="signature">
-            <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#printAsDSL-3da" t="n" class="documentableName ">printAsDSL</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
+            <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#asDSL-3da" t="n" class="documentableName ">asDSL</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
            </div>
           </div>
          </div>
@@ -180,12 +180,12 @@ <h4 class="groupHeader h200">Concrete methods</h4>
           </div>
          </div>
         </div>
-        <div class="documentableElement" id="printAsFormal-3da" data-f-extension="from CNF">
+        <div class="documentableElement" id="asFormal-3da" data-f-extension="from CNF">
          <div class="documentableElement-expander">
           <button class="icon-button ar show-content"></button>
           <div class="header monospace mono-medium">
            <div class="signature">
-            <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#printAsFormal-3da" t="n" class="documentableName ">printAsFormal</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
+            <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="CNF$.html#asFormal-3da" t="n" class="documentableName ">asFormal</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
            </div>
           </div>
          </div>

doc/api/satify/model/expression/Utils$.html

@@ -90,20 +90,20 @@ <h4 class="groupHeader h200">Extensions</h4>
         </div>
         <div>
          <span class="groupHeader"><span t="k">extension </span>(exp: <a href="Expression.html" t="t">Expression</a>)(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">exp</span>: <a href="Expression.html" t="t">Expression</a>)</span>
-         <div class="documentableElement" id="printAsDSL-d34">
+         <div class="documentableElement" id="asDSL-d34">
           <div class="documentableElement-expander">
            <div class="header monospace mono-medium">
             <div class="signature">
-             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="Utils$.html#printAsDSL-d34" t="n" class="documentableName ">printAsDSL</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
+             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="Utils$.html#asDSL-d34" t="n" class="documentableName ">asDSL</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
             </div>
            </div>
           </div>
          </div>
-         <div class="documentableElement" id="printAsFormal-d34">
+         <div class="documentableElement" id="asFormal-d34">
           <div class="documentableElement-expander">
            <div class="header monospace mono-medium">
             <div class="signature">
-             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="Utils$.html#printAsFormal-d34" t="n" class="documentableName ">printAsFormal</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
+             <span class="modifiers"></span><span class="kind"><span t="k">def </span></span><a href="Utils$.html#asFormal-d34" t="n" class="documentableName ">asFormal</a>(<span t="k"></span><span t="k"></span><span data-unresolved-link="" t="n">flat</span>: <span data-unresolved-link="" t="t">Boolean</span>): <span data-unresolved-link="" t="t">String</span>
             </div>
            </div>
           </div>

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) <br/> [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) <br/>  [DPLL Benchmarks](../../src/test/scala/satify/update/solver/dpll/benchmark)                                         |
 
 [Previous](1-methodology.md) | [Next](3-architectural-design.md)

doc/report/4-detailed-design.md

@@ -4,33 +4,36 @@
 
 ## Code organization
 
+<p align=center>
+  <img src="img/packages.svg" alt="packages diagram">
+</p>
+
 ## 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`.
 
 <p align=center>
   <img src="img/mvu-detailed.svg" alt=" Model-View-Update detailed diagram">
 </p>
 
 ## 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
 </p>
 
 
-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