modifications to examples and evaluation scripts

cp-demo/enumerating/SortedList.scala

@@ -44,7 +44,8 @@ object SortedList {
   def main(args : Array[String]) : Unit = {
     val len = if (args.isEmpty) 3 else args(0).toInt
 
-    f2(len)
+    f1(len)
+    // f2(len)
     // f3(len)
     // f4()
   }

demo/ListOperations.scala

@@ -73,13 +73,26 @@ object ListOperations {
     def append(l1 : List, l2 : List) : List = (l1 match {
       case Nil() => l2
       case Cons(x,xs) => Cons(x, append(xs, l2))
-    }) ensuring(content(_) == content(l1) ++ content(l2))
+    }) // ensuring(content(_) == content(l1) ++ content(l2))
 
     def map(f : Int => Int, l : List) : List = l match {
       case Nil() => Nil()
       case Cons(x, xs) => Cons(f(x), map(f, xs))
     }
 
+    def definedForAll(m: Map[Int,Int], l: List): Boolean = l match {
+      case Nil() => true
+      case Cons(x, xs) => m.isDefinedAt(x) && definedForAll(m, xs)
+    }
+
+    def map2(m : Map[Int,Int], l : List) : List = {
+      //require(definedForAll(m, l))
+      l match {
+        case Nil() => Nil()
+        case Cons(x, xs) => Cons(m(x), map2(m, xs))
+      }
+    }
+
     @induct
     def appendMapCommute(l1 : List, l2 : List, f : Int => Int) : Boolean = {
       map(f, append(l1, l2)) == append(map(f, l1), map(f, l2))
@@ -88,7 +101,7 @@ object ListOperations {
     @induct
     def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
 
-    @induct
+    // @induct
     def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
       (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
 

eval/cp/scripts/run-cp-evaluation

@@ -4,57 +4,36 @@ cd ../../..
 
 ts=`date +%F-%R`
 demoFolder="cp-demo"
+cc="./cp-compile"
+rc="./cp-run"
 
 #classes=( "RedBlackTree" "SortedList" )
 
-if [ "$#" -lt "3" ]
+if [ "$#" -lt "4" ]
 then
-  echo "Please provide a class name and bounds for problem size"
+  echo "Please provide a file name, main class name and bounds for problem size"
   exit 1
 fi
 
-class=${1}
-base=${2}
-limit=${3}
+filename=${1}
+mainclass=${2}
+base=${3}
+limit=${4}
 
-evalFolder="eval/cp/data/${ts}-${class}"
+evalFolder="eval/cp/data/${ts}-${mainclass}"
 
 mkdir -p ${evalFolder}
 
-evalFileBase=${evalFolder}/${class}-${ts}-CAV
-./cp CAV ${demoFolder}/${class}.scala || (echo "Could not compile..." && exit 1)
+evalFileBase=${evalFolder}/${mainclass}-${ts}
+${cc} axioms scalaEval ${filename} || (echo "Could not compile..." && exit 1)
 
 for (( i=${base}; i<=${limit}; i++ ))
 do
   currentFile=${evalFileBase}-${i}
-  ./cp-runner ${class} $i | tee -a ${currentFile}
+  ${rc} ${mainclass} $i | tee -a ${currentFile}
   cd eval/cp/scripts
   ./generate-graph ../../../${currentFile}
   cd ../../..
 done
 
-evalFileBase=${evalFolder}/${class}-${ts}-CAV-axioms
-./cp CAV axioms ${demoFolder}/${class}.scala || (echo "Could not compile..." && exit 1)
-
-for (( i=${base}; i<=${limit}; i++ ))
-do
-  currentFile=${evalFileBase}-${i}
-  ./cp-runner ${class} $i | tee -a ${currentFile}
-  cd eval/cp/scripts
-  ./generate-graph ../../../${currentFile}
-  cd ../../..
-done
-
-evalFileBase=${evalFolder}/${class}-${ts}-CAV-axioms-scalaEval
-./cp CAV axioms scalaEval ${demoFolder}/${class}.scala || (echo "Could not compile..." && exit 1)
-
-for (( i=${base}; i<=${limit}; i++ ))
-do
-  currentFile=${evalFileBase}-${i}
-  ./cp-runner ${class} $i | tee -a ${currentFile}
-  cd eval/cp/scripts
-  ./generate-graph ../../../${currentFile}
-  cd ../../..
-done
-
-mv eval/cp/graphs/${class}-${ts}-* ${evalFolder}
+mv eval/cp/graphs/${mainclass}-${ts}-* ${evalFolder}