added test to nnf, re-arranged some functions

pldi2011-testcases/NNF.scala

@@ -9,7 +9,15 @@ object NNF {
   case class Not(f: Formula) extends Formula
   case class Literal(id: Int) extends Formula
 
-  def nnf(formula: Formula): Formula = formula match {
+  def isNNF(f: Formula): Boolean = f match {
+    case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+    case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+    case Not(Literal(_)) => true
+    case Not(_) => false
+    case Literal(_) => true
+  }
+
+  def nnf(formula: Formula): Formula = (formula match {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
     case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
@@ -17,10 +25,10 @@ object NNF {
     case Not(Not(f)) => nnf(f)
     case Not(Literal(_)) => formula
     case Literal(_) => formula
-  }
+  }) ensuring(f => isNNF(f))
 
   def freeVars(f: Formula): Set[Int] = {
-    require(isNNF(f))
+  require(isNNF(f))
     f match {
       case And(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
       case Or(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
@@ -28,12 +36,5 @@ object NNF {
       case Literal(i) => Set[Int](i)
     }
   }
-
-  def isNNF(f: Formula): Boolean = f match {
-    case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
-    case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
-    case Not(Literal(_)) => true
-    case Not(_) => false
-    case Literal(_) => true
-  }
+  def fv(f : Formula) = { freeVars(nnf(f)) }
 }