From 62319679c16906d5887c42c99e2338eb28ca7ecc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Thu, 24 Mar 2011 09:55:48 +0000
Subject: [PATCH] A previous benchmark that seemingly leads to funcheck bug.
---
.../SemanticsPreservation.scala | 44 +++++++++++++++++++
1 file changed, 44 insertions(+)
create mode 100644 pldi2011-testcases/SemanticsPreservation.scala
diff --git a/pldi2011-testcases/SemanticsPreservation.scala b/pldi2011-testcases/SemanticsPreservation.scala
new file mode 100644
index 000000000..a5a2a38f9
--- /dev/null
+++ b/pldi2011-testcases/SemanticsPreservation.scala
@@ -0,0 +1,44 @@
+import scala.collection.immutable.Set
+import funcheck.Utils._
+import funcheck.Annotations._
+
+object SemanticsPreservation {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Variable(id: Int) extends Formula
+
+ @induct
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case n @ Not(_) => n
+ case v @ Variable(_) => v
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Not(_) => false
+ case Variable(_) => true
+ }
+
+ @induct
+ def eval(formula: Formula): Boolean = (formula match {
+ case And(lhs, rhs) => eval(lhs) && eval(rhs)
+ case Or(lhs, rhs) => eval(lhs) || eval(rhs)
+ case Not(f) => !eval(f)
+ case Variable(id) => id > 42
+ }) ensuring(res => res == eval(nnf(formula)))
+
+ @induct
+ def nnfPreservesSemantics(f: Formula): Boolean = {
+ eval(f) == eval(nnf(f))
+ } holds
+
+}
--
GitLab