From e2b8b739793aeed23a721210b65a7639ba84f458 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 24 Jul 2015 03:19:47 +0200
Subject: [PATCH] Add running example
---
testcases/web/demos/009_Repair1.scala | 55 +++++++++++++++++++++++++++
1 file changed, 55 insertions(+)
create mode 100644 testcases/web/demos/009_Repair1.scala
diff --git a/testcases/web/demos/009_Repair1.scala b/testcases/web/demos/009_Repair1.scala
new file mode 100644
index 000000000..cf4363100
--- /dev/null
+++ b/testcases/web/demos/009_Repair1.scala
@@ -0,0 +1,55 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.collection._
+import leon.annotation._
+
+object Running {
+ abstract class Formula
+ case class And(a: Formula, b: Formula) extends Formula
+ case class Or (a: Formula, b: Formula) extends Formula
+ case class Implies(a: Formula, b: Formula) extends Formula
+ case class Not(a: Formula) extends Formula
+ case object LitFalse extends Formula
+ case object LitTrue extends Formula
+
+ def desugar(f: Formula): Formula = {
+ f match {
+ case And(a, b) =>
+ And(desugar(a), desugar(b))
+ case Or(a, b) =>
+ Or(desugar(a), desugar(b))
+ case Implies(a, b) =>
+ if (a == LitFalse) {
+ LitTrue
+ } else {
+ Or(Not(a), b)
+ }
+ case Not(Not(a)) =>
+ desugar(a)
+ case Not(a) =>
+ Not(desugar(a))
+ case f =>
+ f
+ }
+ } ensuring {
+ res => !existsImplies(res) && eval(res) == eval(f)
+ }
+
+ def existsImplies(f: Formula): Boolean = f match {
+ case Implies(a, b) => true
+ case And(a, b) => existsImplies(a) || existsImplies(b)
+ case Or(a, b) => existsImplies(a) || existsImplies(b)
+ case Not(a) => existsImplies(a)
+ case _ => false
+ }
+
+ def eval(f: Formula): Boolean = f match {
+ case Implies(a, b) => !eval(a) || eval(b)
+ case And(a, b) => eval(a) && eval(b)
+ case Or(a, b) => eval(a) || eval(b)
+ case Not(a) => !eval(a)
+ case LitFalse => false
+ case LitTrue => true
+ }
+
+}
--
GitLab