diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/CallGraph.scala index 952e8499ed0a9898af06b6ae1383518b625ee4ca..3ee808dbca7642c7c2f38c177b414379b89036b4 100644 --- a/src/main/scala/leon/CallGraph.scala +++ b/src/main/scala/leon/CallGraph.scala @@ -26,5 +26,44 @@ class CallGraph(val program: Program) { null } +// def hoistIte(expr: Expr): Expr = expr match { +// case ite@IfExpr(c, t, e) => IfExpr(c, hoistIte(t), hoistIte(e)).setType(ite.getType) +// case BinaryOperator(t1, t2) => +// +// } + //def analyse(program: Program) { + // z3Solver.setProgram(program) + // reporter.info("Running test generation") + // val allFuns = program.definedFunctions + // allFuns.foreach(fd => { + // val testcases = generateTestCases(fd) + // reporter.info("Running " + fd.id + " with the following testcases:\n") + // reporter.info(testcases.mkString("\n")) + // }) + //} + + //private def generatePathConditions(funDef: FunDef): Seq[Expr] = if(!funDef.hasImplementation) Seq() else { + // val body = funDef.body.get + // val cleanBody = expandLets(matchToIfThenElse(body)) + // collectWithPathCondition(cleanBody) + //} + + //// prec: there should be no lets and no pattern-matching in this expression + // private def collectWithPathCondition(expression: Expr): Seq[Expr] = { + // var allPaths: Seq[Expr] = Seq() + + // def rec(expr: Expr, path: Expr): Seq[Expr] = expr match { + // case IfExpr(cond, then, elze) => + // (if(!containsIfExpr(then)) Seq(And(path, cond)) else rec(then, And(cond, path))) ++ + // (if(!containsIfExpr(elze)) Seq(And(path, Not(cond))) else rec(then, And(cond, path))) + // case NAryOperator(args, _) => args.flatMap(arg => rec(arg, path)) + // case BinaryOperator(t1, t2, _) => rec(t1, path) ++ rec(t2, path) + // case UnaryOperator(t, _) => rec(t, path) + // case t : Terminal => Seq() + // case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr) + // } + + // rec(expression, BooleanLiteral(true)).distinct + //} } diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala index 3716a41265b6399fc3ea06de189607a7415e2b8b..871d7b4e01ad2fbcfc64a93bac1bd524f58c3b21 100644 --- a/src/main/scala/leon/purescala/Trees.scala +++ b/src/main/scala/leon/purescala/Trees.scala @@ -85,6 +85,8 @@ object Trees { } case class TupleSelect(tuple: Expr, index: Int) extends Expr + case class WayPoint(expr: Expr) extends Expr + object MatchExpr { def apply(scrutinee: Expr, cases: Seq[MatchCase]) : MatchExpr = { scrutinee.getType match { @@ -154,6 +156,7 @@ object Trees { case class TuplePattern(binder: Option[Identifier], subPatterns: Seq[Pattern]) extends Pattern + /* Propositional logic */ object And { def apply(l: Expr, r: Expr) : Expr = (l,r) match { @@ -439,6 +442,7 @@ object Trees { case ArrayLength(a) => Some((a, ArrayLength)) case ArrayClone(a) => Some((a, ArrayClone)) case ArrayMake(t) => Some((t, ArrayMake)) + case WayPoint(t) => Some((t, WayPoint)) case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e))) case _ => None }