From 58c161198e50d8484654d951e2bbb9a157656001 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 10 Jun 2015 17:31:59 +0200
Subject: [PATCH] Assume contracts of inductive calls

---
 src/main/scala/leon/purescala/ExprOps.scala   | 17 +++++++
 .../smtlib/SMTLIBCVC4ProofSolver.scala        | 17 +++----
 .../smtlib/SMTLIBCVC4QuantifiedSolver.scala   | 46 +++++++++++++++++--
 3 files changed, 68 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 8943c6b16..56fe5d401 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -666,6 +666,22 @@ object ExprOps {
     rec(expr, Map.empty)
   }
 
+  /*
+   * Lifts lets to top level, without pushing any used variable out of scope.
+   * Assumes no match expressions (i.e. matchToIfThenElse has been called on e)
+   */
+  def liftLets(e: Expr): Expr = {
+
+    type C = Seq[(Identifier, Expr)]
+
+    def lift(e: Expr, defs: C) = e match {
+      case Let(i, ex, b) => (b, (i, ex) +: defs)
+      case _ => (e, defs)
+    }
+    val (bd, defs) = genericTransform[C](noTransformer, lift, _.flatten)(Seq())(e)
+
+    defs.foldRight(bd){ case ((id, e), body) => let(id, e, body) }
+  }
 
   /**
    * Generates substitutions necessary to transform scrutinee to equivalent
@@ -1082,6 +1098,7 @@ object ExprOps {
   }
 
   private def noCombiner(subCs: Seq[Unit]) = ()
+  private def noTransformer[C](e: Expr, c: C) = (e, c)
 
   def simpleTransform(pre: Expr => Expr, post: Expr => Expr)(expr: Expr) = {
     val newPre  = (e: Expr, c: Unit) => (pre(e), ())
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index d8f94c40c..5a4663786 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -28,13 +28,12 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
   }
 
   // For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
-  override def assertCnstr(expr: Expr) =
-    try {
-      sendCommand(SMTAssert(quantifiedTerm(Exists, expr)))
-    } catch {
-      case _ : IllegalArgumentException =>
-        addError()
-    }
+  override def assertCnstr(e: Expr) = try {
+    sendCommand(SMTAssert(quantifiedTerm(Exists, e)))
+  } catch {
+    case _: IllegalArgumentException =>
+      addError()
+  }
 
   // This solver does not support model extraction
   override def getModel: Map[Identifier, Expr] = {
@@ -47,7 +46,9 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
   override def check: Option[Boolean] = {
     super.check match {
       case Some(true) =>
-        reporter.warning(s"Solver $name found a counterexample, but masking it as unknown because counterexamples are not supported.")
+        reporter.warning(s"Solver $name found a counterexample, " +
+          "but masking it as unknown because counterexamples are not supported."
+        )
         None
       case other => other
     }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index e4f55acef..0e236f9ef 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -3,12 +3,14 @@
 package leon
 package solvers.smtlib
 
+import leon.purescala.ExprOps.CollectorWithPaths
 import purescala._
 import Expressions._
+import ExprOps._
 import Definitions._
-import Constructors.{application, implies}
+import Constructors._
 import DefOps.typedTransitiveCallees
-import verification.VC
+import leon.verification.{VCKinds, VC}
 import smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
 import smtlib.parser.Terms.{Exists => SMTExists, ForAll => SMTForall, _ }
 import smtlib.theories.Core.Equals
@@ -123,13 +125,49 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
 
   }
 
+  // Generates inductive hypotheses for
+  protected def generateInductiveHyp: Expr = {
+    def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = {
+      CollectorWithPaths(f).traverse(expr)
+    }
+
+    //println("Current is" + currentFunDef.get)
+
+    val calls = /*collectWithPC {
+      case f : FunctionInvocation => f
+    }*/functionCallsOf(currentFunDef.get.body.get) //FIXME too many .get
+
+    //println(calls mkString "\n")
+
+    val inductiveHyps = for {
+      fi@FunctionInvocation(tfd, args) <- calls.toSeq
+    } yield {
+      val post = tfd.postcondition map {
+        post => application(replaceFromIDs(tfd.params.map{ _.id}.zip(args).toMap, post), Seq(fi))
+      } getOrElse BooleanLiteral(true)
+      val pre = tfd.precondition getOrElse BooleanLiteral(true)
+      /*implies(pc, */ and(pre, post) //)
+    }
+
+    andJoin(inductiveHyps)
+  }
+
+  protected def withInductiveHyp(vc: VC): Expr = {
+    if (vc.kind == VCKinds.Postcondition) {
+      // We want to check if the negation of the vc is sat under inductive hyp.
+      // So we need to see if (indHyp /\ !vc) is satisfiable
+      liftLets(matchToIfThenElse(and(generateInductiveHyp, not(vc.condition))))
+    } else {
+      not(vc.condition)
+    }
+  }
+
   // We need to know the function context.
   // The reason is we do not want to assume postconditions of functions referring to 
   // the current function, as this may make the proof unsound
   override def assertVC(vc: VC) = {
     currentFunDef = Some(vc.fd)
-    //println("Setting fundef to " + currentFunDef.get.id.uniqueName)
-    super.assertVC(vc)
+    assertCnstr(withInductiveHyp(vc))
   }
 
 }
-- 
GitLab