diff --git a/testcases/SatFun.scala b/testcases/SatFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e910e3e53be9f5ea9936506ac21288eb2a6a3ff9
--- /dev/null
+++ b/testcases/SatFun.scala
@@ -0,0 +1,167 @@
+import scala.collection.Map
+
+object SatFun {
+
+ sealed abstract class Formula
+ case class And(f1: Formula, f2: Formula) extends Formula
+ case class Or(f1: Formula, f2: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Var(i: Int) extends Formula
+
+ //vars are numbered from 1 to n, and Not(Var(n)) is represented as -n
+ sealed abstract class VarList
+ case class VarCons(head: Int, tail: VarList) extends VarList
+ case class VarNil() extends VarList
+
+ sealed abstract class ClauseList
+ case class ClauseCons(head: VarList, tail: ClauseList) extends ClauseList
+ case class ClauseNil() extends ClauseList
+
+ def eval(formula: Formula, assignment: Map[Int, Boolean]): Boolean = formula match {
+ case Var(n) => assignment(n)
+ case Not(f) => !eval(f, assignment)
+ case And(f1, f2) => eval(f1, assignment) && eval(f2, assignment)
+ case Or(f1, f2) => eval(f1, assignment) || eval(f2, assignment)
+ }
+
+ def evalCnf(clauses: ClauseList, assignment: Map[Int, Boolean]): Boolean = clauses match {
+ case ClauseCons(cl, cls) => evalClauseCnf(cl, assignment) && evalCnf(cls, assignment)
+ case ClauseNil() => false
+ }
+ def evalDnf(clauses: ClauseList, assignment: Map[Int, Boolean]): Boolean = clauses match {
+ case ClauseCons(cl, cls) => evalClauseDnf(cl, assignment) || evalDnf(cls, assignment)
+ case ClauseNil() => true
+ }
+ def evalClauseCnf(clause: VarList, assignment: Map[Int, Boolean]): Boolean = clause match {
+ case VarCons(v, vs) => (if(v < 0) assignment(-v) else assignment(v)) || evalClauseCnf(vs, assignment)
+ case VarNil() => false
+ }
+ def evalClauseDnf(clause: VarList, assignment: Map[Int, Boolean]): Boolean = clause match {
+ case VarCons(v, vs) => (if(v < 0) assignment(-v) else assignment(v)) && evalClauseDnf(vs, assignment)
+ case VarNil() => true
+ }
+
+ def vars(formula: Formula): Set[Int] = formula match {
+ case Var(n) => Set(n)
+ case Not(f) => vars(f)
+ case And(f1, f2) => vars(f1) ++ vars(f2)
+ case Or(f1, f2) => vars(f1) ++ vars(f2)
+ }
+
+ def concatClauses(cll1: ClauseList, cll2: ClauseList): ClauseList = cll1 match {
+ case ClauseCons(cl, tail) => ClauseCons(cl, concatClauses(tail, cll2))
+ case ClauseNil() => cll2
+ }
+
+ def concatVars(l1: VarList, l2: VarList): VarList = l1 match {
+ case VarCons(v, vs) => VarCons(v, concatVars(vs, l2))
+ case VarNil() => l2
+ }
+
+ def distributeClause(cl: VarList, cll: ClauseList): ClauseList = cll match {
+ case ClauseCons(cl2, cl2s) => ClauseCons(concatVars(cl, cl2), distributeClause(cl, cl2s))
+ case ClauseNil() => ClauseNil()
+ }
+
+ def distribute(cll1: ClauseList, cll2: ClauseList): ClauseList = cll1 match {
+ case ClauseCons(cl, cls) => concatClauses(distributeClause(cl, cll2), distribute(cls, cll2))
+ case ClauseNil() => cll2
+ }
+
+ def negateClauses(cll: ClauseList): ClauseList = cll match {
+ case ClauseCons(cl, cls) => ClauseCons(negateVars(cl), negateClauses(cls))
+ case ClauseNil() => ClauseNil()
+ }
+
+ def negateVars(lst: VarList): VarList = lst match {
+ case VarCons(v, vs) => VarCons(-v, negateVars(vs))
+ case VarNil() => VarNil()
+ }
+
+ def cnfNaive(formula: Formula): ClauseList = formula match {
+ case And(f1, f2) => {
+ val cnf1 = cnfNaive(f1)
+ val cnf2 = cnfNaive(f2)
+ concatClauses(cnf1, cnf2)
+ }
+ case Or(f1, f2) => {
+ val cnf1 = cnfNaive(f1)
+ val cnf2 = cnfNaive(f2)
+ distribute(cnf1, cnf2)
+ }
+ case Not(And(f1, f2)) => cnfNaive(Or(Not(f1), Not(f2)))
+ case Not(Or(f1, f2)) => cnfNaive(And(Not(f1), Not(f2)))
+ case Not(Not(f)) => cnfNaive(f)
+ case Not(Var(n)) => ClauseCons(VarCons(-n, VarNil()), ClauseNil())
+ case Var(n) => ClauseCons(VarCons(n, VarNil()), ClauseNil())
+ }
+
+ def dnfNaive(formula: Formula): ClauseList = formula match {
+ case And(f1, f2) => {
+ val dnf1 = dnfNaive(f1)
+ val dnf2 = dnfNaive(f2)
+ distribute(dnf1, dnf2)
+ }
+ case Or(f1, f2) => {
+ val dnf1 = dnfNaive(f1)
+ val dnf2 = dnfNaive(f2)
+ concatClauses(dnf1, dnf2)
+ }
+ case Not(And(f1, f2)) => dnfNaive(Or(Not(f1), Not(f2)))
+ case Not(Or(f1, f2)) => dnfNaive(And(Not(f1), Not(f2)))
+ case Not(Not(f)) => dnfNaive(f)
+ case Not(Var(n)) => ClauseCons(VarCons(-n, VarNil()), ClauseNil())
+ case Var(n) => ClauseCons(VarCons(n, VarNil()), ClauseNil())
+ }
+
+ def isContradictory(clause: VarList, vars: Set[Int]): Boolean = clause match {
+ case VarCons(v, vs) => vars.contains(-v) || isContradictory(vs, vars ++ Set(v))
+ case VarNil() => false
+ }
+
+ def isSatDnf(clauses: ClauseList): Boolean = clauses match {
+ case ClauseCons(cl, cls) => !isContradictory(cl, Set.empty) || isSatDnf(cls)
+ case ClauseNil() => false
+ }
+
+ //some non-leon functions to test the program with scala
+ object False {
+ def apply(): Formula = And(Var(1), Not(Var(1)))
+ }
+ object True {
+ def apply(): Formula = Or(Var(1), Not(Var(1)))
+ }
+ object Or {
+ def apply(fs: Formula*): Formula = fs match {
+ case Seq() => False()
+ case Seq(f) => f
+ case fs => fs.reduceLeft((f1, f2) => Or(f1, f2))
+ }
+ }
+ object And {
+ def apply(fs: Formula*): Formula = fs match {
+ case Seq() => True()
+ case Seq(f) => f
+ case fs => fs.reduceLeft((f1, f2) => And(f1, f2))
+ }
+ }
+ def clause2list(cl: VarList): List[Int] = cl match {
+ case VarCons(v, vs) => v :: clause2list(vs)
+ case VarNil() => Nil
+ }
+ def clauses2list(cll: ClauseList): List[List[Int]] = cll match {
+ case ClauseCons(cl, cls) => clause2list(cl) :: clauses2list(cls)
+ case ClauseNil() => Nil
+ }
+
+ def main(args: Array[String]) {
+ val f1 = And(Var(1), Or(Var(1), Not(Var(2)), Var(3)), Var(2), Not(Var(3)))
+ val dnff1 = clauses2list(dnfNaive(f1))
+ val vars1 = vars(f1)
+ vars.foreach(v => {
+
+
+ })
+ println(f1 + " translated in dnf as:\n\t" + dnff1.mkString("\n\t"))
+ }
+}