Disable datatype acyclicity rule (proof reconstruction not yet implem…

…ented)
leanprover-community · Jul 4, 2024 · d53f474 · d53f474
1 parent d198aba
commit d53f474
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean
@@ -72,7 +72,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       identBoolFalseElim.toSimpRule,
       datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
-      datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
+      -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
@@ -97,7 +97,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       identBoolFalseElim.toSimpRule,
       datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
-      datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
+      -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
       (forwardEqualitySubsumption subsumptionTrie).toSimpRule,