Feature/tseitin-little-fix

src/main/scala/satify/model/dpll/PartialAssignment.scala

@@ -6,7 +6,7 @@ import satify.model.cnf.CNF.*
 import satify.model.dpll.*
 import satify.model.dpll.DecisionTree.{Branch, Leaf}
 import satify.model.dpll.OrderedList.list
-import satify.model.expression.SymbolGeneration.{encodingVarPrefix, tseitinVarPrefix}
+import satify.model.expression.SymbolGeneration.{encodingVarPrefix, converterVarPrefix}
 import satify.model.{Assignment, Variable}
 
 /** Represents an [[Assignment]] where the variables could not be yet constrained by the DPLL algorithm.
@@ -94,7 +94,7 @@ object PartialAssignment:
                 optVars.filter(v =>
                   v match
                     case OptionalVariable(name, _)
-                        if name.startsWith(tseitinVarPrefix) || name.startsWith(encodingVarPrefix) =>
+                        if name.startsWith(converterVarPrefix) || name.startsWith(encodingVarPrefix) =>
                       false
                     case _ => true
                 )

src/main/scala/satify/model/expression/SymbolGeneration.scala

@@ -5,7 +5,7 @@ import satify.model.expression.Expression.*
 object SymbolGeneration:
 
   val encodingVarPrefix = "ENC"
-  val tseitinVarPrefix = "TSTN"
+  val converterVarPrefix = "GEN"
 
   /** A generator of new Symbols starting from a prefix. */
   trait SymbolGenerator:

src/main/scala/satify/update/converters/tseitin/TseitinTransformation.scala

@@ -2,7 +2,7 @@ package satify.update.converters.tseitin
 
 import satify.model.cnf.CNF
 import satify.model.expression.Expression
-import satify.model.expression.SymbolGeneration.tseitinVarPrefix
+import satify.model.expression.SymbolGeneration.converterVarPrefix
 
 import scala.annotation.tailrec
 
@@ -100,7 +100,7 @@ private[converters] object TseitinTransformation:
     if subexpressions.size == 1 then subexpressions.head
     else
       var concatenated = subexpressions
-      concatenated = concatenated.prepended(CNFSymbol(tseitinVarPrefix + "0"))
+      concatenated = concatenated.prepended(CNFSymbol(converterVarPrefix + "0"))
       concatenated.reduceRight((s1, s2) =>
         CNFAnd(s1.asInstanceOf[CNFOr | Literal], s2.asInstanceOf[CNFAnd | CNFOr | Literal])
       )

src/main/scala/satify/update/converters/tseitin/Utils.scala

@@ -4,7 +4,7 @@ import satify.model.cnf.CNF.{And as CNFAnd, Not as CNFNot, Or as CNFOr, Symbol a
 import satify.model.cnf.{CNF, Literal}
 import satify.model.expression.Expression
 import satify.model.expression.Expression.*
-import satify.model.expression.SymbolGeneration.{SymbolGenerator, tseitinVarPrefix}
+import satify.model.expression.SymbolGeneration.{SymbolGenerator, converterVarPrefix}
 
 private[converters] object Utils:
 
@@ -14,7 +14,7 @@ private[converters] object Utils:
     */
   def zipWithSymbol(exp: Expression): List[(Symbol, Expression)] =
     given SymbolGenerator with
-      override def prefix: String = tseitinVarPrefix
+      override def prefix: String = converterVarPrefix
     zipWith(exp)(summon[SymbolGenerator].generate)
 
   /** Method to check if an expression is in CNF form and can be converted to CNF form.
@@ -45,18 +45,18 @@ private[converters] object Utils:
       case Or(l, r) => CNFOr(convL(l), convL(r))
       case Symbol(v) => CNFSymbol(v)
       case Not(Symbol(v)) => CNFNot(CNFSymbol(v))
-      case _ => throw new Exception("Expression is not convertible to CNF form")
+      case _ => throw new IllegalArgumentException("Expression is not convertible to CNF form")
 
     def convR(exp: Expression): CNFAnd | CNFOr | Literal = exp match
       case And(l, r) => CNFAnd(convL(l), convR(r))
       case Or(l, r) => CNFOr(convL(l), convL(r))
       case Symbol(v) => CNFSymbol(v)
       case Not(Symbol(v)) => CNFNot(CNFSymbol(v))
-      case _ => throw new Exception("Expression is not convertible to CNF form")
+      case _ => throw new IllegalArgumentException("Expression is not convertible to CNF form")
 
     expression match
       case Symbol(v) => CNFSymbol(v)
       case Not(Symbol(v)) => CNFNot(CNFSymbol(v))
       case And(l, r) => CNFAnd(convL(l), convR(r))
       case Or(l, r) => CNFOr(convL(l), convL(r))
-      case _ => throw new Exception("Expression is not convertible to CNF form")
+      case _ => throw new IllegalArgumentException("Expression is not convertible to CNF form")

src/main/scala/satify/update/solver/dpll/impl/DpllFinder.scala

@@ -8,7 +8,7 @@ import satify.model.cnf.CNF.*
 import satify.model.dpll.*
 import satify.model.dpll.DecisionTree.{Branch, Leaf}
 import satify.model.dpll.PartialAssignment.*
-import satify.model.expression.SymbolGeneration.{encodingVarPrefix, tseitinVarPrefix}
+import satify.model.expression.SymbolGeneration.{encodingVarPrefix, converterVarPrefix}
 import satify.model.{Assignment, Result, Solution}
 import satify.update.solver.dpll.DpllDecision.decide
 import satify.update.solver.dpll.cnf.CNFSat.{isSat, isUnsat}
@@ -113,7 +113,7 @@ object DpllFinder:
           optVariables.filter(v =>
             v match
               case OptionalVariable(name, _)
-                  if name.startsWith(encodingVarPrefix) || name.startsWith(tseitinVarPrefix) =>
+                  if name.startsWith(encodingVarPrefix) || name.startsWith(converterVarPrefix) =>
                 false
               case _ => true
           )

src/test/resources/features/Conversion.feature

@@ -0,0 +1,19 @@
+Feature: Conversion to Conjunctive Normal Form
+
+  Scenario: I want to convert a malformed expression to CNF
+    Given the input "a ad b"
+    When it is reflected to scala compiler
+    Then I should obtain an IllegalArgumentException
+    And no CNF has to be generated
+
+  Scenario: I want to convert a literal to CNF
+    Given the input "a"
+    When it is reflected to scala compiler
+    And converted to CNF Form using Tseitin transformation
+    Then I should obtain the CNF "a"
+
+  Scenario: I want to convert an expression to CNF
+    Given the input "a and b"
+    When it is reflected to scala compiler
+    And converted to CNF Form using Tseitin transformation
+    Then I should obtain the CNF "GEN0 and not(a) or not(b) or GEN0 and a or not(GEN0) and b or not(GEN0)"

src/test/scala/satify/features/TseitinTransformationSteps.scala → src/test/scala/satify/features/ConversionSteps.scala

@@ -5,12 +5,12 @@ import org.scalatest.matchers.should.Matchers.*
 import satify.model.cnf.CNF
 import satify.update.converters.{Converter, ConverterType}
 
-object TseitinTransformationSteps extends ScalaDsl with EN:
+object ConversionSteps extends ScalaDsl with EN:
 
   import DSLSteps.*
   var cnf: Option[CNF] = None
 
-  And("converted to CNF Form") {
+  And("converted to CNF Form using Tseitin transformation") {
     try cnf = Some(Converter(ConverterType.Tseitin).convert(expression.get))
     catch case e: IllegalArgumentException => error = IllegalArgumentException(e.getMessage)
   }

src/test/scala/satify/update/converters/tseitin/ConcatTest.scala

@@ -19,7 +19,7 @@ class ConcatTest extends AnyFlatSpec with Matchers:
     val exps: List[CNF] = List(Symbol("a"), Symbol("b"), Symbol("c"))
     val result: CNF = concat(exps)
     val expected: CNF = And(
-      Symbol("TSTN0"),
+      Symbol("GEN0"),
       And(Symbol("a"), And(Symbol("b"), Symbol("c")))
     )
     result shouldBe expected
@@ -30,7 +30,7 @@ class ConcatTest extends AnyFlatSpec with Matchers:
       List(Or(Symbol("a"), Symbol("b")), And(Symbol("c"), Symbol("d")))
     val result: CNF = concat(exps)
     val expected: CNF = And(
-      Symbol("TSTN0"),
+      Symbol("GEN0"),
       And(
         Or(Symbol("a"), Symbol("b")),
         And(Symbol("c"), Symbol("d"))

src/test/scala/satify/update/converters/tseitin/ReplacingTest.scala

@@ -12,16 +12,16 @@ class ReplacingTest extends AnyFlatSpec with Matchers:
     val exp: Expression = Not(Symbol("b"))
     val result: List[(Symbol, Expression)] = symbolsReplace(exp)
     result should contain only (
-      (Symbol("TSTN0"), Not(Symbol("b")))
+      (Symbol("GEN0"), Not(Symbol("b")))
     )
   }
 
   "In (a ∨ ¬b) the replacement of subexpressions with symbols" should "generate 2 new symbols starting from the ¬b subexpression" in {
     val exp: Expression = Or(Symbol("a"), Not(Symbol("b")))
     val result: List[(Symbol, Expression)] = symbolsReplace(exp)
     val expected: List[(Symbol, Expression)] = List(
-      (Symbol("TSTN1"), Not(Symbol("b"))),
-      (Symbol("TSTN0"), Or(Symbol("a"), Symbol("TSTN1")))
+      (Symbol("GEN1"), Not(Symbol("b"))),
+      (Symbol("GEN0"), Or(Symbol("a"), Symbol("GEN1")))
     )
     result shouldBe expected
   }
@@ -32,9 +32,9 @@ class ReplacingTest extends AnyFlatSpec with Matchers:
     val list: List[(Symbol, Expression)] = symbolsReplace(exp)
 
     val expectedList: List[(Symbol, Expression)] = List(
-      (Symbol("TSTN2"), Not(Symbol("b"))),
-      (Symbol("TSTN1"), And(Symbol("a"), Symbol("TSTN2"))),
-      (Symbol("TSTN0"), Or(Symbol("TSTN1"), Symbol("c")))
+      (Symbol("GEN2"), Not(Symbol("b"))),
+      (Symbol("GEN1"), And(Symbol("a"), Symbol("GEN2"))),
+      (Symbol("GEN0"), Or(Symbol("GEN1"), Symbol("c")))
     )
     expectedList shouldBe list
   }
@@ -51,11 +51,11 @@ class ReplacingTest extends AnyFlatSpec with Matchers:
 
     val result: List[(Symbol, Expression)] = symbolsReplace(exp)
     val expected: List[(Symbol, Expression)] = List(
-      (Symbol("TSTN2"), And(Symbol("a"), Symbol("b"))),
-      (Symbol("TSTN3"), And(Symbol("c"), Symbol("d"))),
-      (Symbol("TSTN4"), And(Symbol("e"), Symbol("f"))),
-      (Symbol("TSTN1"), Or(Symbol("TSTN2"), Symbol("TSTN3"))),
-      (Symbol("TSTN0"), And(Symbol("TSTN1"), Symbol("TSTN4")))
+      (Symbol("GEN2"), And(Symbol("a"), Symbol("b"))),
+      (Symbol("GEN3"), And(Symbol("c"), Symbol("d"))),
+      (Symbol("GEN4"), And(Symbol("e"), Symbol("f"))),
+      (Symbol("GEN1"), Or(Symbol("GEN2"), Symbol("GEN3"))),
+      (Symbol("GEN0"), And(Symbol("GEN1"), Symbol("GEN4")))
     )
     result shouldBe expected
   }
@@ -69,11 +69,11 @@ class ReplacingTest extends AnyFlatSpec with Matchers:
 
     val result: List[(Symbol, Expression)] = symbolsReplace(exp)
     val expected: List[(Symbol, Expression)] = List(
-      (Symbol("TSTN2"), Or(Symbol("a"), Symbol("b"))),
-      (Symbol("TSTN4"), Not(Symbol("c"))),
-      (Symbol("TSTN1"), And(Symbol("a"), Symbol("TSTN2"))),
-      (Symbol("TSTN3"), And(Symbol("TSTN4"), Symbol("d"))),
-      (Symbol("TSTN0"), Or(Symbol("TSTN1"), Symbol("TSTN3")))
+      (Symbol("GEN2"), Or(Symbol("a"), Symbol("b"))),
+      (Symbol("GEN4"), Not(Symbol("c"))),
+      (Symbol("GEN1"), And(Symbol("a"), Symbol("GEN2"))),
+      (Symbol("GEN3"), And(Symbol("GEN4"), Symbol("d"))),
+      (Symbol("GEN0"), Or(Symbol("GEN1"), Symbol("GEN3")))
     )
     result shouldBe expected
   }