001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.proof.finder;
017
018 import java.util.ArrayList;
019 import java.util.List;
020
021 import org.qedeq.kernel.bo.common.Element2Utf8;
022 import org.qedeq.kernel.bo.log.ModuleLogListener;
023 import org.qedeq.kernel.se.base.list.Element;
024 import org.qedeq.kernel.se.base.module.Add;
025 import org.qedeq.kernel.se.base.module.FormalProofLineList;
026 import org.qedeq.kernel.se.base.module.Reason;
027 import org.qedeq.kernel.se.base.module.SubstPred;
028 import org.qedeq.kernel.se.dto.module.AddVo;
029 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
030 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
031 import org.qedeq.kernel.se.dto.module.FormulaVo;
032 import org.qedeq.kernel.se.dto.module.ModusPonensVo;
033 import org.qedeq.kernel.se.dto.module.SubstPredVo;
034
035
036 /**
037 * Utilities for proofs finders.
038 *
039 * @author Michael Meyling
040 */
041 public final class ProofFinderUtility {
042
043 /** Maps new proof line numbers to old ones. */
044 private List new2Old;
045
046 /**
047 * Constructor.
048 *
049 */
050 private ProofFinderUtility() {
051 }
052
053 /**
054 * Shorten given formal proof.
055 *
056 * @param lines Lines of formulas.
057 * @param reasons Reasons for derivation of formula. Must be Add, MP or SubstPred.
058 * @param log For BO logging.
059 * @param trans Transformer (used for logging).
060 * @return Reduced formal proof.
061 */
062 public static FormalProofLineList shortenProof(final List lines, final List reasons,
063 final ModuleLogListener log, final Element2Utf8 trans) {
064 return (new ProofFinderUtility()).shorten(lines, reasons, log, trans);
065 }
066
067 private FormalProofLineList shorten(final List lines, final List reasons,
068 final ModuleLogListener log, final Element2Utf8 trans) {
069 final boolean[] used = new boolean[lines.size()];
070 int n = lines.size() - 1;
071 used[n] = true;
072 while (n >= 0) {
073 if (used[n]) {
074 Reason r = (Reason) reasons.get(n);
075 if (r instanceof ModusPonensBo) {
076 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
077 used[mp.getN1()] = true;
078 used[mp.getN2()] = true;
079 } else if (r instanceof SubstPredBo) {
080 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
081 used[substPred.getN()] = true;
082 } else if (r instanceof Add) {
083 // ignore
084 } else {
085 throw new IllegalStateException("unexpected reason class: " + r.getClass());
086 }
087 }
088 n--;
089 }
090 for (int j = 0; j < lines.size(); j++) {
091 if (used[j]) {
092 log.logMessageState(getUtf8Line(lines, reasons, j, trans));
093 }
094 }
095 new2Old = new ArrayList();
096 for (int j = 0; j < lines.size(); j++) {
097 if (used[j]) {
098 new2Old.add(new Integer(j));
099 }
100 }
101 final FormalProofLineListVo result = new FormalProofLineListVo();
102 for (int j = 0; j < new2Old.size(); j++) {
103 n = ((Integer) new2Old.get(j)).intValue();
104 final Reason r = (Reason) reasons.get(n);
105 final Reason newReason;
106 if (r instanceof ModusPonensBo) {
107 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
108 newReason = new ModusPonensVo("" + (1 + old2new(mp.getN1())),
109 "" + (1 + old2new(mp.getN2())));
110 } else if (r instanceof SubstPredBo) {
111 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
112 newReason = new SubstPredVo("" + (1 + old2new(substPred.getN())),
113 substPred.getPredicateVariable(), substPred.getSubstituteFormula());
114 } else if (r instanceof Add) {
115 final Add add = (Add) reasons.get(n);
116 newReason = new AddVo(add.getReference());
117 } else {
118 throw new IllegalStateException("unexpected reason class: " + r.getClass());
119 }
120 result.add(new FormalProofLineVo("" + (1 + j),
121 new FormulaVo((Element) lines.get(new2old(j))),
122 newReason));
123 }
124 for (int j = 0; j < result.size(); j++) {
125 log.logMessageState(result.get(j).getLabel() + ": "
126 + trans.getUtf8(result.get(j).getFormula().getElement())
127 + " " + result.get(j).getReason());
128 }
129 return result;
130 }
131
132 private int old2new(final int old) {
133 int result = new2Old.indexOf(new Integer(old));
134 if (result < 0) {
135 throw new IllegalArgumentException("not found: " + old);
136 }
137 return result;
138 }
139
140 private int new2old(final int n) {
141 final int result = ((Integer) new2Old.get(n)).intValue();
142 return result;
143 }
144
145 /**
146 * Get UTF-8 representation of proof line.
147 *
148 * @param lines Proof line formulas.
149 * @param reasons Proof line reasons.
150 * @param i Proof line to print.
151 * @param trans Transformer to get UTF-8 out of a formula.
152 * @return UTF-8 display text for proof line.
153 */
154 public static String getUtf8Line(final List lines, final List reasons, final int i,
155 final Element2Utf8 trans) {
156 final StringBuffer result = new StringBuffer();
157 result.append((i + 1) + ": ");
158 Reason reason = (Reason) reasons.get(i);
159 Element formula = (Element) lines.get(i);
160 return getUtf8Line(formula, reason, i, trans);
161 }
162
163 /**
164 * Get UTF-8 representation of proof line.
165 *
166 * @param formula Proof line formula.
167 * @param reason Proof line reason.
168 * @param i Proof line number.
169 * @param trans Transformer to get UTF-8 out of a formula.
170 * @return UTF-8 display text for proof line.
171 */
172 public static String getUtf8Line(final Element formula, final Reason reason, final int i,
173 final Element2Utf8 trans) {
174 final StringBuffer result = new StringBuffer();
175 result.append((i + 1) + ": ");
176 result.append(trans.getUtf8(formula));
177 result.append(" : ");
178 if (reason instanceof SubstPred) {
179 SubstPred s = (SubstPred) reason;
180 result.append("Subst " + s.getReference() + " ");
181 result.append(trans.getUtf8(s.getPredicateVariable()));
182 result.append(" by ");
183 result.append(trans.getUtf8(s.getSubstituteFormula()));
184 } else {
185 result.append(reason);
186 }
187 return result.toString();
188 }
189
190 }
|