From 39b2c3773577fb42f55c773717b1f173b8afeea4 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Thu, 4 Dec 2014 18:11:22 +0100
Subject: [PATCH] Some -partial- updates to proplogic benchmark

---
 .../repair/PropLogic/PropLogic.scala          | 24 +++--------------
 .../repair/PropLogic/PropLogic1.scala         | 27 +++++--------------
 .../repair/PropLogic/PropLogic3.scala         |  7 ++++-
 .../repair/PropLogic/PropLogic4.scala         |  7 ++++-
 .../repair/PropLogic/PropLogic5.scala         |  7 ++++-
 .../repair/PropLogic/PropLogic6.scala         |  7 ++++-
 6 files changed, 35 insertions(+), 44 deletions(-)

diff --git a/testcases/synthesis/repair/PropLogic/PropLogic.scala b/testcases/synthesis/repair/PropLogic/PropLogic.scala
index c33b0500e..718a36e89 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic.scala
@@ -34,7 +34,9 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+    isNNF(res)
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
@@ -44,23 +46,5 @@ object SemanticsPreservation {
     case _ => true
   }
 
-  def partEval(formula : Formula) : Formula = { formula match {
-    case And(Const(false), _ ) => Const(false)
-    case And(_, Const(false)) => Const(false)
-    case And(Const(true), e) => partEval(e)
-    case And(e, Const(true)) => partEval(e)
-    case Or(Const(true), _ ) => Const(true)
-    case Or(_, Const(true)) => Const(true)
-    case Or(Const(false), e) => partEval(e)
-    case Or(e, Const(false)) => partEval(e)
-    case Not(Const(c)) => Const(!c)
-    case other => other
-  }} ensuring { size(_) <= size(formula) }
-
-  
-  @induct
-  def partEvalSound (f : Formula, env : Set[Int]) = {
-    eval(partEval(f))(env) == eval(f)(env)
-  }.holds
-  
+    
 }
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic1.scala b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
index 8ff0b9f15..47752be39 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic1.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+    isNNF(res) && ((formula, res) passes {
+      case Not(Not(Not( Const(a) ))) => Const(!a)
+    })
+  }
+
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
@@ -44,23 +49,5 @@ object SemanticsPreservation {
     case _ => true
   }
 
-  def partEval(formula : Formula) : Formula = { formula match {
-    case And(Const(false), _ ) => Const(false)
-    case And(_, Const(false)) => Const(false)
-    case And(Const(true), e) => partEval(e)
-    case And(e, Const(true)) => partEval(e)
-    case Or(Const(true), _ ) => Const(true)
-    case Or(_, Const(true)) => Const(true)
-    case Or(Const(false), e) => partEval(e)
-    case Or(e, Const(false)) => partEval(e)
-    case Not(Const(c)) => Const(!c)
-    case other => other
-  }} ensuring { size(_) <= size(formula) }
-
-  
-  @induct
-  def partEvalSound (f : Formula, env : Set[Int]) = {
-    eval(partEval(f))(env) == eval(f)(env)
-  }.holds
-  
+    
 }
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic3.scala b/testcases/synthesis/repair/PropLogic/PropLogic3.scala
index b905ed40f..600c59ed2 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic3.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic3.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     // FIXME: forgot to handle the Not(Not(_)) case 
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+     isNNF(res) && ((formula, res) passes {
+       case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+       case x@And(Literal(_), Literal(_)) => x
+     })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic4.scala b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
index 549b91c45..facbe08aa 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic4.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+      isNNF(res) && ((formula, res) passes {
+        case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+        case x@And(Literal(_), Literal(_)) => x
+      })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic5.scala b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
index 4b8a2149a..d86d184ed 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic5.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+       isNNF(res) && ((formula, res) passes {
+         case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+         case x@And(Literal(_), Literal(_)) => x
+       })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic6.scala b/testcases/synthesis/repair/PropLogic/PropLogic6.scala
index 12791f753..4fee819e2 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic6.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic6.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+    isNNF(res) && ((formula, res) passes {
+      case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+      case x@And(Literal(_), Literal(_)) => x
+    })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
-- 
GitLab