From 6c2732d82f95cefeefa79679d63fcb0531445807 Mon Sep 17 00:00:00 2001 From: TigerThePro Date: Tue, 25 May 2021 20:48:44 -0700 Subject: [PATCH] show term ID is now responsive in explain path --- source/DAGView.cs | 4 ---- source/QuantifierModel/InstantiationPath.cs | 4 ---- 2 files changed, 8 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index a75da67..ebf073f 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -507,10 +507,6 @@ private void pathExplanationButton_Click(object sender, EventArgs e) highlightPath(cyclePath); _z3AxiomProfiler.UpdateSync(cyclePath); toRemove = cyclePath.GetInstnationsUnusedInGeneralization(); - if (cyclePath.NeedsIds()) - { - _z3AxiomProfiler.EnableTermIds(); - } } else { diff --git a/source/QuantifierModel/InstantiationPath.cs b/source/QuantifierModel/InstantiationPath.cs index 166d18a..60a01ba 100644 --- a/source/QuantifierModel/InstantiationPath.cs +++ b/source/QuantifierModel/InstantiationPath.cs @@ -561,10 +561,6 @@ private void printCycleInfo(InfoPanelContent content, PrettyPrintFormat format) if (!hasCycle()) return; var cycle = cycleDetector.getCycleQuantifiers(); var generalizationState = cycleDetector.getGeneralization(); - if (generalizationState.NeedsIds) - { - format.showTermId = true; - } if (generalizationState.TrueLoop) {