From f086fac807a8b8df8b2e5e01b71d0ed82c0fbf54 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Thu, 9 Jun 2011 20:51:20 +0000
Subject: [PATCH] properly extract constraints that include logical variables
---
cp-demo/LazyVars.scala | 3 +
src/cp/CallTransformation.scala | 66 +++-
src/cp/CodeExtraction.scala | 567 +++++++++++++++++---------------
src/cp/CodeGeneration.scala | 17 +-
src/cp/ConstraintSolving.scala | 2 +-
src/cp/Extractors.scala | 10 +
src/cp/LTrees.scala | 5 +-
src/cp/RuntimeMethods.scala | 8 +
src/cp/Terms.scala | 18 +-
src/cp/Utils.scala | 2 +-
src/purescala/Trees.scala | 5 -
11 files changed, 405 insertions(+), 298 deletions(-)
diff --git a/cp-demo/LazyVars.scala b/cp-demo/LazyVars.scala
index bcaed292e..e55f64f7c 100644
--- a/cp-demo/LazyVars.scala
+++ b/cp-demo/LazyVars.scala
@@ -11,11 +11,13 @@ object LazyVars {
y <- chooseInt(3, 6)
if y < x
} {
+ println(((a: Int) => a > x).solve)
val i: Int = x
val j: Int = y
println(i, j)
}
+ /*
println("...")
for {
@@ -27,5 +29,6 @@ object LazyVars {
val j: Int = y
println(i, j)
}
+ */
}
}
diff --git a/src/cp/CallTransformation.scala b/src/cp/CallTransformation.scala
index 921ce0e44..c6178d978 100644
--- a/src/cp/CallTransformation.scala
+++ b/src/cp/CallTransformation.scala
@@ -18,8 +18,24 @@ trait CallTransformation
import global._
import CODE._
- private lazy val cpPackage = definitions.getModule("cp")
- private lazy val cpDefinitionsModule = definitions.getModule("cp.Definitions")
+ private lazy val cpPackage = definitions.getModule("cp")
+ private lazy val cpDefinitionsModule = definitions.getModule("cp.Definitions")
+ private lazy val lstreamClass = definitions.getClass("cp.LTrees.LStream")
+ private lazy val withFilter2Function = definitions.getMember(lstreamClass, "withFilter2")
+ private lazy val lClassSym = definitions.getClass("cp.LTrees.L")
+
+ private def isLSym(sym: Symbol): Boolean = {
+ sym == lClassSym
+ }
+
+ private def isLStreamSym(sym: Symbol): Boolean = {
+ sym == lstreamClass
+ }
+
+ private def hasLStreamType(tr: Tree): Boolean = tr.tpe match {
+ case TypeRef(_, sym, _) if isLStreamSym(sym) => true
+ case _ => false
+ }
val purescalaReporter = purescala.Settings.reporter
@@ -30,7 +46,11 @@ trait CallTransformation
case Apply(TypeApply(Select(Select(cpIdent, definitionsName), func2termName), typeTreeList), List(function: Function)) if
(definitionsName.toString == "Definitions" && func2termName.toString.matches("func2term\\d")) => {
val Function(funValDefs, funBody) = function
- extracted += (function.pos -> extractFunction(unit, funValDefs, funBody))
+ extracted += (function.pos -> extractStandardConstraint(unit, funValDefs, funBody))
+ }
+ case Apply(Select(lhs, withFilterName), List(predicate: Function)) if withFilterName.toString == "withFilter" && hasLStreamType(lhs) => {
+ val Function(funValDefs, funBody) = predicate
+ extracted += (predicate.pos -> extractConstraintWithLVars(unit, funValDefs, funBody))
}
case _ =>
}
@@ -66,19 +86,25 @@ trait CallTransformation
val serializedExpr = serialize(matchToIfThenElse(b))
// compute input variables
- val inputVars : Seq[Identifier] = variablesOf(b).filter(!outputVars.contains(_)).toSeq
+ val nonOutputIdentifiers : Seq[Identifier] = variablesOf(b).filter(!outputVars.contains(_)).toSeq
+ val reverseLVars = reverseLvarSubsts
+ val (lvarIdentifiers, inputIdentifiers) = nonOutputIdentifiers.partition(id => reverseLVars.isDefinedAt(Variable(id)))
- purescalaReporter.info("Input variables : " + inputVars.mkString(", "))
+ purescalaReporter.info("Input variables : " + inputIdentifiers.mkString(", "))
purescalaReporter.info("Output variables : " + outputVars.mkString(", "))
- // serialize list of input "Variable"s
- val serializedInputVarList = serialize(inputVars map (iv => Variable(iv)))
+ // list of input "Variables" to concatenate with list of L variables
+ val inputVars = inputIdentifiers map (iv => Variable(iv))
+ val lVars = lvarIdentifiers map (lv => Variable(lv))
+
+ // serialize list of all non-output "Variable"s
+ val serializedInputVarList = serialize(inputVars ++ lVars)
// serialize outputVars sequence
val serializedOutputVars = serialize(outputVars)
// sequence of input values
- val inputVarValues : Tree = codeGen.inputVarValues(serializedInputVarList, inputVars, scalaToExprSym)
+ val inputVarValues : Tree = codeGen.inputVarValues(serializedInputVarList, inputIdentifiers, lvarIdentifiers, scalaToExprSym)
Some((serializedInputVarList, serializedOutputVars, serializedExpr, inputVarValues, outputVars.size))
}
@@ -103,6 +129,30 @@ trait CallTransformation
case None => super.transform(tree)
}
}
+ case Apply(Select(lhs, withFilterName), List(predicate: Function)) if withFilterName.toString == "withFilter" && hasLStreamType(lhs) => {
+ val codeGen = new CodeGenerator(unit, currentOwner, tree.pos)
+
+ val Function(funValDefs, _) = predicate
+ assert(funValDefs.size == 1)
+ val constraintParamType = TypeTree(funValDefs.head.tpt.tpe match {
+ case TypeRef(_, sym, List(paramTpe)) if isLSym(sym) => paramTpe
+ case errorType => sys.error("unexpected type for withFilter predicate parameter: " + errorType)
+ })
+ val typeTreeList = List(constraintParamType, TypeTree(definitions.BooleanClass.tpe))
+
+ transformHelper(tree, predicate, codeGen) match {
+ case Some((serializedInputVarList, serializedOutputVars, serializedExpr, inputVarValues, arity)) => {
+ // create constraint instance
+ val termCode = codeGen.newBaseTerm(exprToScalaSym, serializedProg, serializedInputVarList, serializedOutputVars, serializedExpr, inputVarValues, NULL, typeTreeList, arity)
+ val code = (lhs DOT withFilter2Function) APPLY (Function(funValDefs,termCode) setSymbol predicate.symbol)
+
+ typer.typed(atOwner(currentOwner) {
+ code
+ })
+ }
+ case None => super.transform(tree)
+ }
+ }
// Insert generated method definitions
case cd @ ClassDef(mods, name, tparams, impl) if (cd.symbol.isModuleClass && tparams.isEmpty && !cd.symbol.isSynthetic) => {
diff --git a/src/cp/CodeExtraction.scala b/src/cp/CodeExtraction.scala
index 9794ea1ba..8953612d4 100644
--- a/src/cp/CodeExtraction.scala
+++ b/src/cp/CodeExtraction.scala
@@ -26,24 +26,29 @@ trait CodeExtraction extends Extractors {
private lazy val optionClassSym = definitions.getClass("scala.Option")
private lazy val someClassSym = definitions.getClass("scala.Some")
private lazy val function1TraitSym = definitions.getClass("scala.Function1")
+ private lazy val lClassSym = definitions.getClass("cp.LTrees.L")
- def isSetTraitSym(sym : Symbol) : Boolean = {
+ private def isLSym(sym: Symbol): Boolean = {
+ sym == lClassSym
+ }
+
+ def isSetTraitSym(sym: Symbol): Boolean = {
sym == setTraitSym || sym.tpe.toString.startsWith("scala.Predef.Set")
}
- def isMapTraitSym(sym : Symbol) : Boolean = {
+ def isMapTraitSym(sym: Symbol): Boolean = {
sym == mapTraitSym || sym.tpe.toString.startsWith("scala.Predef.Map")
}
- def isMultisetTraitSym(sym : Symbol) : Boolean = {
+ def isMultisetTraitSym(sym: Symbol): Boolean = {
sym == multisetTraitSym
}
- def isOptionClassSym(sym : Symbol) : Boolean = {
+ def isOptionClassSym(sym: Symbol): Boolean = {
sym == optionClassSym || sym == someClassSym
}
- def isFunction1TraitSym(sym : Symbol) : Boolean = {
+ def isFunction1TraitSym(sym: Symbol): Boolean = {
sym == function1TraitSym
}
@@ -54,9 +59,16 @@ trait CodeExtraction extends Extractors {
private val defsToDefs: scala.collection.mutable.Map[Symbol,FunDef] =
scala.collection.mutable.Map.empty[Symbol,FunDef]
+ /* Mapping from trees whose runtime values will be included in constraints to
+ * replace the corresponding fresh variable */
private val externalSubsts: scala.collection.mutable.Map[Tree,Function0[Expr]] =
scala.collection.mutable.Map.empty[Tree,Function0[Expr]]
+ /* Mapping from L[T] trees whose identifier will be included in constraints
+ * to replace the corresponding fresh variable */
+ private val lvarSubsts: scala.collection.mutable.Map[Tree,Function0[Expr]] =
+ scala.collection.mutable.Map.empty[Tree,Function0[Expr]]
+
def reverseVarSubsts: scala.collection.immutable.Map[Expr,Symbol] =
varSubsts.toMap.map{ case (a, b) => (b(), a) }
@@ -66,6 +78,9 @@ trait CodeExtraction extends Extractors {
def reverseExternalSubsts: scala.collection.immutable.Map[Expr,Tree] =
externalSubsts.toMap.map{ case (a, b) => (b(), a) }
+ def reverseLvarSubsts: scala.collection.immutable.Map[Expr, Tree] =
+ lvarSubsts.toMap.map{ case (a, b) => (b(), a) }
+
def variablesToTrees: scala.collection.immutable.Map[Expr,Tree] =
reverseExternalSubsts ++ (reverseVarSubsts.map{ case (a, b) => (a, Ident(b)) })
@@ -123,7 +138,7 @@ trait CodeExtraction extends Extractors {
scala.collection.mutable.Set.empty[String]
// We first traverse for collecting type definitions
- def collectTypeDefinitions(inSpecObject : Boolean)(tree: Tree) : Unit = tree match {
+ def collectTypeDefinitions(inSpecObject: Boolean)(tree: Tree): Unit = tree match {
case cd @ ExAbstractClass(o2, sym) if inSpecObject || cd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
if(scalaClassNames.contains(o2)) {
unit.error(tree.pos, "A class with the same name already exists.")
@@ -193,7 +208,7 @@ trait CodeExtraction extends Extractors {
// end of class (type) extraction
// Let us now collect function signatures
- def collectFunctionSignatures(inSpecObject : Boolean)(tree: Tree) : Unit = tree match {
+ def collectFunctionSignatures(inSpecObject: Boolean)(tree: Tree): Unit = tree match {
case dd @ ExFunctionDef(n,p,t,b) if inSpecObject || dd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
val mods = dd.mods
val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
@@ -214,7 +229,7 @@ trait CodeExtraction extends Extractors {
new ForeachTreeTraverser(collectFunctionSignatures(false)).traverse(unit.body)
// And finally extract function bodies
- def extractFunctionBodies(inSpecObject : Boolean)(tree: Tree) : Unit = tree match {
+ def extractFunctionBodies(inSpecObject: Boolean)(tree: Tree): Unit = tree match {
case dd @ ExFunctionDef(n,p,t,b) if inSpecObject || dd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
val fd = defsToDefs(dd.symbol)
defsToDefs(dd.symbol) = extractFunDef(fd, b)
@@ -272,14 +287,14 @@ trait CodeExtraction extends Extractors {
case _ => ;
}
- val extractedBody = scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies, false)(realBody)
+ val extractedBody = scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies, false, false)(realBody)
funDef.body = Some(extractedBody)
funDef.precondition = reqCont
funDef.postcondition = ensCont
// We need to make sure that functions don't use outer variables
- val argIDs : Set[Identifier] = funDef.args.map(_.id).toSet
+ val argIDs: Set[Identifier] = funDef.args.map(_.id).toSet
if (!(variablesOf(extractedBody) subsetOf argIDs)) {
unit.error(body.pos, "Function uses variables that are not among its arguments")
throw new ImpureCodeEncounteredException(body)
@@ -306,260 +321,281 @@ trait CodeExtraction extends Extractors {
}
/** Old method for extracting one object definition */
- def extractWellStructuredCode(unit: CompilationUnit): Program = {
- import scala.collection.mutable.HashMap
-
- def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
- case Some(ex) => ex
- case None => stopIfErrors; scala.sys.error("unreachable error.")
- }
-
- def st2ps(tree: Type): purescala.TypeTrees.TypeTree = toPureScalaType(unit)(tree) match {
- case Some(tt) => tt
- case None => stopIfErrors; scala.sys.error("unreachable error.")
- }
-
- def extractTopLevelDef: ObjectDef = {
- val top = unit.body match {
- case p @ PackageDef(name, lst) if lst.size == 0 => {
- unit.error(p.pos, "No top-level definition found.")
- None
- }
-
- case PackageDef(name, lst) if lst.size > 1 => {
- unit.error(lst(1).pos, "Too many top-level definitions.")
- None
- }
-
- case PackageDef(name, lst) => {
- assert(lst.size == 1)
- lst(0) match {
- case ExObjectDef(n, templ) => Some(extractObjectDef(n.toString, templ))
- case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
- None
- }
- }
- }
-
- stopIfErrors
- top.get
- }
-
- def extractObjectDef(nameStr: String, tmpl: Template): ObjectDef = {
- // we assume that the template actually corresponds to an object
- // definition. Typically it should have been obtained from the proper
- // extractor (ExObjectDef)
-
- var classDefs: List[ClassTypeDef] = Nil
- var objectDefs: List[ObjectDef] = Nil
- var funDefs: List[FunDef] = Nil
-
- val scalaClassSyms: scala.collection.mutable.Map[Symbol,Identifier] =
- scala.collection.mutable.Map.empty[Symbol,Identifier]
- val scalaClassArgs: scala.collection.mutable.Map[Symbol,Seq[(String,Tree)]] =
- scala.collection.mutable.Map.empty[Symbol,Seq[(String,Tree)]]
- val scalaClassNames: scala.collection.mutable.Set[String] =
- scala.collection.mutable.Set.empty[String]
-
- // we need the new type definitions before we can do anything...
- tmpl.body.foreach(t =>
- t match {
- case cd @ ExAbstractClass(o2, sym) if cd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
- if(scalaClassNames.contains(o2)) {
- unit.error(t.pos, "A class with the same name already exists.")
- } else {
- scalaClassSyms += (sym -> FreshIdentifier(o2))
- scalaClassNames += o2
- }
- }
- case cd @ ExCaseClass(o2, sym, args) if cd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
- if(scalaClassNames.contains(o2)) {
- unit.error(t.pos, "A class with the same name already exists.")
- } else {
- scalaClassSyms += (sym -> FreshIdentifier(o2))
- scalaClassNames += o2
- scalaClassArgs += (sym -> args)
- }
- }
- case _ => ;
- }
- )
-
- stopIfErrors
-
-
- scalaClassSyms.foreach(p => {
- if(p._1.isAbstractClass) {
- classesToClasses += (p._1 -> new AbstractClassDef(p._2))
- } else if(p._1.isCase) {
- classesToClasses += (p._1 -> new CaseClassDef(p._2))
- }
- })
-
- classesToClasses.foreach(p => {
- val superC: List[ClassTypeDef] = p._1.tpe.baseClasses.filter(bcs => scalaClassSyms.exists(pp => pp._1 == bcs) && bcs != p._1).map(s => classesToClasses(s)).toList
-
- val superAC: List[AbstractClassDef] = superC.map(c => {
- if(!c.isInstanceOf[AbstractClassDef]) {
- unit.error(p._1.pos, "Class is inheriting from non-abstract class.")
- null
- } else {
- c.asInstanceOf[AbstractClassDef]
- }
- }).filter(_ != null)
-
- if(superAC.length > 1) {
- unit.error(p._1.pos, "Multiple inheritance.")
- }
-
- if(superAC.length == 1) {
- p._2.setParent(superAC.head)
- }
-
- if(p._2.isInstanceOf[CaseClassDef]) {
- // this should never fail
- val ccargs = scalaClassArgs(p._1)
- p._2.asInstanceOf[CaseClassDef].fields = ccargs.map(cca => {
- val cctpe = st2ps(cca._2.tpe)
- VarDecl(FreshIdentifier(cca._1).setType(cctpe), cctpe)
- })
- }
- })
-
- classDefs = classesToClasses.valuesIterator.toList
-
- // end of class (type) extraction
-
- // we now extract the function signatures.
- tmpl.body.foreach(
- _ match {
- case ExMainFunctionDef() => ;
- case dd @ ExFunctionDef(n,p,t,b) if dd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
- val mods = dd.mods
- val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
- if(mods.isPrivate) funDef.addAnnotation("private")
- for(a <- dd.symbol.annotations) {
- a.atp.safeToString match {
- case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
- case "funcheck.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
- case _ => ;
- }
- }
- defsToDefs += (dd.symbol -> funDef)
- }
- case _ => ;
- }
- )
-
- // then their bodies.
- tmpl.body.foreach(
- _ match {
- case ExMainFunctionDef() => ;
- case dd @ ExFunctionDef(n,p,t,b) if dd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
- val fd = defsToDefs(dd.symbol)
- defsToDefs(dd.symbol) = extractFunDef(fd, b)
- }
- case _ => ;
- }
- )
-
- funDefs = defsToDefs.valuesIterator.toList
-
- /*
- // we check nothing else is polluting the object.
- tmpl.body.foreach(
- _ match {
- case ExCaseClassSyntheticJunk() => ;
- // case ExObjectDef(o2, t2) => { objectDefs = extractObjectDef(o2, t2) :: objectDefs }
- case ExAbstractClass(_,_) => ;
- case ExCaseClass(_,_,_) => ;
- case ExConstructorDef() => ;
- case ExMainFunctionDef() => ;
- case ExFunctionDef(_,_,_,_) => ;
- case tree => { unit.error(tree.pos, "Don't know what to do with this. Not purescala?"); println(tree) }
- }
- )
- */
-
- val name: Identifier = FreshIdentifier(nameStr)
- val theDef = new ObjectDef(name, objectDefs.reverse ::: classDefs ::: funDefs, Nil)
-
- theDef
- }
-
- def extractFunSig(nameStr: String, params: Seq[ValDef], tpt: Tree): FunDef = {
- val newParams = params.map(p => {
- val ptpe = st2ps(p.tpt.tpe)
- val newID = FreshIdentifier(p.name.toString).setType(ptpe)
- varSubsts(p.symbol) = (() => Variable(newID))
- VarDecl(newID, ptpe)
- })
- new FunDef(FreshIdentifier(nameStr), st2ps(tpt.tpe), newParams)
- }
-
- def extractFunDef(funDef: FunDef, body: Tree): FunDef = {
- var realBody = body
- var reqCont: Option[Expr] = None
- var ensCont: Option[Expr] = None
-
- realBody match {
- case ExEnsuredExpression(body2, resSym, contract) => {
- varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
- val c1 = s2ps(contract)
- // varSubsts.remove(resSym)
- realBody = body2
- ensCont = Some(c1)
- }
- case ExHoldsExpression(body2) => {
- realBody = body2
- ensCont = Some(ResultVariable().setType(BooleanType))
- }
- case _ => ;
- }
-
- realBody match {
- case ExRequiredExpression(body3, contract) => {
- realBody = body3
- reqCont = Some(s2ps(contract))
- }
- case _ => ;
- }
-
- val bodyAttempt = try {
- Some(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies, false)(realBody))
+ // def extractWellStructuredCode(unit: CompilationUnit): Program = {
+ // import scala.collection.mutable.HashMap
+
+ // def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
+ // case Some(ex) => ex
+ // case None => stopIfErrors; scala.sys.error("unreachable error.")
+ // }
+
+ // def st2ps(tree: Type): purescala.TypeTrees.TypeTree = toPureScalaType(unit)(tree) match {
+ // case Some(tt) => tt
+ // case None => stopIfErrors; scala.sys.error("unreachable error.")
+ // }
+
+ // def extractTopLevelDef: ObjectDef = {
+ // val top = unit.body match {
+ // case p @ PackageDef(name, lst) if lst.size == 0 => {
+ // unit.error(p.pos, "No top-level definition found.")
+ // None
+ // }
+
+ // case PackageDef(name, lst) if lst.size > 1 => {
+ // unit.error(lst(1).pos, "Too many top-level definitions.")
+ // None
+ // }
+
+ // case PackageDef(name, lst) => {
+ // assert(lst.size == 1)
+ // lst(0) match {
+ // case ExObjectDef(n, templ) => Some(extractObjectDef(n.toString, templ))
+ // case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
+ // None
+ // }
+ // }
+ // }
+
+ // stopIfErrors
+ // top.get
+ // }
+
+ // def extractObjectDef(nameStr: String, tmpl: Template): ObjectDef = {
+ // // we assume that the template actually corresponds to an object
+ // // definition. Typically it should have been obtained from the proper
+ // // extractor (ExObjectDef)
+
+ // var classDefs: List[ClassTypeDef] = Nil
+ // var objectDefs: List[ObjectDef] = Nil
+ // var funDefs: List[FunDef] = Nil
+
+ // val scalaClassSyms: scala.collection.mutable.Map[Symbol,Identifier] =
+ // scala.collection.mutable.Map.empty[Symbol,Identifier]
+ // val scalaClassArgs: scala.collection.mutable.Map[Symbol,Seq[(String,Tree)]] =
+ // scala.collection.mutable.Map.empty[Symbol,Seq[(String,Tree)]]
+ // val scalaClassNames: scala.collection.mutable.Set[String] =
+ // scala.collection.mutable.Set.empty[String]
+
+ // // we need the new type definitions before we can do anything...
+ // tmpl.body.foreach(t =>
+ // t match {
+ // case cd @ ExAbstractClass(o2, sym) if cd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
+ // if(scalaClassNames.contains(o2)) {
+ // unit.error(t.pos, "A class with the same name already exists.")
+ // } else {
+ // scalaClassSyms += (sym -> FreshIdentifier(o2))
+ // scalaClassNames += o2
+ // }
+ // }
+ // case cd @ ExCaseClass(o2, sym, args) if cd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
+ // if(scalaClassNames.contains(o2)) {
+ // unit.error(t.pos, "A class with the same name already exists.")
+ // } else {
+ // scalaClassSyms += (sym -> FreshIdentifier(o2))
+ // scalaClassNames += o2
+ // scalaClassArgs += (sym -> args)
+ // }
+ // }
+ // case _ => ;
+ // }
+ // )
+
+ // stopIfErrors
+
+
+ // scalaClassSyms.foreach(p => {
+ // if(p._1.isAbstractClass) {
+ // classesToClasses += (p._1 -> new AbstractClassDef(p._2))
+ // } else if(p._1.isCase) {
+ // classesToClasses += (p._1 -> new CaseClassDef(p._2))
+ // }
+ // })
+
+ // classesToClasses.foreach(p => {
+ // val superC: List[ClassTypeDef] = p._1.tpe.baseClasses.filter(bcs => scalaClassSyms.exists(pp => pp._1 == bcs) && bcs != p._1).map(s => classesToClasses(s)).toList
+
+ // val superAC: List[AbstractClassDef] = superC.map(c => {
+ // if(!c.isInstanceOf[AbstractClassDef]) {
+ // unit.error(p._1.pos, "Class is inheriting from non-abstract class.")
+ // null
+ // } else {
+ // c.asInstanceOf[AbstractClassDef]
+ // }
+ // }).filter(_ != null)
+
+ // if(superAC.length > 1) {
+ // unit.error(p._1.pos, "Multiple inheritance.")
+ // }
+
+ // if(superAC.length == 1) {
+ // p._2.setParent(superAC.head)
+ // }
+
+ // if(p._2.isInstanceOf[CaseClassDef]) {
+ // // this should never fail
+ // val ccargs = scalaClassArgs(p._1)
+ // p._2.asInstanceOf[CaseClassDef].fields = ccargs.map(cca => {
+ // val cctpe = st2ps(cca._2.tpe)
+ // VarDecl(FreshIdentifier(cca._1).setType(cctpe), cctpe)
+ // })
+ // }
+ // })
+
+ // classDefs = classesToClasses.valuesIterator.toList
+ //
+ // // end of class (type) extraction
+
+ // // we now extract the function signatures.
+ // tmpl.body.foreach(
+ // _ match {
+ // case ExMainFunctionDef() => ;
+ // case dd @ ExFunctionDef(n,p,t,b) if dd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
+ // val mods = dd.mods
+ // val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
+ // if(mods.isPrivate) funDef.addAnnotation("private")
+ // for(a <- dd.symbol.annotations) {
+ // a.atp.safeToString match {
+ // case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
+ // case "funcheck.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
+ // case _ => ;
+ // }
+ // }
+ // defsToDefs += (dd.symbol -> funDef)
+ // }
+ // case _ => ;
+ // }
+ // )
+
+ // // then their bodies.
+ // tmpl.body.foreach(
+ // _ match {
+ // case ExMainFunctionDef() => ;
+ // case dd @ ExFunctionDef(n,p,t,b) if dd.symbol.annotations.exists(_.atp.safeToString == "cp.Definitions.spec") => {
+ // val fd = defsToDefs(dd.symbol)
+ // defsToDefs(dd.symbol) = extractFunDef(fd, b)
+ // }
+ // case _ => ;
+ // }
+ // )
+
+ // funDefs = defsToDefs.valuesIterator.toList
+
+ // /*
+ // // we check nothing else is polluting the object.
+ // tmpl.body.foreach(
+ // _ match {
+ // case ExCaseClassSyntheticJunk() => ;
+ // // case ExObjectDef(o2, t2) => { objectDefs = extractObjectDef(o2, t2) :: objectDefs }
+ // case ExAbstractClass(_,_) => ;
+ // case ExCaseClass(_,_,_) => ;
+ // case ExConstructorDef() => ;
+ // case ExMainFunctionDef() => ;
+ // case ExFunctionDef(_,_,_,_) => ;
+ // case tree => { unit.error(tree.pos, "Don't know what to do with this. Not purescala?"); println(tree) }
+ // }
+ // )
+ // */
+
+ // val name: Identifier = FreshIdentifier(nameStr)
+ // val theDef = new ObjectDef(name, objectDefs.reverse ::: classDefs ::: funDefs, Nil)
+ //
+ // theDef
+ // }
+
+ // def extractFunSig(nameStr: String, params: Seq[ValDef], tpt: Tree): FunDef = {
+ // val newParams = params.map(p => {
+ // val ptpe = st2ps(p.tpt.tpe)
+ // val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ // varSubsts(p.symbol) = (() => Variable(newID))
+ // VarDecl(newID, ptpe)
+ // })
+ // new FunDef(FreshIdentifier(nameStr), st2ps(tpt.tpe), newParams)
+ // }
+
+ // def extractFunDef(funDef: FunDef, body: Tree): FunDef = {
+ // var realBody = body
+ // var reqCont: Option[Expr] = None
+ // var ensCont: Option[Expr] = None
+
+ // realBody match {
+ // case ExEnsuredExpression(body2, resSym, contract) => {
+ // varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
+ // val c1 = s2ps(contract)
+ // // varSubsts.remove(resSym)
+ // realBody = body2
+ // ensCont = Some(c1)
+ // }
+ // case ExHoldsExpression(body2) => {
+ // realBody = body2
+ // ensCont = Some(ResultVariable().setType(BooleanType))
+ // }
+ // case _ => ;
+ // }
+
+ // realBody match {
+ // case ExRequiredExpression(body3, contract) => {
+ // realBody = body3
+ // reqCont = Some(s2ps(contract))
+ // }
+ // case _ => ;
+ // }
+ //
+ // val bodyAttempt = try {
+ // Some(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies, false)(realBody))
+ // } catch {
+ // case e: ImpureCodeEncounteredException => None
+ // }
+
+ // funDef.body = bodyAttempt
+ // funDef.precondition = reqCont
+ // funDef.postcondition = ensCont
+ // funDef
+ // }
+
+ // // THE EXTRACTION CODE STARTS HERE
+ // val topLevelObjDef: ObjectDef = extractTopLevelDef
+
+ // stopIfErrors
+
+ // val programName: Identifier = unit.body match {
+ // case PackageDef(name, _) => FreshIdentifier(name.toString)
+ // case _ => FreshIdentifier("<program>")
+ // }
+
+ // //Program(programName, ObjectDef("Object", Nil, Nil))
+ // Program(programName, topLevelObjDef)
+ // }
+
+ /* Extract a constraint without L variables */
+ def extractStandardConstraint(unit: CompilationUnit, params: Seq[ValDef], body: Tree): FunDef = {
+ def st2ps(tree: Type): purescala.TypeTrees.TypeTree = {
+ try {
+ scalaType2PureScala(unit, false)(tree)
} catch {
- case e: ImpureCodeEncounteredException => None
+ case ImpureCodeEncounteredException(_) => stopIfErrors; scala.sys.error("unreachable error.")
}
-
- funDef.body = bodyAttempt
- funDef.precondition = reqCont
- funDef.postcondition = ensCont
- funDef
}
- // THE EXTRACTION CODE STARTS HERE
- val topLevelObjDef: ObjectDef = extractTopLevelDef
+ var realBody: Tree = body
+
+ val newParams = params.map(p => {
+ val ptpe = st2ps(p.tpt.tpe)
+ val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ varSubsts(p.symbol) = (() => Variable(newID))
+ VarDecl(newID, ptpe)
+ })
+ val fd = new FunDef(FreshIdentifier("function"), BooleanType, newParams)
stopIfErrors
- val programName: Identifier = unit.body match {
- case PackageDef(name, _) => FreshIdentifier(name.toString)
- case _ => FreshIdentifier("<program>")
- }
+ val bodyAttempt = try { Some(scala2PureScala(unit, false, true, false)(realBody)) } catch { case ImpureCodeEncounteredException(_) => None }
+ fd.body = bodyAttempt
- //Program(programName, ObjectDef("Object", Nil, Nil))
- Program(programName, topLevelObjDef)
+ fd
}
- def extractFunction(unit: CompilationUnit, params: Seq[ValDef], body: Tree) : FunDef = {
- def s2ps(tree: Tree): Expr = {
- try {
- scala2PureScala(unit, false, true)(tree)
- } catch {
- case ImpureCodeEncounteredException(_) => stopIfErrors; scala.sys.error("unreachable error.")
- }
- }
-
+ /* Extract a constraint with L variables */
+ def extractConstraintWithLVars(unit: CompilationUnit, params: Seq[ValDef], body: Tree): FunDef = {
def st2ps(tree: Type): purescala.TypeTrees.TypeTree = {
try {
scalaType2PureScala(unit, false)(tree)
@@ -568,10 +604,11 @@ trait CodeExtraction extends Extractors {
}
}
- var realBody : Tree = body
-
val newParams = params.map(p => {
- val ptpe = st2ps(p.tpt.tpe)
+ val ptpe = st2ps(p.tpt.tpe match {
+ case TypeRef(_, sym, List(paramTpe)) if isLSym(sym) => paramTpe
+ case errorType => sys.error("unexpected type for withFilter predicate parameter: " + errorType)
+ })
val newID = FreshIdentifier(p.name.toString).setType(ptpe)
varSubsts(p.symbol) = (() => Variable(newID))
VarDecl(newID, ptpe)
@@ -580,7 +617,7 @@ trait CodeExtraction extends Extractors {
stopIfErrors
- val bodyAttempt = try { Some(scala2PureScala(unit, false, true)(realBody)) } catch { case ImpureCodeEncounteredException(_) => None }
+ val bodyAttempt = try { Some(scala2PureScala(unit, false, true, true)(body)) } catch { case ImpureCodeEncounteredException(_) => None }
fd.body = bodyAttempt
fd
@@ -592,7 +629,7 @@ trait CodeExtraction extends Extractors {
/** Attempts to convert a scalac AST to a pure scala AST. */
def toPureScala(unit: CompilationUnit)(tree: Tree): Option[Expr] = {
try {
- Some(scala2PureScala(unit, false, false)(tree))
+ Some(scala2PureScala(unit, false, false, false)(tree))
} catch {
case ImpureCodeEncounteredException(_) => None
}
@@ -609,7 +646,7 @@ trait CodeExtraction extends Extractors {
/** Forces conversion from scalac AST to purescala AST, throws an Exception
* if impossible. If not in 'silent mode', non-pure AST nodes are reported as
* errors. */
- private def scala2PureScala(unit: CompilationUnit, silent: Boolean, tolerant: Boolean)(tree: Tree): Expr = {
+ private def scala2PureScala(unit: CompilationUnit, silent: Boolean, tolerant: Boolean, convertForced: Boolean)(tree: Tree): Expr = {
def rewriteCaseDef(cd: CaseDef): MatchCase = {
def pat2pat(p: Tree): Pattern = p match {
case Ident(nme.WILDCARD) => WildcardPattern(None)
@@ -880,6 +917,12 @@ trait CodeExtraction extends Extractors {
val tpe = scalaType2PureScala(unit, silent)(tt.tpe)
Distinct(args.map(rec(_))).setType(BooleanType)
}
+ case ExForceCall(tt, arg) if convertForced => {
+ val tpe = scalaType2PureScala(unit, silent)(tt.tpe)
+ val newID = FreshIdentifier("lvar", true).setType(tpe)
+ lvarSubsts(arg) = (() => Variable(newID))
+ Variable(newID)
+ }
case lc @ ExMethodCall(sy,nm,ar) => {
if(defsToDefs.keysIterator.find(_ == sy).isEmpty && !tolerant) {
if(!silent)
@@ -889,7 +932,7 @@ trait CodeExtraction extends Extractors {
val varTpe = scalaType2PureScala(unit, silent)(lc.tpe)
val newID = FreshIdentifier(nm).setType(varTpe)
externalSubsts(tr) = (() => Variable(newID))
- // println("new mapping : " + tr + " --> " + newID)
+ // println("new mapping: " + tr + " --> " + newID)
Variable(newID)
} else {
val fd = defsToDefs(sy)
@@ -977,7 +1020,7 @@ trait CodeExtraction extends Extractors {
rec(tree)
}
- def mkPosString(pos: scala.tools.nsc.util.Position) : String = {
+ def mkPosString(pos: scala.tools.nsc.util.Position): String = {
pos.line + "," + pos.column
}
}
diff --git a/src/cp/CodeGeneration.scala b/src/cp/CodeGeneration.scala
index 9ffea7e07..72ffcbc9a 100644
--- a/src/cp/CodeGeneration.scala
+++ b/src/cp/CodeGeneration.scala
@@ -37,17 +37,10 @@ trait CodeGeneration {
private lazy val cpPackage = definitions.getModule("cp")
private lazy val runtimeMethodsModule = definitions.getModule("cp.RuntimeMethods")
- private lazy val chooseExecFunction = definitions.getMember(runtimeMethodsModule, "chooseExec")
- private lazy val chooseMinimizingExecFunction = definitions.getMember(runtimeMethodsModule, "chooseMinimizingExec")
- private lazy val chooseMaximizingExecFunction = definitions.getMember(runtimeMethodsModule, "chooseMaximizingExec")
- private lazy val findMinimizingExecFunction = definitions.getMember(runtimeMethodsModule, "findMinimizingExec")
- private lazy val findMaximizingExecFunction = definitions.getMember(runtimeMethodsModule, "findMaximizingExec")
- private lazy val findExecFunction = definitions.getMember(runtimeMethodsModule, "findExec")
- private lazy val findAllExecFunction = definitions.getMember(runtimeMethodsModule, "findAllExec")
- private lazy val findAllMinimizingExecFunction = definitions.getMember(runtimeMethodsModule, "findAllMinimizingExec")
private lazy val inputVarFunction = definitions.getMember(runtimeMethodsModule, "inputVar")
private lazy val skipCounterFunction = definitions.getMember(runtimeMethodsModule, "skipCounter")
private lazy val copySettingsFunction = definitions.getMember(runtimeMethodsModule, "copySettings")
+ private lazy val variableFromLFunction = definitions.getMember(runtimeMethodsModule, "variableFromL")
private lazy val converterClass = definitions.getClass("cp.Converter")
@@ -245,12 +238,14 @@ trait CodeGeneration {
(DEF(methodSym) === matchExpr, methodSym)
}
- def inputVarValues(serializedInputVarList : Serialized, inputVars : Seq[Identifier], scalaToExprSym : Symbol) : Tree = {
+ /* Generates list of values that will replace the specified serialized input variables in a constraint */
+ def inputVarValues(serializedInputVarList : Serialized, inputVars : Seq[Identifier], lVars : Seq[Identifier], scalaToExprSym : Symbol) : Tree = {
val inputVarTrees = inputVars.map((iv: Identifier) => scalaToExprSym APPLY variablesToTrees(Variable(iv))).toList
- (scalaPackage DOT collectionModule DOT immutableModule DOT definitions.ListModule DOT listModuleApplyFunction) APPLY (inputVarTrees)
+ val lvarConversionTrees = lVars.map((lid: Identifier) => variableFromLFunction APPLY reverseLvarSubsts(Variable(lid))).toList
+ (scalaPackage DOT collectionModule DOT immutableModule DOT definitions.ListModule DOT listModuleApplyFunction) APPLY (inputVarTrees ::: lvarConversionTrees)
}
- def newBaseTerm(exprToScalaSym : Symbol, serializedProg : Serialized, serializedInputVarList : Serialized, serializedOutputVars : Serialized, serializedExpr : Serialized, inputVarValues : Tree, function : Function, typeTreeList : List[Tree], arity : Int) : Tree = {
+ def newBaseTerm(exprToScalaSym : Symbol, serializedProg : Serialized, serializedInputVarList : Serialized, serializedOutputVars : Serialized, serializedExpr : Serialized, inputVarValues : Tree, function : Tree, typeTreeList : List[Tree], arity : Int) : Tree = {
TypeApply(
Ident(termModules(arity)), typeTreeList) APPLY(
newConverter(exprToScalaSym),
diff --git a/src/cp/ConstraintSolving.scala b/src/cp/ConstraintSolving.scala
index d019fc2bb..08224728d 100644
--- a/src/cp/ConstraintSolving.scala
+++ b/src/cp/ConstraintSolving.scala
@@ -108,7 +108,7 @@ object ConstraintSolving {
}
private def evaluator(constraint : Term[_,Boolean], ids : Seq[Identifier]) : Option[(Map[Identifier,Expr])=>Boolean] = {
- if (cp.Settings.useScalaEvaluator) {
+ if (cp.Settings.useScalaEvaluator && constraint.evaluator != null) {
Some((m : Map[Identifier,Expr]) => constraint.evaluator(ids.map(modelValue(_, m))))
} else None
}
diff --git a/src/cp/Extractors.scala b/src/cp/Extractors.scala
index b3f14e18d..c36dcf5c3 100644
--- a/src/cp/Extractors.scala
+++ b/src/cp/Extractors.scala
@@ -361,6 +361,16 @@ trait Extractors {
}
}
+ object ExForceCall {
+ def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
+ case Apply(
+ TypeApply(Select(Select(cpIdent, ltreesName), forceName), List(typeTree)),
+ List(arg)) if ltreesName.toString == "LTrees" && forceName.toString == "force" =>
+ Some((typeTree, arg))
+ case _ => None
+ }
+ }
+
// used for case classes selectors.
object ExParameterlessMethodCall {
def unapply(tree: Select): Option[(Tree,Name)] = tree match {
diff --git a/src/cp/LTrees.scala b/src/cp/LTrees.scala
index d9e42e9e0..028b83247 100644
--- a/src/cp/LTrees.scala
+++ b/src/cp/LTrees.scala
@@ -71,6 +71,9 @@ object LTrees {
lStream().withFilter(p)
}
+ def withFilter2(p: (L[T]) => Constraint[T]): FilterMonadic[L[T], Traversable[L[T]]] = {
+ throw new Exception()
+ }
}
implicit def lexpr2bool[T](l: LExpr[T]): Boolean = {
@@ -109,7 +112,7 @@ object LTrees {
def -(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Int] = LMinus(this, x)
def *(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Int] = LTimes(this, x)
def /(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Int] = LDivision(this, x)
- def <(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Boolean] = LLessThan(this, x)
+ // def <(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Boolean] = LLessThan(this, x)
def >(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Boolean] = LGreaterThan(this, x)
def <=(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Boolean] = LLessEquals(this, x)
def >=(x: LExpr[T])(implicit ev: LExpr[T] => LExpr[Int]): LExpr[Boolean] = LGreaterEquals(this, x)
diff --git a/src/cp/RuntimeMethods.scala b/src/cp/RuntimeMethods.scala
index 3747f96b1..784bfa6a9 100644
--- a/src/cp/RuntimeMethods.scala
+++ b/src/cp/RuntimeMethods.scala
@@ -6,6 +6,8 @@ object RuntimeMethods {
import Terms._
import Definitions.UnsatisfiableConstraintException
import Definitions.UnknownConstraintException
+ import LTrees._
+
import purescala.Definitions._
import purescala.Trees._
import purescala.Common._
@@ -112,4 +114,10 @@ object RuntimeMethods {
def inputVar(inputVarList : List[Variable], varName : String) : Variable = {
inputVarList.find(_.id.name == varName).getOrElse(scala.sys.error("Could not find input variable '" + varName + "' in list " + inputVarList))
}
+
+ def variableFromL[T](l: L[T]): Variable = {
+ val ids = l.ids
+ assert(ids.size == 1)
+ Variable(ids.head)
+ }
}
diff --git a/src/cp/Terms.scala b/src/cp/Terms.scala
index 862a114e8..c2b81de23 100644
--- a/src/cp/Terms.scala
+++ b/src/cp/Terms.scala
@@ -123,7 +123,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala1[T1] _
type t2c = (Term1[T1,R]) => Term1[T1,Boolean]
val scalaFunction : (T1) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1])
override def apply(x_0 : T1) : R = scalaFunction(x_0)
@@ -197,7 +197,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala2[T1,T2] _
type t2c = (Term2[T1,T2,R]) => Term2[T1,T2,Boolean]
val scalaFunction : (T1,T2) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2])
override def apply(x_0 : T1, x_1 : T2) : R = scalaFunction(x_0, x_1)
@@ -299,7 +299,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala3[T1,T2,T3] _
type t2c = (Term3[T1,T2,T3,R]) => Term3[T1,T2,T3,Boolean]
val scalaFunction : (T1,T2,T3) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3) : R = scalaFunction(x_0, x_1, x_2)
@@ -426,7 +426,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala4[T1,T2,T3,T4] _
type t2c = (Term4[T1,T2,T3,T4,R]) => Term4[T1,T2,T3,T4,Boolean]
val scalaFunction : (T1,T2,T3,T4) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4) : R = scalaFunction(x_0, x_1, x_2, x_3)
@@ -568,7 +568,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala5[T1,T2,T3,T4,T5] _
type t2c = (Term5[T1,T2,T3,T4,T5,R]) => Term5[T1,T2,T3,T4,T5,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4)
@@ -715,7 +715,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala6[T1,T2,T3,T4,T5,T6] _
type t2c = (Term6[T1,T2,T3,T4,T5,T6,R]) => Term6[T1,T2,T3,T4,T5,T6,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5)
@@ -857,7 +857,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala7[T1,T2,T3,T4,T5,T6,T7] _
type t2c = (Term7[T1,T2,T3,T4,T5,T6,T7,R]) => Term7[T1,T2,T3,T4,T5,T6,T7,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6,T7) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6, x_6 : T7) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5, x_6)
@@ -984,7 +984,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala8[T1,T2,T3,T4,T5,T6,T7,T8] _
type t2c = (Term8[T1,T2,T3,T4,T5,T6,T7,T8,R]) => Term8[T1,T2,T3,T4,T5,T6,T7,T8,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6,T7,T8) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7],converter.expr2scala(s(7)).asInstanceOf[T8])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7],converter.expr2scala(s(7)).asInstanceOf[T8])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6, x_6 : T7, x_7 : T8) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7)
@@ -1086,7 +1086,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala9[T1,T2,T3,T4,T5,T6,T7,T8,T9] _
type t2c = (Term9[T1,T2,T3,T4,T5,T6,T7,T8,T9,R]) => Term9[T1,T2,T3,T4,T5,T6,T7,T8,T9,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6,T7,T8,T9) => R
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7],converter.expr2scala(s(7)).asInstanceOf[T8],converter.expr2scala(s(8)).asInstanceOf[T9])
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7],converter.expr2scala(s(7)).asInstanceOf[T8],converter.expr2scala(s(8)).asInstanceOf[T9])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6, x_6 : T7, x_7 : T8, x_8 : T9) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8)
diff --git a/src/cp/Utils.scala b/src/cp/Utils.scala
index 7562b42af..3dad778ae 100644
--- a/src/cp/Utils.scala
+++ b/src/cp/Utils.scala
@@ -65,7 +65,7 @@ object Utils {
val convertingFunction = converterOf(this).exprSeq2scala%d[%s] _
type t2c = (%s) => %s
val scalaFunction : %s => %s
- val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(%s)
+ lazy val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(%s)
override def apply(%s) : R = scalaFunction(%s)
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index cb230b6dc..2fda697e7 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -340,11 +340,6 @@ object Trees {
val fixedType = BooleanType
}
- case class LogicalVariable(val id: Identifier, val solver: Extensions.Solver, var pushed: Seq[Expr]) extends Expr with Terminal {
- override def getType = id.getType
- override def setType(tt: TypeTree) = { id.setType(tt); this }
- }
-
object UnaryOperator {
def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
case Not(t) => Some((t,Not(_)))
--
GitLab