From 101a4013bc1c1873ff6acbd997d6234a4c7a1176 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 2 May 2012 17:05:36 +0200
Subject: [PATCH] both cnf and dnf transformation does not lead to counter
examples
---
testcases/SatFun.scala | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/testcases/SatFun.scala b/testcases/SatFun.scala
index da37a77fb..e94804a7e 100644
--- a/testcases/SatFun.scala
+++ b/testcases/SatFun.scala
@@ -130,6 +130,10 @@ object SatFun {
val dnfFormula = dnfNaive(formula)
eval(formula, trueVars) == evalDnf(dnfFormula, trueVars)
} ensuring(_ == true)
+ def property2(formula: Formula, trueVars: Set[Int]): Boolean = {
+ val cnfFormula = cnfNaive(formula)
+ eval(formula, trueVars) == evalCnf(cnfFormula, trueVars)
+ } ensuring(_ == true)
def vars(formula: Formula): Set[Int] = formula match {
--
GitLab