Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../../img/srcFileCovDistChart8.png 62% of files have more coverage
206   578   74   7.63
92   386   0.36   9
27     2.74  
3    
 
  ProofFinderImpl       Line # 51 191 65 71.5% 0.7147651
  ProofFinderImpl.SubstituteBase       Line # 487 15 9 85.2% 0.8518519
  ProofFinderImpl.Substitute       Line # 544 0 0 - -1.0
 
  (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.Iterator;
20    import java.util.List;
21    import java.util.SortedSet;
22    import java.util.TreeSet;
23   
24    import org.qedeq.base.io.Parameters;
25    import org.qedeq.base.utility.StringUtility;
26    import org.qedeq.kernel.bo.common.Element2Utf8;
27    import org.qedeq.kernel.bo.log.ModuleLogListener;
28    import org.qedeq.kernel.bo.logic.common.FormulaUtility;
29    import org.qedeq.kernel.bo.logic.common.Operators;
30    import org.qedeq.kernel.bo.logic.proof.common.ProofException;
31    import org.qedeq.kernel.bo.logic.proof.common.ProofFinder;
32    import org.qedeq.kernel.bo.logic.proof.common.ProofFoundException;
33    import org.qedeq.kernel.bo.logic.proof.common.ProofNotFoundException;
34    import org.qedeq.kernel.se.base.list.Element;
35    import org.qedeq.kernel.se.base.list.ElementList;
36    import org.qedeq.kernel.se.base.module.Add;
37    import org.qedeq.kernel.se.base.module.FormalProofLineList;
38    import org.qedeq.kernel.se.base.module.ModusPonens;
39    import org.qedeq.kernel.se.base.module.Reason;
40    import org.qedeq.kernel.se.common.ModuleContext;
41    import org.qedeq.kernel.se.dto.list.DefaultElementList;
42    import org.qedeq.kernel.se.dto.list.ElementSet;
43    import org.qedeq.kernel.se.visitor.InterruptException;
44   
45   
46    /**
47    * Find basic proofs for formulas.
48    *
49    * @author Michael Meyling
50    */
 
51    public class ProofFinderImpl implements ProofFinder {
52   
53    /** List of proof lines. */
54    private List lines;
55   
56    /** List of reasons. */
57    private List reasons;
58   
59    /** Set of all predicate variables that occur in this proof anywhere. */
60    private ElementSet allPredVars;
61   
62    /** Set of all substitution formulas we try. */
63    private ElementSet partGoalFormulas;
64   
65    /** Below this number MP was tried. */
66    private int mpLast;
67   
68    /** Goal to prove. */
69    private Element goalFormula;
70   
71    /** Number of extra propositional variables. */
72    private int extraVars;
73   
74    /** Skip this number list of formulas. */
75    private String skipFormulas;
76   
77    /** Log proof line after this number of new proof lines. */
78    private int logFrequence;
79   
80    /** Ordered substitution methods that implement {@link Substitute}. */
81    private SortedSet substitutionMethods;
82   
83    /** Maximum number of proof lines. */
84    private int maxProofLines;
85   
86    /** Here are we. */
87    private ModuleContext context;
88   
89    /** Log progress herein. */
90    private ModuleLogListener log;
91   
92    /** Transformer to get UTF-8 out of formulas. */
93    private Element2Utf8 trans;
94   
95    /**
96    * Constructor.
97    */
 
98  9 toggle public ProofFinderImpl() {
99    // nothing to do
100    }
101   
 
102  9 toggle public void findProof(final Element formula,
103    final FormalProofLineList proof, final ModuleContext context,
104    final Parameters parameters, final ModuleLogListener log, final Element2Utf8 trans)
105    throws ProofException, InterruptException {
106  9 this.goalFormula = formula;
107  9 this.context = new ModuleContext(context); // use copy constructor to fix it
108  9 this.log = log;
109  9 this.trans = trans;
110  9 substitutionMethods = new TreeSet();
111  9 extraVars = parameters.getInt("extraVars");
112  9 maxProofLines = parameters.getInt("maximumProofLines");
113  9 skipFormulas = parameters.getString("skipFormulas").trim();
114  9 if (skipFormulas.length() > 0) {
115  0 log.logMessageState("skipping the following formula numbers: " + skipFormulas);
116  0 skipFormulas = "," + StringUtility.replace(skipFormulas, " ", "") + ",";
117    }
118    // TODO 20110606 m31: check that we have the correct format (e.g. only "," as separator)
119  9 System.out.println("maximumProofLines = " + maxProofLines);
120  9 int weight = 0;
121  9 weight = parameters.getInt("propositionVariableWeight");
122  9 if (weight > 0) {
123  9 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("propositionVariableOrder")) {
 
124  3676 toggle public void substitute(final int i) throws ProofException {
125  3676 substituteByPropositionVariables(i);
126    }
127    });
128    }
129  9 weight = parameters.getInt("partFormulaWeight");
130  9 if (weight > 0) {
131  2 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("partFormulaOrder")) {
 
132  344 toggle public void substitute(final int i) throws ProofException {
133  344 substitutePartGoalFormulas(i);
134    }
135    });
136    }
137  9 weight = parameters.getInt("disjunctionWeight");
138  9 if (weight > 0) {
139  9 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("disjunctionOrder")) {
 
140  3680 toggle public void substitute(final int i) throws ProofException {
141  3680 substituteDisjunction(i);
142    }
143    });
144    }
145  9 weight = parameters.getInt("implicationWeight");
146  9 if (weight > 0) {
147  0 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("implicationOrder")) {
 
148  0 toggle public void substitute(final int i) throws ProofException {
149  0 substituteImplication(i);
150    }
151    });
152    }
153  9 weight = parameters.getInt("negationWeight");
154  9 if (weight > 0) {
155  0 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("negationOrder")) {
 
156  0 toggle public void substitute(final int i) throws ProofException {
157  0 substituteNegation(i);
158    }
159    });
160    }
161  9 weight = parameters.getInt("conjunctionWeight");
162  9 if (weight > 0) {
163  0 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("conjunctionOrder")) {
 
164  0 toggle public void substitute(final int i) throws ProofException {
165  0 substituteConjunction(i);
166    }
167    });
168    }
169  9 weight = parameters.getInt("equivalenceWeight");
170  9 if (weight > 0) {
171  0 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("equivalenceOrder")) {
 
172  0 toggle public void substitute(final int i) throws ProofException {
173  0 substituteEquivalence(i);
174    }
175    });
176    }
177  9 logFrequence = parameters.getInt("logFrequence");
178   
179  9 lines = new ArrayList();
180  9 reasons = new ArrayList();
181  9 setAllPredVars(proof);
182  9 partGoalFormulas = FormulaUtility.getPartFormulas(goalFormula);
183  9 log.logMessageState("our goal: " + trans.getUtf8(formula));
184  9 int size2 = 0;
185  9 while (true) {
186    // check if the thread should be interrupted
187  1229 if (Thread.interrupted()) {
188  0 throw new InterruptException(this.context);
189    }
190  1229 int size1 = lines.size();
191  1229 tryModusPonensAll();
192  1227 final Iterator iter = substitutionMethods.iterator();
193  4017 while (iter.hasNext()) {
194  2797 final Substitute method = (Substitute) iter.next();
195    // System.out.println(method.getClass());
196  10490 for (int j = 0; j < method.getWeight(); j++) {
197  7700 if (method.nextLine() >= lines.size()) {
198  0 break;
199    }
200  7700 method.substitute();
201  7699 tryModusPonensAll();
202    }
203    }
204    // System.out.println(lines.size());
205  1220 if (size2 == lines.size()) {
206    // we didn't generate new lines, so we just quit
207  0 log.logMessageState(FinderErrors.PROOF_NOT_FOUND_TEXT + size2);
208  0 throw new ProofNotFoundException(FinderErrors.PROOF_NOT_FOUND_CODE,
209    FinderErrors.PROOF_NOT_FOUND_TEXT + size2, context);
210    }
211  1220 size2 = size1;
212    }
213    }
214   
 
215  9 toggle private void setAllPredVars(final FormalProofLineList proof) {
216  9 log.logMessageState("using the following formulas:");
217  9 allPredVars = new ElementSet();
218    // add all "add" proof formulas to our proof line list
219  48 for (int i = 0; i < proof.size(); i++) {
220    // should we skip this formula
221  39 if (skipFormulas.indexOf("," + (i + 1) + ",") >= 0) {
222  0 continue;
223    }
224  39 final Reason reason = proof.get(i).getReason();
225  39 if (!(reason instanceof Add)) {
226  2 continue;
227    }
228  37 final Element formula = proof.get(i).getFormula().getElement();
229  37 lines.add(formula);
230  37 reasons.add(reason);
231  37 log.logMessageState(ProofFinderUtility.getUtf8Line(formula, reason, i, trans));
232  37 allPredVars.union(FormulaUtility.getPropositionVariables(
233    formula));
234    }
235  9 String max = "A";
236  9 final Iterator iter = allPredVars.iterator();
237  36 while (iter.hasNext()) {
238  27 final ElementList v = (ElementList) iter.next();
239  27 final String name = v.getElement(0).getAtom().getString();
240  27 if (-1 == max.compareTo(name)) {
241  18 max = name;
242    }
243    }
244  9 System.out.println("Adding extra variables:");
245  9 for (int i = 1; i <= extraVars; i++) {
246  0 max = (char) (max.charAt(0) + i) + "";
247  0 System.out.println("\t" + max);
248    // add extra predicate variable
249  0 allPredVars.add(FormulaUtility.createPredicateVariable(max));
250    }
251    }
252   
253    /**
254    * Try all Modus Ponens with all new lines. Remember tested maximum.
255    *
256    * @throws ProofException Proof found, or limits exceeded.
257    */
 
258  8928 toggle private void tryModusPonensAll() throws ProofException {
259  8928 int until = lines.size();
260  25560839 for (int i = 0; i < until; i++) {
261  25551919 final Element first = (Element) lines.get(i);
262  25551919 if (!FormulaUtility.isImplication(first)) {
263  11317 continue;
264    }
265  289873976 for (int j = (i < mpLast ? mpLast : 0); j < until; j++) {
266  264333382 if (first.getList().getElement(0).equals(
267    lines.get(j))) {
268  809 final ModusPonens mp = new ModusPonensBo(i, j);
269  809 addFormula(first.getList().getElement(1), mp);
270    }
271    }
272    }
273  8920 mpLast = until;
274    }
275   
276    /**
277    * Make all possible substitutions by propositional variables in a proof line.
278    *
279    * @param i Proof line number we want to try substitution.
280    * @throws ProofException We found a proof or have to end the search!
281    */
 
282  3676 toggle private void substituteByPropositionVariables(final int i) throws ProofException {
283  3676 final Element f = (Element) lines.get(i);
284  3676 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
285  3676 final Iterator iter = vars.iterator();
286  12865 while (iter.hasNext()) {
287  9189 final ElementList var = (ElementList) iter.next();
288  9189 final Iterator all = allPredVars.iterator();
289  36756 while (all.hasNext()) {
290  27567 final ElementList subst = (ElementList) all.next();
291  27567 if (var.equals(subst)) {
292  9189 continue;
293    }
294  18378 final Element created = FormulaUtility.replaceOperatorVariable(
295    f, var, subst);
296  18378 addFormula(created, new SubstPredBo(i, var, subst));
297    }
298    }
299    }
300   
301    /**
302    * Make all substitutions by part goal formulas in a proof line.
303    *
304    * @param i Proof line number we want to try substitution.
305    * @throws ProofException We found a proof or have to end the search!
306    */
 
307  344 toggle private void substitutePartGoalFormulas(final int i) throws ProofException {
308  344 final Element f = (Element) lines.get(i);
309  344 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
310  344 final Iterator iter = vars.iterator();
311  1147 while (iter.hasNext()) {
312  803 final ElementList var = (ElementList) iter.next();
313    {
314  803 final Iterator all = partGoalFormulas.iterator();
315  3305 while (all.hasNext()) {
316  2502 final ElementList subst = (ElementList) all.next();
317  2502 if (var.equals(subst)) {
318  471 continue;
319    }
320  2031 final Element created = FormulaUtility.replaceOperatorVariable(
321    f, var, subst);
322  2031 addFormula(created, new SubstPredBo(i, var, subst));
323    }
324    }
325    }
326    }
327   
328    /**
329    * Make all substitutions by negation in a proof line.
330    *
331    * @param i Proof line number we want to try substitution.
332    * @throws ProofException We found a proof or have to end the search!
333    */
 
334  0 toggle private void substituteNegation(final int i) throws ProofException {
335  0 final Element f = (Element) lines.get(i);
336  0 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
337  0 final Iterator iter = vars.iterator();
338  0 while (iter.hasNext()) {
339  0 final ElementList var = (ElementList) iter.next();
340  0 final Iterator all = allPredVars.iterator();
341  0 while (all.hasNext()) {
342  0 final ElementList var2 = (ElementList) all.next();
343  0 final ElementList subst = new DefaultElementList(Operators.NEGATION_OPERATOR);
344  0 subst.add(var2);
345  0 final Element created = FormulaUtility.replaceOperatorVariable(
346    f, var, subst);
347  0 addFormula(created, new SubstPredBo(i, var, subst));
348    }
349    }
350    }
351   
352    /**
353    * Make all substitutions by conjunction in a proof line.
354    *
355    * @param i Proof line number we want to try substitution.
356    * @throws ProofException We found a proof or have to end the search!
357    */
 
358  0 toggle private void substituteConjunction(final int i) throws ProofException {
359  0 final Element f = (Element) lines.get(i);
360  0 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
361  0 final Iterator iter = vars.iterator();
362  0 while (iter.hasNext()) {
363  0 final ElementList var = (ElementList) iter.next();
364  0 createReplacement(i, f, var, Operators.CONJUNCTION_OPERATOR, true);
365  0 createReplacement(i, f, var, Operators.CONJUNCTION_OPERATOR, false);
366    }
367    }
368   
369    /**
370    * Make all substitutions by disjunction in a proof line.
371    *
372    * @param i Proof line number we want to try substitution.
373    * @throws ProofException We found a proof or have to end the search!
374    */
 
375  3680 toggle private void substituteDisjunction(final int i) throws ProofException {
376  3680 final Element f = (Element) lines.get(i);
377  3680 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
378  3680 final Iterator iter = vars.iterator();
379  12875 while (iter.hasNext()) {
380  9196 final ElementList var = (ElementList) iter.next();
381  9196 createReplacement(i, f, var, Operators.DISJUNCTION_OPERATOR, true);
382  9195 createReplacement(i, f, var, Operators.DISJUNCTION_OPERATOR, false);
383    }
384    }
385   
386    /**
387    * Make all substitutions by implication in a proof line.
388    *
389    * @param i Proof line number we want to try substitution.
390    * @throws ProofException We found a proof or have to end the search!
391    */
 
392  0 toggle private void substituteImplication(final int i) throws ProofException {
393  0 final Element f = (Element) lines.get(i);
394  0 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
395  0 final Iterator iter = vars.iterator();
396  0 while (iter.hasNext()) {
397  0 final ElementList var = (ElementList) iter.next();
398  0 createReplacement(i, f, var, Operators.IMPLICATION_OPERATOR, true);
399  0 createReplacement(i, f, var, Operators.IMPLICATION_OPERATOR, false);
400    }
401    }
402   
403    /**
404    * Make all substitutions by equivalence in a proof line.
405    *
406    * @param i Proof line number we want to try substitution.
407    * @throws ProofException We found a proof or have to end the search!
408    */
 
409  0 toggle private void substituteEquivalence(final int i) throws ProofException {
410  0 final Element f = (Element) lines.get(i);
411  0 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
412  0 final Iterator iter = vars.iterator();
413  0 while (iter.hasNext()) {
414  0 final ElementList var = (ElementList) iter.next();
415  0 createReplacement(i, f, var, Operators.EQUIVALENCE_OPERATOR, true);
416  0 createReplacement(i, f, var, Operators.EQUIVALENCE_OPERATOR, false);
417    }
418    }
419   
420    /**
421    * Substitute predicate variable <code>var</code> by binary operator with old variable
422    * and new variable and add this as a new proof line.
423    *
424    * @param i Proof line number we work on.
425    * @param f Proof line formula.
426    * @param var Predicate variable we want to replace.
427    * @param operator Operator of replacement formula.
428    * @param left Is old variable at left hand of new operator?
429    * @throws ProofException We found a proof or have to end the search!
430    */
 
431  18391 toggle private void createReplacement(final int i, final Element f,
432    final ElementList var, final String operator, final boolean left) throws ProofException {
433  18391 final Iterator a = allPredVars.iterator();
434  73562 while (a.hasNext()) {
435  55172 final ElementList var2 = (ElementList) a.next();
436  55172 final ElementList subst = new DefaultElementList(operator);
437  55172 if (left) {
438  27587 subst.add(var);
439  27587 subst.add(var2);
440    } else {
441  27585 subst.add(var2);
442  27585 subst.add(var);
443    }
444  55172 final Element created = FormulaUtility.replaceOperatorVariable(
445    f, var, subst);
446  55172 addFormula(created, new SubstPredBo(i, var, subst));
447    }
448    }
449   
 
450  76390 toggle private void addFormula(final Element formula, final Reason reason) throws ProofException {
451  76390 if (!lines.contains(formula)) {
452  45074 lines.add(formula);
453  45074 reasons.add(reason);
454    // printLine(lines.size() - 1);
455  45074 if (goalFormula.equals(formula)) {
456  8 final int size = lines.size();
457  8 log.logMessageState(FinderErrors.PROOF_FOUND_TEXT + size);
458  8 throw new ProofFoundException(FinderErrors.PROOF_FOUND_CODE,
459    FinderErrors.PROOF_FOUND_TEXT + size,
460    ProofFinderUtility.shortenProof(lines, reasons, log, trans), context);
461    }
462    // did we reach our maximum?
463  45066 if (lines.size() >= maxProofLines) {
464  1 final int size = lines.size();
465  1 if (logFrequence > 0) {
466  0 log.logMessageState(ProofFinderUtility.getUtf8Line(lines, reasons, lines.size() - 1,
467    trans));
468    }
469  1 log.logMessageState(FinderErrors.PROOF_NOT_FOUND_TEXT + size);
470  1 throw new ProofNotFoundException(FinderErrors.PROOF_NOT_FOUND_CODE,
471    FinderErrors.PROOF_NOT_FOUND_TEXT + size, context);
472    }
473  45065 if (logFrequence > 0 && (lines.size() - 1) % logFrequence == 0) {
474  33 log.logMessageState(ProofFinderUtility.getUtf8Line(lines, reasons, lines.size() - 1,
475    trans));
476    }
477    }
478    }
479   
 
480  0 toggle public String getExecutionActionDescription() {
481  0 return ProofFinderUtility.getUtf8Line(lines, reasons, lines.size() - 1, trans);
482    }
483   
484    /**
485    * These is the basis implementation for substitution methods.
486    */
 
487    private abstract class SubstituteBase implements Substitute {
488   
489    /** Next proof line we will work on. */
490    private int next = 0;
491   
492    /** Weight of proof method. */
493    private final int weight;
494   
495    /** Order of proof method. */
496    private final int order;
497   
 
498  20 toggle SubstituteBase(final int weight, final int order) {
499  20 this.weight = weight;
500  20 this.order = order;
501    }
502   
 
503  10490 toggle public int getWeight() {
504  10490 return weight;
505    }
506   
 
507  24 toggle public int getOrder() {
508  24 return order;
509    }
 
510  7700 toggle public int nextLine() {
511  7700 return next;
512    }
513   
 
514  13 toggle public int compareTo(final Object obj) {
515  13 if (obj instanceof Substitute) {
516  13 Substitute sub = (Substitute) obj;
517    // we don't return 0 because the TreeSet gets no more elements
518    // if we have methods with same order value
519  13 if (order == sub.getOrder()) {
520  2 return -1;
521    }
522  11 if (order < sub.getOrder()) {
523  11 return -1;
524    }
525  0 return 1;
526    }
527  0 return -1;
528    }
529   
 
530  7700 toggle public void substitute() throws ProofException {
531  7700 substitute(next);
532  7699 next++;
533    }
534   
535    public abstract void substitute(int i) throws ProofException;
536   
537    }
538   
539   
540    /**
541    * Work on proof line and substitute proposition variables.
542    *
543    */
 
544    interface Substitute extends Comparable {
545   
546    /**
547    * Return next proof line number we will work on.
548    *
549    * @return Next proof line number we will worked on.
550    */
551    public int nextLine();
552   
553    /**
554    * Substitute next proof line number.
555    *
556    * @throws ProofException We found a proof or have to end the search!
557    */
558    public void substitute() throws ProofException;
559   
560    /**
561    * Get weight of substitution rule. This is the number of runs for this
562    * substitution.
563    *
564    * @return Weight.
565    */
566    public int getWeight();
567   
568    /**
569    * Get order position of substitution rule. This says about the sequence position of this
570    * substitution method.
571    *
572    * @return Order position.
573    */
574    public int getOrder();
575   
576    }
577   
578    }
 
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 .