Release/0.2.0

.github/workflows/ci.yml

@@ -1,8 +1,8 @@
-name: Scala CI
+name: Satify Build, Format and Coverage
 
 on:
   push:
-    branches: [ "main", "develop", "feature/**", "release/**", "hotfix/**" ]
+    branches: [ '**' ]
   pull_request:
     branches: [ "main", "develop", "release/**" ]
 
@@ -35,7 +35,7 @@ jobs:
       - name: Run tests
         run: sbt test
 
-  formatting:
+  format:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
@@ -45,5 +45,18 @@ jobs:
           java-version: '17'
           distribution: 'temurin'
           cache: 'sbt'
-      - name: Check scalafmt formatting
+      - name: Check scalafmt format
         run: sbt scalafmtCheckAll
+
+  coverage:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up JDK 17
+        uses: actions/setup-java@v3
+        with:
+          java-version: '17'
+          distribution: 'temurin'
+          cache: 'sbt'
+      - name: Run tests with coverage
+        run: sbt jacoco

.github/workflows/release.yml

@@ -0,0 +1,36 @@
+name: Create Release
+
+on:
+  pull_request:
+    types:
+      - closed
+    branches:
+      - main
+
+permissions:
+  contents: write
+
+jobs:
+  release:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up JDK 17
+        uses: actions/setup-java@v3
+        with:
+          java-version: '17'
+          distribution: 'temurin'
+          cache: 'sbt'
+
+      - name: Create Jar Asset
+        run: sbt assembly
+
+      - name: Create Release
+        uses: "marvinpinto/action-automatic-releases@latest"
+        with:
+          repo_token: "${{ secrets.GITHUB_TOKEN }}"
+          automatic_release_tag: "latest"
+          title: "Sprint 3 Release"
+          prerelease: true
+          files: |
+            target/scala-3.3.0/satify.jar

CHANGELOG.md

@@ -0,0 +1,32 @@
+# [0.1.0](https://github.com/Mala1180/PPS-22-satify/compare/47a5b9fb00c7757cf5a6520fe326cc164dfefd38...v0.1.0) (2023-08-14)
+
+
+### Bug Fixes
+
+* again scalafmt ([3fd1173](https://github.com/Mala1180/PPS-22-satify/commit/3fd1173279691211cc1488ec2f02a74873b43491))
+* DPLL test ([53831b1](https://github.com/Mala1180/PPS-22-satify/commit/53831b15fb769ba8d39a625f2dac9d75a5945d67))
+* DPLL tests ([12884ab](https://github.com/Mala1180/PPS-22-satify/commit/12884ab36bcb1309c1cabfa00a23af2eafde0b40))
+* initial implementation of Tseiting algorithm in particular substitution of variables: replace method ([bc93d18](https://github.com/Mala1180/PPS-22-satify/commit/bc93d189bec938fea862dfdf8dd785b530dcefa6))
+* reformat code ([742826a](https://github.com/Mala1180/PPS-22-satify/commit/742826a4611352311be2d749b576e78bd5fea0d2))
+* removed ._2 notation, chenged doc for archunit and some gramatical errors, first print of CNF formula obtained ([9b0c45a](https://github.com/Mala1180/PPS-22-satify/commit/9b0c45aad56d8e9afe44b147a4ba7627d48d278c))
+* removed ambiguous symbol T from nested functions in Expression and TseitinTransformation method utils ([f97a5e2](https://github.com/Mala1180/PPS-22-satify/commit/f97a5e209ab0607002bf035b004b0ebc5d70d528))
+* ReplaceTest ([668b5cd](https://github.com/Mala1180/PPS-22-satify/commit/668b5cdc1acdb0f581a09fb03ef38cb4ae66a8ba))
+* simplifyClosestAnd, chore (green): exhaustive search w/CNF simplification ([430a01e](https://github.com/Mala1180/PPS-22-satify/commit/430a01e9f3f96eba89db7ef509979304c8a3c33e))
+* simplifyUpperMostOr propagation through the Or root ([4ca2990](https://github.com/Mala1180/PPS-22-satify/commit/4ca299037752ad8ad196352bd84d7ca95ee93e4c))
+* tests, undo CNF modifications, chore: add scaladoc in dpllcnfutils ([89df6f4](https://github.com/Mala1180/PPS-22-satify/commit/89df6f4b0a8c0c655965f43af547e3566925f181))
+* transformation method and transformations tests ([d8e83ac](https://github.com/Mala1180/PPS-22-satify/commit/d8e83ac96e8476b0feb7f84839f68f2a4292e24e))
+* typo in dt's search test ([44f1711](https://github.com/Mala1180/PPS-22-satify/commit/44f1711e910ace303ab1858e0703db40c379a9b9))
+
+
+### Features
+
+* add DSL with simple operators ([88b4d50](https://github.com/Mala1180/PPS-22-satify/commit/88b4d50034c011b5d9167c3269c8fac0b8190a95))
+* added scalafmt.conf ([47a5b9f](https://github.com/Mala1180/PPS-22-satify/commit/47a5b9fb00c7757cf5a6520fe326cc164dfefd38))
+* added scalatest and file to test it ([53efa07](https://github.com/Mala1180/PPS-22-satify/commit/53efa072e1716f40862f5e980154a578c0133e4f))
+* added Solver entity and cnf converters ([664b4d6](https://github.com/Mala1180/PPS-22-satify/commit/664b4d603a7d4d71b08606bf7e0825aa9f2a8985))
+* finish second backlog, print cnf output ([61bc583](https://github.com/Mala1180/PPS-22-satify/commit/61bc5833512c34d8b7ae9307ad1750bfbb54d1d9))
+* setup architecture mvu with cake pattern ([ae10b4d](https://github.com/Mala1180/PPS-22-satify/commit/ae10b4d2687bf2ccacedba3c1c7c5f14251434c2))
+* setup GUI, add logo ([8eb13d6](https://github.com/Mala1180/PPS-22-satify/commit/8eb13d66192b930361713d18f675cb4c3db1583e))
+
+
+

README.md

@@ -6,42 +6,64 @@
 
 Satify is a pure functional SAT solver written in Scala.
 
-It wants to be **immutable**, **declarative** and **idiomatic** 
-still using the OOP flexibility thanks to syntactic sugar power offered by Scala. 
+It wants to be **immutable**, **declarative** and **idiomatic**
+still using the OOP flexibility thanks to syntactic sugar power offered by Scala 3.
 
 Satify implements two principal algorithms:
+
 - Tseitin transformation to convert a boolean formula in CNF (Conjunctive Normal Form).
 - DPLL (Davis–Putnam–Logemann–Loveland) to solve the satisfiability problem.
 
 Satify can simply take in input a set of clauses and say if it is satisfiable or not.
-This can be done using both math-like and more verbose human-like DSLs.
+This can be done using a versatile DSL providing both math-like and human-like styles.
+
 Moreover, Satify provides a set of problems (N-Queens, Coloring Graph, Nurse Scheduling) to test the solver.
 It will try also to give an instance of the problem satisfiable if it exists.
 
 ## Requirements
+
 To correctly run Satify, you need at least these versions of the following dependencies:
+
 - Scala 3.3.0 (currently LTS)
 - SBT 1.9.1
 - Java 17 (currently LTS)
 
 ## Usage
-To run Satify:
+
+### Downloading the jar
+
+You can download the `jar` of the application in the
+[release](https://github.com/Mala1180/PPS-22-satify/releases) page.
+
+To execute it, run:
+
+```bash
+java -jar path/to/downloaded/jar
+```
+
+### Using sbt
+
+If you have the project locally, you can use `sbt` to run the application:
+
 ```bash
 sbt run
 ```
-To run tests:
+
+Or to run tests:
+
 ```bash
 sbt test
 ```
 
-## Contributions
-If you want to contribute to Satify, you can fork the repository and open a pull request.
-The contributions must follow some constraints: 
-- Attention to code style and quality.
-- Don't use mutable data structures (if it's not strictly necessary).
-- Introduce only tested code.
+---
+You can also generate a new jar (it will be located in `target/scala-3.3.0/` directory):
+
+```bash
+sbt assembly
+```
 
 ## Authors
+
 - Luca Fabri ([w-disaster](https://github.com/w-disaster))
 - Mattia Matteini ([Mala1180](https://github.com/Mala1180))
 - Alberto Paganelli ([paga16-hash](https://github.com/paga16-hash))

build.sbt

@@ -3,6 +3,8 @@ ThisBuild / version := "0.1.0-SNAPSHOT"
 val languageVersion = "3.3.0"
 ThisBuild / scalaVersion := languageVersion
 
+Test / fork := true
+
 val scalaTest = "org.scalatest" %% "scalatest" % "3.2.16" % Test
 val archUnit = "com.tngtech.archunit" % "archunit" % "1.0.0" % Test
 val scalaSwing = "org.scala-lang.modules" %% "scala-swing" % "3.0.0"
@@ -13,5 +15,16 @@ val cucumber = "io.cucumber" %% "cucumber-scala" % "8.14.1" % Test
 lazy val root = (project in file("."))
   .settings(
     name := "satify",
-    libraryDependencies ++= Seq(scalaTest, archUnit, slf4jSimpleLog, scalaSwing, scalaCompiler, cucumber)
+    libraryDependencies ++= Seq(scalaTest, archUnit, slf4jSimpleLog, scalaSwing, scalaCompiler, cucumber),
+    assembly / assemblyJarName := "satify.jar"
+  )
+
+jacocoReportSettings := JacocoReportSettings()
+  .withTitle("Jacoco Satify Coverage Report")
+  .withThresholds(
+    JacocoThresholds(
+      branch = 40,
+      line = 70)
   )
+  .withFormats(JacocoReportFormats.ScalaHTML)
+jacocoExcludes := Seq("*view*", "*update.Message*", "*Main*")

doc/process/2-product-backlog.md

@@ -127,9 +127,9 @@ _No remaining tasks from the previous sprint._
 
 The goals of this sprint are:
 
-- Termination of Tseitin transformation
-- Providing a basic DSL
-- Proceeding with the implementation of the DPLL algorithm
+- Terminate Tseitin transformation
+- Provide a basic DSL
+- Proceed with the implementation of the DPLL algorithm
 
 There will be the first release of the project permitting to take in input an expression through DSL and to apply the
 Tseitin transformation (CNF conversion).