From 36777e9d22e82e0a14173c39c493c217e363786c Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 3 Sep 2015 11:34:39 +0200
Subject: [PATCH] SimplifierWithPaths optionally takes initial path condition
---
src/main/scala/leon/purescala/ExprOps.scala | 67 +++++++++++++++++--
.../leon/purescala/SimplifierWithPaths.scala | 11 +--
.../scala/leon/synthesis/ConvertHoles.scala | 6 +-
src/main/scala/leon/verification/Tactic.scala | 1 -
4 files changed, 69 insertions(+), 16 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c07693a8a..84f196618 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1210,8 +1210,8 @@ object ExprOps {
simplePreTransform(pre)(expr)
}
- def simplifyPaths(sf: SolverFactory[Solver]): Expr => Expr = {
- new SimplifierWithPaths(sf).transform
+ def simplifyPaths(sf: SolverFactory[Solver], initC: List[Expr] = Nil): Expr => Expr = {
+ new SimplifierWithPaths(sf, initC).transform
}
trait Traverser[T] {
@@ -2047,13 +2047,13 @@ object ExprOps {
}
- /** Collects correctness conditions from within an expression
- * (taking into account the path condition).
+ /** Collects from within an expression all conditions under which the evaluation of the expression
+ * will not fail (e.g. by violating a function precondition or evaluating to an error).
*
- * Collection of preconditions of function invocations
- * can be disabled (mainly for [[leon.verification.Tactic]]).
+ * Collection of preconditions of function invocations can be disabled
+ * (mainly for [[leon.verification.Tactic]]).
*
- * @param e The expression to traverse
+ * @param e The expression for which correctness conditions are calculated.
* @param collectFIs Whether we also want to collect preconditions for function invocations
* @return A sequence of pairs (expression, condition)
*/
@@ -2086,6 +2086,59 @@ object ExprOps {
}
+ def simpleCorrectnessCond(e: Expr, path: List[Expr], sf: SolverFactory[Solver]): Expr = {
+ simplifyPaths(sf, path)(
+ andJoin( collectCorrectnessConditions(e) map { _._2 } )
+ )
+ }
+
}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index 9e33ba1f6..dc4dfce46 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -10,11 +10,9 @@ import Extractors._
import Constructors._
import solvers._
-class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
+class SimplifierWithPaths(sf: SolverFactory[Solver], override val initC: List[Expr] = Nil) extends TransformerWithPC {
type C = List[Expr]
- val initC = Nil
-
val solver = SimpleSolverAPI(sf)
protected def register(e: Expr, c: C) = e :: c
@@ -97,10 +95,10 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
case SimpleCase(p, rhs) =>
SimpleCase(p, rec(rhs, cond))
case GuardedCase(p, g, rhs) =>
- // FIXME: This is quite a dirty hack. We just know matchCasePathConditions
+ // @mk: This is quite a dirty hack. We just know matchCasePathConditions
// returns the current guard as the last element.
// We don't include it in the path condition when we recurse into itself.
- val condWithoutGuard = try { cond.init } catch { case _ : UnsupportedOperationException => List() }
+ val condWithoutGuard = cond.dropRight(1)
val newGuard = rec(g, condWithoutGuard)
if (valid(newGuard))
SimpleCase(p, rec(rhs,cond))
@@ -135,6 +133,9 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
BooleanLiteral(true).copiedFrom(e)
}
+ case a @ Assert(pred, _, body) if impliedBy(pred, path) =>
+ body.copiedFrom(a)
+
case b if b.getType == BooleanType && impliedBy(b, path) =>
BooleanLiteral(true).copiedFrom(b)
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 7e6c3e880..a53ff8672 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -26,10 +26,10 @@ object ConvertHoles extends TransformationPhase {
*
* def foo(a: T) {
* require(..a..)
- * val h = choose { (h) => {
- * val res = expr(a, ???)
+ * val h = choose ( h' =>
+ * val res = expr(a, h')
* post(res)
- * }
+ * )
* expr(a, h)
* } ensuring { res =>
* post(res)
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 77691739f..98af8cde0 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -5,7 +5,6 @@ package verification
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
abstract class Tactic(vctx: VerificationContext) {
val description : String
--
GitLab