From 3a30acc1da5a3e29cb4634abe97d230385cc460d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Wed, 23 Mar 2011 16:37:17 +0000
Subject: [PATCH] Generation of solver invocation with a given choose predicate
---
src/funcheck/CallTransformation.scala | 14 ++++----
src/funcheck/CodeGeneration.scala | 47 ++++++++++++++++++++++-----
src/purescala/FairZ3Solver.scala | 5 +++
3 files changed, 52 insertions(+), 14 deletions(-)
diff --git a/src/funcheck/CallTransformation.scala b/src/funcheck/CallTransformation.scala
index a2b0705a2..42913bce2 100644
--- a/src/funcheck/CallTransformation.scala
+++ b/src/funcheck/CallTransformation.scala
@@ -17,10 +17,10 @@ trait CallTransformation
private lazy val cpDefinitionsModule = definitions.getModule("funcheck.CP")
- def transformCalls(unit: CompilationUnit, prog: Program, filename: String) : Unit =
- unit.body = new CallTransformer(unit, prog, filename).transform(unit.body)
+ def transformCalls(unit: CompilationUnit, prog: Program, programFilename: String) : Unit =
+ unit.body = new CallTransformer(unit, prog, programFilename).transform(unit.body)
- class CallTransformer(unit: CompilationUnit, prog: Program, filename: String) extends TypingTransformer(unit) {
+ class CallTransformer(unit: CompilationUnit, prog: Program, programFilename: String) extends TypingTransformer(unit) {
override def transform(tree: Tree) : Tree = {
tree match {
case a @ Apply(TypeApply(Select(s: Select, n), _), rhs @ List(predicate: Function)) if (cpDefinitionsModule == s.symbol && n.toString == "choose") => {
@@ -38,9 +38,11 @@ trait CallTransformation
fd.body match {
case None => println("Could not extract choose predicate: " + funBody); super.transform(tree)
case Some(b) =>
- val (programGet, progSym) = codeGen.generateProgramGet(filename)
- val solverInvocation = codeGen.generateSolverInvocation(b, progSym)
- val code = Block(programGet :: Nil, solverInvocation)
+ val exprFilename = writeExpr(b)
+ val (programGet, progSym) = codeGen.generateProgramGet(programFilename)
+ val (exprGet, exprSym) = codeGen.generateExprGet(exprFilename)
+ val solverInvocation = codeGen.generateSolverInvocation(b, progSym, exprSym)
+ val code = Block(programGet :: exprGet :: Nil, solverInvocation)
typer.typed(atOwner(currentOwner) {
code
diff --git a/src/funcheck/CodeGeneration.scala b/src/funcheck/CodeGeneration.scala
index c81a2d71b..e2052a5e3 100644
--- a/src/funcheck/CodeGeneration.scala
+++ b/src/funcheck/CodeGeneration.scala
@@ -6,27 +6,39 @@ trait CodeGeneration {
self: CallTransformation =>
import global._
- private lazy val serializationModule = definitions.getClass("funcheck.Serialization")
+ private lazy val funcheckPackage = definitions.getModule("funcheck")
+
+ private lazy val serializationModule = definitions.getModule("funcheck.Serialization")
private lazy val getProgramFunction = definitions.getMember(serializationModule, "getProgram")
+ private lazy val getExprFunction = definitions.getMember(serializationModule, "getExpr")
+
private lazy val purescalaPackage = definitions.getModule("purescala")
+
private lazy val definitionsModule = definitions.getModule("purescala.Definitions")
private lazy val programClass = definitions.getClass("purescala.Definitions.Program")
+
+ private lazy val treesModule = definitions.getModule("purescala.Trees")
+ private lazy val exprClass = definitions.getClass("purescala.Trees.Expr")
+
private lazy val fairZ3SolverClass = definitions.getClass("purescala.FairZ3Solver")
- private lazy val decideWithModelFunction = definitions.getMember(fairZ3SolverClass, "decideWithModel")
+ private lazy val restartAndDecideWithModel = definitions.getMember(fairZ3SolverClass, "restartAndDecideWithModel")
private lazy val setProgramFunction = definitions.getMember(fairZ3SolverClass, "setProgram")
private lazy val defaultReporter = definitions.getClass("purescala.DefaultReporter")
- class CodeGenerator(unit: CompilationUnit, owner: Symbol) {
+ class CodeGenerator(unit : CompilationUnit, owner : Symbol) {
- def generateProgramGet(filename: String) : (Tree, Symbol) = {
+ def generateProgramGet(filename : String) : (Tree, Symbol) = {
val progSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "prog")).setInfo(programClass.tpe)
val getStatement =
ValDef(
progSymbol,
Apply(
Select(
- Ident(serializationModule),
+ Select(
+ Ident(funcheckPackage),
+ serializationModule
+ ) ,
getProgramFunction
),
List(Literal(Constant(filename)))
@@ -35,7 +47,26 @@ trait CodeGeneration {
(getStatement, progSymbol)
}
- def generateSolverInvocation(formula: Expr, progSymbol: Symbol) : Tree = {
+ def generateExprGet(filename : String) : (Tree, Symbol) = {
+ val exprSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "expr")).setInfo(exprClass.tpe)
+ val getStatement =
+ ValDef(
+ exprSymbol,
+ Apply(
+ Select(
+ Select(
+ Ident(funcheckPackage),
+ serializationModule
+ ),
+ getExprFunction
+ ),
+ List(Literal(Constant(filename)))
+ )
+ )
+ (getStatement, exprSymbol)
+ }
+
+ def generateSolverInvocation(formula : Expr, progSymbol : Symbol, exprSymbol : Symbol) : Tree = {
val solverSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "solver")).setInfo(fairZ3SolverClass.tpe)
val solverDeclaration =
ValDef(
@@ -65,9 +96,9 @@ trait CodeGeneration {
Apply(
Select(
Ident(solverSymbol),
- decideWithModelFunction
+ restartAndDecideWithModel
),
- List(/* convert pred into scala AST of funcheck expression and plug it here */)
+ List(Ident(exprSymbol), Literal(Constant(false)))
)
Block(
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 6945611ad..7e62e8996 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -238,6 +238,11 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
decideWithModel(vc, forValidity)._1
}
+ def restartAndDecideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
+ restartZ3
+ decideWithModel(vc, forValidity)
+ }
+
def decideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
val unrollingBank = new UnrollingBank
--
GitLab