From e5046873fa174201af5eb4181b9f5b966b4592ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Wed, 23 Mar 2011 11:26:07 +0000
Subject: [PATCH] reorganize call transformation a little.
---
src/funcheck/CallTransformation.scala | 27 ++++++++++++++-------------
src/funcheck/CodeGeneration.scala | 6 +++---
2 files changed, 17 insertions(+), 16 deletions(-)
diff --git a/src/funcheck/CallTransformation.scala b/src/funcheck/CallTransformation.scala
index 661b09708..f3b95a54b 100644
--- a/src/funcheck/CallTransformation.scala
+++ b/src/funcheck/CallTransformation.scala
@@ -32,19 +32,20 @@ trait CallTransformation
println("Here is the extracted FunDef:")
println(fd)
-
- /*
- typer.typed(atOwner(currentOwner) {
- code
- })
- */
- super.transform(tree)
-
- /*
- val solver = new FairZ3Solver(new DefaultReporter)
- solver.setProgram(prog)
- println(solver.decide(fd.body.get, false))
- */
+
+ 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 (readProgram, progSym) = codeGen.generateProgramRead(filename)
+ val solverInvocation = codeGen.generateSolverInvocation(b, progSym)
+ val code = Block(readProgram :: Nil, solverInvocation)
+
+ typer.typed(atOwner(currentOwner) {
+ code
+ })
+ }
}
case _ => super.transform(tree)
diff --git a/src/funcheck/CodeGeneration.scala b/src/funcheck/CodeGeneration.scala
index 3d3cc4970..6850a1679 100644
--- a/src/funcheck/CodeGeneration.scala
+++ b/src/funcheck/CodeGeneration.scala
@@ -40,7 +40,7 @@ trait CodeGeneration {
(readStatement, progSymbol)
}
- def generateSolverInvocation(formula: Expr) : Tree = {
+ def generateSolverInvocation(formula: Expr, progSymbol: Symbol) : Tree = {
val solverSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "solver")).setInfo(fairZ3SolverClass.tpe)
val solverDeclaration =
ValDef(
@@ -63,7 +63,7 @@ trait CodeGeneration {
Ident(solverSymbol),
setProgramFunction
),
- List(/* read program into a var and plug its symbol here */)
+ List(Ident(progSymbol))
)
val invocation =
@@ -72,7 +72,7 @@ trait CodeGeneration {
Ident(solverSymbol),
decideWithModelFunction
),
- List(/* convert pred into scala AST and plug it here */)
+ List(/* convert pred into scala AST of funcheck expression and plug it here */)
)
Block(
--
GitLab