Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
68   194   24   9.71
34   127   0.35   7
7     3.43  
1    
 
  ProofFinderUtility       Line # 41 68 24 92.7% 0.9266055
 
  (6)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.logic.proof.finder;
17   
18    import java.util.ArrayList;
19    import java.util.List;
20   
21    import org.qedeq.kernel.bo.common.Element2Utf8;
22    import org.qedeq.kernel.bo.log.ModuleLogListener;
23    import org.qedeq.kernel.se.base.list.Element;
24    import org.qedeq.kernel.se.base.module.Add;
25    import org.qedeq.kernel.se.base.module.FormalProofLineList;
26    import org.qedeq.kernel.se.base.module.Reason;
27    import org.qedeq.kernel.se.base.module.SubstPred;
28    import org.qedeq.kernel.se.dto.module.AddVo;
29    import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
30    import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
31    import org.qedeq.kernel.se.dto.module.FormulaVo;
32    import org.qedeq.kernel.se.dto.module.ModusPonensVo;
33    import org.qedeq.kernel.se.dto.module.SubstPredVo;
34   
35   
36    /**
37    * Utilities for proofs finders.
38    *
39    * @author Michael Meyling
40    */
 
41    public final class ProofFinderUtility {
42   
43    /** Maps new proof line numbers to old ones. */
44    private List new2Old;
45   
46    /**
47    * Constructor.
48    *
49    */
 
50  8 toggle private ProofFinderUtility() {
51    // nothing to do
52    }
53   
54    /**
55    * Shorten given formal proof.
56    *
57    * @param lines Lines of formulas.
58    * @param reasons Reasons for derivation of formula. Must be Add, MP or SubstPred.
59    * @param log For BO logging.
60    * @param trans Transformer (used for logging).
61    * @return Reduced formal proof.
62    */
 
63  8 toggle public static FormalProofLineList shortenProof(final List lines, final List reasons,
64    final ModuleLogListener log, final Element2Utf8 trans) {
65  8 return (new ProofFinderUtility()).shorten(lines, reasons, log, trans);
66    }
67   
 
68  8 toggle private FormalProofLineList shorten(final List lines, final List reasons,
69    final ModuleLogListener log, final Element2Utf8 trans) {
70  8 final boolean[] used = new boolean[lines.size()];
71  8 int n = lines.size() - 1;
72  8 used[n] = true;
73  45109 while (n >= 0) {
74  45101 if (used[n]) {
75  68 Reason r = (Reason) reasons.get(n);
76  68 if (r instanceof ModusPonensBo) {
77  16 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
78  16 used[mp.getN1()] = true;
79  16 used[mp.getN2()] = true;
80  52 } else if (r instanceof SubstPredBo) {
81  28 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
82  28 used[substPred.getN()] = true;
83  24 } else if (r instanceof Add) {
84    // ignore
85    } else {
86  0 throw new IllegalStateException("unexpected reason class: " + r.getClass());
87    }
88    }
89  45101 n--;
90    }
91  45109 for (int j = 0; j < lines.size(); j++) {
92  45101 if (used[j]) {
93  68 log.logMessageState(getUtf8Line(lines, reasons, j, trans));
94    }
95    }
96  8 new2Old = new ArrayList();
97  45109 for (int j = 0; j < lines.size(); j++) {
98  45101 if (used[j]) {
99  68 new2Old.add(new Integer(j));
100    }
101    }
102  8 final FormalProofLineListVo result = new FormalProofLineListVo();
103  76 for (int j = 0; j < new2Old.size(); j++) {
104  68 n = ((Integer) new2Old.get(j)).intValue();
105  68 final Reason r = (Reason) reasons.get(n);
106  68 final Reason newReason;
107  68 if (r instanceof ModusPonensBo) {
108  16 final ModusPonensBo mp = (ModusPonensBo) reasons.get(n);
109  16 newReason = new ModusPonensVo("" + (1 + old2new(mp.getN1())),
110    "" + (1 + old2new(mp.getN2())));
111  52 } else if (r instanceof SubstPredBo) {
112  28 final SubstPredBo substPred = (SubstPredBo) reasons.get(n);
113  28 newReason = new SubstPredVo("" + (1 + old2new(substPred.getN())),
114    substPred.getPredicateVariable(), substPred.getSubstituteFormula());
115  24 } else if (r instanceof Add) {
116  24 final Add add = (Add) reasons.get(n);
117  24 newReason = new AddVo(add.getReference());
118    } else {
119  0 throw new IllegalStateException("unexpected reason class: " + r.getClass());
120    }
121  68 result.add(new FormalProofLineVo("" + (1 + j),
122    new FormulaVo((Element) lines.get(new2old(j))),
123    newReason));
124    }
125  76 for (int j = 0; j < result.size(); j++) {
126  68 log.logMessageState(result.get(j).getLabel() + ": "
127    + trans.getUtf8(result.get(j).getFormula().getElement())
128    + " " + result.get(j).getReason());
129    }
130  8 return result;
131    }
132   
 
133  60 toggle private int old2new(final int old) {
134  60 int result = new2Old.indexOf(new Integer(old));
135  60 if (result < 0) {
136  0 throw new IllegalArgumentException("not found: " + old);
137    }
138  60 return result;
139    }
140   
 
141  68 toggle private int new2old(final int n) {
142  68 final int result = ((Integer) new2Old.get(n)).intValue();
143  68 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  101 toggle public static String getUtf8Line(final List lines, final List reasons, final int i,
156    final Element2Utf8 trans) {
157  101 if (i < 0) {
158  0 return "beginning to prove";
159    }
160  101 final StringBuffer result = new StringBuffer();
161  101 result.append((i + 1) + ": ");
162  101 Reason reason = (Reason) reasons.get(i);
163  101 Element formula = (Element) lines.get(i);
164  101 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  138 toggle public static String getUtf8Line(final Element formula, final Reason reason, final int i,
177    final Element2Utf8 trans) {
178  138 final StringBuffer result = new StringBuffer();
179  138 result.append((i + 1) + ": ");
180  138 result.append(trans.getUtf8(formula));
181  138 result.append(" : ");
182  138 if (reason instanceof SubstPred) {
183  61 SubstPred s = (SubstPred) reason;
184  61 result.append("Subst " + s.getReference() + " ");
185  61 result.append(trans.getUtf8(s.getPredicateVariable()));
186  61 result.append(" by ");
187  61 result.append(trans.getUtf8(s.getSubstituteFormula()));
188    } else {
189  77 result.append(reason);
190    }
191  138 return result.toString();
192    }
193   
194    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .