add WayPoint expr

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
+  //}
 }

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
     }