diff --git a/src/funcheck/CallTransformation.scala b/src/funcheck/CallTransformation.scala index 42913bce279b7a5b96e75595a7d695146baa5255..160120d7298d13260061b77ed8a97c0d35192449 100644 --- a/src/funcheck/CallTransformation.scala +++ b/src/funcheck/CallTransformation.scala @@ -32,16 +32,16 @@ trait CallTransformation println("Here is the extracted FunDef:") println(fd) - + val codeGen = new CodeGenerator(unit, currentOwner) fd.body match { case None => println("Could not extract choose predicate: " + funBody); super.transform(tree) case Some(b) => val exprFilename = writeExpr(b) - val (programGet, progSym) = codeGen.generateProgramGet(programFilename) - val (exprGet, exprSym) = codeGen.generateExprGet(exprFilename) - val solverInvocation = codeGen.generateSolverInvocation(b, progSym, exprSym) + val (programGet, progSym) = codeGen.getProgram(programFilename) + val (exprGet, exprSym) = codeGen.getExpr(exprFilename) + val solverInvocation = codeGen.invokeSolver(b, progSym, exprSym) val code = Block(programGet :: exprGet :: Nil, solverInvocation) typer.typed(atOwner(currentOwner) { diff --git a/src/funcheck/CodeGeneration.scala b/src/funcheck/CodeGeneration.scala index e2052a5e3e811ba328f2cd84dc5eade8731bfa9a..addd2cefec000e188c261d1baa781900898deb97 100644 --- a/src/funcheck/CodeGeneration.scala +++ b/src/funcheck/CodeGeneration.scala @@ -28,7 +28,7 @@ trait CodeGeneration { class CodeGenerator(unit : CompilationUnit, owner : Symbol) { - def generateProgramGet(filename : String) : (Tree, Symbol) = { + def getProgram(filename : String) : (Tree, Symbol) = { val progSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "prog")).setInfo(programClass.tpe) val getStatement = ValDef( @@ -47,7 +47,7 @@ trait CodeGeneration { (getStatement, progSymbol) } - def generateExprGet(filename : String) : (Tree, Symbol) = { + def getExpr(filename : String) : (Tree, Symbol) = { val exprSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "expr")).setInfo(exprClass.tpe) val getStatement = ValDef( @@ -66,7 +66,7 @@ trait CodeGeneration { (getStatement, exprSymbol) } - def generateSolverInvocation(formula : Expr, progSymbol : Symbol, exprSymbol : Symbol) : Tree = { + def invokeSolver(formula : Expr, progSymbol : Symbol, exprSymbol : Symbol) : Tree = { val solverSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "solver")).setInfo(fairZ3SolverClass.tpe) val solverDeclaration = ValDef( @@ -102,9 +102,9 @@ trait CodeGeneration { ) Block( - solverDeclaration :: setProgram :: invocation :: Nil, - Literal(Constant(0)) - ) + solverDeclaration :: setProgram :: invocation :: Nil, + Literal(Constant(0)) + ) } } } diff --git a/src/funcheck/Serialization.scala b/src/funcheck/Serialization.scala index addb7e24c08570d0c3fa76c67fa40a4cf0106aaa..e10581c0052855fd80f8aae463eb6ea49e0ed603 100644 --- a/src/funcheck/Serialization.scala +++ b/src/funcheck/Serialization.scala @@ -72,6 +72,4 @@ trait Serialization { } } -object Serialization extends Serialization { - -} +object Serialization extends Serialization