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 // nothing to do
052 }
053
054 /**
055 * Shorten given formal proof.
056 *
057 * @param lines Lines of formulas.
058 * @param reasons Reasons for derivation of formula. Must be Add, MP or SubstPred.
059 * @param log For BO logging.
060 * @param trans Transformer (used for logging).
061 * @return Reduced formal proof.
062 */
063 public static FormalProofLineList shortenProof(final List lines, final List reasons,
064 final ModuleLogListener log, final Element2Utf8 trans) {
065 return (new ProofFinderUtility()).shorten(lines, reasons, log, trans);
066 }
067
068 private FormalProofLineList shorten(final List lines, final List reasons,
069 final ModuleLogListener log, final Element2Utf8 trans) {
070 final boolean[] used = new boolean[lines.size()];
071 int n = lines.size() - 1;
072 used[n] = true;
073 while (n >= 0) {
074 if (used[n]) {
075 Reason r = (Reason) reasons.get(n);
076 if (r instanceof ModusPonensBo) {
077 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
078 used[mp.getN1()] = true;
079 used[mp.getN2()] = true;
080 } else if (r instanceof SubstPredBo) {
081 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
082 used[substPred.getN()] = true;
083 } else if (r instanceof Add) {
084 // ignore
085 } else {
086 throw new IllegalStateException("unexpected reason class: " + r.getClass());
087 }
088 }
089 n--;
090 }
091 for (int j = 0; j < lines.size(); j++) {
092 if (used[j]) {
093 log.logMessageState(getUtf8Line(lines, reasons, j, trans));
094 }
095 }
096 new2Old = new ArrayList();
097 for (int j = 0; j < lines.size(); j++) {
098 if (used[j]) {
099 new2Old.add(new Integer(j));
100 }
101 }
102 final FormalProofLineListVo result = new FormalProofLineListVo();
103 for (int j = 0; j < new2Old.size(); j++) {
104 n = ((Integer) new2Old.get(j)).intValue();
105 final Reason r = (Reason) reasons.get(n);
106 final Reason newReason;
107 if (r instanceof ModusPonensBo) {
108 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
109 newReason = new ModusPonensVo("" + (1 + old2new(mp.getN1())),
110 "" + (1 + old2new(mp.getN2())));
111 } else if (r instanceof SubstPredBo) {
112 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
113 newReason = new SubstPredVo("" + (1 + old2new(substPred.getN())),
114 substPred.getPredicateVariable(), substPred.getSubstituteFormula());
115 } else if (r instanceof Add) {
116 final Add add = (Add) reasons.get(n);
117 newReason = new AddVo(add.getReference());
118 } else {
119 throw new IllegalStateException("unexpected reason class: " + r.getClass());
120 }
121 result.add(new FormalProofLineVo("" + (1 + j),
122 new FormulaVo((Element) lines.get(new2old(j))),
123 newReason));
124 }
125 for (int j = 0; j < result.size(); j++) {
126 log.logMessageState(result.get(j).getLabel() + ": "
127 + trans.getUtf8(result.get(j).getFormula().getElement())
128 + " " + result.get(j).getReason());
129 }
130 return result;
131 }
132
133 private int old2new(final int old) {
134 int result = new2Old.indexOf(new Integer(old));
135 if (result < 0) {
136 throw new IllegalArgumentException("not found: " + old);
137 }
138 return result;
139 }
140
141 private int new2old(final int n) {
142 final int result = ((Integer) new2Old.get(n)).intValue();
143 return result;
144 }
145
146 /**
147 * Get UTF-8 representation of proof line.
148 *
149 * @param lines Proof line formulas.
150 * @param reasons Proof line reasons.
151 * @param i Proof line to print.
152 * @param trans Transformer to get UTF-8 out of a formula.
153 * @return UTF-8 display text for proof line.
154 */
155 public static String getUtf8Line(final List lines, final List reasons, final int i,
156 final Element2Utf8 trans) {
157 if (i < 0) {
158 return "beginning to prove";
159 }
160 final StringBuffer result = new StringBuffer();
161 result.append((i + 1) + ": ");
162 Reason reason = (Reason) reasons.get(i);
163 Element formula = (Element) lines.get(i);
164 return getUtf8Line(formula, reason, i, trans);
165 }
166
167 /**
168 * Get UTF-8 representation of proof line.
169 *
170 * @param formula Proof line formula.
171 * @param reason Proof line reason.
172 * @param i Proof line number.
173 * @param trans Transformer to get UTF-8 out of a formula.
174 * @return UTF-8 display text for proof line.
175 */
176 public static String getUtf8Line(final Element formula, final Reason reason, final int i,
177 final Element2Utf8 trans) {
178 final StringBuffer result = new StringBuffer();
179 result.append((i + 1) + ": ");
180 result.append(trans.getUtf8(formula));
181 result.append(" : ");
182 if (reason instanceof SubstPred) {
183 SubstPred s = (SubstPred) reason;
184 result.append("Subst " + s.getReference() + " ");
185 result.append(trans.getUtf8(s.getPredicateVariable()));
186 result.append(" by ");
187 result.append(trans.getUtf8(s.getSubstituteFormula()));
188 } else {
189 result.append(reason);
190 }
191 return result.toString();
192 }
193
194 }
|