From 342b1e47a0ff25ea3a0b2afc322662a7f06f3299 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Wed, 22 Mar 2023 13:47:31 +0300
Subject: [PATCH] Unfold topes with symmetry for TopeEQ, increase number of
 iterations for unfolding

---
 rzk/src/Rzk/Evaluator.hs | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/rzk/src/Rzk/Evaluator.hs b/rzk/src/Rzk/Evaluator.hs
index 64b690d56..3539bfed3 100644
--- 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,7 +354,7 @@ 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
@@ -361,6 +362,7 @@ unfoldTopesInCube2Once
       <> 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