001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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.module.ModuleLabels;
022 import org.qedeq.kernel.bo.service.Element2LatexImpl;
023 import org.qedeq.kernel.bo.service.Element2Utf8Impl;
024 import org.qedeq.kernel.se.base.list.Element;
025 import org.qedeq.kernel.se.base.module.Add;
026 import org.qedeq.kernel.se.base.module.FormalProofLineList;
027 import org.qedeq.kernel.se.base.module.Reason;
028 import org.qedeq.kernel.se.base.module.SubstPred;
029 import org.qedeq.kernel.se.dto.module.AddVo;
030 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
031 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
032 import org.qedeq.kernel.se.dto.module.FormulaVo;
033 import org.qedeq.kernel.se.dto.module.ModusPonensVo;
034 import org.qedeq.kernel.se.dto.module.ReasonTypeVo;
035 import org.qedeq.kernel.se.dto.module.SubstPredVo;
036
037
038 /**
039 * Utilities for proofs finders.
040 *
041 * @author Michael Meyling
042 */
043 public final class ProofFinderUtility {
044
045 /** Maps new proof line numbers to old ones. */
046 private List new2Old;
047
048 /**
049 * Constructor.
050 *
051 */
052 private ProofFinderUtility() {
053 }
054
055 public static FormalProofLineList shortenProof(final List lines, final List reasons) {
056 return (new ProofFinderUtility()).shorten(lines, reasons);
057 }
058
059 private FormalProofLineList shorten(final List lines, final List reasons) {
060 final boolean[] used = new boolean[lines.size()];
061 int n = lines.size() - 1;
062 used[n] = true;
063 while (n >= 0) {
064 if (used[n]) {
065 Reason r = (Reason) reasons.get(n);
066 if (r instanceof ModusPonensBo) {
067 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
068 used[mp.getN1()] = true;
069 used[mp.getN2()] = true;
070 } else if (r instanceof SubstPredBo) {
071 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
072 used[substPred.getN()] = true;
073 } else if (r instanceof Add) {
074 // ignore
075 } else {
076 throw new IllegalStateException("unexpected reason class: " + r.getClass());
077 }
078 }
079 n--;
080 }
081 for (int j = 0; j < lines.size(); j++) {
082 if (used[j]) {
083 printUtf8Line(lines, reasons, j);
084 }
085 }
086 new2Old = new ArrayList();
087 for (int j = 0; j < lines.size(); j++) {
088 if (used[j]) {
089 new2Old.add(new Integer(j));
090 }
091 }
092 final FormalProofLineListVo result = new FormalProofLineListVo();
093 for (int j = 0; j < new2Old.size(); j++) {
094 n = ((Integer) new2Old.get(j)).intValue();
095 final Reason r = (Reason) reasons.get(n);
096 final Reason newReason;
097 if (r instanceof ModusPonensBo) {
098 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
099 newReason = new ModusPonensVo("" + (1 + old2new(mp.getN1())),
100 "" + (1 + old2new(mp.getN2())));
101 } else if (r instanceof SubstPredBo) {
102 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
103 newReason = new SubstPredVo("" + (1 + old2new(substPred.getN())),
104 substPred.getPredicateVariable(), substPred.getSubstituteFormula());
105 } else if (r instanceof Add) {
106 final Add add = (Add) reasons.get(n);
107 newReason = new AddVo(add.getReference());
108 } else {
109 throw new IllegalStateException("unexpected reason class: " + r.getClass());
110 }
111 result.add(new FormalProofLineVo("" + (1 + j),
112 new FormulaVo((Element) lines.get(new2old(j))),
113 new ReasonTypeVo(newReason)));
114 }
115 for (int j = 0; j < result.size(); j++) {
116 System.out.print(result.get(j).getLabel() + ": ");
117 print(result.get(j).getFormula().getElement());
118 System.out.println(" " + result.get(j).getReasonType());
119 }
120 return result;
121 }
122
123 private int old2new(final int old) {
124 int result = new2Old.indexOf(new Integer(old));
125 if (result < 0) {
126 throw new IllegalArgumentException("not found: " + old);
127 }
128 return result;
129 }
130
131 private int new2old(final int n) {
132 final int result = ((Integer) new2Old.get(n)).intValue();
133 return result;
134 }
135
136 /**
137 * Println UTF-8 representation of formula to <code>System.out</code>.
138 *
139 * @param element For this element.
140 */
141 public static void println(final Element element) {
142 System.out.println(getUtf8(element));
143 }
144
145 /**
146 * Print UTF-8 representation of formula to <code>System.out</code>.
147 *
148 * @param element For this element.
149 */
150 public static void print(final Element element) {
151 System.out.print(getUtf8(element));
152 }
153
154 /**
155 * Get UTF-8 representation for formula.
156 *
157 * @param element For this element.
158 * @return Get the UTF-8 display text.
159 */
160 public static String getUtf8(final Element element) {
161 ModuleLabels labels = new ModuleLabels();
162 Element2LatexImpl converter = new Element2LatexImpl(labels);
163 Element2Utf8Impl textConverter = new Element2Utf8Impl(converter);
164 return textConverter.getUtf8(element);
165 }
166
167 /**
168 * Get UTF-8 representation of proof line.
169 *
170 * @param lines Proof line formulas.
171 * @param reasons Proof line reasons.
172 * @param i Proof line to print.
173 * @return UTF-8 display text for proof line.
174 */
175 public static String getUtf8Line(final List lines, final List reasons, final int i) {
176 final StringBuffer result = new StringBuffer();
177 result.append(i + ": ");
178 Reason reason = (Reason) reasons.get(i);
179 Element formula = (Element) lines.get(i);
180 result.append(ProofFinderUtility.getUtf8(formula));
181 result.append(" : ");
182 if (reason instanceof SubstPred) {
183 SubstPred s = (SubstPred) reason;
184 result.append("Subst " + s.getReference() + " ");
185 result.append(ProofFinderUtility.getUtf8(s.getPredicateVariable()));
186 result.append(" by ");
187 result.append(ProofFinderUtility.getUtf8(s.getSubstituteFormula()));
188 } else {
189 result.append(reason);
190 }
191 return result.toString();
192 }
193
194 /**
195 * Print UTF-8 representation of proof line to <code>System.out</code>.
196 *
197 * @param lines Proof line formulas.
198 * @param reasons Proof line reasons.
199 * @param i Proof line to print.
200 */
201 public static void printUtf8Line(final List lines, final List reasons, final int i) {
202 System.out.println(getUtf8Line(lines, reasons, i));
203 }
204
205 }
|