Unfold topes with symmetry for TopeEQ, increase number of iterations …

…for unfolding
rzk-lang · Mar 22, 2023 · 342b1e4 · 342b1e4
1 parent e650cae
commit 342b1e4
Showing 1 changed file with 11 additions and 2 deletions.
diff --git a/rzk/src/Rzk/Evaluator.hs b/rzk/src/Rzk/Evaluator.hs
@@ -14,7 +14,8 @@ module Rzk.Evaluator (
   localConstraint,
   enterPatternScope, enterPatternScope',
   eval,
-  entailTope
+  entailTope,
+  unfoldTopesInCube2,
 ) where
 
 import           Control.Monad.Except
@@ -353,14 +354,15 @@ unfoldRepeatedlyN unfold n xs
 
 unfoldTopesInCube2 :: Eq var => [Term var] -> [Term var]
 unfoldTopesInCube2
-  = unfoldRepeatedlyN unfoldTopesInCube2Once 10
+  = unfoldRepeatedlyN unfoldTopesInCube2Once 50
 
 unfoldTopesInCube2Once :: Eq var => [Term var] -> [Term var]
 unfoldTopesInCube2Once
   = antisymmetryTopesInCube2
       <> distinctTopes
       <> transitivityTopesInCube2
       <> transitivityTopesEQ
+      <> symmetryTopesEQ
       <> unfoldConjunction
 
 unfoldConjunction :: [Term var] -> [Term var]
@@ -388,6 +390,13 @@ transitivityTopesEQ topes =
   , x /= z
   ]
 
+symmetryTopesEQ :: Eq var => [Term var] -> [Term var]
+symmetryTopesEQ topes =
+  [ TopeEQ y x
+  | TopeEQ x y <- topes
+  , x /= y
+  ]
+
 antisymmetryTopesInCube2 :: Eq var => [Term var] -> [Term var]
 antisymmetryTopesInCube2 topes =
   [ TopeEQ x y