Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../../img/srcFileCovDistChart7.png 74% of files have more coverage
382   936   96   20.11
144   755   0.25   19
19     5.05  
1    
 
  ProofChecker1Impl       Line # 56 382 96 70.1% 0.7009174
 
  (9)
 
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.checker;
17   
18    import java.util.HashMap;
19    import java.util.Map;
20   
21    import org.qedeq.base.io.Version;
22    import org.qedeq.base.utility.Enumerator;
23    import org.qedeq.base.utility.EqualsUtility;
24    import org.qedeq.base.utility.StringUtility;
25    import org.qedeq.kernel.bo.logic.common.FormulaUtility;
26    import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
27    import org.qedeq.kernel.bo.logic.common.Operators;
28    import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
29    import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
30    import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
31    import org.qedeq.kernel.se.base.list.Element;
32    import org.qedeq.kernel.se.base.list.ElementList;
33    import org.qedeq.kernel.se.base.module.Add;
34    import org.qedeq.kernel.se.base.module.Existential;
35    import org.qedeq.kernel.se.base.module.FormalProofLine;
36    import org.qedeq.kernel.se.base.module.FormalProofLineList;
37    import org.qedeq.kernel.se.base.module.ModusPonens;
38    import org.qedeq.kernel.se.base.module.Reason;
39    import org.qedeq.kernel.se.base.module.Rename;
40    import org.qedeq.kernel.se.base.module.Rule;
41    import org.qedeq.kernel.se.base.module.SubstFree;
42    import org.qedeq.kernel.se.base.module.SubstFunc;
43    import org.qedeq.kernel.se.base.module.SubstPred;
44    import org.qedeq.kernel.se.base.module.Universal;
45    import org.qedeq.kernel.se.common.ModuleContext;
46    import org.qedeq.kernel.se.common.RuleKey;
47    import org.qedeq.kernel.se.dto.list.DefaultElementList;
48    import org.qedeq.kernel.se.dto.list.ElementSet;
49   
50   
51    /**
52    * Formal proof checker for basic rules.
53    *
54    * @author Michael Meyling
55    */
 
56    public class ProofChecker1Impl implements ProofChecker {
57   
58    /** Proof we want to check. */
59    private FormalProofLineList proof;
60   
61    /** Module context of proof line list. */
62    private ModuleContext moduleContext;
63   
64    /** Current context. */
65    private ModuleContext currentContext;
66   
67    /** Resolver for external references. */
68    private ReferenceResolver resolver;
69   
70    /** All exceptions that occurred during checking. */
71    private LogicalCheckExceptionList exceptions;
72   
73    /** Array with proof status for each proof line. */
74    private boolean[] lineProved;
75   
76    /** Maps local proof line labels to local line number Integers. */
77    private Map label2line;
78   
79    /** Rule version we can check. */
80    private final Version ruleVersion;
81   
82    /** Rule existence checker. */
83    private RuleChecker checker;
84   
85    /**
86    * Constructor.
87    *
88    */
 
89  42 toggle public ProofChecker1Impl() {
90  42 this.ruleVersion = new Version("0.01.00");
91    }
92   
 
93  0 toggle public LogicalCheckExceptionList checkRule(final Rule rule,
94    final ModuleContext context, final RuleChecker checker,
95    final ReferenceResolver resolver) {
96  0 exceptions = new LogicalCheckExceptionList();
97  0 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
98  0 if (rule.getVersion() == null || !ruleVersion.equals(rule.getVersion())) {
99  0 final ProofCheckException ex = new ProofCheckException(
100    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
101    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey
102    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + "{" + ruleVersion + "}",
103    context);
104  0 exceptions.add(ex);
105    }
106  0 return exceptions;
107    }
108   
 
109  43 toggle public LogicalCheckExceptionList checkProof(final Element formula,
110    final FormalProofLineList proof,
111    final RuleChecker checker,
112    final ModuleContext moduleContext,
113    final ReferenceResolver resolver) {
114  43 this.proof = proof;
115  43 this.resolver = resolver;
116  43 this.moduleContext = moduleContext;
117  43 this.checker = checker;
118    // use copy constructor for changing context
119  43 currentContext = new ModuleContext(moduleContext);
120  43 exceptions = new LogicalCheckExceptionList();
121  43 final String context = moduleContext.getLocationWithinModule();
122  43 lineProved = new boolean[proof.size()];
123  43 label2line = new HashMap();
124  450 for (int i = 0; i < proof.size(); i++) {
125  407 boolean ok = true;
126  407 setLocationWithinModule(context + ".get(" + i + ")");
127  407 final FormalProofLine line = proof.get(i);
128  407 if (line == null || line.getFormula() == null
129    || line.getFormula().getElement() == null) {
130  0 ok = false;
131  0 handleProofCheckException(
132    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
133    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
134    getCurrentContext());
135  0 continue;
136    }
137  407 setLocationWithinModule(context + ".get(" + i + ").getReason()");
138  407 final Reason reason = line.getReason();
139  407 if (reason == null) {
140  0 ok = false;
141  0 handleProofCheckException(
142    BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
143    BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
144    getCurrentContext());
145  0 continue;
146    }
147  407 if (line.getLabel() != null && line.getLabel().length() > 0) {
148  406 final Integer n = (Integer) label2line.get(line.getLabel());
149  406 if (n != null) {
150  8 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
151    moduleContext.getLocationWithinModule() + ".get("
152    + label2line.get(line.getLabel())
153    + ").getLabel()");
154  8 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
155  8 handleProofCheckException(
156    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
157    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
158    + line.getLabel(),
159    getCurrentContext(),
160    lc);
161    }
162  406 label2line.put(line.getLabel(), new Integer(i));
163    }
164    // check if only basis rules are used
165    // TODO 20110316 m31: this is a dirty trick to get the context of the reason
166    // perhaps we can solve this more elegantly?
167  407 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
168  407 if (getReason.endsWith("Vo")) {
169  407 getReason = getReason.substring(0, getReason.length() - 2) + "()";
170  407 setLocationWithinModule(context + ".get(" + i + ").getReason()"
171    + getReason);
172    }
173  407 if (reason instanceof Add) {
174  94 ok = check((Add) reason, i, line.getFormula().getElement());
175  313 } else if (reason instanceof Rename) {
176  47 ok = check((Rename) reason, i, line.getFormula().getElement());
177  266 } else if (reason instanceof ModusPonens) {
178  58 ok = check((ModusPonens) reason, i, line.getFormula().getElement());
179  208 } else if (reason instanceof SubstFree) {
180  29 ok = check((SubstFree) reason, i, line.getFormula().getElement());
181  179 } else if (reason instanceof SubstPred) {
182  143 ok = check((SubstPred) reason, i, line.getFormula().getElement());
183  36 } else if (reason instanceof SubstFunc) {
184  7 ok = check((SubstFunc) reason, i, line.getFormula().getElement());
185  29 } else if (reason instanceof Universal) {
186  24 ok = check((Universal) reason, i, line.getFormula().getElement());
187  5 } else if (reason instanceof Existential) {
188  5 ok = check((Existential) reason, i, line.getFormula().getElement());
189    } else {
190  0 ok = false;
191  0 handleProofCheckException(
192    BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
193    BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
194    + reason.getName(),
195    getCurrentContext());
196    }
197  407 lineProved[i] = ok;
198    // check if last proof line is identical with proposition formula
199  407 if (i == proof.size() - 1) {
200  43 if (!formula.equals(line.getFormula().getElement())) {
201  3 handleProofCheckException(
202    BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
203    BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT
204    + reason.getName(),
205    getModuleContextOfProofLineFormula(i));
206    }
207    }
208    }
209  43 return exceptions;
210    }
211   
 
212  94 toggle private boolean check(final Add add, final int i, final Element element) {
213  94 final String context = currentContext.getLocationWithinModule();
214  94 boolean ok = true;
215  94 if (add.getReference() == null) {
216  1 ok = false;
217  1 setLocationWithinModule(context + ".getReference()");
218  1 handleProofCheckException(
219    BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
220    BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
221    getCurrentContext());
222  1 return ok;
223    }
224  93 if (!resolver.isProvedFormula(add.getReference())) {
225  4 ok = false;
226  4 setLocationWithinModule(context + ".getReference()");
227  4 handleProofCheckException(
228    BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
229    BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
230    + add.getReference(),
231    getCurrentContext());
232  4 return ok;
233    }
234  89 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
235  89 final Element current = resolver.getNormalizedFormula(element);
236  89 if (!EqualsUtility.equals(expected, current)) {
237  0 ok = false;
238  0 handleProofCheckException(
239    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
240    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
241    + add.getReference(),
242    getDiffModuleContextOfProofLineFormula(i, expected));
243  0 return ok;
244    }
245  89 final RuleKey defined = checker.getRule(add.getName());
246  89 if (defined == null) {
247  0 ok = false;
248  0 handleProofCheckException(
249    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
250    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
251    + add.getName(),
252    getCurrentContext());
253  0 return ok;
254  89 } else if (!ruleVersion.equals(defined.getVersion())) {
255  0 ok = false;
256  0 handleProofCheckException(
257    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
258    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
259    getCurrentContext());
260  0 return ok;
261    }
262  89 return ok;
263    }
264   
 
265  47 toggle private boolean check(final Rename rename, final int i, final Element element) {
266  47 final String context = currentContext.getLocationWithinModule();
267  47 boolean ok = true;
268  47 final Integer n = (Integer) label2line.get(rename.getReference());
269  47 if (n == null) {
270  3 ok = false;
271  3 setLocationWithinModule(context + ".getReference()");
272  3 handleProofCheckException(
273    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
274    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
275    + rename.getReference(),
276    getCurrentContext());
277    // } else if (!lineProved[n.intValue()]) {
278    // ok = false;
279    // setLocationWithinModule(context + ".getReference()");
280    // handleProofCheckException(
281    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
282    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
283    // + rename.getReference(),
284    // getCurrentContext());
285    } else {
286  44 final Element f = getNormalizedProofLine(n);
287  44 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
288    rename.getOriginalSubjectVariable(),
289    rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
290    new Enumerator());
291  44 final Element current = resolver.getNormalizedFormula(element);
292  44 if (!EqualsUtility.equals(expected, current)) {
293  7 ok = false;
294  7 handleProofCheckException(
295    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
296    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
297    + rename.getReference(),
298    getDiffModuleContextOfProofLineFormula(i, expected));
299    } else {
300  37 ok = true;
301    }
302    }
303  47 final RuleKey defined = checker.getRule(rename.getName());
304  47 if (defined == null) {
305  0 ok = false;
306  0 handleProofCheckException(
307    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
308    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
309    + rename.getName(),
310    getCurrentContext());
311  0 return ok;
312  47 } else if (!ruleVersion.equals(defined.getVersion())) {
313  0 ok = false;
314  0 handleProofCheckException(
315    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
316    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
317    getCurrentContext());
318  0 return ok;
319    }
320  47 return ok;
321    }
322   
 
323  29 toggle private boolean check(final SubstFree substFree, final int i, final Element element) {
324  29 final String context = currentContext.getLocationWithinModule();
325  29 boolean ok = true;
326  29 final Integer n = (Integer) label2line.get(substFree.getReference());
327  29 if (n == null) {
328  1 ok = false;
329  1 setLocationWithinModule(context + ".getReference()");
330  1 handleProofCheckException(
331    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
332    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
333    + substFree.getReference(),
334    getCurrentContext());
335    // } else if (!lineProved[n.intValue()]) {
336    // ok = false;
337    // setLocationWithinModule(context + ".getReference()");
338    // handleProofCheckException(
339    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
340    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
341    // + substfree.getReference(),
342    // getCurrentContext());
343    } else {
344  28 final Element f = getNormalizedProofLine(n);
345  28 final Element current = resolver.getNormalizedFormula(element);
346  28 final Element expected = f.replace(substFree.getSubjectVariable(),
347    resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
348  28 if (!EqualsUtility.equals(current, expected)) {
349  5 ok = false;
350  5 handleProofCheckException(
351    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
352    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
353    + substFree.getReference(),
354    getDiffModuleContextOfProofLineFormula(i, expected));
355  5 return ok;
356    }
357    }
358  24 final RuleKey defined = checker.getRule(substFree.getName());
359  24 if (defined == null) {
360  0 ok = false;
361  0 handleProofCheckException(
362    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
363    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
364    + substFree.getName(),
365    getCurrentContext());
366  0 return ok;
367  24 } else if (!ruleVersion.equals(defined.getVersion())) {
368  0 ok = false;
369  0 handleProofCheckException(
370    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
371    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
372    getCurrentContext());
373  0 return ok;
374    }
375  24 return ok;
376    }
377   
 
378  143 toggle private boolean check(final SubstPred substPred, final int i, final Element element) {
379  143 final String context = currentContext.getLocationWithinModule();
380  143 boolean ok = true;
381  143 final Integer n = (Integer) label2line.get(substPred.getReference());
382  143 if (n == null) {
383  10 ok = false;
384  10 setLocationWithinModule(context + ".getReference()");
385  10 handleProofCheckException(
386    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
387    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
388    + substPred.getReference(),
389    getCurrentContext());
390    // } else if (!lineProved[n.intValue()]) {
391    // ok = false;
392    // setLocationWithinModule(context + ".getReference()");
393    // handleProofCheckException(
394    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
395    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
396    // + substpred.getReference(),
397    // getCurrentContext());
398    } else {
399  133 final Element alpha = getNormalizedProofLine(n);
400  133 final Element current = resolver.getNormalizedFormula(element);
401  133 if (substPred.getSubstituteFormula() == null) {
402  4 ok = false;
403  4 handleProofCheckException(
404    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
405    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
406    getCurrentContext());
407  4 return ok;
408    }
409  129 final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
410  129 final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
411  129 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
412  129 if (!EqualsUtility.equals(current, expected)) {
413  4 ok = false;
414  4 handleProofCheckException(
415    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
416    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
417    + substPred.getReference(),
418    getDiffModuleContextOfProofLineFormula(i, expected));
419  4 return ok;
420    }
421    // check precondition: predicate variable p must have n pairwise different free subject
422    // variables as arguments
423  125 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
424  125 if (predFree.size() != p.getList().size() - 1) {
425  0 ok = false;
426  0 setLocationWithinModule(context + ".getPredicateVariable()");
427  0 handleProofCheckException(
428    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
429    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
430    getDiffModuleContextOfProofLineFormula(i, expected));
431  0 return ok;
432    }
433  145 for (int j = 1; j < p.getList().size(); j++) {
434  20 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
435  0 ok = false;
436  0 setLocationWithinModule(context + ".getPredicateVariable()");
437  0 handleProofCheckException(
438    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
439    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
440    getCurrentContext());
441  0 return ok;
442    }
443    }
444    // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
445    // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
446  125 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
447  125 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
448  125 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
449  0 ok = false;
450  0 setLocationWithinModule(context + ".getSubstituteFormula()");
451  0 handleProofCheckException(
452    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
453    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
454    getCurrentContext());
455  0 return ok;
456    }
457    // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
458    // no bound variable of $\beta(x_1, \ldots, x_n)$
459  125 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
460  125 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
461  0 ok = false;
462  0 setLocationWithinModule(context + ".getSubstituteFormula()");
463  0 handleProofCheckException(
464    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
465    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
466    getCurrentContext());
467  0 return ok;
468    }
469    // check precondition: resulting formula is well formed was already done by well formed
470    // checker
471    }
472  135 final RuleKey defined = checker.getRule(substPred.getName());
473  135 if (defined == null) {
474  0 ok = false;
475  0 handleProofCheckException(
476    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
477    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
478    + substPred.getName(),
479    getCurrentContext());
480  0 return ok;
481  135 } else if (!ruleVersion.equals(defined.getVersion())) {
482  0 ok = false;
483  0 handleProofCheckException(
484    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
485    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
486    getCurrentContext());
487  0 return ok;
488    }
489  135 return ok;
490    }
491   
 
492  7 toggle private boolean check(final SubstFunc substFunc, final int i, final Element element) {
493  7 final String context = currentContext.getLocationWithinModule();
494  7 boolean ok = true;
495  7 final Integer n = (Integer) label2line.get(substFunc.getReference());
496  7 if (n == null) {
497  1 ok = false;
498  1 setLocationWithinModule(context + ".getReference()");
499  1 handleProofCheckException(
500    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
501    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
502    + substFunc.getReference(),
503    getCurrentContext());
504    // } else if (!lineProved[n.intValue()]) {
505    // ok = false;
506    // setLocationWithinModule(context + ".getReference()");
507    // handleProofCheckException(
508    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
509    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
510    // + substfunc.getReference(),
511    // getCurrentContext());
512    } else {
513  6 final Element alpha = getNormalizedProofLine(n);
514  6 final Element current = resolver.getNormalizedFormula(element);
515  6 if (substFunc.getSubstituteTerm() == null) {
516  0 ok = false;
517  0 handleProofCheckException(
518    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
519    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
520    getCurrentContext());
521  0 return ok;
522    }
523  6 final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
524  6 final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
525  6 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
526  6 if (!EqualsUtility.equals(current, expected)) {
527  1 ok = false;
528  1 handleProofCheckException(
529    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
530    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
531    + substFunc.getReference(),
532    getDiffModuleContextOfProofLineFormula(i, expected));
533  1 return ok;
534    }
535    // check precondition: function variable $\sigma$ must have n pairwise different free
536    // subject variables as arguments
537  5 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
538  5 if (funcFree.size() != sigma.getList().size() - 1) {
539  0 ok = false;
540  0 setLocationWithinModule(context + ".getPredicateVariable()");
541  0 handleProofCheckException(
542    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
543    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
544    getDiffModuleContextOfProofLineFormula(i, expected));
545  0 return ok;
546    }
547  10 for (int j = 1; j < sigma.getList().size(); j++) {
548  5 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
549  0 ok = false;
550  0 setLocationWithinModule(context + ".getPredicateVariable()");
551  0 handleProofCheckException(
552    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
553    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
554    getCurrentContext());
555  0 return ok;
556    }
557    }
558    // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
559    // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
560  5 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
561  5 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
562  5 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
563  0 ok = false;
564  0 setLocationWithinModule(context + ".getSubstituteFormula()");
565  0 handleProofCheckException(
566    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
567    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
568    getCurrentContext());
569  0 return ok;
570    }
571    // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
572    // contains no bound variable of $\tau(x_1, \ldots, x_n)$
573  5 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
574  5 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
575  0 ok = false;
576  0 setLocationWithinModule(context + ".getSubstituteFormula()");
577  0 handleProofCheckException(
578    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
579    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
580    getCurrentContext());
581  0 return ok;
582    }
583    // check precondition: resulting formula is well formed was already done by well formed
584    // checker
585    }
586  6 final RuleKey defined = checker.getRule(substFunc.getName());
587  6 if (defined == null) {
588  0 ok = false;
589  0 handleProofCheckException(
590    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
591    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
592    + substFunc.getName(),
593    getCurrentContext());
594  0 return ok;
595  6 } else if (!ruleVersion.equals(defined.getVersion())) {
596  0 ok = false;
597  0 handleProofCheckException(
598    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
599    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
600    getCurrentContext());
601  0 return ok;
602    }
603  6 return ok;
604    }
605   
 
606  58 toggle private boolean check(final ModusPonens mp, final int i, final Element element) {
607  58 final String context = currentContext.getLocationWithinModule();
608  58 boolean ok = true;
609  58 final Integer n1 = (Integer) label2line.get(mp.getReference1());
610  58 if (n1 == null) {
611  6 ok = false;
612  6 setLocationWithinModule(context + ".getReference1()");
613  6 handleProofCheckException(
614    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
615    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
616    + mp.getReference1(),
617    getCurrentContext());
618    // } else if (!lineProved[n1.intValue()]) {
619    // ok = false;
620    // setLocationWithinModule(context + ".getReference1()");
621    // handleProofCheckException(
622    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
623    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
624    // + mp.getReference1(),
625    // getCurrentContext());
626    }
627  58 final Integer n2 = (Integer) label2line.get(mp.getReference2());
628  58 if (n2 == null) {
629  4 ok = false;
630  4 setLocationWithinModule(context + ".getReference2()");
631  4 handleProofCheckException(
632    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
633    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
634    + mp.getReference2(),
635    getCurrentContext());
636    // } else if (!lineProved[n2.intValue()]) {
637    // ok = false;
638    // setLocationWithinModule(context + ".getReference2()");
639    // handleProofCheckException(
640    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
641    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
642    // + mp.getReference1(),
643    // getCurrentContext());
644    }
645  58 if (ok) {
646  52 final Element f1 = getNormalizedProofLine(n1);
647  52 final Element f2 = getNormalizedProofLine(n2);
648  52 final Element current = getNormalizedProofLine(i);
649  52 if (!FormulaUtility.isImplication(f1)) {
650  0 ok = false;
651  0 setLocationWithinModule(context + ".getReference1()");
652  0 handleProofCheckException(
653    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
654    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
655    + mp.getReference1(),
656    getCurrentContext());
657  52 } else if (!f2.equals(f1.getList().getElement(0))) {
658  1 ok = false;
659  1 setLocationWithinModule(context + ".getReference2()");
660  1 handleProofCheckException(
661    BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
662    BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
663    + mp.getReference2(),
664    getCurrentContext(),
665    getModuleContextOfProofLineFormula(n1.intValue()));
666  51 } else if (!current.equals(f1.getList().getElement(1))) {
667  0 ok = false;
668  0 setLocationWithinModule(context + ".getReference1()");
669  0 handleProofCheckException(
670    BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
671    BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
672    + mp.getReference1(),
673    getCurrentContext(),
674    getModuleContextOfProofLineFormula(n1.intValue()));
675    } else {
676  51 ok = true;
677    }
678    }
679  58 final RuleKey defined = checker.getRule(mp.getName());
680  58 if (defined == null) {
681  0 ok = false;
682  0 handleProofCheckException(
683    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
684    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
685    + mp.getName(),
686    getCurrentContext());
687  0 return ok;
688  58 } else if (!ruleVersion.equals(defined.getVersion())) {
689  0 ok = false;
690  0 handleProofCheckException(
691    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
692    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
693    getCurrentContext());
694  0 return ok;
695    }
696  58 return ok;
697    }
698   
 
699  24 toggle private boolean check(final Universal universal, final int i, final Element element) {
700  24 final String context = currentContext.getLocationWithinModule();
701  24 boolean ok = true;
702  24 final Integer n = (Integer) label2line.get(universal.getReference());
703  24 if (n == null) {
704  1 ok = false;
705  1 setLocationWithinModule(context + ".getReference()");
706  1 handleProofCheckException(
707    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
708    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
709    + universal.getReference(),
710    getCurrentContext());
711    // } else if (!lineProved[n.intValue()]) {
712    // ok = false;
713    // setLocationWithinModule(context + ".getReference()");
714    // handleProofCheckException(
715    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
716    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
717    // + universal.getReference(),
718    // getCurrentContext());
719    } else {
720  23 final Element f = getNormalizedProofLine(n);
721  23 final Element current = resolver.getNormalizedFormula(element);
722  23 if (!FormulaUtility.isImplication(f)) {
723  0 ok = false;
724  0 setLocationWithinModule(context + ".getReference()");
725  0 handleProofCheckException(
726    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
727    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
728    + universal.getReference(),
729    getCurrentContext());
730  0 return ok;
731    }
732  23 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
733  3 ok = false;
734  3 setLocationWithinModule(context + ".getSubjectVariable()");
735  3 handleProofCheckException(
736    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
737    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
738    getCurrentContext());
739  3 return ok;
740    }
741  20 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
742  20 expected.add((f.getList().getElement(0)));
743  20 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
744  20 uni.add(universal.getSubjectVariable());
745  20 uni.add(f.getList().getElement(1));
746  20 expected.add(uni);
747  20 if (!EqualsUtility.equals(current, expected)) {
748  1 ok = false;
749  1 handleProofCheckException(
750    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
751    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
752    + universal.getReference(),
753    getDiffModuleContextOfProofLineFormula(i, expected));
754  1 return ok;
755    }
756    }
757  20 final RuleKey defined = checker.getRule(universal.getName());
758  20 if (defined == null) {
759  0 ok = false;
760  0 handleProofCheckException(
761    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
762    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
763    + universal.getName(),
764    getCurrentContext());
765  0 return ok;
766  20 } else if (!ruleVersion.equals(defined.getVersion())) {
767  0 ok = false;
768  0 handleProofCheckException(
769    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
770    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
771    getCurrentContext());
772  0 return ok;
773    }
774  20 return ok;
775    }
776   
 
777  5 toggle private boolean check(final Existential existential, final int i, final Element element) {
778  5 final String context = currentContext.getLocationWithinModule();
779  5 boolean ok = true;
780  5 final Integer n = (Integer) label2line.get(existential.getReference());
781  5 if (n == null) {
782  0 ok = false;
783  0 setLocationWithinModule(context + ".getReference()");
784  0 handleProofCheckException(
785    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
786    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
787    + existential.getReference(),
788    getCurrentContext());
789    // } else if (!lineProved[n.intValue()]) {
790    // ok = false;
791    // setLocationWithinModule(context + ".getReference()");
792    // handleProofCheckException(
793    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
794    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
795    // + existential.getReference(),
796    // getCurrentContext());
797    } else {
798  5 final Element f = getNormalizedProofLine(n);
799  5 final Element current = resolver.getNormalizedFormula(element);
800  5 if (!FormulaUtility.isImplication(f)) {
801  0 ok = false;
802  0 setLocationWithinModule(context + ".getReference()");
803  0 handleProofCheckException(
804    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
805    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
806    + existential.getReference(),
807    getCurrentContext());
808  0 return ok;
809    }
810  5 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
811  1 ok = false;
812  1 setLocationWithinModule(context + ".getSubjectVariable()");
813  1 handleProofCheckException(
814    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
815    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
816    getCurrentContext());
817  1 return ok;
818    }
819  4 final DefaultElementList expected = new DefaultElementList(f.getList().getOperator());
820  4 final ElementList exi = new DefaultElementList(
821    Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
822  4 exi.add(existential.getSubjectVariable());
823  4 exi.add(f.getList().getElement(0));
824  4 expected.add(exi);
825  4 expected.add((f.getList().getElement(1)));
826  4 if (!EqualsUtility.equals(current, expected)) {
827  0 ok = false;
828  0 handleProofCheckException(
829    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
830    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
831    + existential.getReference(),
832    getDiffModuleContextOfProofLineFormula(i, expected));
833  0 return ok;
834    }
835    }
836  4 final RuleKey defined = checker.getRule(existential.getName());
837  4 if (defined == null) {
838  0 ok = false;
839  0 handleProofCheckException(
840    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
841    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
842    + existential.getName(),
843    getCurrentContext());
844  0 return ok;
845  4 } else if (!ruleVersion.equals(defined.getVersion())) {
846  0 ok = false;
847  0 handleProofCheckException(
848    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
849    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
850    getCurrentContext());
851  0 return ok;
852    }
853  4 return ok;
854    }
855   
 
856  4 toggle private ModuleContext getModuleContextOfProofLineFormula(final int i) {
857  4 return new ModuleContext(moduleContext.getModuleLocation(),
858    moduleContext.getLocationWithinModule() + ".get(" + i
859    + ").getFormula().getElement()");
860    }
861   
 
862  18 toggle private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
863    final Element expected) {
864  18 final String diff = FormulaUtility.getDifferenceLocation(
865    proof.get(i).getFormula().getElement(), expected);
866  18 return new ModuleContext(moduleContext.getModuleLocation(),
867    moduleContext.getLocationWithinModule() + ".get(" + i
868    + ").getFormula().getElement()" + diff);
869    }
870   
 
871  343 toggle private Element getNormalizedProofLine(final Integer n) {
872  343 if (n == null) {
873  0 return null;
874    }
875  343 return getNormalizedProofLine(n.intValue());
876    }
877   
 
878  395 toggle private Element getNormalizedProofLine(final int i) {
879  395 if (i < 0 || i >= proof.size()) {
880  0 return null;
881    }
882  395 return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
883    }
884   
885    /**
886    * Add new {@link ProofCheckException} to exception list.
887    *
888    * @param code Error code.
889    * @param msg Error message.
890    * @param context Error context.
891    */
 
892  60 toggle private void handleProofCheckException(final int code, final String msg,
893    final ModuleContext context) {
894    // System.out.println(context);
895    // System.setProperty("qedeq.test.xmlLocationFailures", "true");
896  60 final ProofCheckException ex = new ProofCheckException(code, msg, context);
897  60 exceptions.add(ex);
898    }
899   
900    /**
901    * Add new {@link ProofCheckException} to exception list.
902    *
903    * @param code Error code.
904    * @param msg Error message.
905    * @param context Error context.
906    * @param referenceContext Reference context.
907    */
 
908  9 toggle private void handleProofCheckException(final int code, final String msg,
909    final ModuleContext context, final ModuleContext referenceContext) {
910    // System.out.println(context);
911    // System.setProperty("qedeq.test.xmlLocationFailures", "true");
912  9 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
913    referenceContext);
914  9 exceptions.add(ex);
915    }
916   
917    /**
918    * Set location information where are we within the original module.
919    *
920    * @param locationWithinModule Location within module.
921    */
 
922  144 toggle protected void setLocationWithinModule(final String locationWithinModule) {
923  144 getCurrentContext().setLocationWithinModule(locationWithinModule);
924    }
925   
926    /**
927    * Get current context within original.
928    *
929    * @return Current context.
930    */
 
931  3555 toggle protected final ModuleContext getCurrentContext() {
932  3555 return currentContext;
933    }
934   
935   
936    }
 
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 .