diff --git a/demo/ListOperations.scala b/demo/ListOperations.scala
index 3a08ac8f916661e89e2455eeaa2edf0593765f7e..086c05a22a427987c1bb0bb6934123f4f59c4392 100644
--- a/demo/ListOperations.scala
+++ b/demo/ListOperations.scala
@@ -75,6 +75,25 @@ object ListOperations {
case Cons(x,xs) => Cons(x, append(xs, l2))
}) ensuring(content(_) == content(l1) ++ content(l2))
+ def map(f : Map[Int,Int], l : List) : List = {
+ require(definedForAll(f, l))
+ l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => Cons(f(x), map(f, xs))
+ }
+ }
+
+ @induct
+ def appendMapCommute(l1 : List, l2 : List, f : Map[Int, Int]) : Boolean = {
+ require(definedForAll(f, l1) && definedForAll(f, l2))
+ map(f, append(l1, l2)) == append(map(f, l1), map(f, l2))
+ } holds
+
+ def definedForAll(f : Map[Int, Int], l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x, xs) => f.isDefinedAt(x) && definedForAll(f, xs)
+ }
+
@induct
def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala
index c3e368be4ad432f1d2e291066263795402b6f7fe..7a212b667d54e2e42f1662c8a5044d26cb3ef34e 100644
--- a/src/purescala/DefaultTactic.scala
+++ b/src/purescala/DefaultTactic.scala
@@ -189,7 +189,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
}
// prec: there should be no lets and no pattern-matching in this expression
- private def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
+ def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
var collected : Set[(Seq[Expr],Expr)] = Set.empty
def rec(expr: Expr, path: List[Expr]) : Unit = {
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index cbc3ae4f0b068fdbcc59791c574823ad19d1b793..0be2fcbfd2da21ac10d4eedc6818de0b9691fd57 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -666,6 +666,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
//z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
+ reporter.info(" - finished unrolling")
unrollingStopwatch.stop
}
}
diff --git a/src/purescala/InductionTactic.scala b/src/purescala/InductionTactic.scala
index 32307c13c0c5de2e2fc20efa890c04547ac69c90..d93cc5957327f317dcf354dd8ea8413848d086e6 100644
--- a/src/purescala/InductionTactic.scala
+++ b/src/purescala/InductionTactic.scala
@@ -9,18 +9,6 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
override val description = "Induction tactic for suitable functions"
override val shortDescription = "induction"
- private def singleAbsClassDef(args: VarDecls) : Option[AbstractClassDef] = {
- val filtered = args.filter(arg =>
- arg.getType match {
- case AbstractClassType(_) => true
- case _ => false
- })
- if (filtered.size != 1) None else (filtered.head.getType match {
- case AbstractClassType(classDef) => Some(classDef)
- case _ => scala.sys.error("This should not happen.")
- })
- }
-
private def firstAbsClassDef(args: VarDecls) : Option[(AbstractClassDef, VarDecl)] = {
val filtered = args.filter(arg =>
arg.getType match {
@@ -86,4 +74,82 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
defaultPost
}
}
+
+ override def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
+ val defaultPrec = super.generatePreconditions(function)
+ firstAbsClassDef(function.args) match {
+ case Some((classDef, arg)) => {
+ val toRet = if(function.hasBody) {
+ val cleanBody = expandLets(matchToIfThenElse(function.body.get))
+
+ val allPathConds = collectWithPathCondition((t => t match {
+ case FunctionInvocation(fd, _) if(fd.hasPrecondition) => true
+ case _ => false
+ }), cleanBody)
+
+ def withPrec(path: Seq[Expr], shouldHold: Expr) : Expr = if(function.hasPrecondition) {
+ Not(And(And(matchToIfThenElse(function.precondition.get) +: path), Not(shouldHold)))
+ } else {
+ Not(And(And(path), Not(shouldHold)))
+ }
+
+ val conditionsForAllPaths : Seq[Seq[VerificationCondition]] = allPathConds.map(pc => {
+ val path : Seq[Expr] = pc._1
+ val fi = pc._2.asInstanceOf[FunctionInvocation]
+ val FunctionInvocation(fd, args) = fi
+
+ val conditionsForEachChild = (for (child <- classDef.knownChildren) yield (child match {
+ case ccd @ CaseClassDef(id, prnt, vds) => {
+ val argAsVar = arg.toVariable
+ val selectors = selectorsOfParentType(classDefToClassType(classDef), ccd, argAsVar)
+
+ val prec : Expr = freshenLocals(matchToIfThenElse(fd.precondition.get))
+ val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe))
+ val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
+ val newBody : Expr = replace(substMap, prec)
+ val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
+
+ val toProve = withPrec(path, newCall)
+
+ val conditionForChild =
+ if (selectors.isEmpty)
+ toProve
+ else {
+ val inductiveHypothesis = (for (sel <- selectors) yield {
+ val prec : Expr = freshenLocals(matchToIfThenElse(fd.precondition.get))
+ val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe))
+ val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
+ val newBody : Expr = replace(substMap, prec)
+ val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
+
+ val toReplace = withPrec(path, newCall)
+ replace(Map(argAsVar -> sel), toReplace)
+ })
+ Implies(And(inductiveHypothesis), toProve)
+ }
+ new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), function, VCKind.Precondition, this).setPosInfo(fi)
+ }
+ case _ => scala.sys.error("Abstract class has non-case class subtype")
+ }))
+ println("Induction tactic yields the following VCs:")
+ println(conditionsForEachChild.map(vc => vc.condition).mkString("\n"))
+ conditionsForEachChild
+ }).toSeq
+
+ conditionsForAllPaths.flatten
+ } else {
+ Seq.empty
+ }
+
+ // println("PRECS VCs FOR " + function.id.name)
+ // println(toRet.toList.map(vc => vc.posInfo + " -- " + vc.condition).mkString("\n\n"))
+
+ toRet
+ }
+ case None => {
+ reporter.warning("Induction tactic currently supports exactly one argument of abstract class type")
+ defaultPrec
+ }
+ }
+ }
}