From d53f474c91d39d49d0d30fa8d8deca51c4559690 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Thu, 4 Jul 2024 16:13:14 -0400 Subject: [PATCH] Disable datatype acyclicity rule (proof reconstruction not yet implemented) --- Duper/Saturate.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean index cc87a7a..9cb8f1d 100644 --- 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,