Fix conversion of formulas

diff --git a/Connections.hs b/Connections.hs
index c36d5c5715833fb88f8d620a6e433e768b795c04..e5c456588f9d26567208e42b8c2c7e69439a4f3e 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -194,6 +194,16 @@ orFormula (Dir Zero) phi = phi
 orFormula phi (Dir Zero) = phi
 orFormula phi psi        = phi :\/: psi
 
+dnf :: Formula -> Set (Set (Name,Dir))
+dnf (Dir One) = Set.singleton Set.empty
+dnf (Dir Zero) = Set.empty
+dnf (Atom n) = Set.singleton (Set.singleton (n,1))
+dnf (NegAtom n) = Set.singleton (Set.singleton (n,0))
+dnf (phi :\/: psi) = dnf phi `Set.union` dnf psi
+dnf (phi :/\: psi) = Set.fromList [ a `Set.union` b
+                                  | a <- Set.toList (dnf phi)
+                                  , b <- Set.toList (dnf psi) ]
+
 -- evalFormula :: Formula -> Face -> Formula
 -- evalFormula phi alpha =
 --   Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha

diff --git a/Eval.hs b/Eval.hs
index 35c3801e4a027721fa46cc4ee2e9f8293972a081..fccd22e775dfdeb24325f055c563b89761fdc076 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -753,4 +753,4 @@ instance Convertible a => Convertible (System a) where
                   and (elems (intersectionWith (conv k) ts ts'))
 
 instance Convertible Formula where
-  conv _ phi psi = sort (invFormula phi 1) == sort (invFormula psi 1)
+  conv _ phi psi = dnf phi == dnf psi