diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index f86908c749ed508c8ee350389a2d52a239b5511a..7f20b7195fbd670aeeff28c706aba16b296864ed 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -6,7 +6,7 @@ package codegen
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps.{simplestValue, matchToIfThenElse, collect, variablesOf, CollectorWithPaths}
+import purescala.ExprOps._
import purescala.Types._
import purescala.Constructors._
import purescala.Extractors._
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 2bc4a2bbc337b0e6952090627ccfb0257fb1d947..7ef36c23cfdbc5a540f8eb4b11f9dddc1012ba59 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -667,11 +667,11 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
None
}
case (up @ UnapplyPattern(ob, _, subs), scrut) =>
- e(FunctionInvocation(up.unapplyFun, Seq(scrut))) match {
- case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.Nil.get =>
+ e(functionInvocation(up.unapplyFun.fd, Seq(scrut))) match {
+ case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get =>
None
- case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Cons.get =>
- val res = subs zip unwrapTuple(arg, up.unapplyFun.returnType.isInstanceOf[TupleType]) map {
+ case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get =>
+ val res = subs zip unwrapTuple(arg, subs.size) map {
case (s,a) => matchesPattern(s,a)
}
if (res.forall(_.isDefined)) {
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index f9ef63bdd9ad8650d44877ad03ff109fbd387200..9cc6dd132036ffdde4a5ef70e2be87e6276f9f3c 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -252,12 +252,12 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
} else {
Stream()
}
- case (up @ UnapplyPattern(ob, _, subs), scrut) =>
- e(FunctionInvocation(up.unapplyFun, Seq(scrut))) flatMap {
- case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.Nil.get =>
+ case (UnapplyPattern(ob, unapplyFun, subs), scrut) =>
+ e(functionInvocation(unapplyFun.fd, Seq(scrut))) flatMap {
+ case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get =>
None
- case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Cons.get =>
- val subMaps = subs zip unwrapTuple(arg, up.unapplyFun.returnType.isInstanceOf[TupleType]) map {
+ case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get =>
+ val subMaps = subs zip unwrapTuple(arg, subs.size) map {
case (s,a) => matchesPattern(s,a)
}
cartesianProduct(subMaps).map( _.flatten.toMap ++ obind(ob, expr))
@@ -305,7 +305,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
Some(step(expr, es))
} catch {
case _: RuntimeError =>
- // EvalErrors stop the computation alltogether
+ // EvalErrors stop the computation altogether
None
}
}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 68a4f4bf3d93f3b94c1b71a10d55ab6121a1792d..dc4b7481cc545219455e6b4cbb8068f1ce04617d 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -528,9 +528,8 @@ trait ASTExtractors {
true
case _ => false
}
-
}
-
+
object ExDefaultValueFunction{
/** Matches a function that defines the default value of a parameter */
def unapply(dd: DefDef): Option[(Symbol, Seq[Symbol], Seq[ValDef], Type, String, Int, Tree)] = {
@@ -539,11 +538,11 @@ trait ASTExtractors {
case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
vparamss.size <= 1 && name != nme.CONSTRUCTOR && sym.isSynthetic
) =>
-
+
// Split the name into pieces, to find owner of the parameter + param.index
// Form has to be <owner name>$default$<param index>
val symPieces = sym.name.toString.reverse.split("\\$", 3).reverseMap(_.reverse)
-
+
try {
if (symPieces(1) != "default" || symPieces(0) == "copy") throw new IllegalArgumentException("")
val ownerString = symPieces(0)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 81d146863afcc9cf02e026ff582156567ff13eea..8c01b7731c2dd412d22da5816b6f6873ca0e0219 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -246,13 +246,13 @@ trait CodeExtraction extends ASTExtractors {
// ignore
None
- case t@ExAbstractClass(o2, sym, _) =>
+ case t @ ExAbstractClass(o2, sym, _) =>
Some(getClassDef(sym, t.pos))
- case t@ExCaseClass(o2, sym, args, _) =>
+ case t @ ExCaseClass(o2, sym, args, _) =>
Some(getClassDef(sym, t.pos))
- case t@ExObjectDef(n, templ) =>
+ case t @ ExObjectDef(n, templ) =>
// Module
val id = FreshIdentifier(n)
val leonDefs = templ.body.flatMap {
@@ -481,16 +481,31 @@ trait CodeExtraction extends ASTExtractors {
Nil
}
- val tparams = tparamsMap.map(t => TypeParameterDef(t._2))
-
- val defCtx = DefContext(tparamsMap.toMap)
-
val parent = sym.tpe.parents.headOption match {
case Some(TypeRef(_, parentSym, tps)) if seenClasses contains parentSym =>
getClassDef(parentSym, sym.pos) match {
case acd: AbstractClassDef =>
+ val defCtx = DefContext(tparamsMap.toMap)
val newTps = tps.map(extractType(_)(defCtx, sym.pos))
- Some(AbstractClassType(acd, newTps))
+ val zip = (newTps zip tparamsMap.map(_._2))
+ if (newTps.size != tparamsMap.size) {
+ outOfSubsetError(sym.pos, "Child classes should have the same number of type parameters as their parent")
+ None
+ } else if (zip.exists {
+ case (TypeParameter(_), _) => false
+ case _ => true
+ }) {
+ outOfSubsetError(sym.pos, "Child class type params should have a simple mapping to parent params")
+ None
+ } else if (zip.exists {
+ case (TypeParameter(id), ctp) => id.name != ctp.id.name
+ case _ => false
+ }) {
+ outOfSubsetError(sym.pos, "Child type params should be identical to parent class's (e.g. C[T1,T2] extends P[T1,T2])")
+ None
+ } else {
+ Some(acd.typed -> acd.tparams)
+ }
case cd =>
outOfSubsetError(sym.pos, s"Class $id cannot extend ${cd.id}")
@@ -501,11 +516,18 @@ trait CodeExtraction extends ASTExtractors {
None
}
+ val tparams = parent match {
+ case Some((p, tparams)) => tparams
+ case None => tparamsMap.map(t => TypeParameterDef(t._2))
+ }
+
+ val defCtx = DefContext((tparamsMap.map(_._1) zip tparams.map(_.tp)).toMap)
+
// Extract class
val cd = if (sym.isAbstractClass) {
- AbstractClassDef(id, tparams, parent)
+ AbstractClassDef(id, tparams, parent.map(_._1))
} else {
- CaseClassDef(id, tparams, parent, sym.isModuleClass)
+ CaseClassDef(id, tparams, parent.map(_._1), sym.isModuleClass)
}
cd.setPos(sym.pos)
//println(s"Registering $sym")
@@ -513,7 +535,7 @@ trait CodeExtraction extends ASTExtractors {
cd.addFlags(annotationsOf(sym).map { case (name, args) => ClassFlag.fromName(name, args) }.toSet)
// Register parent
- parent.foreach(_.classDef.registerChild(cd))
+ parent.map(_._1).foreach(_.classDef.registerChild(cd))
// Extract case class fields
cd match {
@@ -522,30 +544,14 @@ trait CodeExtraction extends ASTExtractors {
val fields = args.map { case (fsym, t) =>
val tpe = leonType(t.tpt.tpe)(defCtx, fsym.pos)
val id = cachedWithOverrides(fsym, Some(ccd), tpe)
- LeonValDef(id.setPos(t.pos), Some(tpe)).setPos(t.pos)
+ if (tpe != id.getType) println(tpe, id.getType)
+ LeonValDef(id.setPos(t.pos)).setPos(t.pos)
}
//println(s"Fields of $sym")
ccd.setFields(fields)
case _ =>
}
- // Validates type parameters
- parent foreach { pct =>
- if(pct.classDef.tparams.size == tparams.size) {
- val pcd = pct.classDef
- val ptps = pcd.tparams.map(_.tp)
-
- val targetType = AbstractClassType(pcd, ptps)
- val fromChild = cd.typed(ptps).parent.get
-
- if (fromChild != targetType) {
- outOfSubsetError(sym.pos, "Child type should form a simple bijection with parent class type (e.g. C[T1,T2] extends P[T1,T2])")
- }
- } else {
- outOfSubsetError(sym.pos, "Child classes should have the same number of type parameters as their parent")
- }
- }
-
//println(s"Body of $sym")
// We collect the methods and fields
@@ -629,9 +635,10 @@ trait CodeExtraction extends ASTExtractors {
val newParams = sym.info.paramss.flatten.map{ sym =>
val ptpe = leonType(sym.tpe)(nctx, sym.pos)
- val newID = FreshIdentifier(sym.name.toString, ptpe).setPos(sym.pos)
+ val tpe = if (sym.isByNameParam) FunctionType(Seq(), ptpe) else ptpe
+ val newID = FreshIdentifier(sym.name.toString, tpe).setPos(sym.pos)
owners += (newID -> None)
- LeonValDef(newID).setPos(sym.pos)
+ LeonValDef(newID, sym.isByNameParam).setPos(sym.pos)
}
val tparamsDef = tparams.map(t => TypeParameterDef(t._2))
@@ -768,8 +775,9 @@ trait CodeExtraction extends ASTExtractors {
vd.defaultValue = paramsToDefaultValues.get(s.symbol)
}
- val newVars = for ((s, vd) <- params zip funDef.params) yield {
- s.symbol -> (() => Variable(vd.id))
+ val newVars = for ((s, vd) <- params zip funDef.params) yield s.symbol -> {
+ if (s.symbol.isByNameParam) () => Application(Variable(vd.id), Seq())
+ else () => Variable(vd.id)
}
val fctx = dctx.withNewVars(newVars).copy(isExtern = funDef.annotations("extern"))
@@ -1084,11 +1092,11 @@ trait CodeExtraction extends ASTExtractors {
}
val restTree = rest match {
- case Some(rst) => {
+ case Some(rst) =>
val nctx = dctx.withNewVar(vs -> (() => Variable(newID)))
extractTree(rst)(nctx)
- }
- case None => UnitLiteral()
+ case None =>
+ UnitLiteral()
}
rest = None
@@ -1520,23 +1528,24 @@ trait CodeExtraction extends ASTExtractors {
val fd = getFunDef(sym, c.pos)
val newTps = tps.map(t => extractType(t))
+ val argsByName = (fd.params zip args).map(p => if (p._1.isLazy) Lambda(Seq(), p._2) else p._2)
- FunctionInvocation(fd.typed(newTps), args)
+ FunctionInvocation(fd.typed(newTps), argsByName)
case (IsTyped(rec, ct: ClassType), _, args) if isMethod(sym) =>
val fd = getFunDef(sym, c.pos)
val cd = methodToClass(fd)
val newTps = tps.map(t => extractType(t))
+ val argsByName = (fd.params zip args).map(p => if (p._1.isLazy) Lambda(Seq(), p._2) else p._2)
- MethodInvocation(rec, cd, fd.typed(newTps), args)
+ MethodInvocation(rec, cd, fd.typed(newTps), argsByName)
case (IsTyped(rec, ft: FunctionType), _, args) =>
application(rec, args)
- case (IsTyped(rec, cct: CaseClassType), name, Nil) if cct.fields.exists(_.id.name == name) =>
-
- val fieldID = cct.fields.find(_.id.name == name).get.id
+ case (IsTyped(rec, cct: CaseClassType), name, Nil) if cct.classDef.fields.exists(_.id.name == name) =>
+ val fieldID = cct.classDef.fields.find(_.id.name == name).get.id
caseClassSelector(cct, rec, fieldID)
@@ -1778,6 +1787,9 @@ trait CodeExtraction extends ASTExtractors {
case tpe if tpe == NothingClass.tpe =>
Untyped
+ case ct: ConstantType =>
+ extractType(ct.value.tpe)
+
case TypeRef(_, sym, _) if isBigIntSym(sym) =>
IntegerType
diff --git a/src/main/scala/leon/invariant/datastructure/DisjointSet.scala b/src/main/scala/leon/invariant/datastructure/DisjointSets.scala
similarity index 94%
rename from src/main/scala/leon/invariant/datastructure/DisjointSet.scala
rename to src/main/scala/leon/invariant/datastructure/DisjointSets.scala
index 4cab7291bfa58dd3d79993233251d7dd589e0019..003bb31d1233ce7ab3ad1fe0dbe775008ae7f806 100644
--- a/src/main/scala/leon/invariant/datastructure/DisjointSet.scala
+++ b/src/main/scala/leon/invariant/datastructure/DisjointSets.scala
@@ -1,8 +1,6 @@
package leon
package invariant.datastructure
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.annotation.migration
import scala.collection.mutable.{Map => MutableMap}
class DisjointSets[T] {
diff --git a/src/main/scala/leon/invariant/datastructure/Graph.scala b/src/main/scala/leon/invariant/datastructure/Graph.scala
index 484f04668c08a6b02f8acfd2db12b343e4b4c303..7262b4b4ef4932a89f76406ed49e4d5e00ee9be1 100644
--- a/src/main/scala/leon/invariant/datastructure/Graph.scala
+++ b/src/main/scala/leon/invariant/datastructure/Graph.scala
@@ -66,7 +66,7 @@ class DirectedGraph[T] {
}
})
}
- if (!queue.isEmpty) {
+ if (queue.nonEmpty) {
val (head :: tail) = queue
queue = tail
BFSReachRecur(head)
diff --git a/src/main/scala/leon/invariant/datastructure/Maps.scala b/src/main/scala/leon/invariant/datastructure/Maps.scala
index 777a79375d874588f3be108d702aa6dc8118df79..ca2dcb98e99f247651dfd1b8632c570630fce7f0 100644
--- a/src/main/scala/leon/invariant/datastructure/Maps.scala
+++ b/src/main/scala/leon/invariant/datastructure/Maps.scala
@@ -1,13 +1,6 @@
package leon
-package invariant.util
+package invariant.datastructure
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
import scala.annotation.tailrec
class MultiMap[A, B] extends scala.collection.mutable.HashMap[A, scala.collection.mutable.Set[B]] with scala.collection.mutable.MultiMap[A, B] {
diff --git a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala b/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
similarity index 92%
rename from src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
rename to src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
index 647616fce1bab0eb01182ad50d75c060ce4ff737..7a9605c922e21373abb6df06fe9d585a104da2ba 100644
--- a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
@@ -1,16 +1,13 @@
package leon
package invariant.engine
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
-import invariant.templateSolvers._
import transformations._
import invariant.structure.FunctionUtils._
-import transformations.InstUtil._
import leon.invariant.structure.Formula
import leon.invariant.structure.Call
import leon.invariant.util._
@@ -20,7 +17,6 @@ import leon.solvers.Model
import Util._
import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd: FunDef)
extends FunctionTemplateSolver {
@@ -183,23 +179,21 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd:
var timeTmpl: Option[Expr] = None
var recTmpl: Option[Expr] = None
var othersTmpls: Seq[Expr] = Seq[Expr]()
- tmplConjuncts.foreach(conj => {
- conj match {
- case Operator(Seq(lhs, _), _) if (tupleSelectToInst.contains(lhs)) =>
- tupleSelectToInst(lhs) match {
- case n if n == TPR.name =>
- tprTmpl = Some(conj)
- case n if n == Time.name =>
- timeTmpl = Some(conj)
- case n if n == Rec.name =>
- recTmpl = Some(conj)
- case _ =>
- othersTmpls = othersTmpls :+ conj
- }
- case _ =>
- othersTmpls = othersTmpls :+ conj
- }
- })
+ tmplConjuncts.foreach {
+ case conj@Operator(Seq(lhs, _), _) if (tupleSelectToInst.contains(lhs)) =>
+ tupleSelectToInst(lhs) match {
+ case n if n == TPR.name =>
+ tprTmpl = Some(conj)
+ case n if n == Time.name =>
+ timeTmpl = Some(conj)
+ case n if n == Rec.name =>
+ recTmpl = Some(conj)
+ case _ =>
+ othersTmpls = othersTmpls :+ conj
+ }
+ case conj =>
+ othersTmpls = othersTmpls :+ conj
+ }
(tprTmpl, recTmpl, timeTmpl, othersTmpls)
}
}
diff --git a/src/main/scala/leon/invariant/engine/ConstraintTracker.scala b/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
index 3058a267eceef7c5ec1aa537c4766bee15a93204..95927a66ad3bda803a329b61e284f854a94bfcb4 100644
--- a/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
+++ b/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
@@ -1,19 +1,8 @@
package leon
package invariant.engine
-import z3.scala._
-import purescala._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import evaluators._
-import java.io._
-
-import invariant.factories._
-import invariant.util._
import invariant.structure._
class ConstraintTracker(ctx : InferenceContext, program: Program, rootFun : FunDef/*, temFactory: TemplateFactory*/) {
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index e79926e62158a095b755b48db43c8f3e46c41590..3ef178a03095a74dc8233dfd1ec3739abbdb3cef 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -1,21 +1,7 @@
package leon
package invariant.engine
-import purescala.Common._
import purescala.Definitions._
-import purescala.ExprOps._
-import purescala.Expressions._
-import purescala.Extractors._
-import purescala.Types._
-import verification.VerificationReport
-import invariant.templateSolvers._
-import invariant.factories._
-import invariant.util._
-import invariant.structure.FunctionUtils._
-import invariant.structure._
-import transformations._
-import leon.purescala.ScalaPrinter
-import leon.purescala.PrettyPrinter
/**
* @author ravi
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index b735cb8de7101f3bf109c6318cc7a05c571ba4b7..a6cdc317d1fcd17aba9abaa5199975e664ada9bf 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -12,7 +12,6 @@ import invariant.util._
import verification._
import verification.VCKinds
import InferInvariantsPhase._
-import Util._
import ProgramUtil._
/**
@@ -71,13 +70,13 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
instrumentedProg.definedFunctions.foreach((fd) => {
if (!foundStrongest && fd.hasPostcondition) {
val cond = fd.postcondition.get
- postTraversal((e) => e match {
+ postTraversal {
case Equals(_, _) => {
rel = Equals.apply _
foundStrongest = true
}
case _ => ;
- })(cond)
+ }(cond)
}
})
rel
diff --git a/src/main/scala/leon/invariant/engine/InferenceEngine.scala b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
index 85491acf1924560e5fe020a38176b513da989690..6ca6ef6327d00465bbbe5141bd69b6ce1e6338a6 100644
--- a/src/main/scala/leon/invariant/engine/InferenceEngine.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
@@ -1,31 +1,18 @@
package leon
package invariant.engine
-import z3.scala._
-import purescala.Common._
import purescala.Definitions._
-import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import solvers._
import java.io._
-import verification.VerificationReport
import verification.VC
import scala.util.control.Breaks._
-import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
-import invariant.util.Util._
-import invariant.structure._
import invariant.structure.FunctionUtils._
-import leon.invariant.factories.TemplateFactory
import transformations._
import leon.utils._
import Util._
-import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
/**
* @author ravi
@@ -85,13 +72,13 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
} else {
var remFuncs = functionsToAnalyze
var b = 200
- var maxCegisBound = 200
+ val maxCegisBound = 200
breakable {
while (b <= maxCegisBound) {
Stats.updateCumStats(1, "CegisBoundsTried")
val succeededFuncs = analyseProgram(program, remFuncs, progressCallback)
remFuncs = remFuncs.filterNot(succeededFuncs.contains _)
- if (remFuncs.isEmpty) break;
+ if (remFuncs.isEmpty) break
b += 5 //increase bounds in steps of 5
}
//println("Inferrence did not succeeded for functions: " + remFuncs.map(_.id))
@@ -200,7 +187,7 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
first = false
ic
}
- progressCallback.map(cb => cb(inferCond))
+ progressCallback.foreach(cb => cb(inferCond))
}
val funsWithTemplates = inferredFuns.filter { fd =>
val origFd = functionByName(fd.id.name, startProg).get
diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index d5f0196278d04489f657940caf74e30009fd02b9..4b0fb349f591780da0856e4ccbbe7e49f30c8d83 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -9,8 +9,6 @@ import purescala.Expressions._
import purescala.ExprOps._
import purescala.Definitions._
import purescala.Common._
-import invariant.templateSolvers._
-import invariant.factories._
import invariant.util._
import invariant.structure._
import leon.transformations.InstUtil
@@ -18,7 +16,6 @@ import leon.purescala.PrettyPrinter
import Util._
import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
import FunctionUtils._
import purescala._
@@ -64,7 +61,7 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
"║ └─────────┘" + (" " * (size - 12)) + "║"
private def infoLine(str: String, size: Int): String = {
- "║ " + str + (" " * (size - str.size - 2)) + " ║"
+ "║ " + str + (" " * (size - str.length - 2)) + " ║"
}
private def fit(str: String, maxLength: Int): String = {
@@ -77,11 +74,11 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
private def funName(fd: FunDef) = InstUtil.userFunctionName(fd)
- override def summaryString: String = if (conditions.size > 0) {
- val maxTempSize = (conditions.map(_.status.size).max + 3)
+ override def summaryString: String = if (conditions.nonEmpty) {
+ val maxTempSize = (conditions.map(_.status.length).max + 3)
val outputStrs = conditions.map(vc => {
val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
- "%-15s %s %-4s".format(fit(funName(vc.fd), 15), vc.status + (" " * (maxTempSize - vc.status.size)), timeStr)
+ "%-15s %s %-4s".format(fit(funName(vc.fd), 15), vc.status + (" " * (maxTempSize - vc.status.length)), timeStr)
})
val summaryStr = {
val totalTime = conditions.foldLeft(0.0)((a, ic) => a + ic.time.getOrElse(0.0))
@@ -89,7 +86,7 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
"total: %-4d inferred: %-4d unknown: %-4d time: %-3.3f".format(
conditions.size, inferredConds, conditions.size - inferredConds, totalTime)
}
- val entrySize = (outputStrs :+ summaryStr).map(_.size).max + 2
+ val entrySize = (outputStrs :+ summaryStr).map(_.length).max + 2
infoHeader(entrySize) +
outputStrs.map(str => infoLine(str, entrySize)).mkString("\n", "\n", "\n") +
@@ -129,7 +126,7 @@ object InferenceReportUtil {
def fullNameWoInst(fd: FunDef) = {
val splits = DefOps.fullName(fd)(ctx.inferProgram).split("-")
- if (!splits.isEmpty) splits(0)
+ if (splits.nonEmpty) splits(0)
else ""
}
@@ -148,8 +145,8 @@ object InferenceReportUtil {
}
def mapExpr(ine: Expr): Expr = {
- val replaced = simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(TypedFunDef(fd, targs), args) =>
+ val replaced = simplePostTransform {
+ case e@FunctionInvocation(TypedFunDef(fd, targs), args) =>
if (initToOutput.contains(fd)) {
FunctionInvocation(TypedFunDef(initToOutput(fd), targs), args)
} else {
@@ -159,8 +156,8 @@ object InferenceReportUtil {
case _ => e
}
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
replaced
}
// copy bodies and specs
diff --git a/src/main/scala/leon/invariant/engine/SpecInstatiator.scala b/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
similarity index 100%
rename from src/main/scala/leon/invariant/engine/SpecInstatiator.scala
rename to src/main/scala/leon/invariant/engine/SpecInstantiator.scala
diff --git a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
index c568910684e89d78862a516583eb0baf31174888..1e717dbc1a23723680ecdffeb27b3f78553d1747 100644
--- a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
+++ b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
@@ -1,26 +1,15 @@
package leon
package invariant.engine
-import z3.scala._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet }
-import java.io._
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ Set => MutableSet }
-import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
-import invariant.structure._
-import Util._
-import PredicateUtil._
import ProgramUtil._
+import scala.collection.mutable.{Set => MutableSet}
/**
* An enumeration based template generator.
* Enumerates all numerical terms in some order (this enumeration is incomplete for termination).
@@ -126,7 +115,7 @@ class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr, Expr
if (fun != rootFun && !callGraph.transitivelyCalls(fun, rootFun)) {
//check if every argument has at least one satisfying assignment?
- if (fun.params.filter((vardecl) => !ttCurrent.contains(vardecl.getType)).isEmpty) {
+ if (!fun.params.exists((vardecl) => !ttCurrent.contains(vardecl.getType))) {
//here compute all the combinations
val newcalls = generateFunctionCalls(fun)
@@ -153,7 +142,7 @@ class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr, Expr
//return all the integer valued terms of newTerms
//++ newTerms.getOrElse(Int32Type, Seq[Expr]()) (for now not handling int 32 terms)
val numericTerms = (newTerms.getOrElse(RealType, Seq[Expr]()) ++ newTerms.getOrElse(IntegerType, Seq[Expr]())).toSeq
- if (!numericTerms.isEmpty) {
+ if (numericTerms.nonEmpty) {
//create a linear combination of intTerms
val newTemp = numericTerms.foldLeft(null: Expr)((acc, t: Expr) => {
val summand = Times(t, TemplateIdFactory.freshTemplateVar(): Expr)
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index 4bb5bbc3d76a341151ff9478b139f2ad8157485d..3fe13e7c93fefdfcc4321159b0fa7b354788a801 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -1,31 +1,24 @@
package leon
package invariant.engine
-import z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
import purescala.DefOps._
-import solvers._
-import solvers.z3.FairZ3Solver
-import java.io._
import purescala.ScalaPrinter
+
+import solvers._
import verification._
-import scala.reflect.runtime.universe
-import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
import invariant.structure._
import transformations._
import FunctionUtils._
-import leon.invariant.templateSolvers.ExtendedUFSolver
import Util._
import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
/**
* @author ravi
@@ -119,7 +112,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
case (Some(model), callsInPath) =>
toRefineCalls = callsInPath
//Validate the model here
- instantiateAndValidateModel(model, constTracker.getFuncs.toSeq)
+ instantiateAndValidateModel(model, constTracker.getFuncs)
Some(InferResult(true, Some(model),
constTracker.getFuncs.toList))
case (None, callsInPath) =>
@@ -129,7 +122,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
}
}
}
- } while (!infRes.isDefined)
+ } while (infRes.isEmpty)
infRes
}
@@ -227,7 +220,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
val resvar = FreshIdentifier("res", fd.returnType, true)
// FIXME: Is this correct (ResultVariable(fd.returnType) -> resvar.toVariable))
val ninv = replace(Map(ResultVariable(fd.returnType) -> resvar.toVariable), inv)
- Some(Lambda(Seq(ValDef(resvar, Some(fd.returnType))), ninv))
+ Some(Lambda(Seq(ValDef(resvar)), ninv))
}
} else if (fd.postcondition.isDefined) {
val Lambda(resultBinder, _) = fd.postcondition.get
diff --git a/src/main/scala/leon/invariant/factories/AxiomFactory.scala b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
index 6fdf7fa633def45017de8df5fbab4250ce70928e..907db46ab1cf1fbd4efcc19f58ae5867142575f6 100644
--- a/src/main/scala/leon/invariant/factories/AxiomFactory.scala
+++ b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
@@ -1,24 +1,13 @@
package leon
package invariant.factories
-import z3.scala._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import java.io._
-import leon.invariant._
-import scala.util.control.Breaks._
-import scala.concurrent._
-import scala.concurrent.duration._
import invariant.engine._
import invariant.util._
import invariant.structure._
import FunctionUtils._
-import Util._
import PredicateUtil._
class AxiomFactory(ctx : InferenceContext) {
@@ -85,7 +74,6 @@ class AxiomFactory(ctx : InferenceContext) {
//this is applicable only to binary operations
def undistributeCalls(call1: Call, call2: Call): (Expr,Expr) = {
- val fd = call1.fi.tfd.fd
val tfd = call1.fi.tfd
val Seq(a1,b1) = call1.fi.args
@@ -93,9 +81,7 @@ class AxiomFactory(ctx : InferenceContext) {
val r1 = call1.retexpr
val r2 = call2.retexpr
- val dret1 = TVarFactory.createTemp("dt", IntegerType).toVariable
val dret2 = TVarFactory.createTemp("dt", IntegerType).toVariable
- val dcall1 = Call(dret1, FunctionInvocation(tfd,Seq(a2,Plus(b1,b2))))
val dcall2 = Call(dret2, FunctionInvocation(tfd,Seq(Plus(a1,a2),b2)))
(LessEquals(b1,b2), And(LessEquals(Plus(r1,r2),dret2), dcall2.toExpr))
}
diff --git a/src/main/scala/leon/invariant/factories/TemplateFactory.scala b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
index ab1f51359151de13ef8cd506f4f1c9da9472c208..b44fcfa684d66168cad5de3e0cca7d8df5d11f50 100644
--- a/src/main/scala/leon/invariant/factories/TemplateFactory.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
@@ -1,23 +1,16 @@
package leon
package invariant.factories
-import z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import java.io._
-import scala.collection.mutable.{ Map => MutableMap }
-import invariant._
import scala.collection.mutable.{Map => MutableMap}
-import invariant.engine._
import invariant.util._
import invariant.structure._
import FunctionUtils._
-import Util._
import PredicateUtil._
import ProgramUtil._
@@ -28,7 +21,7 @@ object TemplateIdFactory {
def getTemplateIds : Set[Identifier] = ids
def freshIdentifier(name : String = "", idType: TypeTree = RealType) : Identifier = {
- val idname = if(name.isEmpty()) "a?"
+ val idname = if(name.isEmpty) "a?"
else name + "?"
val freshid = FreshIdentifier(idname, idType, true)
ids += freshid
@@ -72,7 +65,7 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
//a mapping from function definition to the template
private var templateMap = {
//initialize the template map with predefined user maps
- var muMap = MutableMap[FunDef, Expr]()
+ val muMap = MutableMap[FunDef, Expr]()
functionsWOFields(prog.definedFunctions).foreach { fd =>
val tmpl = fd.template
if (tmpl.isDefined) {
@@ -114,7 +107,7 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
//initialize the template for the function
if (!templateMap.contains(fd)) {
- if(!tempGen.isDefined) templateMap += (fd -> getDefaultTemplate(fd))
+ if(tempGen.isEmpty) templateMap += (fd -> getDefaultTemplate(fd))
else {
templateMap += (fd -> tempGen.get.getNextTemplate(fd))
refinementSet += fd
diff --git a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
index ccaabc57aabecb9fa22fd94a5972c1a554196729..dbcdc4c5e1a2de62fb5a1c1e81ebe17b4449a584 100644
--- a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
@@ -1,23 +1,15 @@
package leon
package invariant.factories
-import z3.scala._
-import purescala._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
-import java.io._
-import invariant.engine._
import invariant.util._
import invariant.structure._
import leon.solvers.Model
import leon.invariant.util.RealValuedExprEvaluator
-import Util._
import PredicateUtil._
-import ProgramUtil._
object TemplateInstantiator {
/**
@@ -51,17 +43,17 @@ object TemplateInstantiator {
*/
def instantiate(expr: Expr, tempVarMap: Map[Expr, Expr], prettyInv: Boolean = false): Expr = {
//do a simple post transform and replace the template vars by their values
- val inv = simplePostTransform((tempExpr: Expr) => tempExpr match {
- case e @ Operator(Seq(lhs, rhs), op) if ((e.isInstanceOf[Equals] || e.isInstanceOf[LessThan]
+ val inv = simplePostTransform {
+ case tempExpr@(e@Operator(Seq(lhs, rhs), op)) if ((e.isInstanceOf[Equals] || e.isInstanceOf[LessThan]
|| e.isInstanceOf[LessEquals] || e.isInstanceOf[GreaterThan]
|| e.isInstanceOf[GreaterEquals])
&&
- !getTemplateVars(tempExpr).isEmpty) => {
+ getTemplateVars(tempExpr).nonEmpty) => {
val linearTemp = LinearConstraintUtil.exprToTemplate(tempExpr)
instantiateTemplate(linearTemp, tempVarMap, prettyInv)
}
- case _ => tempExpr
- })(expr)
+ case tempExpr => tempExpr
+ }(expr)
inv
}
diff --git a/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala b/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
index 469317998a98f979a9a90770fd9c902544eee584..96c8d212a59cfc39c8cc428dc521f8e4a278a004 100644
--- a/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
@@ -1,12 +1,8 @@
package leon
package invariant.factories
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
import invariant._
import invariant.engine._
import invariant.util._
diff --git a/src/main/scala/leon/invariant/structure/Constraint.scala b/src/main/scala/leon/invariant/structure/Constraint.scala
index 9d2490fe5f8b61b6847636007c61d6ba3c0dba34..39fd20bca11971ba0feadf26e20331970f9a9ca7 100644
--- a/src/main/scala/leon/invariant/structure/Constraint.scala
+++ b/src/main/scala/leon/invariant/structure/Constraint.scala
@@ -1,23 +1,10 @@
package leon
package invariant.structure
-import z3.scala._
-import purescala._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import solvers.{ Solver, TimeoutSolver }
-import solvers.z3.FairZ3Solver
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ Map => MutableMap }
-import evaluators._
-import java.io._
-import solvers.z3.UninterpretedZ3Solver
import invariant.util._
-import Util._
import PredicateUtil._
trait Constraint {
@@ -42,9 +29,7 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
}
val coeffTemplate = {
//assert if the coefficients are templated expressions
- assert(coeffTemp.values.foldLeft(true)((acc, e) => {
- acc && isTemplateExpr(e)
- }))
+ assert(coeffTemp.values.forall(e => isTemplateExpr(e)))
coeffTemp
}
@@ -110,7 +95,7 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
rhsExprs :+= InfiniteIntegerLiteral(-v)
case Some(c) =>
lhsExprs :+= c
- case _ => Nil
+ case _ =>
}
val lhsExprOpt = ((None: Option[Expr]) /: lhsExprs) {
case (acc, minterm) =>
@@ -175,9 +160,7 @@ class LinearConstraint(opr: Seq[Expr] => Expr, cMap: Map[Expr, Expr], constant:
val coeffMap = {
//assert if the coefficients are only constant expressions
- assert(cMap.values.foldLeft(true)((acc, e) => {
- acc && variablesOf(e).isEmpty
- }))
+ assert(cMap.values.forall(e => variablesOf(e).isEmpty))
//TODO: here we should try to simplify the constant expressions
cMap
}
diff --git a/src/main/scala/leon/invariant/structure/Formula.scala b/src/main/scala/leon/invariant/structure/Formula.scala
index daed61ff679cba61666a6c227005c103a31d8d01..c17711e102877861010359256ff902ad7d51d70b 100644
--- a/src/main/scala/leon/invariant/structure/Formula.scala
+++ b/src/main/scala/leon/invariant/structure/Formula.scala
@@ -22,8 +22,7 @@ import PredicateUtil._
/**
* Data associated with a call
*/
-class CallData(val guard : Variable, val parents: List[FunDef]) {
-}
+class CallData(val guard : Variable, val parents: List[FunDef])
/**
* Representation of an expression as a set of implications.
@@ -81,13 +80,13 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
})
}
- val f1 = simplePostTransform((e: Expr) => e match {
- case Or(args) => {
- val newargs = args.map(arg => arg match {
- case v: Variable if (disjuncts.contains(v)) => arg
- case v: Variable if (conjuncts.contains(v)) => throw new IllegalStateException("or gaurd inside conjunct: "+e+" or-guard: "+v)
- case _ => {
- val atoms = arg match {
+ val f1 = simplePostTransform {
+ case e@Or(args) => {
+ val newargs = args.map {
+ case arg@(v: Variable) if (disjuncts.contains(v)) => arg
+ case v: Variable if (conjuncts.contains(v)) => throw new IllegalStateException("or gaurd inside conjunct: " + e + " or-guard: " + v)
+ case arg => {
+ val atoms = arg match {
case And(atms) => atms
case _ => Seq(arg)
}
@@ -98,14 +97,14 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
disjuncts += (g -> ctrs)
g
}
- })
+ }
//create a temporary for Or
val gor = TVarFactory.createTemp("b", BooleanType).toVariable
val newor = createOr(newargs)
conjuncts += (gor -> newor)
gor
}
- case And(args) => {
+ case e@And(args) => {
val newargs = args.map(arg => if (getTemplateVars(e).isEmpty) {
arg
} else {
@@ -118,8 +117,8 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
})
createAnd(newargs)
}
- case _ => e
- })(ExpressionTransformer.simplify(simplifyArithmetic(
+ case e => e
+ }(ExpressionTransformer.simplify(simplifyArithmetic(
//TODO: this is a hack as of now. Fix this.
//Note: it is necessary to convert real literals to integers since the linear constraint cannot handle real literals
if(ctx.usereals) ExpressionTransformer.FractionalLiteralToInt(ine)
@@ -151,7 +150,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
val e @ Or(guards) = conjuncts(gd)
//pick one guard that is true
val guard = guards.collectFirst { case g @ Variable(id) if (model(id) == tru) => g }
- if (!guard.isDefined)
+ if (guard.isEmpty)
throw new IllegalStateException("No satisfiable guard found: " + e)
guard.get +: traverseAnds(guard.get, model)
}
@@ -236,16 +235,16 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
//replace all conjunct guards in disjuncts by their mapping
val disjs : Map[Expr,Expr] = disjuncts.map((entry) => {
val (g,ctrs) = entry
- val newctrs = ctrs.map(_ match {
+ val newctrs = ctrs.map {
case BoolConstraint(g@Variable(_)) if conjuncts.contains(g) => conjuncts(g)
case ctr@_ => ctr.toExpr
- })
+ }
(g, createAnd(newctrs))
})
- val rootexprs = roots.map(_ match {
- case g@Variable(_) if conjuncts.contains(g) => conjuncts(g)
- case e@_ => e
- })
+ val rootexprs = roots.map {
+ case g@Variable(_) if conjuncts.contains(g) => conjuncts(g)
+ case e@_ => e
+ }
//replace every guard in the 'disjs' by its disjunct. DO this as long as every guard is replaced in every disjunct
var unpackedDisjs = disjs
var replacedGuard = true
diff --git a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
index 7910df7230e82f7ac8b695bc8089fcd64c005e3a..5ed3316a44bb6d0baaec32dd1962fbe7f78af0f5 100644
--- a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
+++ b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
@@ -3,23 +3,15 @@ package invariant.structure
import purescala._
import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet }
import scala.collection.mutable.{ Map => MutableMap }
-import java.io._
import invariant.util._
import BigInt._
-import Constructors._
-import Util._
import PredicateUtil._
-class NotImplementedException(message: String) extends RuntimeException(message) {
-
-}
+class NotImplementedException(message: String) extends RuntimeException(message)
//a collections of utility methods that manipulate the templates
object LinearConstraintUtil {
@@ -31,14 +23,14 @@ object LinearConstraintUtil {
//some utility methods
def getFIs(ctr: LinearConstraint): Set[FunctionInvocation] = {
- val fis = ctr.coeffMap.keys.collect((e) => e match {
+ val fis = ctr.coeffMap.keys.collect {
case fi: FunctionInvocation => fi
- })
+ }
fis.toSet
}
def evaluate(lt: LinearTemplate): Option[Boolean] = lt match {
- case lc: LinearConstraint if (lc.coeffMap.size == 0) =>
+ case lc: LinearConstraint if lc.coeffMap.isEmpty =>
ExpressionTransformer.simplify(lt.toExpr) match {
case BooleanLiteral(v) => Some(v)
case _ => None
@@ -74,7 +66,7 @@ object LinearConstraintUtil {
}
} else coeffMap += (term -> simplifyArithmetic(coeff))
- if (!variablesOf(coeff).isEmpty) {
+ if (variablesOf(coeff).nonEmpty) {
isTemplate = true
}
}
@@ -86,7 +78,7 @@ object LinearConstraintUtil {
} else
constant = Some(simplifyArithmetic(coeff))
- if (!variablesOf(coeff).isEmpty) {
+ if (variablesOf(coeff).nonEmpty) {
isTemplate = true
}
}
@@ -341,7 +333,6 @@ object LinearConstraintUtil {
//now consider each constraint look for (a) equality involving the elimVar or (b) check if all bounds are lower
//or (c) if all bounds are upper.
var elimExpr : Option[Expr] = None
- var bestExpr = false
var elimCtr : Option[LinearConstraint] = None
var allUpperBounds : Boolean = true
var allLowerBounds : Boolean = true
@@ -354,7 +345,7 @@ object LinearConstraintUtil {
foundEquality = true
//here, sometimes we replace an existing expression with a better one if available
- if (!elimExpr.isDefined || shouldReplace(elimExpr.get, lc, elimVar)) {
+ if (elimExpr.isEmpty || shouldReplace(elimExpr.get, lc, elimVar)) {
//if the coeffcient of elimVar is +ve the the sign of the coeff of every other term should be changed
val InfiniteIntegerLiteral(elimCoeff) = lc.coeffMap(elimVar.toVariable)
//make sure the value of the coefficient is 1 or -1
diff --git a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
index 98f162fea4b2974702c4672274ed6d8f86075690..15ae673019e9c50eb3ff257fc88114c935230342 100644
--- a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
@@ -1,23 +1,17 @@
package leon
package invariant.templateSolvers
-import z3.scala._
+
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import java.io._
-import scala.util.control.Breaks._
import solvers._
-import solvers.z3._
import invariant.engine._
import invariant.factories._
import invariant.util._
import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.invariant.util.RealValuedExprEvaluator._
-import Util._
import PredicateUtil._
import SolverUtil._
@@ -95,7 +89,7 @@ class CegisCore(ctx: InferenceContext,
val tempVarSum = if (minimizeSum) {
//compute the sum of the tempIds
val rootTempIds = getTemplateVars(cegisSolver.rootFun.getTemplate)
- if (rootTempIds.size >= 1) {
+ if (rootTempIds.nonEmpty) {
rootTempIds.tail.foldLeft(rootTempIds.head.asInstanceOf[Expr])((acc, tvar) => Plus(acc, tvar))
} else zero
} else zero
@@ -126,7 +120,7 @@ class CegisCore(ctx: InferenceContext,
//sanity checks
val spuriousTempIds = variablesOf(instFormula).intersect(TemplateIdFactory.getTemplateIds)
- if (!spuriousTempIds.isEmpty)
+ if (spuriousTempIds.nonEmpty)
throw new IllegalStateException("Found a template variable in instFormula: " + spuriousTempIds)
if (hasReals(instFormula))
throw new IllegalStateException("Reals in instFormula: " + instFormula)
@@ -144,21 +138,21 @@ class CegisCore(ctx: InferenceContext,
//simplify the tempctrs, evaluate every atom that does not involve a template variable
//this should get rid of all functions
val satctrs =
- simplePreTransform((e) => e match {
+ simplePreTransform {
//is 'e' free of template variables ?
- case _ if (variablesOf(e).filter(TemplateIdFactory.IsTemplateIdentifier _).isEmpty) => {
+ case e if !variablesOf(e).exists(TemplateIdFactory.IsTemplateIdentifier _) => {
//evaluate the term
val value = solver1.evalExpr(e)
if (value.isDefined) value.get
else throw new IllegalStateException("Cannot evaluate expression: " + e)
}
- case _ => e
- })(Not(formula))
+ case e => e
+ }(Not(formula))
solver1.free()
//sanity checks
val spuriousProgIds = variablesOf(satctrs).filterNot(TemplateIdFactory.IsTemplateIdentifier _)
- if (!spuriousProgIds.isEmpty)
+ if (spuriousProgIds.nonEmpty)
throw new IllegalStateException("Found a progam variable in tempctrs: " + spuriousProgIds)
val tempctrs = if (!solveAsInt) ExpressionTransformer.IntLiteralToReal(satctrs) else satctrs
@@ -201,7 +195,7 @@ class CegisCore(ctx: InferenceContext,
println("2: " + (if (res1.isDefined) "solved" else "timed out") + "... in " + (t4 - t3) / 1000.0 + "s")
if (res1.isDefined) {
- if (res1.get == false) {
+ if (!res1.get) {
//there exists no solution for templates
(Some(false), newctr, Model.empty)
diff --git a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
index 805f09a941139d817309a3a10df0b07cd57a21aa..9a9c1b0b4290b07408adb33c0e174813de831a29 100644
--- a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
@@ -4,16 +4,9 @@ package leon
package invariant.templateSolvers
import z3.scala._
-import leon.solvers._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.Extractors._
-import purescala.ExprOps._
-import purescala.Types._
-import leon.LeonContext
import leon.solvers.z3.UninterpretedZ3Solver
-import leon.solvers.smtlib.SMTLIBZ3Solver
/**
* A uninterpreted solver extended with additional functionalities.
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 19dee9ab4be261cd2378d2146864fb9566912ca3..a4e20f61a7424ee59724b8cf4374cecbcaf84f9f 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -1,26 +1,19 @@
package leon
package invariant.templateSolvers
-import z3.scala._
-import purescala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import java.io._
import solvers.SimpleSolverAPI
-import scala.collection.mutable.{ Map => MutableMap }
import invariant.engine._
-import invariant.factories._
import invariant.util._
import Util._
-import ProgramUtil._
import SolverUtil._
import PredicateUtil._
-import TimerUtil._
import invariant.structure._
+import invariant.datastructure._
import leon.solvers.TimeoutSolver
import leon.solvers.SolverFactory
import leon.solvers.TimeoutSolverFactory
@@ -83,8 +76,8 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
println("#" * 20)
//Optimization 1: Check if ants are unsat (already handled)
- val pathVC = createAnd(antsSimple.map(_.toExpr).toSeq ++ conseqsSimple.map(_.toExpr).toSeq)
- val notPathVC = And(createAnd(antsSimple.map(_.toExpr).toSeq), Not(createAnd(conseqsSimple.map(_.toExpr).toSeq)))
+ val pathVC = createAnd(antsSimple.map(_.toExpr) ++ conseqsSimple.map(_.toExpr))
+ val notPathVC = And(createAnd(antsSimple.map(_.toExpr)), Not(createAnd(conseqsSimple.map(_.toExpr))))
val (satVC, _) = uisolver.solveSAT(pathVC)
val (satNVC, _) = uisolver.solveSAT(notPathVC)
@@ -135,7 +128,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
strictCtrLambdas :+= l
GreaterEquals(l, zero)
}
- }).toSeq :+ GreaterEquals(lambda0, zero))
+ }) :+ GreaterEquals(lambda0, zero))
//add the constraints on constant terms
val sumConst = ants.foldLeft(UMinus(lambda0): Expr)((acc, ant) => ant.constTemplate match {
@@ -206,7 +199,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
// factor out common nonlinear terms and create an equiv-satisfiable constraint
def reduceCommonNLTerms(ctrs: Expr) = {
- var nlUsage = new CounterMap[Expr]()
+ val nlUsage = new CounterMap[Expr]()
postTraversal{
case t: Times => nlUsage.inc(t)
case e => ;
@@ -223,7 +216,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
// try eliminate nonlinearity to whatever extent possible
var elimMap = Map[Identifier, (Identifier, Identifier)]() // maps the fresh identifiers to the product of the identifiers they represent.
def reduceNonlinearity(farkasctrs: Expr): Expr = {
- var varCounts = new CounterMap[Identifier]()
+ val varCounts = new CounterMap[Identifier]()
// collect # of uses of each variable
postTraversal {
case Variable(id) => varCounts.inc(id)
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 41d672fe5a94861197430a69c9516985e46f2511..90cffa3f181d11deb499a06ec538a515ed164ac1 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -9,7 +9,6 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import evaluators._
-import scala.collection.mutable.{ Map => MutableMap }
import java.io._
import solvers._
import solvers.combinators._
@@ -369,7 +368,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val cegisSolver = new CegisCore(ctx, program, timeout.toInt, this)
val (res, ctr, model) = cegisSolver.solve(tempIds, expr, precond, solveAsInt = false, initModel)
- if (!res.isDefined)
+ if (res.isEmpty)
reporter.info("cegis timed-out on the disjunct...")
(res, ctr, model)
}
@@ -508,7 +507,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val InfiniteIntegerLiteral(v) = model(id)
v
}
- def eval: (Expr => Boolean) = e => e match {
+ def eval: (Expr => Boolean) = {
case And(args) => args.forall(eval)
// case Iff(Variable(id1), Variable(id2)) => model(id1) == model(id2)
case Equals(Variable(id1), Variable(id2)) => model(id1) == model(id2) //note: ADTs can also be compared for equality
@@ -516,7 +515,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
case GreaterEquals(Variable(id1), Variable(id2)) => modelVal(id1) >= modelVal(id2)
case GreaterThan(Variable(id1), Variable(id2)) => modelVal(id1) > modelVal(id2)
case LessThan(Variable(id1), Variable(id2)) => modelVal(id1) < modelVal(id2)
- case _ => throw new IllegalStateException("Predicate not handled: " + e)
+ case e => throw new IllegalStateException("Predicate not handled: " + e)
}
eval
}
@@ -526,14 +525,14 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
//println("Identifier: "+id)
model(id).asInstanceOf[FractionalLiteral]
}
- (e: Expr) => e match {
+ {
case Equals(Variable(id1), Variable(id2)) => model(id1) == model(id2) //note: ADTs can also be compared for equality
- case Operator(Seq(Variable(id1), Variable(id2)), op) if (e.isInstanceOf[LessThan]
+ case e@Operator(Seq(Variable(id1), Variable(id2)), op) if (e.isInstanceOf[LessThan]
|| e.isInstanceOf[LessEquals] || e.isInstanceOf[GreaterThan]
|| e.isInstanceOf[GreaterEquals]) => {
evaluateRealPredicate(op(Seq(modelVal(id1), modelVal(id2))))
}
- case _ => throw new IllegalStateException("Predicate not handled: " + e)
+ case e => throw new IllegalStateException("Predicate not handled: " + e)
}
}
@@ -587,11 +586,11 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
var calls = Set[Call]()
var cons = Set[Expr]()
- satCtrs.foreach(ctr => ctr match {
+ satCtrs.foreach {
case t: Call => calls += t
case t: ADTConstraint if (t.cons.isDefined) => cons += t.cons.get
case _ => ;
- })
+ }
val callExprs = calls.map(_.toExpr)
var t1 = System.currentTimeMillis()
@@ -617,11 +616,11 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
//exclude guards, separate calls and cons from the rest
var lnctrs = Set[LinearConstraint]()
var temps = Set[LinearTemplate]()
- (satCtrs ++ callCtrs ++ axiomCtrs ++ theoryCtrs).foreach(ctr => ctr match {
+ (satCtrs ++ callCtrs ++ axiomCtrs ++ theoryCtrs).foreach {
case t: LinearConstraint => lnctrs += t
case t: LinearTemplate => temps += t
case _ => ;
- })
+ }
if (this.debugChooseDisjunct) {
lnctrs.map(_.toExpr).foreach((ctr) => {
@@ -693,7 +692,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
var elimRems = Set[Identifier]()
elimLnctrs.foreach((lc) => {
val evars = variablesOf(lc.toExpr).intersect(elimVars)
- if (!evars.isEmpty) {
+ if (evars.nonEmpty) {
elimCtrs :+= lc
elimCtrCount += 1
elimRems ++= evars
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
index a2a6524c6d6f52ffa232129b4adb2ff0f794ee42..d67955ff9efd38dd9c5c70b0684b04b5cda1661b 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
@@ -1,15 +1,9 @@
package leon
package invariant.templateSolvers
-import z3.scala._
-import purescala.Common._
+
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
-import java.io._
-import leon.invariant._
-import scala.util.control.Breaks._
import solvers._
import invariant.engine._
@@ -18,7 +12,6 @@ import invariant.util._
import invariant.structure._
import Util._
import PredicateUtil._
-import SolverUtil._
class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun: FunDef,
ctrTracker: ConstraintTracker, minimizer: Option[(Expr, Model) => Model])
@@ -42,10 +35,10 @@ class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun
//in the sequel we instantiate axioms for multiplication
val inst1 = unaryMultAxioms(formula, calls, predEval(model))
val inst2 = binaryMultAxioms(formula,calls, predEval(model))
- val multCtrs = (inst1 ++ inst2).flatMap(_ match {
+ val multCtrs = (inst1 ++ inst2).flatMap {
case And(args) => args.map(ConstraintUtil.createConstriant _)
case e => Seq(ConstraintUtil.createConstriant(e))
- })
+ }
Stats.updateCounterStats(multCtrs.size, "MultAxiomBlowup", "disjuncts")
ctx.reporter.info("Number of multiplication induced predicates: "+multCtrs.size)
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index dceed68279e089122875d19c86664425df49aa22..a85a7d4f5b9f55af812da50d577ec36d350b7ce5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -1,18 +1,11 @@
package leon
package invariant.templateSolvers
-import z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
import java.io._
-import leon.invariant._
-import scala.util.control.Breaks._
-import scala.concurrent._
-import scala.concurrent.duration._
import invariant.engine._
import invariant.factories._
import invariant.util._
diff --git a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
index f41ec7e8963a45978fb4a9ac3fe091de48140d10..6b2aa300b2792f7f86b5f01565ee783731f8d863 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
@@ -1,20 +1,14 @@
package leon
package invariant.templateSolvers
-import z3.scala._
-import purescala.Common._
+
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
-import java.io._
import invariant.datastructure.UndirectedGraph
-import scala.util.control.Breaks._
import invariant.util._
import leon.purescala.TypeOps
import PredicateUtil._
-import SolverUtil._
-import Util._
class UFADTEliminator(ctx: LeonContext, program: Program) {
@@ -113,7 +107,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
lhs :+ rhs
}
//remove self equalities.
- val preds = eqs.filter(_ match {
+ val preds = eqs.filter {
case Operator(Seq(Variable(lid), Variable(rid)), _) => {
if (lid == rid) false
else {
@@ -121,8 +115,8 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
else false
}
}
- case e @ _ => throw new IllegalStateException("Not an equality or Iff: " + e)
- })
+ case e@_ => throw new IllegalStateException("Not an equality or Iff: " + e)
+ }
preds
}
@@ -134,21 +128,21 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
axiomatizeADTCons(call1, call2)
}
- if (makeEfficient && ants.exists(_ match {
+ if (makeEfficient && ants.exists {
case Equals(l, r) if (l.getType != RealType && l.getType != BooleanType && l.getType != IntegerType) => true
case _ => false
- })) {
+ }) {
Seq()
} else {
var unsatIntEq: Option[Expr] = None
var unsatOtherEq: Option[Expr] = None
ants.foreach(eq =>
- if (!unsatOtherEq.isDefined) {
+ if (unsatOtherEq.isEmpty) {
eq match {
case Equals(lhs @ Variable(_), rhs @ Variable(_)) if !predEval(Equals(lhs, rhs)) => {
if (lhs.getType != Int32Type && lhs.getType != RealType && lhs.getType != IntegerType)
unsatOtherEq = Some(eq)
- else if (!unsatIntEq.isDefined)
+ else if (unsatIntEq.isEmpty)
unsatIntEq = Some(eq)
}
case _ => ;
diff --git a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
index 6750bd59c144fa656b2d820516d6691e3e169862..9bf2889ed103f0e14083a031e5b80c700e5c89d0 100644
--- a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
+++ b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
@@ -8,10 +8,7 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import java.io._
-import java.io._
import purescala.ScalaPrinter
-import invariant.structure.Call
-import invariant.structure.FunctionUtils._
import leon.invariant.factories.TemplateIdFactory
import PredicateUtil._
import Util._
@@ -185,7 +182,7 @@ object ExpressionTransformer {
}
}
val (nexp, ncjs) = transform(inexpr, false)
- val res = if (!ncjs.isEmpty) {
+ val res = if (ncjs.nonEmpty) {
createAnd(nexp +: ncjs.toSeq)
} else nexp
res
@@ -283,31 +280,30 @@ object ExpressionTransformer {
def flattenArgs(args: Seq[Expr], insideFunction: Boolean): (Seq[Expr], Set[Expr]) = {
var newConjuncts = Set[Expr]()
- val newargs = args.map((arg) =>
- arg match {
- case v: Variable => v
- case r: ResultVariable => r
- case _ => {
- val (nexpr, ncjs) = flattenFunc(arg, insideFunction)
-
- newConjuncts ++= ncjs
-
- nexpr match {
- case v: Variable => v
- case r: ResultVariable => r
- case _ => {
- val freshArgVar = Variable(TVarFactory.createTemp("arg", arg.getType))
- newConjuncts += Equals(freshArgVar, nexpr)
- freshArgVar
- }
+ val newargs = args.map {
+ case v: Variable => v
+ case r: ResultVariable => r
+ case arg => {
+ val (nexpr, ncjs) = flattenFunc(arg, insideFunction)
+
+ newConjuncts ++= ncjs
+
+ nexpr match {
+ case v: Variable => v
+ case r: ResultVariable => r
+ case _ => {
+ val freshArgVar = Variable(TVarFactory.createTemp("arg", arg.getType))
+ newConjuncts += Equals(freshArgVar, nexpr)
+ freshArgVar
}
}
- })
+ }
+ }
(newargs, newConjuncts)
}
val (nexp, ncjs) = flattenFunc(inExpr, false)
- if (!ncjs.isEmpty) {
+ if (ncjs.nonEmpty) {
createAnd(nexp +: ncjs.toSeq)
} else nexp
}
@@ -387,7 +383,7 @@ object ExpressionTransformer {
*/
def pullAndOrs(expr: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case Or(args) => {
val newArgs = args.foldLeft(Seq[Expr]())((acc, arg) => arg match {
case Or(inArgs) => acc ++ inArgs
@@ -402,8 +398,8 @@ object ExpressionTransformer {
})
createAnd(newArgs)
}
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
}
def classSelToCons(e: Expr): Expr = {
@@ -466,15 +462,15 @@ object ExpressionTransformer {
*/
def unFlatten(ine: Expr, freevars: Set[Identifier]): Expr = {
var tempMap = Map[Expr, Expr]()
- val newinst = simplePostTransform((e: Expr) => e match {
- case Equals(v @ Variable(id), rhs @ _) if !freevars.contains(id) =>
+ val newinst = simplePostTransform {
+ case e@Equals(v@Variable(id), rhs@_) if !freevars.contains(id) =>
if (tempMap.contains(v)) e
else {
tempMap += (v -> rhs)
tru
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
val closure = (e: Expr) => replace(tempMap, e)
fix(closure)(newinst)
}
@@ -510,11 +506,11 @@ object ExpressionTransformer {
def isSubExpr(key: Expr, expr: Expr): Boolean = {
var found = false
- simplePostTransform((e: Expr) => e match {
- case _ if (e == key) =>
+ simplePostTransform {
+ case e if (e == key) =>
found = true; e
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
found
}
@@ -524,7 +520,7 @@ object ExpressionTransformer {
def simplify(expr: Expr): Expr = {
//Note: some simplification are already performed by the class constructors (see Tree.scala)
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case Equals(lhs, rhs) if (lhs == rhs) => tru
case LessEquals(lhs, rhs) if (lhs == rhs) => tru
case GreaterEquals(lhs, rhs) if (lhs == rhs) => tru
@@ -536,8 +532,8 @@ object ExpressionTransformer {
case LessThan(InfiniteIntegerLiteral(v1), InfiniteIntegerLiteral(v2)) => BooleanLiteral(v1 < v2)
case GreaterEquals(InfiniteIntegerLiteral(v1), InfiniteIntegerLiteral(v2)) => BooleanLiteral(v1 >= v2)
case GreaterThan(InfiniteIntegerLiteral(v1), InfiniteIntegerLiteral(v2)) => BooleanLiteral(v1 > v2)
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
}
/**
@@ -545,7 +541,7 @@ object ExpressionTransformer {
* Note: (a) Not(Equals()) and Not(Variable) is allowed
*/
def isDisjunct(e: Expr): Boolean = e match {
- case And(args) => args.foldLeft(true)((acc, arg) => acc && isDisjunct(arg))
+ case And(args) => args.forall(arg => isDisjunct(arg))
case Not(Equals(_, _)) | Not(Variable(_)) => true
case Or(_) | Implies(_, _) | Not(_) | Equals(_, _) => false
case _ => true
@@ -556,7 +552,7 @@ object ExpressionTransformer {
* Note: (a) Not(Equals()) and Not(Variable) is allowed
*/
def isConjunct(e: Expr): Boolean = e match {
- case Or(args) => args.foldLeft(true)((acc, arg) => acc && isConjunct(arg))
+ case Or(args) => args.forall(arg => isConjunct(arg))
case Not(Equals(_, _)) | Not(Variable(_)) => true
case And(_) | Implies(_, _) | Not(_) | Equals(_, _) => false
case _ => true
@@ -568,17 +564,17 @@ object ExpressionTransformer {
case And(args) => {
//have we seen an or ?
if (seen == 2) false
- else args.foldLeft(true)((acc, arg) => acc && uniOP(arg, 1))
+ else args.forall(arg => uniOP(arg, 1))
}
case Or(args) => {
//have we seen an And ?
if (seen == 1) false
- else args.foldLeft(true)((acc, arg) => acc && uniOP(arg, 2))
+ else args.forall(arg => uniOP(arg, 2))
}
case t: Terminal => true
/*case u @ UnaryOperator(e1, op) => uniOP(e1, seen)
case b @ BinaryOperator(e1, e2, op) => uniOP(e1, seen) && uniOP(e2, seen)*/
- case n @ Operator(args, op) => args.foldLeft(true)((acc, arg) => acc && uniOP(arg, seen))
+ case n @ Operator(args, op) => args.forall(arg => uniOP(arg, seen))
}
def printRec(e: Expr, indent: Int): Unit = {
@@ -588,7 +584,7 @@ object ExpressionTransformer {
e match {
case And(args) => {
var start = true
- args.map((arg) => {
+ args.foreach((arg) => {
wr.print(" " * (indent + 1))
if (!start) wr.print("^")
printRec(arg, indent + 1)
@@ -597,7 +593,7 @@ object ExpressionTransformer {
}
case Or(args) => {
var start = true
- args.map((arg) => {
+ args.foreach((arg) => {
wr.print(" " * (indent + 1))
if (!start) wr.print("v")
printRec(arg, indent + 1)
@@ -627,8 +623,8 @@ object ExpressionTransformer {
}
def distribute(e: Expr): Expr = {
- simplePreTransform(_ match {
- case e @ FunctionInvocation(TypedFunDef(fd, _), Seq(e1, e2)) if isMultFunctions(fd) =>
+ simplePreTransform {
+ case e@FunctionInvocation(TypedFunDef(fd, _), Seq(e1, e2)) if isMultFunctions(fd) =>
val newe = (e1, e2) match {
case (Plus(sum1, sum2), _) =>
// distribute e2 over e1
@@ -655,7 +651,7 @@ object ExpressionTransformer {
}
newe
case other => other
- })(e)
+ }(e)
}
distribute(e)
}
diff --git a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala b/src/main/scala/leon/invariant/util/LetTupleSimplification.scala
similarity index 92%
rename from src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
rename to src/main/scala/leon/invariant/util/LetTupleSimplification.scala
index bd99992014bd94ab29c099b7a03eb7e452e154c0..83b7b0cba056c0c7f377caa2c4f76134bab81e24 100644
--- a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
+++ b/src/main/scala/leon/invariant/util/LetTupleSimplification.scala
@@ -7,14 +7,8 @@ import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
-import java.io._
-import java.io._
-import purescala.ScalaPrinter
import leon.utils._
import PredicateUtil._
-
-import invariant.structure.Call
-import invariant.structure.FunctionUtils._
import leon.transformations.InstUtil._
/**
@@ -31,13 +25,13 @@ object LetTupleSimplification {
val bone = BigInt(1)
def letSanityChecks(ine: Expr) = {
- simplePostTransform(_ match {
- case letExpr @ Let(binderId, letValue, body)
- if (binderId.getType != letValue.getType) =>
- throw new IllegalStateException("Binder and value type mismatch: "+
- s"(${binderId.getType},${letValue.getType})")
+ simplePostTransform {
+ case letExpr@Let(binderId, letValue, body)
+ if (binderId.getType != letValue.getType) =>
+ throw new IllegalStateException("Binder and value type mismatch: " +
+ s"(${binderId.getType},${letValue.getType})")
case e => e
- })(ine)
+ }(ine)
}
/**
@@ -130,11 +124,11 @@ object LetTupleSimplification {
(arg1, arg2) match {
case (_: TupleSelect, _) => error = true
case (_, _: TupleSelect) => error = true
- case _ => { ; }
+ case _ =>
}
}
- case _ => { ; }
+ case _ =>
}
}
@@ -172,8 +166,8 @@ object LetTupleSimplification {
// in the sequel, we are using the fact that 'depth' is positive and
// 'ine' contains only 'depth' variables
- val simpe = simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(tfd, args) if (tfd.fd == maxFun) => {
+ val simpe = simplePostTransform {
+ case e@FunctionInvocation(tfd, args) if (tfd.fd == maxFun) => {
if (debugMaxSimplify) {
println("Simplifying: " + e)
}
@@ -183,20 +177,20 @@ object LetTupleSimplification {
import invariant.structure.LinearConstraintUtil._
val lt = exprToTemplate(LessEquals(Minus(arg1, arg2), InfiniteIntegerLiteral(0)))
//now, check if all the variables in 'lt' have only positive coefficients
- val allPositive = lt.coeffTemplate.forall(entry => entry match {
+ val allPositive = lt.coeffTemplate.forall {
case (k, IntLiteral(v)) if (v >= 0) => true
case _ => false
- }) && (lt.constTemplate match {
+ } && (lt.constTemplate match {
case None => true
case Some(IntLiteral(v)) if (v >= 0) => true
case _ => false
})
if (allPositive) arg1
else {
- val allNegative = lt.coeffTemplate.forall(entry => entry match {
+ val allNegative = lt.coeffTemplate.forall {
case (k, IntLiteral(v)) if (v <= 0) => true
case _ => false
- }) && (lt.constTemplate match {
+ } && (lt.constTemplate match {
case None => true
case Some(IntLiteral(v)) if (v <= 0) => true
case _ => false
@@ -222,14 +216,14 @@ object LetTupleSimplification {
// case FunctionInvocation(tfd, args) if(tfd.fd.id.name == "max") => {
// throw new IllegalStateException("Found just max in expression " + e + "\n")
// }
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
simpe
}
def inlineMax(ine: Expr): Expr = {
//inline 'max' operations here
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(tfd, args) if (tfd.fd == maxFun) =>
val Seq(arg1, arg2) = args
val bindWithLet = (value: Expr, body: (Expr with Terminal) => Expr) => {
@@ -245,8 +239,8 @@ object LetTupleSimplification {
}
bindWithLet(arg1, a1 => bindWithLet(arg2, a2 =>
IfExpr(GreaterEquals(a1, a2), a1, a2)))
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
def removeLetsFromLetValues(ine: Expr): Expr = {
@@ -317,10 +311,10 @@ object LetTupleSimplification {
Tuple(args :+ e2)
}))
}
- replaceLetBody(transLet, (e: Expr) => e match {
+ replaceLetBody(transLet, {
case Tuple(args) =>
op(args)
- case _ => op(Seq(e)) //here, there was only one argument
+ case e => op(Seq(e)) //here, there was only one argument
})
}
transe
@@ -378,7 +372,7 @@ object LetTupleSimplification {
res
}
- val transforms = removeLetsFromLetValues _ andThen fixpoint(postMap(simplerLet)) _ andThen simplifyArithmetic
+ val transforms = removeLetsFromLetValues _ andThen fixpoint(postMap(simplerLet)) andThen simplifyArithmetic
transforms(ine)
}
@@ -398,7 +392,7 @@ object LetTupleSimplification {
val allLeaves = getLeaves(e, true)
// Here the expression is not of the form we are currently simplifying
- if (allLeaves.size == 0) e
+ if (allLeaves.isEmpty) e
else {
// fold constants here
val allConstantsOpped = allLeaves.foldLeft(identity)((acc, e) => e match {
@@ -406,17 +400,17 @@ object LetTupleSimplification {
case _ => acc
})
- val allNonConstants = allLeaves.filter((e) => e match {
+ val allNonConstants = allLeaves.filter {
case _: InfiniteIntegerLiteral => false
case _ => true
- })
+ }
// Reconstruct the expressin tree with the non-constants and the result of constant evaluation above
if (allConstantsOpped != identity) {
allNonConstants.foldLeft(InfiniteIntegerLiteral(allConstantsOpped): Expr)((acc: Expr, currExpr) => makeTree(acc, currExpr))
}
else {
- if (allNonConstants.size == 0) InfiniteIntegerLiteral(identity)
+ if (allNonConstants.isEmpty) InfiniteIntegerLiteral(identity)
else {
allNonConstants.tail.foldLeft(allNonConstants.head)((acc: Expr, currExpr) => makeTree(acc, currExpr))
}
@@ -455,10 +449,11 @@ object LetTupleSimplification {
((a: BigInt, b: BigInt) => if (a > b) a else b),
getAllMaximands,
0,
- ((e1, e2) => {
+ (e1, e2) => {
val typedMaxFun = TypedFunDef(maxFun, Seq())
FunctionInvocation(typedMaxFun, Seq(e1, e2))
- }))
+ }
+ )
maxSimplifiedExpr
})(e)
diff --git a/src/main/scala/leon/invariant/util/Minimizer.scala b/src/main/scala/leon/invariant/util/Minimizer.scala
index e39378f267c0970d85797d19eef468c3a35f1db4..3794f55463490ae048574f3613f720ba092d0ff2 100644
--- a/src/main/scala/leon/invariant/util/Minimizer.scala
+++ b/src/main/scala/leon/invariant/util/Minimizer.scala
@@ -1,22 +1,15 @@
package leon
package invariant.util
-import z3.scala._
-import purescala.Common._
+
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
import solvers._
-import solvers.z3._
import solvers.smtlib.SMTLIBZ3Solver
-import leon.invariant._
-import scala.util.control.Breaks._
import invariant.engine.InferenceContext
import invariant.factories._
-import leon.invariant.templateSolvers.ExtendedUFSolver
import leon.invariant.util.RealValuedExprEvaluator._
-import invariant.util.TimerUtil._
class Minimizer(ctx: InferenceContext, program: Program) {
diff --git a/src/main/scala/leon/invariant/util/RealToIntExpr.scala b/src/main/scala/leon/invariant/util/RealToInt.scala
similarity index 96%
rename from src/main/scala/leon/invariant/util/RealToIntExpr.scala
rename to src/main/scala/leon/invariant/util/RealToInt.scala
index 54650b2c4111b32e127070cdc23889708a81b6fd..6c1860160f2bebc5bf0cb574b9c9934985246f45 100644
--- a/src/main/scala/leon/invariant/util/RealToIntExpr.scala
+++ b/src/main/scala/leon/invariant/util/RealToInt.scala
@@ -2,12 +2,9 @@ package leon
package invariant.util
import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import leon.invariant._
import invariant.factories._
import solvers._
diff --git a/src/main/scala/leon/invariant/util/RealExprEvaluator.scala b/src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala
similarity index 100%
rename from src/main/scala/leon/invariant/util/RealExprEvaluator.scala
rename to src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala
diff --git a/src/main/scala/leon/invariant/util/SolverUtil.scala b/src/main/scala/leon/invariant/util/SolverUtil.scala
index e67385c435ea94b24ef63ed8fe8bdbf41f602570..466ec1d2def3831b42c1f0b4bc6eaad3351ef716 100644
--- a/src/main/scala/leon/invariant/util/SolverUtil.scala
+++ b/src/main/scala/leon/invariant/util/SolverUtil.scala
@@ -1,21 +1,13 @@
package leon
package invariant.util
-import utils._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
-import leon.invariant._
import solvers.z3._
import solvers._
-import invariant.engine._
-import invariant.factories._
-import invariant.structure._
-import FunctionUtils._
import leon.invariant.templateSolvers.ExtendedUFSolver
import java.io._
import Util._
@@ -55,7 +47,7 @@ object SolverUtil {
case id @ _ if (id.name.toString == "c?") => id.toVariable -> InfiniteIntegerLiteral(2)
}.toMap
//println("found ids: " + idmap.keys)
- if (!idmap.keys.isEmpty) {
+ if (idmap.keys.nonEmpty) {
val newpathcond = replace(idmap, expr)
//check if this is solvable
val solver = SimpleSolverAPI(SolverFactory(() => new ExtendedUFSolver(ctx, prog)))
@@ -76,8 +68,8 @@ object SolverUtil {
var controlVars = Map[Variable, Expr]()
var newEqs = Map[Expr, Expr]()
val solver = new ExtendedUFSolver(ctx, prog)
- val newe = simplePostTransform((e: Expr) => e match {
- case And(_) | Or(_) => {
+ val newe = simplePostTransform {
+ case e@(And(_) | Or(_)) => {
val v = TVarFactory.createTemp("a", BooleanType).toVariable
newEqs += (v -> e)
val newe = Equals(v, e)
@@ -88,8 +80,8 @@ object SolverUtil {
solver.assertCnstr(Or(newe, cvar))
v
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
//create new variable and add it in disjunction
val cvar = FreshIdentifier("ctrl", BooleanType, true).toVariable
controlVars += (cvar -> newe)
diff --git a/src/main/scala/leon/invariant/util/Stats.scala b/src/main/scala/leon/invariant/util/Stats.scala
index 76a1f12ee4eede0ba631969ebb7bf3076bb3bf08..72239ac32227122c5f65c1ea73ac231d04014a11 100644
--- a/src/main/scala/leon/invariant/util/Stats.scala
+++ b/src/main/scala/leon/invariant/util/Stats.scala
@@ -1,19 +1,11 @@
package leon
package invariant.util
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import scala.collection.mutable.{ Map => MutableMap }
-import java.io._
-import leon.invariant._
import java.io._
import scala.collection.mutable.{Map => MutableMap}
-
/**
* A generic statistics object that provides:
* (a) Temporal variables that change over time. We track the total sum and max of the values the variable takes over time
diff --git a/src/main/scala/leon/invariant/util/TemporaryVarFactory.scala b/src/main/scala/leon/invariant/util/TVarFactory.scala
similarity index 81%
rename from src/main/scala/leon/invariant/util/TemporaryVarFactory.scala
rename to src/main/scala/leon/invariant/util/TVarFactory.scala
index c85c7837b1c4dbf35e2a90b87d93bccca929a6c9..6743e802b27ef44b1b966555d6965130373b5f8b 100644
--- a/src/main/scala/leon/invariant/util/TemporaryVarFactory.scala
+++ b/src/main/scala/leon/invariant/util/TVarFactory.scala
@@ -2,11 +2,8 @@ package leon
package invariant.util
import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet}
object TVarFactory {
diff --git a/src/main/scala/leon/invariant/util/TimerUtil.scala b/src/main/scala/leon/invariant/util/TimerUtil.scala
index 1284951709d4c374c56f1115b8b946f1a796855d..77e9b520116234e1d4bb6fee6ddf7563deed1640 100644
--- a/src/main/scala/leon/invariant/util/TimerUtil.scala
+++ b/src/main/scala/leon/invariant/util/TimerUtil.scala
@@ -2,9 +2,6 @@ package leon
package invariant.util
import utils._
-import solvers._
-import invariant.engine._
-import purescala.Expressions._
object TimerUtil {
/**
@@ -12,13 +9,13 @@ object TimerUtil {
*/
def scheduleTask(callBack: () => Unit, timeOut: Long): Option[java.util.Timer] = {
if (timeOut > 0) {
- val timer = new java.util.Timer();
+ val timer = new java.util.Timer()
timer.schedule(new java.util.TimerTask() {
def run() {
callBack()
timer.cancel() //the timer will be cancelled after it runs
}
- }, timeOut);
+ }, timeOut)
Some(timer)
} else None
}
@@ -30,7 +27,6 @@ class InterruptOnSignal(it: Interruptible) {
private var keepRunning = true
override def run(): Unit = {
- val startTime: Long = System.currentTimeMillis
while (!signal && keepRunning) {
Thread.sleep(100) // a relatively infrequent poll
}
diff --git a/src/main/scala/leon/invariant/util/TreeUtil.scala b/src/main/scala/leon/invariant/util/TreeUtil.scala
index 6e3e45f22a49bc3ef70d0d18e3d0371fedac2654..4109e59877c192570e95bb83b819ebd0a59edef7 100644
--- a/src/main/scala/leon/invariant/util/TreeUtil.scala
+++ b/src/main/scala/leon/invariant/util/TreeUtil.scala
@@ -33,8 +33,8 @@ object ProgramUtil {
*/
def copyProgram(prog: Program, mapdefs: (Seq[Definition] => Seq[Definition])): Program = {
prog.copy(units = prog.units.collect {
- case unit if (!unit.defs.isEmpty) => unit.copy(defs = unit.defs.collect {
- case module : ModuleDef if (!module.defs.isEmpty) =>
+ case unit if unit.defs.nonEmpty => unit.copy(defs = unit.defs.collect {
+ case module : ModuleDef if module.defs.nonEmpty =>
module.copy(defs = mapdefs(module.defs))
case other => other
})
@@ -43,8 +43,8 @@ object ProgramUtil {
def createTemplateFun(plainTemp: Expr): FunctionInvocation = {
val tmpl = Lambda(getTemplateIds(plainTemp).toSeq.map(id => ValDef(id)), plainTemp)
- val tmplFd = new FunDef(FreshIdentifier("tmpl", FunctionType(Seq(tmpl.getType), BooleanType), false), Seq(), Seq(ValDef(FreshIdentifier("arg", tmpl.getType),
- Some(tmpl.getType))), BooleanType)
+ val tmplFd = new FunDef(FreshIdentifier("tmpl", FunctionType(Seq(tmpl.getType), BooleanType), false), Seq(),
+ Seq(ValDef(FreshIdentifier("arg", tmpl.getType))), BooleanType)
tmplFd.body = Some(BooleanLiteral(true))
FunctionInvocation(TypedFunDef(tmplFd, Seq()), Seq(tmpl))
}
@@ -71,11 +71,11 @@ object ProgramUtil {
}
def mapFunctionsInExpr(funmap: Map[FunDef, FunDef])(ine: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(tfd, args) if funmap.contains(tfd.fd) =>
FunctionInvocation(TypedFunDef(funmap(tfd.fd), tfd.tps), args)
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
/**
@@ -161,7 +161,7 @@ object ProgramUtil {
}
def translateExprToProgram(ine: Expr, currProg: Program, newProg: Program): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(TypedFunDef(fd, tps), args) =>
functionByName(fullName(fd)(currProg), newProg) match {
case Some(nfd) =>
@@ -169,8 +169,8 @@ object ProgramUtil {
case _ =>
throw new IllegalStateException(s"Cannot find translation for ${fd.id.name}")
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
def getFunctionReturnVariable(fd: FunDef) = {
@@ -205,18 +205,18 @@ object PredicateUtil {
*/
def isTemplateExpr(expr: Expr): Boolean = {
var foundVar = false
- simplePostTransform((e: Expr) => e match {
- case Variable(id) => {
+ simplePostTransform {
+ case e@Variable(id) => {
if (!TemplateIdFactory.IsTemplateIdentifier(id))
foundVar = true
e
}
- case ResultVariable(_) => {
+ case e@ResultVariable(_) => {
foundVar = true
e
}
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
!foundVar
}
@@ -234,13 +234,13 @@ object PredicateUtil {
*/
def hasReals(expr: Expr): Boolean = {
var foundReal = false
- simplePostTransform((e: Expr) => e match {
- case _ => {
+ simplePostTransform {
+ case e => {
if (e.getType == RealType)
- foundReal = true;
+ foundReal = true
e
}
- })(expr)
+ }(expr)
foundReal
}
@@ -252,13 +252,13 @@ object PredicateUtil {
*/
def hasInts(expr: Expr): Boolean = {
var foundInt = false
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case e: Terminal if (e.getType == Int32Type || e.getType == IntegerType) => {
- foundInt = true;
+ foundInt = true
e
}
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
foundInt
}
@@ -268,29 +268,29 @@ object PredicateUtil {
def atomNum(e: Expr): Int = {
var count: Int = 0
- simplePostTransform((e: Expr) => e match {
- case And(args) => {
+ simplePostTransform {
+ case e@And(args) => {
count += args.size
e
}
- case Or(args) => {
+ case e@Or(args) => {
count += args.size
e
}
- case _ => e
- })(e)
+ case e => e
+ }(e)
count
}
def numUIFADT(e: Expr): Int = {
var count: Int = 0
- simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(_, _) | CaseClass(_, _) | Tuple(_) => {
+ simplePostTransform {
+ case e@(FunctionInvocation(_, _) | CaseClass(_, _) | Tuple(_)) => {
count += 1
e
}
- case _ => e
- })(e)
+ case e => e
+ }(e)
count
}
@@ -327,12 +327,12 @@ object PredicateUtil {
//replaces occurrences of mult by Times
def multToTimes(ine: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(TypedFunDef(fd, _), args) if isMultFunctions(fd) => {
Times(args(0), args(1))
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
def createAnd(exprs: Seq[Expr]): Expr = {
diff --git a/src/main/scala/leon/invariant/util/Util.scala b/src/main/scala/leon/invariant/util/Util.scala
index f8358dec14f22f420a2b19b90dcf9dd9d308d80d..a792f1586479d5989773cdeee7e322eaa66983a6 100644
--- a/src/main/scala/leon/invariant/util/Util.scala
+++ b/src/main/scala/leon/invariant/util/Util.scala
@@ -1,19 +1,16 @@
package leon
package invariant.util
-import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Types._
-import leon.purescala.PrettyPrintable
-import leon.purescala.PrinterContext
+import purescala.PrettyPrintable
+import purescala.PrinterContext
import purescala.PrinterHelpers._
object FileCountGUID {
var fileCount = 0
def getID: Int = {
- var oldcnt = fileCount
+ val oldcnt = fileCount
fileCount += 1
oldcnt
}
@@ -32,7 +29,7 @@ case class ResultVariable(tpe: TypeTree) extends Expr with Terminal with PrettyP
val getType = tpe
override def toString: String = "#res"
- def printWith(implicit pctx: PrinterContext) {
+ def printWith(implicit pctx: PrinterContext) = {
p"#res"
}
}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 0ba5436ed42004b888831fcc1c3e861113cc5a27..a4f365a2508f72646488aef29641035ddba0e2d1 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -111,7 +111,7 @@ object Constructors {
canBeSubtypeOf(actualType, typeParamsOf(formalType).toSeq, formalType) match {
case Some(tmap) =>
FunctionInvocation(fd.typed(fd.tparams map { tpd => tmap.getOrElse(tpd.tp, tpd.tp) }), args)
- case None => sys.error(s"$actualType cannot be a subtype of $formalType!")
+ case None => throw LeonFatalError(s"$args:$actualType cannot be a subtype of $formalType!")
}
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 986053706cbac5e55ddf234a0174aac4aadf8fb2..464c91445906d075800412b5f1eb7343ac36a004 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -3,7 +3,6 @@
package leon
package purescala
-import sun.reflect.generics.tree.ReturnType
import utils.Library
import Common._
import Expressions._
@@ -41,27 +40,21 @@ object Definitions {
}
}
- /** A ValDef represents a parameter of a [[purescala.Definitions.FunDef function]] or
- * a [[purescala.Definitions.CaseClassDef case class]].
- *
- * The optional [[tpe]], if present, overrides the type of the underlying Identifier [[id]].
- * This is useful to instantiate argument types of polymorphic classes. To be consistent,
- * never use the type of [[id]] directly; use [[ValDef#getType]] instead.
- */
- case class ValDef(id: Identifier, tpe: Option[TypeTree] = None) extends Definition with Typed {
+ /**
+ * A ValDef declares a new identifier to be of a certain type.
+ * The optional tpe, if present, overrides the type of the underlying Identifier id
+ * This is useful to instantiate argument types of polymorphic functions
+ */
+ case class ValDef(id: Identifier, isLazy: Boolean = false) extends Definition with Typed {
self: Serializable =>
- val getType = tpe getOrElse id.getType
+ val getType = id.getType
var defaultValue : Option[FunDef] = None
def subDefinitions = Seq()
- /** Transform this [[ValDef]] into a [[Expressions.Variable Variable]]
- *
- * Warning: the variable will not have the same type as this ValDef, but currently
- * the Identifier type is enough for all uses in Leon.
- */
+ /** Transform this [[ValDef]] into a [[Expressions.Variable Variable]] */
def toVariable : Variable = Variable(id)
}
@@ -161,7 +154,7 @@ object Definitions {
object UnitDef {
def apply(id: Identifier, modules : Seq[ModuleDef]) : UnitDef =
- UnitDef(id,Nil, Nil, modules,true)
+ UnitDef(id, Nil, Nil, modules, true)
}
/** Objects work as containers for class definitions, functions (def's) and
@@ -486,11 +479,20 @@ object Definitions {
def translated(e: Expr): Expr = instantiateType(e, typesMap, paramsMap)
+ /** A mapping from this [[TypedFunDef]]'s formal parameters to real arguments
+ *
+ * @param realArgs The arguments to which the formal argumentas are mapped
+ * */
def paramSubst(realArgs: Seq[Expr]) = {
require(realArgs.size == params.size)
(paramIds zip realArgs).toMap
}
+ /** Substitute this [[TypedFunDef]]'s formal parameters with real arguments in some expression
+ *
+ * @param realArgs The arguments to which the formal argumentas are mapped
+ * @param e The expression in which the substitution will take place
+ */
def withParamSubst(realArgs: Seq[Expr], e: Expr) = {
replaceFromIDs(paramSubst(realArgs), e)
}
@@ -510,11 +512,10 @@ object Definitions {
if (typesMap.isEmpty) {
(fd.params, Map())
} else {
- val newParams = fd.params.map {
- case vd @ ValDef(id, _) =>
- val newTpe = translated(vd.getType)
- val newId = FreshIdentifier(id.name, newTpe, true).copiedFrom(id)
- ValDef(newId).setPos(vd)
+ val newParams = fd.params.map { vd =>
+ val newTpe = translated(vd.getType)
+ val newId = FreshIdentifier(vd.id.name, newTpe, true).copiedFrom(vd.id)
+ vd.copy(id = newId).setPos(vd)
}
val paramsMap: Map[Identifier, Identifier] = (fd.params zip newParams).map { case (vd1, vd2) => vd1.id -> vd2.id }.toMap
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 678305670feb63f25720a9428608bedf846b66e6..4f6c968f37f230ff3c69487c6adc27397e5ab1aa 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -542,8 +542,8 @@ object ExprOps {
}
val normalized = postMap {
- case Lambda(args, body) => Some(Lambda(args.map(vd => ValDef(subst(vd.id), vd.tpe)), body))
- case Forall(args, body) => Some(Forall(args.map(vd => ValDef(subst(vd.id), vd.tpe)), body))
+ case Lambda(args, body) => Some(Lambda(args.map(vd => vd.copy(id = subst(vd.id))), body))
+ case Forall(args, body) => Some(Forall(args.map(vd => vd.copy(id = subst(vd.id))), body))
case Let(i, e, b) => Some(Let(subst(i), e, b))
case MatchExpr(scrut, cses) => Some(MatchExpr(scrut, cses.map { cse =>
cse.copy(pattern = replacePatternBinders(cse.pattern, subst))
@@ -794,7 +794,7 @@ object ExprOps {
})
case CaseClassPattern(_, cct, subps) =>
- val subExprs = (subps zip cct.fields) map {
+ val subExprs = (subps zip cct.classDef.fields) map {
case (p, f) => p.binder.map(_.toVariable).getOrElse(caseClassSelector(cct, in, f.id))
}
@@ -871,8 +871,8 @@ object ExprOps {
}
case CaseClassPattern(ob, cct, subps) =>
- assert(cct.fields.size == subps.size)
- val pairs = cct.fields.map(_.id).toList zip subps.toList
+ assert(cct.classDef.fields.size == subps.size)
+ val pairs = cct.classDef.fields.map(_.id).toList zip subps.toList
val subTests = pairs.map(p => rec(caseClassSelector(cct, in, p._1), p._2))
val together = and(bind(ob, in) +: subTests :_*)
and(IsInstanceOf(in, cct), together)
@@ -883,7 +883,7 @@ object ExprOps {
val subTests = subps.zipWithIndex.map{case (p, i) => rec(tupleSelect(in, i+1, subps.size), p)}
and(bind(ob, in) +: subTests: _*)
- case up@UnapplyPattern(ob, fd, subps) =>
+ case up @ UnapplyPattern(ob, fd, subps) =>
def someCase(e: Expr) = {
// In the case where unapply returns a Some, it is enough that the subpatterns match
andJoin(unwrapTuple(e, subps.size) zip subps map { case (ex, p) => rec(ex, p).setPos(p) }).setPos(e)
@@ -907,7 +907,7 @@ object ExprOps {
pattern match {
case CaseClassPattern(b, cct, subps) =>
assert(cct.fields.size == subps.size)
- val pairs = cct.fields.map(_.id).toList zip subps.toList
+ val pairs = cct.classDef.fields.map(_.id).toList zip subps.toList
val subMaps = pairs.map(p => mapForPattern(caseClassSelector(cct, asInstOf(in, cct), p._1), p._2))
val together = subMaps.flatten.toMap
bindIn(b, Some(cct)) ++ together
@@ -1497,8 +1497,8 @@ object ExprOps {
val isType = IsInstanceOf(Variable(on), cct)
- val recSelectors = cct.fields.collect {
- case vd if vd.getType == on.getType => vd.id
+ val recSelectors = (cct.classDef.fields zip cct.fieldsTypes).collect {
+ case (vd, tpe) if tpe == on.getType => vd.id
}
if (recSelectors.isEmpty) {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 7030dfb946ad4a465a4f46964d0afd51b06e1513..ae93221bfe8313cf8cef20ed084d559a2a472133 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -331,7 +331,7 @@ object Expressions {
// Hacky, but ok
lazy val optionType = unapplyFun.returnType.asInstanceOf[AbstractClassType]
lazy val Seq(noneType, someType) = optionType.knownCCDescendants.sortBy(_.fields.size)
- lazy val someValue = someType.fields.head
+ lazy val someValue = someType.classDef.fields.head
// Pattern match unapply(scrut)
// In case of None, return noneCase.
// In case of Some(v), return someCase(v).
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 6a8c8f9c9415a6ebc3b9c46de5d5e326a50858da..2014739eaa3fba0c84ce10685087262e7e227872 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -27,7 +27,7 @@ object MethodLifting extends TransformationPhase {
// Common for both cases
val ct = ccd.typed
val binder = FreshIdentifier(ccd.id.name.toLowerCase, ct, true)
- val fBinders = ct.fields.map{ f => f.id -> f.id.freshen }.toMap
+ val fBinders = (ccd.fieldsIds zip ct.fields).map(p => p._1 -> p._2.id.freshen).toMap
def subst(e: Expr): Expr = e match {
case CaseClassSelector(`ct`, This(`ct`), i) =>
Variable(fBinders(i)).setPos(e)
@@ -37,19 +37,19 @@ object MethodLifting extends TransformationPhase {
e
}
- ccd.methods.find( _.id == fdId).map { m =>
+ ccd.methods.find(_.id == fdId).map { m =>
// Ancestor's method is a method in the case class
- val subPatts = ct.fields map (f => WildcardPattern(Some(fBinders(f.id))))
+ val subPatts = ccd.fields map (f => WildcardPattern(Some(fBinders(f.id))))
val patt = CaseClassPattern(Some(binder), ct, subPatts)
val newE = simplePreTransform(subst)(breakDown(m.fullBody))
val cse = SimpleCase(patt, newE).setPos(newE)
(List(cse), true)
- } orElse ccd.fields.find( _.id == fdId).map { f =>
+ } orElse ccd.fields.find(_.id == fdId).map { f =>
// Ancestor's method is a case class argument in the case class
- val subPatts = ct.fields map (fld =>
+ val subPatts = ccd.fields map (fld =>
if (fld.id == f.id)
WildcardPattern(Some(fBinders(f.id)))
else
@@ -112,7 +112,7 @@ object MethodLifting extends TransformationPhase {
val fdParams = fd.params map { vd =>
val newId = FreshIdentifier(vd.id.name, tSubst(vd.id.getType))
- ValDef(newId).setPos(vd.getPos)
+ vd.copy(id = newId).setPos(vd.getPos)
}
val paramsMap = fd.params.zip(fdParams).map{ case (from, to) => from.id -> to.id }.toMap
val eSubst: Expr => Expr = instantiateType(_, tMap, paramsMap)
@@ -140,7 +140,7 @@ object MethodLifting extends TransformationPhase {
val retType = instantiateType(fd.returnType, tparamsMap)
val fdParams = fd.params map { vd =>
val newId = FreshIdentifier(vd.id.name, instantiateType(vd.id.getType, tparamsMap))
- ValDef(newId).setPos(vd.getPos)
+ vd.copy(id = newId).setPos(vd.getPos)
}
val receiver = FreshIdentifier("thiss", recType).setPos(cd.id)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b7372ba044d89e294c829c1149e5ef05ada7014a..e77825dd212725a46f346fe6582463b4b7f90f2a 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -357,8 +357,8 @@ class PrettyPrinter(opts: PrinterOptions,
case Not(expr) => p"\u00AC$expr"
- case vd@ValDef(id, _) =>
- p"$id : ${vd.getType}"
+ case vd @ ValDef(id, lzy) =>
+ p"$id :${if (lzy) "=> " else ""} ${vd.getType}"
vd.defaultValue.foreach { fd => p" = ${fd.body.get}" }
case This(_) => p"this"
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index f15b3e5af687b0e72e531fa5e6bfd20c68f310cd..84825d29a8ea2a293f04732fab06b2a88a36a4b8 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -185,14 +185,6 @@ object TypeOps {
freshId(id, typeParamSubst(tps map { case (tpd, tp) => tpd.tp -> tp })(id.getType))
}
- def instantiateType(vd: ValDef, tps: Map[TypeParameterDef, TypeTree]): ValDef = {
- val ValDef(id, forcedType) = vd
- ValDef(
- freshId(id, instantiateType(id.getType, tps)),
- forcedType map ((tp: TypeTree) => instantiateType(tp, tps))
- )
- }
-
def instantiateType(tpe: TypeTree, tps: Map[TypeParameterDef, TypeTree]): TypeTree = {
if (tps.isEmpty) {
tpe
@@ -314,7 +306,7 @@ object TypeOps {
TypeParameterDef(tpeSub(p.tp).asInstanceOf[TypeParameter])
}
val returnType = tpeSub(fd.returnType)
- val params = fd.params map (instantiateType(_, tps))
+ val params = fd.params map (vd => vd.copy(id = freshId(vd.id, tpeSub(vd.getType))))
val newFd = fd.duplicate(id, tparams, params, returnType)
val subCalls = preMap {
case fi @ FunctionInvocation(tfd, args) if tfd.fd == fd =>
@@ -343,7 +335,7 @@ object TypeOps {
case l @ Lambda(args, body) =>
val newArgs = args.map { arg =>
val tpe = tpeSub(arg.getType)
- ValDef(freshId(arg.id, tpe))
+ arg.copy(id = freshId(arg.id, tpe))
}
val mapping = args.map(_.id) zip newArgs.map(_.id)
Lambda(newArgs, rec(idsMap ++ mapping)(body)).copiedFrom(l)
@@ -351,7 +343,7 @@ object TypeOps {
case f @ Forall(args, body) =>
val newArgs = args.map { arg =>
val tpe = tpeSub(arg.getType)
- ValDef(freshId(arg.id, tpe))
+ arg.copy(id = freshId(arg.id, tpe))
}
val mapping = args.map(_.id) zip newArgs.map(_.id)
Forall(newArgs, rec(idsMap ++ mapping)(body)).copiedFrom(f)
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 654971373ae1d3a1aa078a4c70e1671cc2a79e2d..3a0a85bb24045df18ab65b0afa488a34c8921315 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -103,8 +103,14 @@ object Types {
if (tmap.isEmpty) {
classDef.fields
} else {
- // This is the only case where ValDef overrides the type of its Identifier
- classDef.fields.map(vd => ValDef(vd.id, Some(instantiateType(vd.getType, tmap))))
+ // !! WARNING !!
+ // vd.id changes but this should not be an issue as selector uses
+ // classDef.params ids which do not change!
+ classDef.fields.map { vd =>
+ val newTpe = instantiateType(vd.getType, tmap)
+ val newId = FreshIdentifier(vd.id.name, newTpe).copiedFrom(vd.id)
+ vd.copy(id = newId).setPos(vd)
+ }
}
}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 3dd72ad613023fe5e9a30a7375aa34926de2c586..4959ae799c8f34b25dbdf1cac812ef8d954b4717 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -3,13 +3,11 @@
package leon
package repair
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Types._
import purescala.DefOps._
-import purescala.Quantification._
import purescala.Constructors._
import purescala.Extractors.unwrapTuple
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index f7d395feb913244ed24e5aa0379c1e2e8480610c..b9c0dfd94e449ac5a7d130e1279da8ebb7c19b92 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -13,7 +13,7 @@ import purescala.ExprOps._
import purescala.Types._
import utils._
-import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks}
+import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks, optUnfoldFactor}
import templates._
import evaluators._
@@ -27,6 +27,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
val assumePreHolds = context.findOptionOrDefault(optAssumePre)
val disableChecks = context.findOptionOrDefault(optNoChecks)
+ val unfoldFactor = context.findOptionOrDefault(optUnfoldFactor)
protected var lastCheckResult : (Boolean, Option[Boolean], Option[HenkinModel]) = (false, None, None)
@@ -306,14 +307,17 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
if(!hasFoundAnswer) {
reporter.debug("- We need to keep going.")
- val toRelease = unrollingBank.getBlockersToUnlock
+ // unfolling `unfoldFactor` times
+ for (i <- 1 to unfoldFactor.toInt) {
+ val toRelease = unrollingBank.getBlockersToUnlock
- reporter.debug(" - more unrollings")
+ reporter.debug(" - more unrollings")
- val newClauses = unrollingBank.unrollBehind(toRelease)
+ val newClauses = unrollingBank.unrollBehind(toRelease)
- for(ncl <- newClauses) {
- solver.assertCnstr(ncl)
+ for (ncl <- newClauses) {
+ solver.assertCnstr(ncl)
+ }
}
reporter.debug(" - finished unrolling")
diff --git a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
index 911af8d84b6b6ccc94dd6ed781a77ca99e8a7771..2d3218c7b09edfa465618117a66b7f428f755b1c 100644
--- a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
+++ b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
@@ -26,7 +26,7 @@ object AdaptationPhase extends TransformationPhase {
CaseClassType(dummy, List(tp))
def mkDummyParameter(tp: TypeParameter) =
- ValDef(FreshIdentifier("dummy", mkDummyTyp(tp)), Some(mkDummyTyp(tp)))
+ ValDef(FreshIdentifier("dummy", mkDummyTyp(tp)))
def mkDummyArgument(tree: TypeTree) =
CaseClass(CaseClassType(dummy, List(tree)), Nil)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index dc267825c8356451944b5fb6b7f9de5d55504232..e2eda5e1cc84da7e72fcea0f4b1ce24ff6d91fc9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -19,8 +19,10 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
Seq(
"-q",
"--produce-models",
- "--no-incremental",
- "--tear-down-incremental",
+ "--incremental",
+// "--no-incremental",
+// "--tear-down-incremental",
+// "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
"--rewrite-divk",
"--print-success",
"--lang", "smt"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
index d49e3316716ae2277af5ea35c6115d076e7029bd..d52ac0704e65d119bf3f81c4a30d58723f9aea81 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
@@ -9,8 +9,6 @@ import purescala.Definitions._
import purescala.Constructors._
import purescala.ExprOps._
-import _root_.smtlib.parser.Commands.{Assert => _, FunDef => _, _}
-
trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
protected var currentFunDef: Option[FunDef] = None
@@ -30,14 +28,10 @@ trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
val inductiveHyps = for {
fi@FunctionInvocation(tfd, args) <- functionCallsOf(cond).toSeq
} yield {
- val formalToRealArgs = tfd.paramIds.zip(args).toMap
- val post = tfd.postcondition map { post =>
- application(
- replaceFromIDs(formalToRealArgs, post),
- Seq(fi)
- )
- } getOrElse BooleanLiteral(true)
-
+ val post = application(
+ tfd.withParamSubst(args, tfd.postOrTrue),
+ Seq(fi)
+ )
and(tfd.precOrTrue, post)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index f13ed21a2929a0b845e9c0138092bb36b5fc6428..72ecfb9d34039ad03675d2d5523c34462f9de20e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -9,7 +9,7 @@ import purescala.Expressions._
import purescala.ExprOps._
import purescala.Definitions._
-import _root_.smtlib.parser.Commands.{Assert => SMTAssert, _}
+import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => SMTFunDef, _}
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
@@ -62,27 +62,37 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
}
protected def getModel(filter: Identifier => Boolean): Model = {
- val syms = variables.aSet.filter(filter).toList.map(variables.aToB)
+ val syms = variables.aSet.filter(filter).map(variables.aToB)
if (syms.isEmpty) {
Model.empty
} else {
try {
- val cmd: Command = GetValue(
- syms.head,
- syms.tail.map(s => QualifiedIdentifier(SMTIdentifier(s)))
- )
+ val cmd = GetModel()
emit(cmd) match {
- case GetValueResponseSuccess(valuationPairs) =>
+ case GetModelResponseSuccess(smodel) =>
+ var modelFunDefs = Map[SSymbol, DefineFun]()
- new Model(valuationPairs.collect {
- case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
- val id = variables.toA(sym)
+ // first-pass to gather functions
+ for (me <- smodel) me match {
+ case me @ DefineFun(SMTFunDef(a, args, _, _)) if args.nonEmpty =>
+ modelFunDefs += a -> me
+ case _ =>
+ }
+
+ var model = Map[Identifier, Expr]()
+
+ for (me <- smodel) me match {
+ case DefineFun(SMTFunDef(s, args, kind, e)) if syms(s) =>
+ val id = variables.toA(s)
+ model += id -> fromSMT(e, id.getType)(Map(), modelFunDefs)
+ case _ =>
+ }
+
+ new Model(model)
- (id, fromSMT(value, id.getType)(Map(), Map()))
- }.toMap)
case _ =>
- Model.empty //FIXME improve this
+ Model.empty // FIXME improve this
}
} catch {
case e : SMTLIBUnsupportedError =>
@@ -100,6 +110,7 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
variables.push()
genericValues.push()
sorts.push()
+ lambdas.push()
functions.push()
errors.push()
@@ -113,6 +124,7 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
variables.pop()
genericValues.pop()
sorts.pop()
+ lambdas.pop()
functions.pop()
errors.pop()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index f5ee66b505ef6e31dcabf8695a7eaef9b8c36c2a..4ab8fa908b666c09f2f6b65fa03fdd941c4c6e41 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -11,6 +11,7 @@ import purescala.Expressions._
import purescala.Extractors._
import purescala.ExprOps._
import purescala.Types._
+import purescala.TypeOps._
import purescala.Constructors._
import purescala.Definitions._
@@ -18,7 +19,7 @@ import _root_.smtlib.common._
import _root_.smtlib.printer.{ RecursivePrinter => SMTPrinter }
import _root_.smtlib.parser.Commands.{
Constructor => SMTConstructor,
- FunDef => _,
+ FunDef => SMTFunDef,
Assert => _,
_
}
@@ -125,6 +126,7 @@ trait SMTLIBTarget extends Interruptible {
/* Symbol handling */
protected object SimpleSymbol {
+ def apply(sym: SSymbol) = QualifiedIdentifier(SMTIdentifier(sym))
def unapply(term: Term): Option[SSymbol] = term match {
case QualifiedIdentifier(SMTIdentifier(sym, Seq()), None) => Some(sym)
case _ => None
@@ -132,9 +134,7 @@ trait SMTLIBTarget extends Interruptible {
}
import scala.language.implicitConversions
- protected implicit def symbolToQualifiedId(s: SSymbol): QualifiedIdentifier = {
- QualifiedIdentifier(SMTIdentifier(s))
- }
+ protected implicit def symbolToQualifiedId(s: SSymbol): QualifiedIdentifier = SimpleSymbol(s)
protected val adtManager = new ADTManager(context)
@@ -148,14 +148,15 @@ trait SMTLIBTarget extends Interruptible {
protected def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
/* Metadata for CC, and variables */
- protected val constructors = new IncrementalBijection[TypeTree, SSymbol]()
- protected val selectors = new IncrementalBijection[(TypeTree, Int), SSymbol]()
- protected val testers = new IncrementalBijection[TypeTree, SSymbol]()
- protected val variables = new IncrementalBijection[Identifier, SSymbol]()
+ protected val constructors = new IncrementalBijection[TypeTree, SSymbol]()
+ protected val selectors = new IncrementalBijection[(TypeTree, Int), SSymbol]()
+ protected val testers = new IncrementalBijection[TypeTree, SSymbol]()
+ protected val variables = new IncrementalBijection[Identifier, SSymbol]()
protected val genericValues = new IncrementalBijection[GenericValue, SSymbol]()
- protected val sorts = new IncrementalBijection[TypeTree, Sort]()
- protected val functions = new IncrementalBijection[TypedFunDef, SSymbol]()
- protected val errors = new IncrementalBijection[Unit, Boolean]()
+ protected val sorts = new IncrementalBijection[TypeTree, Sort]()
+ protected val functions = new IncrementalBijection[TypedFunDef, SSymbol]()
+ protected val lambdas = new IncrementalBijection[FunctionType, SSymbol]()
+ protected val errors = new IncrementalBijection[Unit, Boolean]()
protected def hasError = errors.getB(()) contains true
protected def addError() = errors += () -> true
@@ -249,7 +250,7 @@ trait SMTLIBTarget extends Interruptible {
declareSort(RawArrayType(from, library.optionType(to)))
case FunctionType(from, to) =>
- Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(tupleTypeWrap(from)), declareSort(to)))
+ Ints.IntSort()
case tp: TypeParameter =>
declareUninterpretedSort(tp)
@@ -332,6 +333,20 @@ trait SMTLIBTarget extends Interruptible {
}
}
+ protected def declareLambda(tpe: FunctionType): SSymbol = {
+ val realTpe = bestRealType(tpe).asInstanceOf[FunctionType]
+ lambdas.cachedB(realTpe) {
+ val id = FreshIdentifier("dynLambda")
+ val s = id2sym(id)
+ emit(DeclareFun(
+ s,
+ (realTpe +: realTpe.from).map(declareSort),
+ declareSort(realTpe.to)
+ ))
+ s
+ }
+ }
+
/* Translate a Leon Expr to an SMTLIB term */
def sortToSMT(s: Sort): SExpr = {
@@ -528,7 +543,10 @@ trait SMTLIBTarget extends Interruptible {
* ===== Everything else =====
*/
case ap @ Application(caller, args) =>
- ArraysEx.Select(toSMT(caller), toSMT(tupleWrap(args)))
+ FunctionApplication(
+ declareLambda(caller.getType.asInstanceOf[FunctionType]),
+ (caller +: args).map(toSMT)
+ )
case Not(u) => Core.Not(toSMT(u))
case UMinus(u) => Ints.Neg(toSMT(u))
@@ -623,6 +641,92 @@ trait SMTLIBTarget extends Interruptible {
/* Translate an SMTLIB term back to a Leon Expr */
protected def fromSMT(t: Term, otpe: Option[TypeTree] = None)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
+ object EQ {
+ def unapply(t: Term): Option[(Term, Term)] = t match {
+ case Core.Equals(e1, e2) => Some((e1, e2))
+ case FunctionApplication(f, Seq(e1, e2)) if f.toString == "=" => Some((e1, e2))
+ case _ => None
+ }
+ }
+
+ object AND {
+ def unapply(t: Term): Option[Seq[Term]] = t match {
+ case Core.And(e1, e2) => Some(Seq(e1, e2))
+ case FunctionApplication(SimpleSymbol(SSymbol("and")), args) => Some(args)
+ case _ => None
+ }
+ def apply(ts: Seq[Term]): Term = ts match {
+ case Seq() => throw new IllegalArgumentException
+ case Seq(t) => t
+ case _ => FunctionApplication(SimpleSymbol(SSymbol("and")), ts)
+ }
+ }
+
+ object Num {
+ def unapply(t: Term): Option[BigInt] = t match {
+ case SNumeral(n) => Some(n)
+ case FunctionApplication(f, Seq(SNumeral(n))) if f.toString == "-" => Some(-n)
+ case _ => None
+ }
+ }
+
+ def extractLambda(n: BigInt, ft: FunctionType): Expr = {
+ val FunctionType(from, to) = ft
+ lambdas.getB(ft) match {
+ case None => simplestValue(ft)
+ case Some(dynLambda) => letDefs.get(dynLambda) match {
+ case None => simplestValue(ft)
+ case Some(DefineFun(SMTFunDef(a, SortedVar(dispatcher, dkind) +: args, rkind, body))) =>
+ val lambdaArgs = from.map(tpe => FreshIdentifier("x", tpe, true))
+ val argsMap: Map[Term, Identifier] = (args.map(sv => symbolToQualifiedId(sv.name)) zip lambdaArgs).toMap
+
+ val d = symbolToQualifiedId(dispatcher)
+ def dispatch(t: Term): Term = t match {
+ case Core.ITE(EQ(di, Num(ni)), thenn, elze) if di == d =>
+ if (ni == n) thenn else dispatch(elze)
+ case Core.ITE(AND(EQ(di, Num(ni)) +: rest), thenn, elze) if di == d =>
+ if (ni == n) Core.ITE(AND(rest), thenn, dispatch(elze)) else dispatch(elze)
+ case _ => t
+ }
+
+ def extract(t: Term): Expr = {
+ def recCond(term: Term): Seq[Expr] = term match {
+ case AND(es) =>
+ es.foldLeft(Seq.empty[Expr]) {
+ case (seq, e) => seq ++ recCond(e)
+ }
+ case EQ(e1, e2) =>
+ argsMap.get(e1).map(l => l -> e2) orElse argsMap.get(e2).map(l => l -> e1) match {
+ case Some((lambdaArg, term)) => Seq(Equals(lambdaArg.toVariable, fromSMT(term, lambdaArg.getType)))
+ case _ => Seq.empty
+ }
+ case arg =>
+ argsMap.get(arg) match {
+ case Some(lambdaArg) => Seq(lambdaArg.toVariable)
+ case _ => Seq.empty
+ }
+ }
+
+ def recCases(term: Term): Expr = term match {
+ case Core.ITE(cond, thenn, elze) =>
+ IfExpr(andJoin(recCond(cond)), recCases(thenn), recCases(elze))
+ case AND(es) if to == BooleanType =>
+ andJoin(recCond(term))
+ case EQ(e1, e2) if to == BooleanType =>
+ andJoin(recCond(term))
+ case _ =>
+ fromSMT(term, to)
+ }
+
+ val body = recCases(t)
+ Lambda(lambdaArgs.map(ValDef(_)), body)
+ }
+
+ extract(dispatch(body))
+ }
+ }
+ }
+
// Use as much information as there is, if there is an expected type, great, but it might not always be there
(t, otpe) match {
case (_, Some(UnitType)) =>
@@ -656,6 +760,9 @@ trait SMTLIBTarget extends Interruptible {
}
}
+ case (Num(n), Some(ft: FunctionType)) =>
+ extractLambda(n, ft)
+
case (SNumeral(n), Some(RealType)) =>
FractionalLiteral(n, 1)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index eac8f47f948f5eceb8c728c900c15d31fc8fd310..3d4a06a838a5057a693d85754bb5113e1ce7d0ae 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -76,7 +76,6 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
val n = s.name.split("!").toList.last
GenericValue(tp, n.toInt)
-
case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe)) =>
if (letDefs contains k) {
// Need to recover value form function model
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 00bdbfa07ca49c450cd91b3fce0e67dc7655402a..75d163815a17fbf31c56b684d58e3d26efe7feaa 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -6,29 +6,194 @@ package templates
import purescala.Common._
import purescala.Expressions._
+import purescala.Extractors._
import purescala.ExprOps._
import purescala.Types._
import utils._
import Instantiation._
-class LambdaManager[T](protected[templates] val encoder: TemplateEncoder[T]) extends IncrementalState {
+case class App[T](caller: T, tpe: FunctionType, args: Seq[T]) {
+ override def toString = "(" + caller + " : " + tpe + ")" + args.mkString("(", ",", ")")
+}
+
+object LambdaTemplate {
+
+ def apply[T](
+ ids: (Identifier, T),
+ encoder: TemplateEncoder[T],
+ manager: QuantificationManager[T],
+ pathVar: (Identifier, T),
+ arguments: Seq[(Identifier, T)],
+ condVars: Map[Identifier, T],
+ exprVars: Map[Identifier, T],
+ condTree: Map[Identifier, Set[Identifier]],
+ guardedExprs: Map[Identifier, Seq[Expr]],
+ quantifications: Seq[QuantificationTemplate[T]],
+ lambdas: Seq[LambdaTemplate[T]],
+ baseSubstMap: Map[Identifier, T],
+ dependencies: Map[Identifier, T],
+ lambda: Lambda
+ ) : LambdaTemplate[T] = {
+
+ val id = ids._2
+ val tpe = ids._1.getType.asInstanceOf[FunctionType]
+ val (clauses, blockers, applications, matchers, templateString) =
+ Template.encode(encoder, pathVar, arguments, condVars, exprVars, guardedExprs, lambdas,
+ substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
+
+ val lambdaString : () => String = () => {
+ "Template for lambda " + ids._1 + ": " + lambda + " is :\n" + templateString()
+ }
+
+ val (structuralLambda, structSubst) = normalizeStructure(lambda)
+ val keyDeps = dependencies.map { case (id, idT) => structSubst(id) -> idT }
+ val key = structuralLambda.asInstanceOf[Lambda]
+
+ new LambdaTemplate[T](
+ ids,
+ encoder,
+ manager,
+ pathVar,
+ arguments,
+ condVars,
+ exprVars,
+ condTree,
+ clauses,
+ blockers,
+ applications,
+ quantifications,
+ matchers,
+ lambdas,
+ keyDeps,
+ key,
+ lambdaString
+ )
+ }
+}
+
+class LambdaTemplate[T] private (
+ val ids: (Identifier, T),
+ val encoder: TemplateEncoder[T],
+ val manager: QuantificationManager[T],
+ val pathVar: (Identifier, T),
+ val arguments: Seq[(Identifier, T)],
+ val condVars: Map[Identifier, T],
+ val exprVars: Map[Identifier, T],
+ val condTree: Map[Identifier, Set[Identifier]],
+ val clauses: Seq[T],
+ val blockers: Map[T, Set[TemplateCallInfo[T]]],
+ val applications: Map[T, Set[App[T]]],
+ val quantifications: Seq[QuantificationTemplate[T]],
+ val matchers: Map[T, Set[Matcher[T]]],
+ val lambdas: Seq[LambdaTemplate[T]],
+ private[templates] val dependencies: Map[Identifier, T],
+ private[templates] val structuralKey: Lambda,
+ stringRepr: () => String) extends Template[T] {
+
+ val args = arguments.map(_._2)
+ val tpe = ids._1.getType.asInstanceOf[FunctionType]
+
+ def substitute(substituter: T => T): LambdaTemplate[T] = {
+ val newStart = substituter(start)
+ val newClauses = clauses.map(substituter)
+ val newBlockers = blockers.map { case (b, fis) =>
+ val bp = if (b == start) newStart else b
+ bp -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+ }
+
+ val newApplications = applications.map { case (b, fas) =>
+ val bp = if (b == start) newStart else b
+ bp -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
+ }
+
+ val newQuantifications = quantifications.map(_.substitute(substituter))
+
+ val newMatchers = matchers.map { case (b, ms) =>
+ val bp = if (b == start) newStart else b
+ bp -> ms.map(_.substitute(substituter))
+ }
+
+ val newLambdas = lambdas.map(_.substitute(substituter))
+
+ val newDependencies = dependencies.map(p => p._1 -> substituter(p._2))
+
+ new LambdaTemplate[T](
+ ids._1 -> substituter(ids._2),
+ encoder,
+ manager,
+ pathVar._1 -> newStart,
+ arguments,
+ condVars,
+ exprVars,
+ condTree,
+ newClauses,
+ newBlockers,
+ newApplications,
+ newQuantifications,
+ newMatchers,
+ newLambdas,
+ newDependencies,
+ structuralKey,
+ stringRepr
+ )
+ }
+
+ private lazy val str : String = stringRepr()
+ override def toString : String = str
+
+ lazy val key: (Expr, Seq[T]) = {
+ def rec(e: Expr): Seq[Identifier] = e match {
+ case Variable(id) =>
+ if (dependencies.isDefinedAt(id)) {
+ Seq(id)
+ } else {
+ Seq.empty
+ }
+
+ case Operator(es, _) => es.flatMap(rec)
+
+ case _ => Seq.empty
+ }
+
+ structuralKey -> rec(structuralKey).distinct.map(dependencies)
+ }
+
+ override def equals(that: Any): Boolean = that match {
+ case t: LambdaTemplate[T] =>
+ val (lambda1, deps1) = key
+ val (lambda2, deps2) = t.key
+ (lambda1 == lambda2) && {
+ (deps1 zip deps2).forall { case (id1, id2) =>
+ (manager.byID.get(id1), manager.byID.get(id2)) match {
+ case (Some(t1), Some(t2)) => t1 == t2
+ case _ => id1 == id2
+ }
+ }
+ }
+
+ case _ => false
+ }
+
+ override def hashCode: Int = key.hashCode
+
+ override def instantiate(substMap: Map[T, T]): Instantiation[T] = {
+ super.instantiate(substMap) ++ manager.instantiateAxiom(this, substMap)
+ }
+}
+
+class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(encoder) {
private[templates] lazy val trueT = encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
- protected val byID = new IncrementalMap[T, LambdaTemplate[T]]
- protected val byType = new IncrementalMap[FunctionType, Set[(T, LambdaTemplate[T])]].withDefaultValue(Set.empty)
- protected val applications = new IncrementalMap[FunctionType, Set[(T, App[T])]].withDefaultValue(Set.empty)
- protected val freeLambdas = new IncrementalMap[FunctionType, Set[T]].withDefaultValue(Set.empty)
+ protected[templates] val byID = new IncrementalMap[T, LambdaTemplate[T]]
+ protected val byType = new IncrementalMap[FunctionType, Set[LambdaTemplate[T]]].withDefaultValue(Set.empty)
+ protected val applications = new IncrementalMap[FunctionType, Set[(T, App[T])]].withDefaultValue(Set.empty)
+ protected val freeLambdas = new IncrementalMap[FunctionType, Set[T]].withDefaultValue(Set.empty)
private val instantiated = new IncrementalSet[(T, App[T])]
- protected def incrementals: List[IncrementalState] =
- List(byID, byType, applications, freeLambdas, instantiated)
-
- def clear(): Unit = incrementals.foreach(_.clear())
- def reset(): Unit = incrementals.foreach(_.reset())
- def push(): Unit = incrementals.foreach(_.push())
- def pop(): Unit = incrementals.foreach(_.pop())
+ override protected def incrementals: List[IncrementalState] =
+ super.incrementals ++ List(byID, byType, applications, freeLambdas, instantiated)
def registerFree(lambdas: Seq[(Identifier, T)]): Unit = {
for ((id, idT) <- lambdas) id.getType match {
@@ -40,21 +205,26 @@ class LambdaManager[T](protected[templates] val encoder: TemplateEncoder[T]) ext
def instantiateLambda(template: LambdaTemplate[T]): Instantiation[T] = {
val idT = template.ids._2
- var clauses : Clauses[T] = equalityClauses(idT, template)
+ var clauses : Clauses[T] = equalityClauses(template)
var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
// make sure the new lambda isn't equal to any free lambda var
clauses ++= freeLambdas(template.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
byID += idT -> template
- byType += template.tpe -> (byType(template.tpe) + (idT -> template))
- for (blockedApp @ (_, App(caller, tpe, args)) <- applications(template.tpe)) {
- val equals = encoder.mkEquals(idT, caller)
- appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(template, equals, args)))
- }
+ if (byType(template.tpe)(template)) {
+ (clauses, Map.empty, Map.empty)
+ } else {
+ byType += template.tpe -> (byType(template.tpe) + template)
+
+ for (blockedApp @ (_, App(caller, tpe, args)) <- applications(template.tpe)) {
+ val equals = encoder.mkEquals(idT, caller)
+ appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(template, equals, args)))
+ }
- (clauses, Map.empty, appBlockers)
+ (clauses, Map.empty, appBlockers)
+ }
}
def instantiateApp(blocker: T, app: App[T]): Instantiation[T] = {
@@ -75,8 +245,8 @@ class LambdaManager[T](protected[templates] val encoder: TemplateEncoder[T]) ext
// so that UnrollingBank will generate the initial block!
val init = instantiation withApps Map(key -> Set.empty)
val inst = byType(tpe).foldLeft(init) {
- case (instantiation, (idT, template)) =>
- val equals = encoder.mkEquals(idT, caller)
+ case (instantiation, template) =>
+ val equals = encoder.mkEquals(template.ids._2, caller)
instantiation withApp (key -> TemplateAppInfo(template, equals, args))
}
@@ -88,16 +258,21 @@ class LambdaManager[T](protected[templates] val encoder: TemplateEncoder[T]) ext
}
}
- private def equalityClauses(idT: T, template: LambdaTemplate[T]): Seq[T] = {
- byType(template.tpe).map { case (thatIdT, that) =>
- val equals = encoder.mkEquals(idT, thatIdT)
- template.contextEquality(that) match {
- case None => encoder.mkNot(equals)
- case Some(Seq()) => equals
- case Some(seq) => encoder.mkEquals(encoder.mkAnd(seq : _*), equals)
+ private def equalityClauses(template: LambdaTemplate[T]): Seq[T] = {
+ val (s1, deps1) = template.key
+ byType(template.tpe).map { that =>
+ val (s2, deps2) = that.key
+ val equals = encoder.mkEquals(template.ids._2, that.ids._2)
+ if (s1 == s2) {
+ val pairs = (deps1 zip deps2).filter(p => p._1 != p._2)
+ if (pairs.isEmpty) equals else {
+ val eqs = pairs.map(p => encoder.mkEquals(p._1, p._2))
+ encoder.mkEquals(encoder.mkAnd(eqs : _*), equals)
+ }
+ } else {
+ encoder.mkNot(equals)
}
}.toSeq
}
-
}
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index f2d1c1d6f47f52b266faf0b39173977874ea5179..c7f715b5eefe573d88eeb94b45293ba7cde646bf 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -45,7 +45,7 @@ case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[Either[T, Matcher[T]]]
class QuantificationTemplate[T](
val quantificationManager: QuantificationManager[T],
- val start: T,
+ val pathVar: (Identifier, T),
val qs: (Identifier, T),
val q2s: (Identifier, T),
val insts: (Identifier, T),
@@ -53,16 +53,19 @@ class QuantificationTemplate[T](
val quantifiers: Seq[(Identifier, T)],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
+ val condTree: Map[Identifier, Set[Identifier]],
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Seq[LambdaTemplate[T]]) {
+ lazy val start = pathVar._2
+
def substitute(substituter: T => T): QuantificationTemplate[T] = {
new QuantificationTemplate[T](
quantificationManager,
- substituter(start),
+ pathVar._1 -> substituter(start),
qs,
q2s,
insts,
@@ -70,6 +73,7 @@ class QuantificationTemplate[T](
quantifiers,
condVars,
exprVars,
+ condTree,
clauses.map(substituter),
blockers.map { case (b, fis) =>
substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
@@ -97,6 +101,7 @@ object QuantificationTemplate {
quantifiers: Seq[(Identifier, T)],
condVars: Map[Identifier, T],
exprVars: Map[Identifier, T],
+ condTree: Map[Identifier, Set[Identifier]],
guardedExprs: Map[Identifier, Seq[Expr]],
lambdas: Seq[LambdaTemplate[T]],
subst: Map[Identifier, T]
@@ -111,8 +116,8 @@ object QuantificationTemplate {
substMap = subst + q2s + insts + guards + qs)
new QuantificationTemplate[T](quantificationManager,
- pathVar._2, qs, q2s, insts, guards._2, quantifiers,
- condVars, exprVars, clauses, blockers, applications, matchers, lambdas)
+ pathVar, qs, q2s, insts, guards._2, quantifiers,
+ condVars, exprVars, condTree, clauses, blockers, applications, matchers, lambdas)
}
}
@@ -190,20 +195,6 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(typeInsts, partialInsts, lambdaInsts)
}
- def toto: (Map[TypeTree, Matchers], Map[T, Matchers], Map[Lambda, Matchers]) = {
- var typeInsts: Map[TypeTree, Matchers] = Map.empty
- var partialInsts: Map[T, Matchers] = Map.empty
- var lambdaInsts: Map[Lambda, Matchers] = Map.empty
-
- for ((key, matchers) <- ignored.instantiations) key match {
- case TypeKey(tpe) => typeInsts += tpe -> matchers
- case CallerKey(caller, _) => partialInsts += caller -> matchers
- case LambdaKey(lambda, _) => lambdaInsts += lambda -> matchers
- }
-
- (typeInsts, partialInsts, lambdaInsts)
- }
-
override def registerFree(ids: Seq[(Identifier, T)]): Unit = {
super.registerFree(ids)
known ++= ids.map(_._2)
@@ -214,7 +205,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
case _ => 0
}).max
- private def encodeEnablers(es: Set[T]): T = encoder.mkAnd(es.toSeq.sortBy(_.toString) : _*)
+ private def encodeEnablers(es: Set[T]): T =
+ if (es.isEmpty) trueT else encoder.mkAnd(es.toSeq.sortBy(_.toString) : _*)
private type Matchers = Set[(T, Matcher[T])]
@@ -338,16 +330,20 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private trait MatcherQuantification {
+ val pathVar: (Identifier, T)
val quantified: Set[T]
val matchers: Set[Matcher[T]]
val allMatchers: Map[T, Set[Matcher[T]]]
val condVars: Map[Identifier, T]
val exprVars: Map[Identifier, T]
+ val condTree: Map[Identifier, Set[Identifier]]
val clauses: Seq[T]
val blockers: Map[T, Set[TemplateCallInfo[T]]]
val applications: Map[T, Set[App[T]]]
val lambdas: Seq[LambdaTemplate[T]]
+ lazy val start = pathVar._2
+
private lazy val depth = matchers.map(matcherDepth).max
private lazy val transMatchers: Set[Matcher[T]] = (for {
(b, ms) <- allMatchers.toSeq
@@ -404,6 +400,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private def extractSubst(mapping: Set[(Set[T], Matcher[T], Matcher[T])]): (Set[T], Map[T,Either[T, Matcher[T]]], Boolean) = {
var constraints: Set[T] = Set.empty
+ var eqConstraints: Set[(T, T)] = Set.empty
var matcherEqs: List[(T, T)] = Nil
var subst: Map[T, Either[T, Matcher[T]]] = Map.empty
@@ -414,17 +411,20 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(qarg, arg) <- (qargs zip args)
} qarg match {
case Left(quant) if subst.isDefinedAt(quant) =>
- constraints += encoder.mkEquals(quant, Matcher.argValue(arg))
+ eqConstraints += (quant -> Matcher.argValue(arg))
case Left(quant) if quantified(quant) =>
subst += quant -> arg
case Right(qam) =>
val argVal = Matcher.argValue(arg)
- constraints += encoder.mkEquals(qam.encoded, argVal)
+ eqConstraints += (qam.encoded -> argVal)
matcherEqs :+= qam.encoded -> argVal
}
val substituter = encoder.substitute(subst.mapValues(Matcher.argValue))
- val enablers = (if (constraints.isEmpty) Set(trueT) else constraints).map(substituter)
+ val substConstraints = constraints.filter(_ != trueT).map(substituter)
+ val substEqs = eqConstraints.map(p => substituter(p._1) -> p._2)
+ .filter(p => p._1 != p._2).map(p => encoder.mkEquals(p._1, p._2))
+ val enablers = substConstraints ++ substEqs
val isStrict = matcherEqs.forall(p => substituter(p._1) == p._2)
(enablers, subst, isStrict)
@@ -435,29 +435,35 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
for (mapping <- mappings(bs, matcher)) {
val (enablers, subst, isStrict) = extractSubst(mapping)
- val enabler = encodeEnablers(enablers)
+ val (enabler, optEnabler) = freshBlocker(enablers)
- val baseSubstMap = (condVars ++ exprVars).map { case (id, idT) => idT -> encoder.encodeId(id) }
- val lambdaSubstMap = lambdas map(lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
- val substMap = subst.mapValues(Matcher.argValue) ++ baseSubstMap ++ lambdaSubstMap ++ instanceSubst(enabler)
+ if (optEnabler.isDefined) {
+ instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
+ }
- instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
- clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
+ val baseSubstMap = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
+ freshConds(pathVar._1 -> enabler, condVars, condTree)
+ val lambdaSubstMap = lambdas map (lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
+ val substMap = subst.mapValues(Matcher.argValue) ++ baseSubstMap ++ lambdaSubstMap ++ instanceSubst(enablers)
+ if (!skip(substMap)) {
+ instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
+ clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
- val msubst = subst.collect { case (c, Right(m)) => c -> m }
- val substituter = encoder.substitute(substMap)
+ val msubst = subst.collect { case (c, Right(m)) => c -> m }
+ val substituter = encoder.substitute(substMap)
- for ((b,ms) <- allMatchers; m <- ms) {
- val sb = enablers + substituter(b)
- val sm = m.substitute(substituter, matcherSubst = msubst)
+ for ((b,ms) <- allMatchers; m <- ms) {
+ val sb = enablers ++ (if (b == start) Set.empty else Set(substituter(b)))
+ val sm = m.substitute(substituter, matcherSubst = msubst)
- if (matchers(m)) {
- handled += sb -> sm
- } else if (transMatchers(m) && isStrict) {
- instantiation ++= instCtx.instantiate(sb, sm)(quantifications.toSeq : _*)
- } else {
- ignored += sb -> sm
+ if (matchers(m)) {
+ handled += sb -> sm
+ } else if (transMatchers(m) && isStrict) {
+ instantiation ++= instCtx.instantiate(sb, sm)(quantifications.toSeq : _*)
+ } else {
+ ignored += sb -> sm
+ }
}
}
}
@@ -465,10 +471,13 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
instantiation
}
- protected def instanceSubst(enabler: T): Map[T, T]
+ protected def instanceSubst(enablers: Set[T]): Map[T, T]
+
+ protected def skip(subst: Map[T, T]): Boolean = false
}
private class Quantification (
+ val pathVar: (Identifier, T),
val qs: (Identifier, T),
val q2s: (Identifier, T),
val insts: (Identifier, T),
@@ -478,6 +487,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val allMatchers: Map[T, Set[Matcher[T]]],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
+ val condTree: Map[Identifier, Set[Identifier]],
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
@@ -485,10 +495,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
var currentQ2Var: T = qs._2
- protected def instanceSubst(enabler: T): Map[T, T] = {
+ protected def instanceSubst(enablers: Set[T]): Map[T, T] = {
val nextQ2Var = encoder.encodeId(q2s._1)
- val subst = Map(qs._2 -> currentQ2Var, guardVar -> enabler,
+ val subst = Map(qs._2 -> currentQ2Var, guardVar -> encodeEnablers(enablers),
q2s._2 -> nextQ2Var, insts._2 -> encoder.encodeId(insts._1))
currentQ2Var = nextQ2Var
@@ -498,9 +508,23 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private lazy val blockerId = FreshIdentifier("blocker", BooleanType, true)
private lazy val blockerCache: MutableMap[T, T] = MutableMap.empty
+ private def freshBlocker(enablers: Set[T]): (T, Option[T]) = enablers.toSeq match {
+ case Seq(b) if isBlocker(b) => (b, None)
+ case _ =>
+ val enabler = encodeEnablers(enablers)
+ blockerCache.get(enabler) match {
+ case Some(b) => (b, None)
+ case None =>
+ val nb = encoder.encodeId(blockerId)
+ blockerCache += enabler -> nb
+ for (b <- enablers if isBlocker(b)) implies(b, nb)
+ blocker(nb)
+ (nb, Some(enabler))
+ }
+ }
- private class Axiom (
- val start: T,
+ private class LambdaAxiom (
+ val pathVar: (Identifier, T),
val blocker: T,
val guardVar: T,
val quantified: Set[T],
@@ -508,22 +532,24 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val allMatchers: Map[T, Set[Matcher[T]]],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
+ val condTree: Map[Identifier, Set[Identifier]],
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
val lambdas: Seq[LambdaTemplate[T]]) extends MatcherQuantification {
- protected def instanceSubst(enabler: T): Map[T, T] = {
- val newBlocker = blockerCache.get(enabler) match {
- case Some(b) => b
- case None =>
- val nb = encoder.encodeId(blockerId)
- blockerCache += enabler -> nb
- blockerCache += nb -> nb
- nb
- }
+ protected def instanceSubst(enablers: Set[T]): Map[T, T] = {
+ // no need to add an equality clause here since it is already contained in the Axiom clauses
+ val (newBlocker, optEnabler) = freshBlocker(enablers)
+ val guardT = if (optEnabler.isDefined) encoder.mkAnd(start, optEnabler.get) else start
+ Map(guardVar -> guardT, blocker -> newBlocker)
+ }
- Map(guardVar -> encoder.mkAnd(start, enabler), blocker -> newBlocker)
+ override protected def skip(subst: Map[T, T]): Boolean = {
+ val substituter = encoder.substitute(subst)
+ allMatchers.forall { case (b, ms) =>
+ ms.forall(m => matchers(m) || instCtx(Set(substituter(b)) -> m.substitute(substituter)))
+ }
}
}
@@ -577,7 +603,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val enablingClause = encoder.mkImplies(guardT, blockerT)
instantiateAxiom(
- substMap(template.start),
+ template.pathVar._1 -> substMap(template.start),
blockerT,
guardT,
quantifiers,
@@ -585,6 +611,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
allMatchers + (template.start -> (allMatchers.getOrElse(template.start, Set.empty) + selfMatcher)),
template.condVars map { case (id, idT) => id -> substituter(idT) },
template.exprVars map { case (id, idT) => id -> substituter(idT) },
+ template.condTree,
(template.clauses map substituter) :+ enablingClause,
template.blockers map { case (b, fis) =>
substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
@@ -598,7 +625,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
def instantiateAxiom(
- start: T,
+ pathVar: (Identifier, T),
blocker: T,
guardVar: T,
quantifiers: Seq[(Identifier, T)],
@@ -606,6 +633,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
allMatchers: Map[T, Set[Matcher[T]]],
condVars: Map[Identifier, T],
exprVars: Map[Identifier, T],
+ condTree: Map[Identifier, Set[Identifier]],
clauses: Seq[T],
blockers: Map[T, Set[TemplateCallInfo[T]]],
applications: Map[T, Set[App[T]]],
@@ -617,8 +645,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
var instantiation = Instantiation.empty[T]
for (matchers <- matchQuorums) {
- val axiom = new Axiom(start, blocker, guardVar, quantified,
- matchers, allMatchers, condVars, exprVars,
+ val axiom = new LambdaAxiom(pathVar, blocker, guardVar, quantified,
+ matchers, allMatchers, condVars, exprVars, condTree,
clauses, blockers, applications, lambdas
)
@@ -638,7 +666,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
m <- matchers
sm = m.substitute(substituter)
if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
- } instantiation ++= instCtx.instantiate(Set(trueT), sm)(quantifications.toSeq : _*)
+ } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
instantiation
}
@@ -654,13 +682,16 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val subst = substMap + (template.qs._2 -> newQ)
val substituter = encoder.substitute(subst)
- val quantification = new Quantification(template.qs._1 -> newQ,
+ val quantification = new Quantification(
+ template.pathVar._1 -> substituter(template.start),
+ template.qs._1 -> newQ,
template.q2s, template.insts, template.guardVar,
quantified,
matchers map (_.substitute(substituter)),
template.matchers map { case (b, ms) => substituter(b) -> ms.map(_.substitute(substituter)) },
template.condVars,
template.exprVars,
+ template.condTree,
template.clauses map substituter,
template.blockers map { case (b, fis) =>
substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
@@ -697,7 +728,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(_, ms) <- template.matchers; m <- ms
sm = m.substitute(substituter)
if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
- } instantiation ++= instCtx.instantiate(Set(trueT), sm)(quantifications.toSeq : _*)
+ } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
instantiation
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 5e6b7213c968558a7143b5ced41487b14d2a9ea3..4434eafd5ae0569640b1c4f7cc60c3946ef56d7b 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -9,15 +9,29 @@ import purescala.Expressions._
import purescala.Extractors._
import purescala.ExprOps._
import purescala.Types._
+import purescala.TypeOps._
import purescala.Definitions._
import purescala.Constructors._
import purescala.Quantification._
+import Instantiation._
+
class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val assumePreHolds: Boolean) {
private var cache = Map[TypedFunDef, FunctionTemplate[T]]()
private var cacheExpr = Map[Expr, FunctionTemplate[T]]()
+ private type Clauses = (
+ Map[Identifier,T],
+ Map[Identifier,T],
+ Map[Identifier, Set[Identifier]],
+ Map[Identifier, Seq[Expr]],
+ Seq[LambdaTemplate[T]],
+ Seq[QuantificationTemplate[T]]
+ )
+
+ private def emptyClauses: Clauses = (Map.empty, Map.empty, Map.empty, Map.empty, Seq.empty, Seq.empty)
+
val manager = new QuantificationManager[T](encoder)
def mkTemplate(body: Expr): FunctionTemplate[T] = {
@@ -71,16 +85,14 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val substMap : Map[Identifier, T] = arguments.toMap + pathVar
- val (bodyConds, bodyExprs, bodyGuarded, bodyLambdas, bodyQuantifications) = if (isRealFunDef) {
- invocationEqualsBody.map(expr => mkClauses(start, expr, substMap)).getOrElse {
- (Map[Identifier,T](), Map[Identifier,T](), Map[Identifier,Seq[Expr]](), Seq[LambdaTemplate[T]](), Seq[QuantificationTemplate[T]]())
- }
+ val (bodyConds, bodyExprs, bodyTree, bodyGuarded, bodyLambdas, bodyQuantifications) = if (isRealFunDef) {
+ invocationEqualsBody.map(expr => mkClauses(start, expr, substMap)).getOrElse(emptyClauses)
} else {
mkClauses(start, lambdaBody.get, substMap)
}
// Now the postcondition.
- val (condVars, exprVars, guardedExprs, lambdas, quantifications) = tfd.postcondition match {
+ val (condVars, exprVars, condTree, guardedExprs, lambdas, quantifications) = tfd.postcondition match {
case Some(post) =>
val newPost : Expr = application(matchToIfThenElse(post), Seq(invocation))
@@ -95,19 +107,15 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
newPost
}
- val (postConds, postExprs, postGuarded, postLambdas, postQuantifications) = mkClauses(start, postHolds, substMap)
- val allGuarded = (bodyGuarded.keys ++ postGuarded.keys).map { k =>
- k -> (bodyGuarded.getOrElse(k, Seq.empty) ++ postGuarded.getOrElse(k, Seq.empty))
- }.toMap
-
- (bodyConds ++ postConds, bodyExprs ++ postExprs, allGuarded, bodyLambdas ++ postLambdas, bodyQuantifications ++ postQuantifications)
+ val (postConds, postExprs, postTree, postGuarded, postLambdas, postQuantifications) = mkClauses(start, postHolds, substMap)
+ (bodyConds ++ postConds, bodyExprs ++ postExprs, bodyTree merge postTree, bodyGuarded merge postGuarded, bodyLambdas ++ postLambdas, bodyQuantifications ++ postQuantifications)
case None =>
- (bodyConds, bodyExprs, bodyGuarded, bodyLambdas, bodyQuantifications)
+ (bodyConds, bodyExprs, bodyTree, bodyGuarded, bodyLambdas, bodyQuantifications)
}
val template = FunctionTemplate(tfd, encoder, manager,
- pathVar, arguments, condVars, exprVars, guardedExprs, quantifications, lambdas, isRealFunDef)
+ pathVar, arguments, condVars, exprVars, condTree, guardedExprs, quantifications, lambdas, isRealFunDef)
cache += tfd -> template
template
}
@@ -173,11 +181,21 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
(quantified, flatConj)
}
- def mkClauses(pathVar: Identifier, expr: Expr, substMap: Map[Identifier, T]):
- (Map[Identifier,T], Map[Identifier,T], Map[Identifier, Seq[Expr]], Seq[LambdaTemplate[T]], Seq[QuantificationTemplate[T]]) = {
+ def mkClauses(pathVar: Identifier, expr: Expr, substMap: Map[Identifier, T]): Clauses = {
+ val (p, (condVars, exprVars, condTree, guardedExprs, lambdas, quantifications)) = mkExprClauses(pathVar, expr, substMap)
+ val allGuarded = guardedExprs + (pathVar -> (p +: guardedExprs.getOrElse(pathVar, Seq.empty)))
+ (condVars, exprVars, condTree, allGuarded, lambdas, quantifications)
+ }
+
+ private def mkExprClauses(pathVar: Identifier, expr: Expr, substMap: Map[Identifier, T]): (Expr, Clauses) = {
var condVars = Map[Identifier, T]()
- @inline def storeCond(id: Identifier) : Unit = condVars += id -> encoder.encodeId(id)
+ var condTree = Map[Identifier, Set[Identifier]](pathVar -> Set.empty).withDefaultValue(Set.empty)
+ def storeCond(pathVar: Identifier, id: Identifier) : Unit = {
+ condVars += id -> encoder.encodeId(id)
+ condTree += pathVar -> (condTree(pathVar) + id)
+ }
+
@inline def encodedCond(id: Identifier) : T = substMap.getOrElse(id, condVars(id))
var exprVars = Map[Identifier, T]()
@@ -210,13 +228,32 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
def requireDecomposition(e: Expr) = {
exists{
- case (_: Choose) | (_: Forall) => true
+ case (_: Choose) | (_: Forall) | (_: Lambda) => true
case (_: Assert) | (_: Ensuring) => true
case (_: FunctionInvocation) | (_: Application) => true
case _ => false
}(e)
}
+ def groupWhile[T](es: Seq[T])(p: T => Boolean): Seq[Seq[T]] = {
+ var res: Seq[Seq[T]] = Nil
+
+ var c = es
+ while (!c.isEmpty) {
+ val (span, rest) = c.span(p)
+
+ if (span.isEmpty) {
+ res :+= Seq(rest.head)
+ c = rest.tail
+ } else {
+ res :+= span
+ c = rest
+ }
+ }
+
+ res
+ }
+
def rec(pathVar: Identifier, expr: Expr): Expr = {
expr match {
case a @ Assert(cond, err, body) =>
@@ -260,13 +297,71 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
case p : Passes => sys.error("'Passes's should have been eliminated before generating templates.")
case i @ Implies(lhs, rhs) =>
- implies(rec(pathVar, lhs), rec(pathVar, rhs))
+ if (requireDecomposition(i)) {
+ rec(pathVar, Or(Not(lhs), rhs))
+ } else {
+ implies(rec(pathVar, lhs), rec(pathVar, rhs))
+ }
case a @ And(parts) =>
- andJoin(parts.map(rec(pathVar, _)))
+ val partitions = groupWhile(parts)(!requireDecomposition(_))
+ partitions.map(andJoin) match {
+ case Seq(e) => e
+ case seq =>
+ val newExpr : Identifier = FreshIdentifier("e", BooleanType, true)
+ storeExpr(newExpr)
+
+ def recAnd(pathVar: Identifier, partitions: Seq[Expr]): Unit = partitions match {
+ case x :: Nil if !requireDecomposition(x) =>
+ storeGuarded(pathVar, Equals(Variable(newExpr), x))
+
+ case x :: xs =>
+ val newBool : Identifier = FreshIdentifier("b", BooleanType, true)
+ storeCond(pathVar, newBool)
+
+ val xrec = rec(pathVar, x)
+ storeGuarded(pathVar, Equals(Variable(newBool), xrec))
+ storeGuarded(pathVar, Implies(Not(Variable(newBool)), Not(Variable(newExpr))))
+
+ recAnd(newBool, xs)
+
+ case Nil =>
+ storeGuarded(pathVar, Variable(newExpr))
+ }
+
+ recAnd(pathVar, seq)
+ Variable(newExpr)
+ }
case o @ Or(parts) =>
- orJoin(parts.map(rec(pathVar, _)))
+ val partitions = groupWhile(parts)(!requireDecomposition(_))
+ partitions.map(orJoin) match {
+ case Seq(e) => e
+ case seq =>
+ val newExpr : Identifier = FreshIdentifier("e", BooleanType, true)
+ storeExpr(newExpr)
+
+ def recOr(pathVar: Identifier, partitions: Seq[Expr]): Unit = partitions match {
+ case x :: Nil if !requireDecomposition(x) =>
+ storeGuarded(pathVar, Equals(Variable(newExpr), x))
+
+ case x :: xs =>
+ val newBool : Identifier = FreshIdentifier("b", BooleanType, true)
+ storeCond(pathVar, newBool)
+
+ val xrec = rec(pathVar, x)
+ storeGuarded(pathVar, Equals(Not(Variable(newBool)), xrec))
+ storeGuarded(pathVar, Implies(Not(Variable(newBool)), Variable(newExpr)))
+
+ recOr(newBool, xs)
+
+ case Nil =>
+ storeGuarded(pathVar, Not(Variable(newExpr)))
+ }
+
+ recOr(pathVar, seq)
+ Variable(newExpr)
+ }
case i @ IfExpr(cond, thenn, elze) => {
if(!requireDecomposition(i)) {
@@ -276,8 +371,8 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val newBool2 : Identifier = FreshIdentifier("b", BooleanType, true)
val newExpr : Identifier = FreshIdentifier("e", i.getType, true)
- storeCond(newBool1)
- storeCond(newBool2)
+ storeCond(pathVar, newBool1)
+ storeCond(pathVar, newBool2)
storeExpr(newExpr)
@@ -314,17 +409,17 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val idArgs : Seq[Identifier] = lambdaArgs(l)
val trArgs : Seq[T] = idArgs.map(id => substMap.getOrElse(id, encoder.encodeId(id)))
- val lid = FreshIdentifier("lambda", l.getType, true)
+ val lid = FreshIdentifier("lambda", bestRealType(l.getType), true)
val clause = liftedEquals(Variable(lid), l, idArgs, inlineFirst = true)
val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
val clauseSubst: Map[Identifier, T] = localSubst ++ (idArgs zip trArgs)
- val (lambdaConds, lambdaExprs, lambdaGuarded, lambdaTemplates, lambdaQuants) = mkClauses(pathVar, clause, clauseSubst)
+ val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaTemplates, lambdaQuants) = mkClauses(pathVar, clause, clauseSubst)
val ids: (Identifier, T) = lid -> storeLambda(lid)
val dependencies: Map[Identifier, T] = variablesOf(l).map(id => id -> localSubst(id)).toMap
val template = LambdaTemplate(ids, encoder, manager, pathVar -> encodedCond(pathVar),
- idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaGuarded, lambdaQuants, lambdaTemplates, localSubst, dependencies, l)
+ idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaQuants, lambdaTemplates, localSubst, dependencies, l)
registerLambda(template)
Variable(lid)
@@ -350,14 +445,16 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val qs: (Identifier, T) = q -> encoder.encodeId(q)
val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
val clauseSubst: Map[Identifier, T] = localSubst ++ (idQuantifiers zip trQuantifiers)
- val (qConds, qExprs, qGuarded, qTemplates, qQuants) = mkClauses(pathVar, clause, clauseSubst)
+ val (p, (qConds, qExprs, qTree, qGuarded, qTemplates, qQuants)) = mkExprClauses(pathVar, flatConj, clauseSubst)
assert(qQuants.isEmpty, "Unhandled nested quantification in "+clause)
- val binder = Equals(Variable(q), And(Variable(q2), Variable(inst)))
- val allQGuarded = qGuarded + (pathVar -> (binder +: qGuarded.getOrElse(pathVar, Seq.empty)))
+ val allGuarded = qGuarded + (pathVar -> (Seq(
+ Equals(Variable(inst), Implies(Variable(guard), p)),
+ Equals(Variable(q), And(Variable(q2), Variable(inst)))
+ ) ++ qGuarded.getOrElse(pathVar, Seq.empty)))
val template = QuantificationTemplate[T](encoder, manager, pathVar -> encodedCond(pathVar),
- qs, q2, inst, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, allQGuarded, qTemplates, localSubst)
+ qs, q2, inst, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qTree, allGuarded, qTemplates, localSubst)
registerQuantification(template)
Variable(q)
}
@@ -369,9 +466,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
}
val p = rec(pathVar, expr)
- storeGuarded(pathVar, p)
-
- (condVars, exprVars, guardedExprs, lambdas, quantifications)
+ (p, (condVars, exprVars, condTree, guardedExprs, lambdas, quantifications))
}
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateInfo.scala b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
index 977aeb5711b66c006161ff1af28fe5b9604456eb..033f15dd6f251026a260ed6344212239e1714a37 100644
--- a/src/main/scala/leon/solvers/templates/TemplateInfo.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
@@ -14,6 +14,6 @@ case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[T]) {
case class TemplateAppInfo[T](template: LambdaTemplate[T], equals: T, args: Seq[T]) {
override def toString = {
- template.ids._1 + "|" + equals + args.mkString("(", ",", ")")
+ template.ids._2 + "|" + equals + args.mkString("(", ",", ")")
}
}
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
similarity index 69%
rename from src/main/scala/leon/solvers/templates/Templates.scala
rename to src/main/scala/leon/solvers/templates/TemplateManager.scala
index 5e7302c549720a0291ecedf592c4a28d181b59fd..bb6629ec16988a79eb686259aea4fa32c6111dbb 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -11,10 +11,11 @@ import purescala.Quantification._
import purescala.Extractors._
import purescala.ExprOps._
import purescala.Types._
+import purescala.TypeOps._
-case class App[T](caller: T, tpe: FunctionType, args: Seq[T]) {
- override def toString = "(" + caller + " : " + tpe + ")" + args.mkString("(", ",", ")")
-}
+import utils._
+
+import scala.collection.generic.CanBuildFrom
object Instantiation {
type Clauses[T] = Seq[T]
@@ -24,12 +25,18 @@ object Instantiation {
def empty[T] = (Seq.empty[T], Map.empty[T, Set[TemplateCallInfo[T]]], Map.empty[(T, App[T]), Set[TemplateAppInfo[T]]])
- implicit class MapWrapper[A,B](map: Map[A,Set[B]]) {
+ implicit class MapSetWrapper[A,B](map: Map[A,Set[B]]) {
def merge(that: Map[A,Set[B]]): Map[A,Set[B]] = (map.keys ++ that.keys).map { k =>
k -> (map.getOrElse(k, Set.empty) ++ that.getOrElse(k, Set.empty))
}.toMap
}
+ implicit class MapSeqWrapper[A,B](map: Map[A,Seq[B]]) {
+ def merge(that: Map[A,Seq[B]]): Map[A,Seq[B]] = (map.keys ++ that.keys).map { k =>
+ k -> (map.getOrElse(k, Seq.empty) ++ that.getOrElse(k, Seq.empty))
+ }.toMap
+ }
+
implicit class InstantiationWrapper[T](i: Instantiation[T]) {
def ++(that: Instantiation[T]): Instantiation[T] = {
val (thisClauses, thisBlockers, thisApps) = i
@@ -55,10 +62,11 @@ trait Template[T] { self =>
val encoder : TemplateEncoder[T]
val manager : QuantificationManager[T]
- val start : T
+ val pathVar: (Identifier, T)
val args : Seq[T]
val condVars : Map[Identifier, T]
val exprVars : Map[Identifier, T]
+ val condTree : Map[Identifier, Set[Identifier]]
val clauses : Seq[T]
val blockers : Map[T, Set[TemplateCallInfo[T]]]
val applications : Map[T, Set[App[T]]]
@@ -66,6 +74,8 @@ trait Template[T] { self =>
val matchers : Map[T, Set[Matcher[T]]]
val lambdas : Seq[LambdaTemplate[T]]
+ lazy val start = pathVar._2
+
private var substCache : Map[Seq[T],Map[T,T]] = Map.empty
def instantiate(aVar: T, args: Seq[T]): Instantiation[T] = {
@@ -73,7 +83,8 @@ trait Template[T] { self =>
val baseSubstMap : Map[T,T] = substCache.get(args) match {
case Some(subst) => subst
case None =>
- val subst = (condVars ++ exprVars).map { case (id, idT) => idT -> encoder.encodeId(id) } ++
+ val subst = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
+ manager.freshConds(pathVar._1 -> aVar, condVars, condTree) ++
(this.args zip args)
substCache += args -> subst
subst
@@ -108,7 +119,7 @@ object Template {
val (fiArgs, appArgs) = args.splitAt(tfd.params.size)
val app @ Application(caller, arguments) = rec(FunctionInvocation(tfd, fiArgs), appArgs)
- Matcher(encodeExpr(caller), caller.getType, arguments.map(arg => Left(encodeExpr(arg))), encodeExpr(app))
+ Matcher(encodeExpr(caller), bestRealType(caller.getType), arguments.map(arg => Left(encodeExpr(arg))), encodeExpr(app))
}
def encode[T](
@@ -134,7 +145,9 @@ object Template {
}).toSeq
val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(_._2)))
- val optIdApp = optApp.map { case (idT, tpe) => App(idT, tpe, arguments.map(_._2)) }
+ val optIdApp = optApp.map { case (idT, tpe) =>
+ App(idT, bestRealType(tpe).asInstanceOf[FunctionType], arguments.map(_._2))
+ }
lazy val invocMatcher = optCall.filter(_.returnType.isInstanceOf[FunctionType])
.map(tfd => invocationMatcher(encodeExpr)(tfd, arguments.map(_._1.toVariable)))
@@ -152,7 +165,7 @@ object Template {
for (e <- es) {
funInfos ++= firstOrderCallsOf(e).map(p => TemplateCallInfo(p._1, p._2.map(encodeExpr)))
appInfos ++= firstOrderAppsOf(e).map { case (c, args) =>
- App(encodeExpr(c), c.getType.asInstanceOf[FunctionType], args.map(encodeExpr))
+ App(encodeExpr(c), bestRealType(c.getType).asInstanceOf[FunctionType], args.map(encodeExpr))
}
matchInfos ++= fold[Map[Expr, Matcher[T]]] { (expr, res) =>
@@ -167,7 +180,7 @@ object Template {
case None => Left(encodeExpr(arg))
})
- Some(expr -> Matcher(encodeExpr(c), c.getType, encodedArgs, encodeExpr(expr)))
+ Some(expr -> Matcher(encodeExpr(c), bestRealType(c.getType), encodedArgs, encodeExpr(expr)))
case _ => None
})
}(e).values
@@ -270,6 +283,7 @@ object FunctionTemplate {
arguments: Seq[(Identifier, T)],
condVars: Map[Identifier, T],
exprVars: Map[Identifier, T],
+ condTree: Map[Identifier, Set[Identifier]],
guardedExprs: Map[Identifier, Seq[Expr]],
quantifications: Seq[QuantificationTemplate[T]],
lambdas: Seq[LambdaTemplate[T]],
@@ -291,10 +305,11 @@ object FunctionTemplate {
tfd,
encoder,
manager,
- pathVar._2,
+ pathVar,
arguments.map(_._2),
condVars,
exprVars,
+ condTree,
clauses,
blockers,
applications,
@@ -311,10 +326,11 @@ class FunctionTemplate[T] private(
val tfd: TypedFunDef,
val encoder: TemplateEncoder[T],
val manager: QuantificationManager[T],
- val start: T,
+ val pathVar: (Identifier, T),
val args: Seq[T],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
+ val condTree: Map[Identifier, Set[Identifier]],
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
@@ -333,152 +349,40 @@ class FunctionTemplate[T] private(
}
}
-object LambdaTemplate {
-
- def apply[T](
- ids: (Identifier, T),
- encoder: TemplateEncoder[T],
- manager: QuantificationManager[T],
- pathVar: (Identifier, T),
- arguments: Seq[(Identifier, T)],
- condVars: Map[Identifier, T],
- exprVars: Map[Identifier, T],
- guardedExprs: Map[Identifier, Seq[Expr]],
- quantifications: Seq[QuantificationTemplate[T]],
- lambdas: Seq[LambdaTemplate[T]],
- baseSubstMap: Map[Identifier, T],
- dependencies: Map[Identifier, T],
- lambda: Lambda
- ) : LambdaTemplate[T] = {
-
- val id = ids._2
- val tpe = ids._1.getType.asInstanceOf[FunctionType]
- val (clauses, blockers, applications, matchers, templateString) =
- Template.encode(encoder, pathVar, arguments, condVars, exprVars, guardedExprs, lambdas,
- substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
-
- val lambdaString : () => String = () => {
- "Template for lambda " + ids._1 + ": " + lambda + " is :\n" + templateString()
- }
-
- val (structuralLambda, structSubst) = normalizeStructure(lambda)
- val keyDeps = dependencies.map { case (id, idT) => structSubst(id) -> idT }
- val key = structuralLambda.asInstanceOf[Lambda]
-
- new LambdaTemplate[T](
- ids,
- encoder,
- manager,
- pathVar._2,
- arguments,
- condVars,
- exprVars,
- clauses,
- blockers,
- applications,
- quantifications,
- matchers,
- lambdas,
- keyDeps,
- key,
- lambdaString
- )
- }
-}
-
-class LambdaTemplate[T] private (
- val ids: (Identifier, T),
- val encoder: TemplateEncoder[T],
- val manager: QuantificationManager[T],
- val start: T,
- val arguments: Seq[(Identifier, T)],
- val condVars: Map[Identifier, T],
- val exprVars: Map[Identifier, T],
- val clauses: Seq[T],
- val blockers: Map[T, Set[TemplateCallInfo[T]]],
- val applications: Map[T, Set[App[T]]],
- val quantifications: Seq[QuantificationTemplate[T]],
- val matchers: Map[T, Set[Matcher[T]]],
- val lambdas: Seq[LambdaTemplate[T]],
- private[templates] val dependencies: Map[Identifier, T],
- private[templates] val structuralKey: Lambda,
- stringRepr: () => String) extends Template[T] {
+class TemplateManager[T](protected[templates] val encoder: TemplateEncoder[T]) extends IncrementalState {
+ private val condImplies = new IncrementalMap[T, Set[T]].withDefaultValue(Set.empty)
+ private val condImplied = new IncrementalMap[T, Set[T]].withDefaultValue(Set.empty)
- val args = arguments.map(_._2)
- val tpe = ids._1.getType.asInstanceOf[FunctionType]
+ protected def incrementals: List[IncrementalState] = List(condImplies, condImplied)
- def substitute(substituter: T => T): LambdaTemplate[T] = {
- val newStart = substituter(start)
- val newClauses = clauses.map(substituter)
- val newBlockers = blockers.map { case (b, fis) =>
- val bp = if (b == start) newStart else b
- bp -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- }
+ def clear(): Unit = incrementals.foreach(_.clear())
+ def reset(): Unit = incrementals.foreach(_.reset())
+ def push(): Unit = incrementals.foreach(_.push())
+ def pop(): Unit = incrementals.foreach(_.pop())
- val newApplications = applications.map { case (b, fas) =>
- val bp = if (b == start) newStart else b
- bp -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- }
+ def freshConds(path: (Identifier, T), condVars: Map[Identifier, T], tree: Map[Identifier, Set[Identifier]]): Map[T, T] = {
+ val subst = condVars.map { case (id, idT) => idT -> encoder.encodeId(id) }
+ val mapping = condVars.mapValues(subst) + path
- val newQuantifications = quantifications.map(_.substitute(substituter))
-
- val newMatchers = matchers.map { case (b, ms) =>
- val bp = if (b == start) newStart else b
- bp -> ms.map(_.substitute(substituter))
+ for ((parent, children) <- tree; ep = mapping(parent); child <- children) {
+ val ec = mapping(child)
+ condImplies += ep -> (condImplies(ep) + ec)
+ condImplied += ec -> (condImplied(ec) + ep)
}
- val newLambdas = lambdas.map(_.substitute(substituter))
-
- val newDependencies = dependencies.map(p => p._1 -> substituter(p._2))
-
- new LambdaTemplate[T](
- ids._1 -> substituter(ids._2),
- encoder,
- manager,
- newStart,
- arguments,
- condVars,
- exprVars,
- newClauses,
- newBlockers,
- newApplications,
- newQuantifications,
- newMatchers,
- newLambdas,
- newDependencies,
- structuralKey,
- stringRepr
- )
+ subst
}
- private lazy val str : String = stringRepr()
- override def toString : String = str
-
- def contextEquality(that: LambdaTemplate[T]) : Option[Seq[T]] = {
- if (structuralKey != that.structuralKey) {
- None // can't be equal
- } else if (dependencies.isEmpty) {
- Some(Seq.empty) // must be equal
- } else {
- def rec(e1: Expr, e2: Expr): Seq[T] = (e1,e2) match {
- case (Variable(id1), Variable(id2)) =>
- if (dependencies.isDefinedAt(id1)) {
- Seq(encoder.mkEquals(dependencies(id1), that.dependencies(id2)))
- } else {
- Seq.empty
- }
-
- case (Operator(es1, _), Operator(es2, _)) =>
- (es1 zip es2).flatMap(p => rec(p._1, p._2))
-
- case _ => Seq.empty
- }
-
- Some(rec(structuralKey, that.structuralKey))
+ def blocker(b: T): Unit = condImplies += (b -> Set.empty)
+ def isBlocker(b: T): Boolean = condImplies.isDefinedAt(b) || condImplied.isDefinedAt(b)
+
+ def implies(b1: T, b2: T): Unit = implies(b1, Set(b2))
+ def implies(b1: T, b2s: Set[T]): Unit = {
+ val fb2s = b2s.filter(_ != b1)
+ condImplies += b1 -> (condImplies(b1) ++ fb2s)
+ for (b2 <- fb2s) {
+ condImplied += b2 -> (condImplies(b2) + b1)
}
}
- override def instantiate(substMap: Map[T, T]): Instantiation[T] = {
- super.instantiate(substMap) ++ manager.instantiateAxiom(this, substMap)
- }
}
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index ddfb22b0bdbd2a3be90e8950b7a21144b472d299..d1c4432a3c69f1882c9b4a1787a12dc8cf64f520 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -19,7 +19,8 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
private val manager = templateGenerator.manager
// Function instantiations have their own defblocker
- private val defBlockers = new IncrementalMap[TemplateCallInfo[T], T]()
+ private val defBlockers = new IncrementalMap[TemplateCallInfo[T], T]()
+ private val lambdaBlockers = new IncrementalMap[TemplateAppInfo[T], T]()
// Keep which function invocation is guarded by which guard,
// also specify the generation of the blocker.
@@ -32,6 +33,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def push() {
callInfos.push()
defBlockers.push()
+ lambdaBlockers.push()
appInfos.push()
appBlockers.push()
blockerToApps.push()
@@ -41,6 +43,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def pop() {
callInfos.pop()
defBlockers.pop()
+ lambdaBlockers.pop()
appInfos.pop()
appBlockers.pop()
blockerToApps.pop()
@@ -50,6 +53,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def clear() {
callInfos.clear()
defBlockers.clear()
+ lambdaBlockers.clear()
appInfos.clear()
appBlockers.clear()
blockerToApps.clear()
@@ -59,6 +63,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def reset() {
callInfos.reset()
defBlockers.reset()
+ lambdaBlockers.reset()
appInfos.reset()
appBlockers.reset()
blockerToApps.clear()
@@ -257,6 +262,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
// we need to define this defBlocker and link it to definition
val defBlocker = encoder.encodeId(FreshIdentifier("d", BooleanType))
defBlockers += info -> defBlocker
+ manager.implies(id, defBlocker)
val template = templateGenerator.mkTemplate(tfd)
//reporter.debug(template)
@@ -279,7 +285,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
// We connect it to the defBlocker: blocker => defBlocker
if (defBlocker != id) {
- newCls ++= List(encoder.mkImplies(id, defBlocker))
+ newCls :+= encoder.mkImplies(id, defBlocker)
}
reporter.debug("Unrolling behind "+info+" ("+newCls.size+")")
@@ -293,22 +299,32 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
for ((app @ (b, _), (gen, _, _, _, infos)) <- thisAppInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
var newCls = Seq.empty[T]
- val nb = encoder.encodeId(FreshIdentifier("b", BooleanType, true))
- newCls :+= encoder.mkEquals(nb, encoder.mkAnd(equals, b))
+ val lambdaBlocker = lambdaBlockers.get(info) match {
+ case Some(lambdaBlocker) => lambdaBlocker
- val (newExprs, callBlocks, appBlocks) = template.instantiate(nb, args)
- val blockExprs = freshAppBlocks(appBlocks.keys)
+ case None =>
+ val lambdaBlocker = encoder.encodeId(FreshIdentifier("d", BooleanType))
+ lambdaBlockers += info -> lambdaBlocker
+ manager.implies(b, lambdaBlocker)
- for ((b, newInfos) <- callBlocks) {
- registerCallBlocker(nextGeneration(gen), b, newInfos)
- }
+ val (newExprs, callBlocks, appBlocks) = template.instantiate(lambdaBlocker, args)
+ val blockExprs = freshAppBlocks(appBlocks.keys)
+
+ for ((b, newInfos) <- callBlocks) {
+ registerCallBlocker(nextGeneration(gen), b, newInfos)
+ }
- for ((newApp, newInfos) <- appBlocks) {
- registerAppBlocker(nextGeneration(gen), newApp, newInfos)
+ for ((newApp, newInfos) <- appBlocks) {
+ registerAppBlocker(nextGeneration(gen), newApp, newInfos)
+ }
+
+ newCls ++= newExprs
+ newCls ++= blockExprs
+ lambdaBlocker
}
- newCls ++= newExprs
- newCls ++= blockExprs
+ val enabler = if (equals == manager.trueT) b else encoder.mkAnd(equals, b)
+ newCls :+= encoder.mkImplies(enabler, lambdaBlocker)
reporter.debug("Unrolling behind "+info+" ("+newCls.size+")")
for (cl <- newCls) {
@@ -318,6 +334,12 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
newClauses ++= newCls
}
+ /*
+ for ((app @ (b, _), (gen, _, _, _, infos)) <- thisAppInfos if infos.isEmpty) {
+ registerAppBlocker(nextGeneration(gen), app, infos)
+ }
+ */
+
reporter.debug(s" - ${newClauses.size} new clauses")
//context.reporter.ifDebug { debug =>
// debug(s" - new clauses:")
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 547ec3f9bd3a1f490cc8cb97643531208faa1fd6..5fd73851864805fd8b9e804b17f944fb3f71d5db 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -91,10 +91,11 @@ trait AbstractZ3Solver extends Solver {
protected val adtManager = new ADTManager(context)
// Bijections between Leon Types/Functions/Ids to Z3 Sorts/Decls/ASTs
- protected val functions = new IncrementalBijection[TypedFunDef, Z3FuncDecl]()
- protected val generics = new IncrementalBijection[GenericValue, Z3FuncDecl]()
- protected val sorts = new IncrementalBijection[TypeTree, Z3Sort]()
- protected val variables = new IncrementalBijection[Expr, Z3AST]()
+ protected val functions = new IncrementalBijection[TypedFunDef, Z3FuncDecl]()
+ protected val generics = new IncrementalBijection[GenericValue, Z3FuncDecl]()
+ protected val lambdas = new IncrementalBijection[FunctionType, Z3FuncDecl]()
+ protected val sorts = new IncrementalBijection[TypeTree, Z3Sort]()
+ protected val variables = new IncrementalBijection[Expr, Z3AST]()
protected val constructors = new IncrementalBijection[TypeTree, Z3FuncDecl]()
protected val selectors = new IncrementalBijection[(TypeTree, Int), Z3FuncDecl]()
@@ -108,6 +109,7 @@ trait AbstractZ3Solver extends Solver {
z3 = new Z3Context(z3cfg)
functions.clear()
+ lambdas.clear()
generics.clear()
sorts.clear()
variables.clear()
@@ -190,7 +192,6 @@ trait AbstractZ3Solver extends Solver {
}
}
}
-
}
// Prepares some of the Z3 sorts, but *not* the tuple sorts; these are created on-demand.
@@ -230,7 +231,6 @@ trait AbstractZ3Solver extends Solver {
declareStructuralSort(tpe)
}
-
case tt @ SetType(base) =>
sorts.cachedB(tt) {
z3.mkSetSort(typeToSort(base))
@@ -257,10 +257,8 @@ trait AbstractZ3Solver extends Solver {
case ft @ FunctionType(from, to) =>
sorts.cachedB(ft) {
- val fromSort = typeToSort(tupleTypeWrap(from))
- val toSort = typeToSort(to)
-
- z3.mkArraySort(fromSort, toSort)
+ val symbol = z3.mkFreshStringSymbol(ft.toString)
+ z3.mkUninterpretedSort(symbol)
}
case other =>
@@ -496,7 +494,15 @@ trait AbstractZ3Solver extends Solver {
z3.mkApp(functionDefToDecl(tfd), args.map(rec): _*)
case fa @ Application(caller, args) =>
- z3.mkSelect(rec(caller), rec(tupleWrap(args)))
+ val ft @ FunctionType(froms, to) = normalizeType(caller.getType)
+ val funDecl = lambdas.cachedB(ft) {
+ val sortSeq = (ft +: froms).map(tpe => typeToSort(tpe))
+ val returnSort = typeToSort(to)
+
+ val name = FreshIdentifier("dynLambda").uniqueName
+ z3.mkFreshFuncDecl(name, sortSeq, returnSort)
+ }
+ z3.mkApp(funDecl, (caller +: args).map(rec): _*)
case ElementOfSet(e, s) => z3.mkSetMember(rec(e), rec(s))
case SubsetOf(s1, s2) => z3.mkSetSubset(rec(s1), rec(s2))
@@ -563,7 +569,7 @@ trait AbstractZ3Solver extends Solver {
def rec(t: Z3AST, tpe: TypeTree): Expr = {
val kind = z3.getASTKind(t)
kind match {
- case Z3NumeralIntAST(Some(v)) => {
+ case Z3NumeralIntAST(Some(v)) =>
val leading = t.toString.substring(0, 2 min t.toString.length)
if(leading == "#x") {
_root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
@@ -586,8 +592,8 @@ trait AbstractZ3Solver extends Solver {
unsupported(other, "Unexpected type for BV value: " + other)
}
}
- }
- case Z3NumeralIntAST(None) => {
+
+ case Z3NumeralIntAST(None) =>
val ts = t.toString
reporter.ifDebug(printer => printer(ts))(DebugSectionSynthesis)
if(ts.length > 4 && ts.substring(0, 2) == "bv" && ts.substring(ts.length - 4) == "[32]") {
@@ -612,7 +618,9 @@ trait AbstractZ3Solver extends Solver {
case None => unsound(t, "could not translate Z3NumeralIntAST numeral")
}
}
+
case Z3NumeralRealAST(n: BigInt, d: BigInt) => FractionalLiteral(n, d)
+
case Z3AppAST(decl, args) =>
val argsSize = args.size
if(argsSize == 0 && (variables containsB t)) {
@@ -669,6 +677,22 @@ trait AbstractZ3Solver extends Solver {
case None => unsound(t, "invalid array AST")
}
+ case ft @ FunctionType(fts, tt) => lambdas.getB(ft) match {
+ case None => simplestValue(ft)
+ case Some(decl) => model.getModelFuncInterpretations.find(_._1 == decl) match {
+ case None => simplestValue(ft)
+ case Some((_, mapping, elseValue)) =>
+ val leonElseValue = rec(elseValue, tt)
+ PartialLambda(mapping.flatMap { case (z3Args, z3Result) =>
+ if (t == z3Args.head) {
+ List((z3Args.tail zip fts).map(p => rec(p._1, p._2)) -> rec(z3Result, tt))
+ } else {
+ Nil
+ }
+ }, Some(leonElseValue), ft)
+ }
+ }
+
case tp: TypeParameter =>
val id = t.toString.split("!").last.toInt
GenericValue(tp, id)
@@ -691,13 +715,6 @@ trait AbstractZ3Solver extends Solver {
FiniteMap(elems, from, to)
}
- case ft @ FunctionType(fts, tt) =>
- rec(t, RawArrayType(tupleTypeWrap(fts), tt)) match {
- case r: RawArrayValue =>
- val elems = r.elems.toSeq.map { case (k, v) => unwrapTuple(k, fts.size) -> v }
- PartialLambda(elems, Some(r.default), ft)
- }
-
case tpe @ SetType(dt) =>
model.getSetValue(t) match {
case None => unsound(t, "invalid set AST")
@@ -742,7 +759,8 @@ trait AbstractZ3Solver extends Solver {
case _ => unsound(t, "unexpected AST")
}
}
- rec(tree, tpe)
+
+ rec(tree, normalizeType(tpe))
}
protected[leon] def softFromZ3Formula(model: Z3Model, tree: Z3AST, tpe: TypeTree) : Option[Expr] = {
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
index 256dcf38fc5dc99f31ce2f6fb30dc12e0caa5268..70ebd260f931a6a428a84afad9640accf193887d 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -14,9 +14,10 @@ trait FairZ3Component extends LeonComponent {
val optUnrollCores = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unrolling while remaining fair", false)
val optAssumePre = LeonFlagOptionDef("assumepre", "Assume precondition holds (pre && f(x) = body) when unfolding", false)
val optNoChecks = LeonFlagOptionDef("nochecks", "Disable counter-example check in presence of foralls" , false)
+ val optUnfoldFactor = LeonLongOptionDef("unfoldFactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre)
+ Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre, optUnfoldFactor)
}
object FairZ3Component extends FairZ3Component
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index c129243d15b661d9e42d578447fdea6cb1aea3e0..6a96848c5fb283ec1a6ae22817afff95f9300122 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -136,23 +136,21 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
private val freeVars = new IncrementalSet[Identifier]()
private val constraints = new IncrementalSeq[Expr]()
-
val unrollingBank = new UnrollingBank(context, templateGenerator)
+ private val incrementals: List[IncrementalState] = List(
+ errors, freeVars, constraints, functions, generics, lambdas, sorts, variables,
+ constructors, selectors, testers, unrollingBank
+ )
+
def push() {
- errors.push()
solver.push()
- unrollingBank.push()
- freeVars.push()
- constraints.push()
+ incrementals.foreach(_.push())
}
def pop() {
- errors.pop()
solver.pop(1)
- unrollingBank.pop()
- freeVars.pop()
- constraints.pop()
+ incrementals.foreach(_.pop())
}
override def check: Option[Boolean] = {
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index de63b992559c66a4a641609fa16914505c01cdd5..ed7c0652b60384f362bbecc9db8dd93d9a2e2523 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -23,10 +23,10 @@ case object ADTDual extends NormalizingRule("ADTDual") {
val (toRemove, toAdd) = exprs.collect {
case eq @ Equals(cc @ CaseClass(ct, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) & xs).nonEmpty =>
- (eq, IsInstanceOf(e, ct) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
+ (eq, IsInstanceOf(e, ct) +: (ct.classDef.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
case eq @ Equals(e, cc @ CaseClass(ct, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) & xs).nonEmpty =>
- (eq, IsInstanceOf(e, ct) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
+ (eq, IsInstanceOf(e, ct) +: (ct.classDef.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
}.unzip
if (toRemove.nonEmpty) {
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index dde6ce913dea17b33d1618a6dd9fe4391591468e..df2c44193412a55af004dfa7695901044a4b5b53 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -96,7 +96,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val cases = for ((sol, (cct, problem, pattern)) <- sols zip subInfo) yield {
if (sol.pre != BooleanLiteral(true)) {
- val substs = (for ((field,arg) <- cct.fields zip problem.as ) yield {
+ val substs = (for ((field,arg) <- cct.classDef.fields zip problem.as ) yield {
(arg, caseClassSelector(cct, id.toVariable, field.id))
}).toMap
globalPre ::= and(IsInstanceOf(Variable(id), cct), replaceFromIDs(substs, sol.pre))
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 227dd691c29734e0dd85feb179f40fac15ceea7a..6b2f9e8585a98ab9677aa5f1c439b2a1afa136ef 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -24,7 +24,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
val ccSubsts = for (IsInstanceOf(s, cct: CaseClassType) <- instanceOfs) yield {
- val fieldsVals = (for (f <- cct.fields) yield {
+ val fieldsVals = (for (f <- cct.classDef.fields) yield {
val id = f.id
clauses.find {
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index c5a8ccb69c870b16f91e1c1dcfa5cb933bc8138b..799e51db6c1d08895ffb23793fc7328e881a7242 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -6,7 +6,7 @@ package termination
import purescala.Expressions._
import purescala.Common._
import purescala.Definitions._
-import purescala.Constructors.tupleWrap
+import purescala.Constructors._
class ChainProcessor(
val checker: TerminationChecker,
@@ -33,40 +33,40 @@ class ChainProcessor(
reporter.debug("-+> Multiple looping points, can't build chain proof")
None
} else {
+ val funDef = loopPoints.headOption getOrElse {
+ chainsMap.collectFirst { case (fd, (fds, chains)) if chains.nonEmpty => fd }.get
+ }
- def exprs(fd: FunDef): (Expr, Seq[(Seq[Expr], Expr)], Set[Chain]) = {
- val fdChains = chainsMap(fd)._2
-
- val e1 = tupleWrap(fd.params.map(_.toVariable))
- val e2s = fdChains.toSeq.map { chain =>
- val freshParams = chain.finalParams.map(arg => FreshIdentifier(arg.id.name, arg.id.getType, true))
- (chain.loop(finalArgs = freshParams), tupleWrap(freshParams.map(_.toVariable)))
- }
+ val chains = chainsMap(funDef)._2
- (e1, e2s, fdChains)
+ val e1 = tupleWrap(funDef.params.map(_.toVariable))
+ val e2s = chains.toSeq.map { chain =>
+ val freshParams = chain.finalParams.map(arg => FreshIdentifier(arg.id.name, arg.id.getType, true))
+ (chain.loop(finalArgs = freshParams), tupleWrap(freshParams.map(_.toVariable)))
}
- val funDefs = if (loopPoints.size == 1) Set(loopPoints.head) else problem.funSet
-
reporter.debug("-+> Searching for structural size decrease")
- val (se1, se2s, _) = exprs(funDefs.head)
- val structuralFormulas = modules.structuralDecreasing(se1, se2s)
+ val structuralFormulas = modules.structuralDecreasing(e1, e2s)
val structuralDecreasing = structuralFormulas.exists(formula => definitiveALL(formula))
reporter.debug("-+> Searching for numerical converging")
- // worth checking multiple funDefs as the endpoint discovery can be context sensitive
- val numericDecreasing = funDefs.exists { fd =>
- val (ne1, ne2s, fdChains) = exprs(fd)
- val numericFormulas = modules.numericConverging(ne1, ne2s, fdChains)
- numericFormulas.exists(formula => definitiveALL(formula))
- }
+ val numericFormulas = modules.numericConverging(e1, e2s, chains)
+ val numericDecreasing = numericFormulas.exists(formula => definitiveALL(formula))
if (structuralDecreasing || numericDecreasing)
Some(problem.funDefs map Cleared)
- else
- None
+ else {
+ val chainsUnlooping = chains.flatMap(c1 => chains.flatMap(c2 => c1 compose c2)).forall {
+ chain => !definitiveSATwithModel(andJoin(chain.loop())).isDefined
+ }
+
+ if (chainsUnlooping)
+ Some(problem.funDefs map Cleared)
+ else
+ None
+ }
}
}
}
diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala
index d2bae17b326623178671a2fc7db26954e013057e..92a11c6452c88f49986cd9382cae9ed72f70619a 100644
--- a/src/main/scala/leon/termination/ProcessingPipeline.scala
+++ b/src/main/scala/leon/termination/ProcessingPipeline.scala
@@ -165,8 +165,8 @@ abstract class ProcessingPipeline(context: LeonContext, initProgram: Program) ex
val components = SCC.scc(callGraph)
for (fd <- funDefs -- components.toSet.flatten) clearedMap(fd) = "Non-recursive"
-
- components.map(fds => Problem(fds.toSeq))
+ val newProblems = components.filter(fds => fds.forall { fd => !terminationMap.isDefinedAt(fd) })
+ newProblems.map(fds => Problem(fds.toSeq))
}
def verifyTermination(funDef: FunDef): Unit = {
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 99124c5e64ed8bb61e3c44a015775280d06c584e..3f7be09f145d2768ff00f8573f078d6e90bc1b2d 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -34,7 +34,7 @@ trait Solvable extends Processor {
val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size"),Seq(sizeModule))
val newProgram : Program = program.copy( units = sizeUnit :: program.units)
- SolverFactory.getFromSettings(context, newProgram).withTimeout(500.millisecond)
+ SolverFactory.getFromSettings(context, newProgram).withTimeout(10.seconds)
}
type Solution = (Option[Boolean], Map[Identifier, Expr])
diff --git a/src/main/scala/leon/transformations/InstrumentationUtil.scala b/src/main/scala/leon/transformations/InstrumentationUtil.scala
index 2c461e466298614ebae30df8a33ff901fea72fa5..1c3b744d8f667b3a1bb7b653ff299868fe98b38a 100644
--- a/src/main/scala/leon/transformations/InstrumentationUtil.scala
+++ b/src/main/scala/leon/transformations/InstrumentationUtil.scala
@@ -63,7 +63,7 @@ object InstUtil {
val vary = yid.toVariable
val args = Seq(xid, yid)
val maxType = FunctionType(Seq(IntegerType, IntegerType), IntegerType)
- val mfd = new FunDef(FreshIdentifier("max", maxType, false), Seq(), args.map((arg) => ValDef(arg, Some(arg.getType))), IntegerType)
+ val mfd = new FunDef(FreshIdentifier("max", maxType, false), Seq(), args.map(arg => ValDef(arg)), IntegerType)
val cond = GreaterEquals(varx, vary)
mfd.body = Some(IfExpr(cond, varx, vary))
diff --git a/src/main/scala/leon/transformations/IntToRealProgram.scala b/src/main/scala/leon/transformations/IntToRealProgram.scala
index 21229282b398fcc10cd9548ddaead2f25d8087a3..5ab16991398e5dcb4352e870795fff51045fb9c9 100644
--- a/src/main/scala/leon/transformations/IntToRealProgram.scala
+++ b/src/main/scala/leon/transformations/IntToRealProgram.scala
@@ -72,8 +72,7 @@ abstract class ProgramTypeTransformer {
}
def mapDecl(decl: ValDef): ValDef = {
- val newtpe = mapType(decl.getType)
- new ValDef(mapId(decl.id), Some(newtpe))
+ decl.copy(id = mapId(decl.id))
}
def mapType(tpe: TypeTree): TypeTree = {
@@ -141,9 +140,9 @@ abstract class ProgramTypeTransformer {
// FIXME
//add a new postcondition
newfd.fullBody = if (fd.postcondition.isDefined && newfd.body.isDefined) {
- val Lambda(Seq(ValDef(resid, _)), pexpr) = fd.postcondition.get
+ val Lambda(Seq(ValDef(resid, lzy)), pexpr) = fd.postcondition.get
val tempRes = mapId(resid).toVariable
- Ensuring(newfd.body.get, Lambda(Seq(ValDef(tempRes.id, Some(tempRes.getType))), transformExpr(pexpr)))
+ Ensuring(newfd.body.get, Lambda(Seq(ValDef(tempRes.id, lzy)), transformExpr(pexpr)))
// Some(mapId(resid), transformExpr(pexpr))
} else NoTree(fd.returnType)
@@ -233,4 +232,4 @@ class RealToIntProgram extends ProgramTypeTransformer {
}
def mappedFun(fd: FunDef): FunDef = newFundefs(fd)
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
index d17968dc05b789b936554b9c10dbde22ac360dfb..a696dae0580baf44c6ef955c72ccdcce9791bdab 100644
--- a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
+++ b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
@@ -26,7 +26,7 @@ object MultFuncs {
val vary = yid.toVariable
val args = Seq(xid, yid)
val funcType = FunctionType(Seq(domain, domain), domain)
- val mfd = new FunDef(FreshIdentifier("pmult", funcType, false), Seq(), args.map((arg) => ValDef(arg, Some(arg.getType))), domain)
+ val mfd = new FunDef(FreshIdentifier("pmult", funcType, false), Seq(), args.map(arg => ValDef(arg)), domain)
val tmfd = TypedFunDef(mfd, Seq())
//define a body (a) using mult(x,y) = if(x == 0 || y ==0) 0 else mult(x-1,y) + y
@@ -47,7 +47,7 @@ object MultFuncs {
val post1 = Implies(guard, defn2)
// mfd.postcondition = Some((resvar.id, And(Seq(post0, post1))))
- mfd.fullBody = Ensuring(mfd.body.get, Lambda(Seq(ValDef(resvar.id, Some(resvar.getType))), And(Seq(post0, post1))))
+ mfd.fullBody = Ensuring(mfd.body.get, Lambda(Seq(ValDef(resvar.id)), And(Seq(post0, post1))))
//set function properties (for now, only monotonicity)
mfd.addFlags(Set(Annotation("theoryop", Seq()), Annotation("monotonic", Seq()))) //"distributive" ?
mfd
@@ -59,7 +59,7 @@ object MultFuncs {
val yid = FreshIdentifier("y", domain)
val args = Seq(xid, yid)
val funcType = FunctionType(Seq(domain, domain), domain)
- val fd = new FunDef(FreshIdentifier("mult", funcType, false), Seq(), args.map((arg) => ValDef(arg, Some(arg.getType))), domain)
+ val fd = new FunDef(FreshIdentifier("mult", funcType, false), Seq(), args.map(arg => ValDef(arg)), domain)
val tpivMultFun = TypedFunDef(pivMultFun, Seq())
//the body is defined as mult(x,y) = val px = if(x < 0) -x else x;
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index 87c5795838b460314d19805cbb8ca6caae4ee233..c4830cf40ca429358b0d2e420bbbe7f7d1f5c276 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -111,7 +111,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
def mapPost(pred: Expr, from: FunDef, to: FunDef) = {
pred match {
- case Lambda(Seq(ValDef(fromRes, _)), postCond) if (instFuncs.contains(from)) =>
+ case Lambda(Seq(ValDef(fromRes, lzy)), postCond) if (instFuncs.contains(from)) =>
val toResId = FreshIdentifier(fromRes.name, to.returnType, true)
val newpost = postMap((e: Expr) => e match {
case Variable(`fromRes`) =>
@@ -124,7 +124,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
case _ =>
None
})(postCond)
- Lambda(Seq(ValDef(toResId)), mapExpr(newpost))
+ Lambda(Seq(ValDef(toResId, lzy)), mapExpr(newpost))
case _ =>
mapExpr(pred)
}
@@ -489,4 +489,4 @@ abstract class Instrumenter(program: Program, si: SerialInstrumenter) {
*/
def instrumentMatchCase(me: MatchExpr, mc: MatchCase,
caseExprCost: Expr, scrutineeCost: Expr): Expr
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 65f96a090d4449845921252737bb35a3c3b9a327..dd437c224170c908e9175815354748a4236e4880 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -21,7 +21,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
private def selectorsOfParentType(parentType: ClassType, cct: CaseClassType, expr: Expr): Seq[Expr] = {
- val childrenOfSameType = cct.fields.filter(_.getType == parentType)
+ val childrenOfSameType = (cct.classDef.fields zip cct.fieldsTypes).collect { case (vd, tpe) if tpe == parentType => vd }
for (field <- childrenOfSameType) yield {
caseClassSelector(cct, expr, field.id)
}
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index 21119c4e2728c99850e3af0d1c12e498866f771e..ea09de821427e39cffa3ea9c304e7d1e5a910a4c 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -57,7 +57,6 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
}
}
-
try {
val vcs = generateVCs(vctx, toVerify)
diff --git a/src/sphinx/purescala.rst b/src/sphinx/purescala.rst
index ee41a7ec83a68ff479b2316b9085b5302c017237..7cde91421d3a77cfc68162b6c643e4396a8bc85b 100644
--- a/src/sphinx/purescala.rst
+++ b/src/sphinx/purescala.rst
@@ -36,6 +36,51 @@ Pure Scala supports two kinds of top-level declarations:
.. _adts:
+
+Boolean
+#######
+
+Booleans are used to express truth conditions in Leon.
+Unlike some proof assistants, there is no separation
+at the type level between
+Boolean values and the truth conditions of conjectures
+and theorems.
+
+Typical propositional operations are available using Scala
+notation, along
+with a new shorthand for implication. The `if` expression
+is also present.
+
+.. code-block:: scala
+
+ a && b
+ a || b
+ a == b
+ !a
+ a ==> b // Leon syntax for boolean implication
+
+Leon uses short-circuit interpretation of `&&`, `||`, and `==>`,
+which evaluates the second argument only when needed:
+
+.. code-block:: scala
+
+ a && b === if (a) b else false
+
+ a || b === if (a) true else b
+
+ a ==> b === if (a) b else true
+
+This aspect is important because of:
+
+1. evaluation of expressions, which is kept compatible with Scala
+
+2. verification condition generation for safety: arguments of Boolean operations
+may be operations with preconditions; these preconditions apply only in case
+that the corresponding argument is evaluated.
+
+3. termination checking, which takes into account that only one of the paths in an if expression is evaluated for a given truth value of the condition.
+
+
Algebraic Data Types
--------------------
@@ -266,16 +311,6 @@ TupleX
val y = 1 -> 2 // alternative Scala syntax for Tuple2
x._1 // == 1
-Boolean
-#######
-
-.. code-block:: scala
-
- a && b
- a || b
- a == b
- !a
- a ==> b // Leon syntax for boolean implication
Int
###
diff --git a/src/test/resources/regression/termination/valid/NNF.scala b/src/test/resources/regression/termination/valid/NNF.scala
new file mode 100644
index 0000000000000000000000000000000000000000..455cef7ec5201fd17edee71059dc38c9d7afa3d8
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/NNF.scala
@@ -0,0 +1,99 @@
+import leon.lang._
+import leon.annotation._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: BigInt) extends Formula
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
+ case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
+ case Not(f) => Not(simplify(f))
+ case Literal(_) => f
+ }) ensuring(isSimplified(_))
+
+ def isSimplified(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Implies(_,_) => false
+ case Not(f) => isSimplified(f)
+ case Literal(_) => true
+ }
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => nnf(Or(Not(lhs), rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => false
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ def evalLit(id : BigInt) : Boolean = (id == 42) // could be any function
+ def eval(f: Formula) : Boolean = f match {
+ case And(lhs, rhs) => eval(lhs) && eval(rhs)
+ case Or(lhs, rhs) => eval(lhs) || eval(rhs)
+ case Implies(lhs, rhs) => !eval(lhs) || eval(rhs)
+ case Not(f) => !eval(f)
+ case Literal(id) => evalLit(id)
+ }
+
+ @induct
+ def simplifySemantics(f: Formula) : Boolean = {
+ eval(f) == eval(simplify(f))
+ } holds
+
+ // Note that matching is exhaustive due to precondition.
+ def vars(f: Formula): Set[BigInt] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[BigInt](i)
+ case Literal(i) => Set[BigInt](i)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ @induct
+ def wrongCommutative(f: Formula) : Boolean = {
+ nnf(simplify(f)) == simplify(nnf(f))
+ } holds
+
+ @induct
+ def simplifyPreservesNNF(f: Formula) : Boolean = {
+ require(isNNF(f))
+ isNNF(simplify(f))
+ } holds
+
+ @induct
+ def nnfIsStable(f: Formula) : Boolean = {
+ require(isNNF(f))
+ nnf(f) == f
+ } holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ } holds
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/CallByName1.scala b/src/test/resources/regression/verification/purescala/invalid/CallByName1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c96ab1617e254c19d8b08a8ecbd818d9cdc305e4
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/CallByName1.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object CallByName1 {
+ def byName1(i: Int, a: => Int): Int = {
+ if (i > 0) a + 1
+ else 0
+ }
+
+ def byName2(i: Int, a: => Int): Int = {
+ if (i > 0) byName1(i - 1, a) + 2
+ else 0
+ }
+
+ def test(): Boolean = {
+ byName1(1, byName2(3, 0)) == 0 && byName1(1, byName2(3, 0)) == 1
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index 547978dbcca900272b76aac30dfd8e2a8f9e2c62..a8927f360e817d10761723c8a4b7e9085bf0738d 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -78,7 +78,7 @@ object PropositionalLogic {
require(isNNF(f))
nnf(f) == f
}.holds
-
+
@induct
def simplifyIsStable(f: Formula) : Boolean = {
require(isSimplified(f))
diff --git a/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala b/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9ee698e1d42d38214a0290cbad859b0b5ad87405
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object AndTest {
+
+ def nonterm(x: BigInt) : BigInt = {
+ nonterm(x + 1)
+ } ensuring(res => false)
+
+ def precond(y : BigInt) = y < 0
+
+ /**
+ * Leon should find a counter-example here.
+ **/
+ def foo(y: BigInt) : Boolean = {
+ require(precond(y))
+ y >= 0 && (nonterm(0) == 0)
+ } holds
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala b/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala
index 20ff95383b4f7042b0eba32fcc4e5c8b0cea3680..674ca7c69fa29333755d8908f707ae9931d20bf2 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala
@@ -6,10 +6,14 @@ object Unap1 {
}
object Unapply1 {
+
+ sealed abstract class Bool
+ case class True() extends Bool
+ case class False() extends Bool
- def bar: Boolean = { (42, false, ()) match {
- case Unap1(_, b) if b => b
+ def bar: Bool = { (42, False().asInstanceOf[Bool], ()) match {
+ case Unap1(_, b) if b == True() => b
case Unap1((), b) => b
- }} ensuring { res => res }
+ }} ensuring { res => res == True() }
}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala b/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala
index ae4167c20026f0e926494af6cf3a11f25e9399e5..7efd6e220fd1c7fcd08fbaa5b7016bf6801e151f 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala
@@ -5,7 +5,12 @@ object Unap2 {
}
object Unapply {
- def bar: Boolean = { (42, false, ()) match {
- case Unap2(_, b) if b => b
- }} ensuring { res => res }
+
+ sealed abstract class Bool
+ case class True() extends Bool
+ case class False() extends Bool
+
+ def bar: Bool = { (42, False().asInstanceOf[Bool], ()) match {
+ case Unap2(_, b) if b == True() => b
+ }} ensuring { res => res == True() }
}
diff --git a/src/test/resources/regression/verification/purescala/valid/CallByName1.scala b/src/test/resources/regression/verification/purescala/valid/CallByName1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..912acdc481e8191bd072bd7eaeb13684cd93c384
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/CallByName1.scala
@@ -0,0 +1,9 @@
+import leon.lang._
+
+object CallByName1 {
+ def add(a: => Int, b: => Int): Int = a + b
+
+ def test(): Int = {
+ add(1,2)
+ } ensuring (_ == 3)
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Client.scala b/src/test/resources/regression/verification/purescala/valid/Client.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c0dd37cda62e30202e9255b534685f9e0e9b840a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Client.scala
@@ -0,0 +1,18 @@
+import leon.collection._
+import leon.lang._
+
+object Minimal {
+
+ case class Client(f: Int => List[Int])
+
+ val client = Client(x => List(1))
+
+ // def f(x: Int) = List(1)
+ // val client = Client(f)
+
+ def theorem() = {
+ client.f(0).size != BigInt(0)
+ } holds
+
+}
+
diff --git a/src/test/resources/regression/verification/purescala/valid/FlatMap.scala b/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
index 3f1dd39ffd79dd10d1300a9aa0ac60f2b29d46a0..878b61456b6658b13f05d0e5f1b05dc25d959676 100644
--- a/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
object FlatMap {
@@ -17,7 +18,7 @@ object FlatMap {
def associative_append_lemma_induct[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
l1 match {
case Nil() => associative_append_lemma(l1, l2, l3)
- case Cons(head, tail) => associative_append_lemma(l1, l2, l3) && associative_append_lemma_induct(tail, l2, l3)
+ case Cons(head, tail) => associative_append_lemma(l1, l2, l3) because associative_append_lemma_induct(tail, l2, l3)
}
}.holds
@@ -31,20 +32,21 @@ object FlatMap {
}
def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
- associative_lemma(list, f, g) &&
- append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
- (glist match {
- case Cons(ghead, gtail) =>
- associative_lemma_induct(list, flist, gtail, f, g)
- case Nil() => flist match {
- case Cons(fhead, ftail) =>
- associative_lemma_induct(list, ftail, g(fhead), f, g)
- case Nil() => list match {
- case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
- case Nil() => true
+ associative_lemma(list, f, g) because {
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) because
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
}
- }
- })
+ })
+ }
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala b/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
index ff0444f269dd6f9b2a2b7f2b54e13f54c6755ab2..6920231115fea93a1b7c7cefc27691a0ee2471bb 100644
--- a/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
+++ b/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
@@ -2,6 +2,7 @@
import leon._
import leon.lang._
+import leon.proof._
object FoldAssociative {
@@ -56,7 +57,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_split(list, x) && (list match {
+ lemma_split(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_split_induct(tail, x - 1)
case _ => true
@@ -77,7 +78,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_reassociative(list, x) && (list match {
+ lemma_reassociative(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_reassociative_induct(tail, x - 1)
case _ => true
@@ -93,7 +94,7 @@ object FoldAssociative {
def lemma_reassociative_presplit_induct(l1: List, l2: List): Boolean = {
val f = (x: Int, s: Int) => x + s
val list = append(l1, l2)
- lemma_reassociative_presplit(l1, l2) && (l1 match {
+ lemma_reassociative_presplit(l1, l2) because (l1 match {
case Cons(head, tail) =>
lemma_reassociative_presplit_induct(tail, l2)
case Nil() => true
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists1.scala b/src/test/resources/regression/verification/purescala/valid/Lists1.scala
index 4dbee2b7137c8a427cf7bd302e3849050f0b2bc7..0b10f27d05354ef02fab45cc935f7f3695bee378 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists1.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
import leon.annotation._
@@ -21,10 +22,10 @@ object Lists1 {
}
def exists_lemma_induct[T](list: List[T], f: T => Boolean): Boolean = {
- list match {
- case Nil() => exists_lemma(list, f)
- case Cons(head, tail) => exists_lemma(list, f) && exists_lemma_induct(tail, f)
- }
+ exists_lemma(list, f) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => exists_lemma_induct(tail, f)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists2.scala b/src/test/resources/regression/verification/purescala/valid/Lists2.scala
index 57d86819bf5cb17a77e451aead68393f7c30ed17..79126cb2226b55c811313c1c82375b977265ffc2 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists2.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
object Lists2 {
abstract class List[T]
@@ -22,10 +23,10 @@ object Lists2 {
}
def positive_lemma_induct(list: List[Int]): Boolean = {
- list match {
- case Nil() => positive_lemma(list)
- case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
- }
+ positive_lemma(list) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => positive_lemma_induct(tail)
+ })
}.holds
def remove[T](list: List[T], e: T) : List[T] = {
@@ -41,10 +42,10 @@ object Lists2 {
}
def remove_lemma_induct[T](list: List[T], e: T): Boolean = {
- list match {
- case Nil() => remove_lemma(list, e)
- case Cons(head, tail) => remove_lemma(list, e) && remove_lemma_induct(tail, e)
- }
+ remove_lemma(list, e) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => remove_lemma_induct(tail, e)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists3.scala b/src/test/resources/regression/verification/purescala/valid/Lists3.scala
index 1dae4a5c6f5ecf649bc78d2b19151007cc57a47d..dedab2a4e32aee2bf02e816ad8677e02a0a669a2 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists3.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists3.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
object Lists3 {
abstract class List[T]
@@ -26,10 +27,10 @@ object Lists3 {
}
def positive_lemma_induct(list: List[Int]): Boolean = {
- list match {
- case Nil() => positive_lemma(list)
- case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
- }
+ positive_lemma(list) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => positive_lemma_induct(tail)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists4.scala b/src/test/resources/regression/verification/purescala/valid/Lists4.scala
index d4e212aff31bd011ce143901efa34a5a428f0d94..124d944da9e0769e74d43c4b3612f5a79657d9fa 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists4.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists4.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
object Lists4 {
abstract class List[T]
@@ -17,10 +18,10 @@ object Lists4 {
}
def map_lemma_induct[D,E,F](list: List[D], f: D => E, g: E => F): Boolean = {
- list match {
- case Nil() => map_lemma(list, f, g)
- case Cons(head, tail) => map_lemma(list, f, g) && map_lemma_induct(tail, f, g)
- }
+ map_lemma(list, f, g) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => map_lemma_induct(tail, f, g)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists5.scala b/src/test/resources/regression/verification/purescala/valid/Lists5.scala
index f8fd9491fee2ad4a27ed9a4230ba1b30afec3093..9826dc372a2a79ae733696126de8565394148ff8 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists5.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists5.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
object Lists5 {
@@ -26,9 +27,9 @@ object Lists5 {
}
def equivalence_lemma_induct[T](f: T => Boolean, list: List[T]): Boolean = {
- list match {
- case Cons(head, tail) => equivalence_lemma(f, list) && equivalence_lemma_induct(f, tail)
- case Nil() => equivalence_lemma(f, list)
- }
+ equivalence_lemma(f, list) because (list match {
+ case Cons(head, tail) => equivalence_lemma_induct(f, tail)
+ case Nil() => true
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists6.scala b/src/test/resources/regression/verification/purescala/valid/Lists6.scala
index 8257249830949d07dc36c0c74633d166bebbe561..763fabdaddab6a7d4732dcd2c102beb897b27d0e 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists6.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists6.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
object Lists6 {
@@ -16,7 +17,7 @@ object Lists6 {
}
def associative_lemma_induct[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
- associative_lemma(list, f, g) && (list match {
+ associative_lemma(list, f, g) because (list match {
case Cons(head, tail) => associative_lemma_induct(tail, f, g)
case Nil() => true
})
diff --git a/src/test/resources/regression/verification/purescala/valid/Monads3.scala b/src/test/resources/regression/verification/purescala/valid/Monads3.scala
index 05b46ceb0f02a96811b7ca8a4606b4b4b30de3e3..fc0e7149b7f43455b0531c4f2502d592bbd764da 100644
--- a/src/test/resources/regression/verification/purescala/valid/Monads3.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Monads3.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
object Monads3 {
@@ -22,20 +23,21 @@ object Monads3 {
}
def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
- associative_lemma(list, f, g) &&
- append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
- (glist match {
- case Cons(ghead, gtail) =>
- associative_lemma_induct(list, flist, gtail, f, g)
- case Nil() => flist match {
- case Cons(fhead, ftail) =>
- associative_lemma_induct(list, ftail, g(fhead), f, g)
- case Nil() => list match {
- case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
- case Nil() => true
+ associative_lemma(list, f, g) because {
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) because
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
}
- }
- })
+ })
+ }
}.holds
def left_unit_law[T,U](x: T, f: T => List[U]): Boolean = {
@@ -47,7 +49,7 @@ object Monads3 {
}
def right_unit_induct[T,U](list: List[T]): Boolean = {
- right_unit_law(list) && (list match {
+ right_unit_law(list) because (list match {
case Cons(head, tail) => right_unit_induct(tail)
case Nil() => true
})
@@ -62,7 +64,7 @@ object Monads3 {
}
def flatMap_to_zero_induct[T,U](list: List[T]): Boolean = {
- flatMap_to_zero_law(list) && (list match {
+ flatMap_to_zero_law(list) because (list match {
case Cons(head, tail) => flatMap_to_zero_induct(tail)
case Nil() => true
})
diff --git a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
index 29133762e6da8118e1e380b6fabb4fb3880d482b..35ca7537645182c003ebd3e8003e6db7c5648de2 100644
--- a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
@@ -2,6 +2,7 @@
import leon._
import leon.lang._
+import leon.proof._
object ParBalance {
@@ -72,7 +73,7 @@ object ParBalance {
def balanced_foldLeft_equivalence(list: List, p: (BigInt, BigInt)): Boolean = {
require(p._1 >= 0 && p._2 >= 0)
val f = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
- (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) && (list match {
+ (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) because (list match {
case Cons(head, tail) =>
val p2 = f(p, head)
balanced_foldLeft_equivalence(tail, p2)
@@ -178,14 +179,14 @@ object ParBalance {
}.holds
def reverse_init_equivalence(list: List): Boolean = {
- reverse(init(list)) == tail(reverse(list)) && (list match {
+ reverse(init(list)) == tail(reverse(list)) because (list match {
case Cons(head, tail) => reverse_init_equivalence(tail)
case Nil() => true
})
}.holds
def reverse_equality_equivalence(l1: List, l2: List): Boolean = {
- (l1 == l2) == (reverse(l1) == reverse(l2)) && ((l1, l2) match {
+ (l1 == l2) == (reverse(l1) == reverse(l2)) because ((l1, l2) match {
case (Cons(h1, t1), Cons(h2, t2)) => reverse_equality_equivalence(t1, t2)
case _ => true
})
@@ -198,7 +199,7 @@ object ParBalance {
// always decreasing, so that the termination checker can prove termination.
def reverse_reverse_equivalence(s: BigInt, list: List): Boolean = {
require(size(list) == s)
- reverse(reverse(list)) == list && ((list, reverse(list)) match {
+ reverse(reverse(list)) == list because ((list, reverse(list)) match {
case (Cons(h1, t1), Cons(h2, t2)) =>
reverse_reverse_equivalence(size(t1), t1) && reverse_reverse_equivalence(size(t2), t2)
case _ => true
diff --git a/src/test/resources/regression/verification/purescala/valid/Unapply.scala b/src/test/resources/regression/verification/purescala/valid/Unapply.scala
index 941b1f370d740204e8fa850a9d5e5a787b1c401e..1885837d990c32185a42c1232a53de48c3935340 100644
--- a/src/test/resources/regression/verification/purescala/valid/Unapply.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Unapply.scala
@@ -5,8 +5,18 @@ object Unap {
}
object Unapply {
- def bar: Boolean = { (42, true, ()) match {
- case Unap(_, b) if b => b
- case Unap((), b) => !b
- }} ensuring { res => res }
+
+ sealed abstract class Bool
+ case class True() extends Bool
+ case class False() extends Bool
+
+ def not(b: Bool): Bool = b match {
+ case True() => False()
+ case False() => True()
+ }
+
+ def bar: Bool = { (42, True().asInstanceOf[Bool], ()) match {
+ case Unap(_, b) if b == True() => b
+ case Unap((), b) => not(b)
+ }} ensuring { res => res == True() }
}
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index ff882c96157cb6b85b02e101a3c0b84e0cfe058f..84b0087caee305b66e16d82ad2adcd9f4b10e06d 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -187,6 +187,38 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
| def f3 = C(42).isInstanceOf[A]
|}""".stripMargin,
+ """import leon.lang._
+ |import leon.collection._
+ |
+ |object Foo {
+ | def unapply(i: BigInt): Option[BigInt] = if (i > 0) Some(i) else None()
+ |}
+ |
+ |object Unapply {
+ | def foo =
+ | (BigInt(1) match {
+ | case Foo(i) => i
+ | case _ => BigInt(0)
+ | }) + (BigInt(-12) match {
+ | case Foo(i) => i
+ | case _ => BigInt(2)
+ | })
+ |
+ | def size[A](l: List[A]): BigInt = l match {
+ | case _ :: _ :: _ :: Nil() => 3
+ | case _ :: _ :: Nil() => 2
+ | case _ :: Nil() => 1
+ | case Nil() => 0
+ | case _ :: _ => 42
+ | }
+ |
+ | def s1 = size(1 :: 2 :: 3 :: Nil[Int]())
+ | def s2 = size(Nil[Int]())
+ | def s3 = size(List(1,2,3,4,5,6,7,8))
+ |
+ |}
+ """.stripMargin,
+
"""object Casts1 {
| abstract class Foo
| case class Bar1(v: BigInt) extends Foo
@@ -371,6 +403,15 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
}
}
+ test("Unapply") { implicit fix =>
+ for(e <- allEvaluators) {
+ eval(e, fcall("Unapply.foo")()) === bi(3)
+ eval(e, fcall("Unapply.s1")()) === bi(3)
+ eval(e, fcall("Unapply.s2")()) === bi(0)
+ eval(e, fcall("Unapply.s3")()) === bi(42)
+ }
+ }
+
test("Casts1") { implicit fix =>
def bar1(es: Expr*) = cc("Casts1.Bar1")(es: _*)
def bar2(es: Expr*) = cc("Casts1.Bar2")(es: _*)
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 5b6667d5f4233521a4dc79a5d309618e49e8f07d..6301f4ea1a61144f4b38cd2d7660579c192f5089 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -47,7 +47,7 @@ class RepairSuite extends LeonRegressionSuite {
test(name) {
pipeline.run(ctx, List(path))
if(reporter.errorCount > 0) {
- fail("Errors during repair:\n")//+reporter.lastErrors.mkString("\n"))
+ fail("Errors during repair:\n"+reporter.lastErrors.mkString("\n"))
}
}
}
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
index 974615e6484304de738ebdd43ecafbb323e589c2..569eb95df2f7f66a05d7a825765adb6123b4d854 100644
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -59,10 +59,10 @@ class PureScalaValidSuite3 extends PureScalaValidSuite {
val optionVariants = List(opts(2))
}
class PureScalaValidSuiteZ3 extends PureScalaValidSuite {
- val optionVariants = Nil//if (isZ3Available) List(opts(3)) else Nil
+ val optionVariants = if (isZ3Available) List(opts(3)) else Nil
}
class PureScalaValidSuiteCVC4 extends PureScalaValidSuite {
- val optionVariants = Nil//if (isCVC4Available) List(opts(4)) else Nil
+ val optionVariants = if (isCVC4Available) opts.takeRight(1) else Nil
}
class PureScalaInvalidSuite extends PureScalaVerificationSuite {
diff --git a/testcases/verification/compilation/ExprCompiler.scala b/testcases/verification/compilation/ExprCompiler.scala
index 7518c21fb8ba7349e49c37c8acac6f99aaae2cdd..d6b7d74caa52a4a49255e71781c86f1052c439db 100644
--- a/testcases/verification/compilation/ExprCompiler.scala
+++ b/testcases/verification/compilation/ExprCompiler.scala
@@ -17,22 +17,22 @@ object TinyCertifiedCompiler {
def compile[A](e: ExprTree[A]): List[ByteCode[A]] = {
e match {
case Const(c) =>
- Cons(Load(c), Nil[ByteCode[A]]())
+ Cons(Load(c), Nil())
case Op(e1, e2) =>
- (compile(e1) ++ compile(e2)) ++ Cons(OpInst(), Nil[ByteCode[A]]())
+ (compile(e1) ++ compile(e2)) ++ Cons(OpInst(), Nil())
}
}
- def op[A](x: A, y: A): A = {
+ def op[A](x: A, y: A): A = { // uninterpreted
???[A]
}
def run[A](bytecode: List[ByteCode[A]], S: List[A]): List[A] = {
(bytecode, S) match {
case (Cons(Load(c), tail), _) =>
- run(tail, Cons[A](c, S)) // adding elements to the head of the stack
+ run(tail, c :: S) // adding elements to the head of the stack
case (Cons(OpInst(), tail), Cons(x, Cons(y, rest))) =>
- run(tail, Cons[A](op(y, x), rest))
+ run(tail, op(y, x) :: rest)
case (Cons(_, tail), _) =>
run(tail, S)
case (Nil(), _) => // no bytecode to execute
@@ -43,8 +43,7 @@ object TinyCertifiedCompiler {
def interpret[A](e: ExprTree[A]): A = {
e match {
case Const(c) => c
- case Op(e1, e2) =>
- op(interpret(e1), interpret(e2))
+ case Op(e1, e2) => op(interpret(e1), interpret(e2))
}
}
@@ -53,8 +52,7 @@ object TinyCertifiedCompiler {
(run(l1 ++ l2, S) == run(l2, run(l1, S))) because
// induction scheme (induct over l1)
(l1 match {
- case Nil() =>
- true
+ case Nil() => true
case Cons(h, tail) =>
(h, S) match {
case (Load(c), _) =>
@@ -63,8 +61,7 @@ object TinyCertifiedCompiler {
runAppendLemma(tail, l2, Cons[A](op(y, x), rest))
case (_, _) =>
runAppendLemma(tail, l2, S)
- case _ =>
- true
+ case _ => true
}
})
}.holds
@@ -74,16 +71,15 @@ object TinyCertifiedCompiler {
(run(compile(e), S) == interpret(e) :: S) because
// induction scheme
(e match {
- case Const(c) =>
- true
+ case Const(c) => true
case Op(e1, e2) =>
// lemma instantiation
val c1 = compile(e1)
val c2 = compile(e2)
- runAppendLemma((c1 ++ c2), Cons[ByteCode[A]](OpInst[A](), Nil[ByteCode[A]]()), S) &&
+ runAppendLemma((c1 ++ c2), Cons[ByteCode[A]](OpInst[A](), Nil()), S) &&
runAppendLemma(c1, c2, S) &&
compileInterpretEquivalenceLemma(e1, S) &&
compileInterpretEquivalenceLemma(e2, Cons[A](interpret(e1), S))
})
- } holds
+ }.holds
}
diff --git a/testcases/verification/higher-order/valid/FlatMap.scala b/testcases/verification/higher-order/valid/FlatMap.scala
index 56f8c47e86d835055e6c3a9ea44cb7b886e464fb..06d356c5fe5b1e7443831e7d541450c36449ef18 100644
--- a/testcases/verification/higher-order/valid/FlatMap.scala
+++ b/testcases/verification/higher-order/valid/FlatMap.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.proof._
import leon.collection._
object FlatMap {
@@ -13,10 +14,10 @@ object FlatMap {
}
def associative_append_lemma_induct[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
- l1 match {
- case Nil() => associative_append_lemma(l1, l2, l3)
- case Cons(head, tail) => associative_append_lemma(l1, l2, l3) && associative_append_lemma_induct(tail, l2, l3)
- }
+ associative_append_lemma(l1, l2, l3) because (l1 match {
+ case Nil() => true
+ case Cons(head, tail) => associative_append_lemma_induct(tail, l2, l3)
+ })
}.holds
def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
@@ -29,20 +30,21 @@ object FlatMap {
}
def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
- associative_lemma(list, f, g) &&
- append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
- (glist match {
- case Cons(ghead, gtail) =>
- associative_lemma_induct(list, flist, gtail, f, g)
- case Nil() => flist match {
- case Cons(fhead, ftail) =>
- associative_lemma_induct(list, ftail, g(fhead), f, g)
- case Nil() => list match {
- case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
- case Nil() => true
+ associative_lemma(list, f, g) because {
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) because
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
}
- }
- })
+ })
+ }
}.holds
}
diff --git a/testcases/web/verification/10_FoldAssociative.scala b/testcases/web/verification/10_FoldAssociative.scala
index ff0444f269dd6f9b2a2b7f2b54e13f54c6755ab2..6920231115fea93a1b7c7cefc27691a0ee2471bb 100644
--- a/testcases/web/verification/10_FoldAssociative.scala
+++ b/testcases/web/verification/10_FoldAssociative.scala
@@ -2,6 +2,7 @@
import leon._
import leon.lang._
+import leon.proof._
object FoldAssociative {
@@ -56,7 +57,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_split(list, x) && (list match {
+ lemma_split(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_split_induct(tail, x - 1)
case _ => true
@@ -77,7 +78,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_reassociative(list, x) && (list match {
+ lemma_reassociative(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_reassociative_induct(tail, x - 1)
case _ => true
@@ -93,7 +94,7 @@ object FoldAssociative {
def lemma_reassociative_presplit_induct(l1: List, l2: List): Boolean = {
val f = (x: Int, s: Int) => x + s
val list = append(l1, l2)
- lemma_reassociative_presplit(l1, l2) && (l1 match {
+ lemma_reassociative_presplit(l1, l2) because (l1 match {
case Cons(head, tail) =>
lemma_reassociative_presplit_induct(tail, l2)
case Nil() => true