Always write into freshly created files for serialization

src/cp/CPComponent.scala

@@ -39,7 +39,7 @@ class CPComponent(val global: Global, val pluginInstance: CPPlugin)
       // new ForeachTreeTraverser(plop).traverse(unit.body)
 
       val prog: purescala.Definitions.Program = extractCode(unit, true)
-      val filename = writeProgram(prog)
+      val filename = writeObject(prog)
       println("Program extracted and written into: " + filename)
 
       transformCalls(unit, prog, filename)

src/cp/CallTransformation.scala

@@ -55,7 +55,6 @@ trait CallTransformation
               // retrieve program, expression, and list of output variables
               val (programAssignment, progSym)                = codeGen.assignProgram(programFilename)
               val (exprAssignment, exprSym)                   = codeGen.assignExpr(exprFilename)
-              val (outputVarListAssignment, outputVarListSym) = codeGen.assignOutputVarList(outputVarListFilename)
 
               // compute input variables and assert equalities
               val inputVars = variablesOf(b).filter{ v => !outputVarList.contains(v.name) }.toList
@@ -68,7 +67,7 @@ trait CallTransformation
               val (andExprAssignment, andExprSym) = codeGen.assignAndExpr((ID(exprSym) :: equalities) : _*)
 
               // invoke solver and get ordered list of assignments
-              val (solverInvocation, outcomeTupleSym)         = codeGen.invokeSolver(progSym, andExprSym)
+              val (solverInvocation, outcomeTupleSym)         = codeGen.invokeSolver(progSym, if (inputVars.isEmpty) exprSym else andExprSym)
               val (modelAssignment, modelSym)                 = codeGen.assignModel(outcomeTupleSym)
 
               // TODO generate all correct e2s invocations
@@ -88,7 +87,16 @@ trait CallTransformation
                 New(tupleTypeTree,List(returnExpressions map (Ident(_))))
               }
 
-              val code = BLOCK(List(programAssignment, exprAssignment, outputVarListAssignment, andExprAssignment) ::: solverInvocation ::: List(modelAssignment) ::: valueAssignments ::: List(returnExpr) : _*)
+              val code = BLOCK(List(programAssignment, exprAssignment, andExprAssignment) ::: solverInvocation ::: List(modelAssignment) ::: valueAssignments ::: List(returnExpr) : _*)
+
+              /** generated code: */
+              val prog1: purescala.Definitions.Program = cp.Serialization.getProgram(programFilename);
+              val expr1: purescala.Trees.Expr = cp.Serialization.getExpr(exprFilename);
+              val andExpr1: purescala.Trees.Expr = new And(scala.collection.immutable.List.apply[purescala.Trees.Expr](expr1));
+              val solver1: purescala.FairZ3Solver = new FairZ3Solver(new DefaultReporter());
+              solver1.setProgram(prog1);
+              val outcome1: (Option[Boolean], Map[purescala.Common.Identifier,purescala.Trees.Expr]) = solver1.restartAndDecideWithModel(expr1, false);
+              println("the outcome: " + outcome1)
 
               typer.typed(atOwner(currentOwner) {
                 code
@@ -154,7 +162,7 @@ object CallTransformation {
     outcomeTuple._1
   }
 
-  def inputVar(inputVarList : List[Variable], varName : String) : Variable =
+  def inputVar(inputVarList : List[Variable], varName : String) : Variable = {
     inputVarList.find(_.id.name == varName).getOrElse(scala.Predef.error("Could not find input variable '" + varName + "' in list " + inputVarList))
-
+  }
 }

src/cp/CodeGeneration.scala

@@ -14,6 +14,8 @@ trait CodeGeneration {
 
   private lazy val exceptionClass = definitions.getClass("java.lang.Exception")
 
+  private lazy val collectionModule = definitions.getModule("scala.collection")
+  private lazy val immutableModule =  definitions.getModule("scala.collection.immutable")
   private lazy val listMapFunction = definitions.getMember(definitions.ListClass, "map")
   private lazy val listClassApplyFunction = definitions.getMember(definitions.ListClass, "apply")
   private lazy val listModuleApplyFunction = definitions.getMember(definitions.ListModule, "apply")
@@ -224,7 +226,7 @@ trait CodeGeneration {
               List(
                 List(
                   (((cpPackage DOT serializationModule DOT getProgramFunction) APPLY LIT(programFilename)) DOT caseClassDefFunction) APPLY LIT(scalaSym.nameString),
-                  listModuleApplyFunction APPLY (memberSyms map {
+                  (scalaPackage DOT collectionModule DOT immutableModule DOT definitions.ListModule DOT listModuleApplyFunction) APPLY (memberSyms map {
                     case ms => methodSym APPLY (scalaBinderSym DOT ms)
                   })
                 )
@@ -255,7 +257,7 @@ trait CodeGeneration {
 
     def assignAndExpr(exprs : Tree*) : (Tree, Symbol) = {
       val andSym = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "andExpr")).setInfo(exprClass.tpe)
-      val statement = VAL(andSym) === NEW(ID(andClass), listModuleApplyFunction APPLY (exprs.toList))
+      val statement = VAL(andSym) === NEW(ID(andClass), (scalaPackage DOT collectionModule DOT immutableModule DOT definitions.ListModule DOT listModuleApplyFunction) APPLY (exprs.toList))
       (statement, andSym)
     }
 

src/cp/Serialization.scala

@@ -39,15 +39,6 @@ trait Serialization {
     writeObject(file, obj)
   }
 
-  def writeProgram(prog : Program) : String = {
-    directory.mkdir()
-
-    val file = new java.io.File(directory, programFileName(prog))
-    file.delete()
-
-    writeObject(file, prog)
-  }
-
   private def readObject[A](filename : String) : A = {
     val fis = new FileInputStream(filename)
     val ois = new ObjectInputStream(fis)
@@ -59,13 +50,13 @@ trait Serialization {
   }
 
   def getProgram(filename : String) : Program = cachedProgram match {
-    case None => val r = readObject[Program](filename); cachedProgram = Some(r); r
-    case Some(cp) => cp
+    case Some(cp) => println("using cached program"); cp
+    case None => println("reading program from file " + filename); val r = readObject[Program](filename); cachedProgram = Some(r); r
   }
 
   def getExpr(filename : String) : Expr = exprMap.get(filename) match {
-    case Some(e) => e
-    case None => val e = readObject[Expr](filename); exprMap += (filename -> e); e
+    case Some(e) => println("using cached expr"); e
+    case None => println("reading expr from file " + filename); val e = readObject[Expr](filename); exprMap += (filename -> e); e
   }
 
   def getOutputVarList(filename : String) : List[String] = outputVarListMap.get(filename) match {
@@ -74,8 +65,8 @@ trait Serialization {
   }
 
   def getInputVarList(filename : String) : List[Variable] = inputVarListMap.get(filename) match {
-    case Some(l) => l
-    case None => val l = readObject[List[Variable]](filename); inputVarListMap += (filename -> l); l
+    case Some(l) => println("using cached input var list"); l
+    case None => println("reading input var list from file " + filename); val l = readObject[List[Variable]](filename); inputVarListMap += (filename -> l); l
   }
 }