From 213c124874d3dd987333efee9f879dd9b35d320b Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 31 Oct 2012 15:25:52 +0100
Subject: [PATCH] path-aware simplifications (untested for now)
---
src/main/scala/leon/purescala/TreeOps.scala | 72 +++++++++++++++++++
.../leon/test/purescala/TreeOpsTest.scala | 29 ++++++++
2 files changed, 101 insertions(+)
create mode 100644 src/test/scala/leon/test/purescala/TreeOpsTest.scala
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 802d72ed9..6bc44b67c 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1218,4 +1218,76 @@ object TreeOps {
simplePreTransform(pre)(expr)
}
+
+ // NOTE : this is currently untested, use at your own risk !
+ // (or better yet, write tests for it)
+ // PS
+ def simplifyPaths(solver : Solver)(expr : Expr) : Expr = {
+ def impliedBy(e : Expr, path : Seq[Expr]) : Boolean = {
+ solver.solve(Implies(And(path), e)) match {
+ case Some(true) => true
+ case _ => false
+ }
+ }
+
+ def contradictedBy(e : Expr, path : Seq[Expr]) : Boolean = {
+ solver.solve(Implies(And(path), Not(e))) match {
+ case Some(true) => true
+ case _ => false
+ }
+ }
+
+ def rec(e : Expr, path : Seq[Expr]): Expr = e match {
+
+ case IfExpr(cond, then, elze) =>
+ val rc = rec(cond, path)
+ rc match {
+ case BooleanLiteral(true) => rec(then, path)
+ case BooleanLiteral(false) => rec(elze, path)
+ case _ => IfExpr(rc, rec(then, rc +: path), rec(elze, Not(rc) +: path))
+ }
+
+ case And(es) =>
+ var extPath = path
+ var continue = true
+ And(for(e <- es if continue) yield {
+ val se = rec(e, extPath)
+ if(se == BooleanLiteral(false)) continue = false
+ extPath = se +: extPath
+ se
+ })
+
+ case Or(es) =>
+ var extPath = path
+ var continue = true
+ Or(for(e <- es if continue) yield {
+ val se = rec(e, extPath)
+ if(se == BooleanLiteral(true)) continue = true
+ extPath = se +: extPath
+ se
+ })
+
+ case b if b.getType == BooleanType && impliedBy(b, path) =>
+ BooleanLiteral(true)
+
+ case b if b.getType == BooleanType && contradictedBy(b, path) =>
+ BooleanLiteral(false)
+
+ case UnaryOperator(e, builder) =>
+ builder(rec(e, path))
+
+ case BinaryOperator(e1, e2, builder) =>
+ builder(rec(e1, path), rec(e2, path))
+
+ case NAryOperator(es, builder) =>
+ builder(es.map(rec(_, path)))
+
+ case t : Terminal => t
+
+ case _ =>
+ sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
+ }
+
+ rec(expr, Nil)
+ }
}
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTest.scala b/src/test/scala/leon/test/purescala/TreeOpsTest.scala
new file mode 100644
index 000000000..a0ee0fdf3
--- /dev/null
+++ b/src/test/scala/leon/test/purescala/TreeOpsTest.scala
@@ -0,0 +1,29 @@
+package leon.test.purescala
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.SilentReporter
+
+import org.scalatest.FunSuite
+
+class TreeOpsTest extends FunSuite {
+ private val silentReporter = new SilentReporter
+
+ private val emptyProgram = Program(
+ FreshIdentifier("Empty"),
+ ObjectDef(FreshIdentifier("Empty"), Seq.empty, Seq.empty)
+ )
+
+ test("Path-aware simplifications") {
+ import leon.solvers.z3.UninterpretedZ3Solver
+ val solver = new UninterpretedZ3Solver(silentReporter)
+ solver.setProgram(emptyProgram)
+
+ // TODO actually testing something here would be better, sorry
+ // PS
+
+ assert(true)
+ }
+}
--
GitLab