Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../../../img/srcFileCovDistChart5.png 87% of files have more coverage
547   1,282   166   16.09
220   1,091   0.3   34
34     4.88  
1    
 
  ProofChecker2Impl       Line # 61 547 166 44.6% 0.4456929
 
  (5)
 
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.io.VersionSet;
23    import org.qedeq.base.utility.Enumerator;
24    import org.qedeq.base.utility.EqualsUtility;
25    import org.qedeq.base.utility.StringUtility;
26    import org.qedeq.kernel.bo.logic.common.FormulaChecker;
27    import org.qedeq.kernel.bo.logic.common.FormulaUtility;
28    import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
29    import org.qedeq.kernel.bo.logic.common.Operators;
30    import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
31    import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
32    import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
33    import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
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.ConditionalProof;
38    import org.qedeq.kernel.se.base.module.Existential;
39    import org.qedeq.kernel.se.base.module.FormalProofLine;
40    import org.qedeq.kernel.se.base.module.FormalProofLineList;
41    import org.qedeq.kernel.se.base.module.ModusPonens;
42    import org.qedeq.kernel.se.base.module.Reason;
43    import org.qedeq.kernel.se.base.module.Rename;
44    import org.qedeq.kernel.se.base.module.Rule;
45    import org.qedeq.kernel.se.base.module.SubstFree;
46    import org.qedeq.kernel.se.base.module.SubstFunc;
47    import org.qedeq.kernel.se.base.module.SubstPred;
48    import org.qedeq.kernel.se.base.module.Universal;
49    import org.qedeq.kernel.se.common.ModuleAddress;
50    import org.qedeq.kernel.se.common.ModuleContext;
51    import org.qedeq.kernel.se.common.RuleKey;
52    import org.qedeq.kernel.se.dto.list.DefaultElementList;
53    import org.qedeq.kernel.se.dto.list.ElementSet;
54   
55   
56    /**
57    * Formal proof checker for basic rules and conditional proof.
58    *
59    * @author Michael Meyling
60    */
 
61    public class ProofChecker2Impl implements ProofChecker, ReferenceResolver {
62   
63    /** Proof we want to check. */
64    private FormalProofLineList proof;
65   
66    /** Module context of proof line list. */
67    private ModuleContext moduleContext;
68   
69    /** Current context. */
70    private ModuleContext currentContext;
71   
72    /** Resolver for external references. */
73    private ReferenceResolver resolver;
74   
75    /** All exceptions that occurred during checking. */
76    private LogicalCheckExceptionList exceptions;
77   
78    /** Array with proof status for each proof line. */
79    private boolean[] lineProved;
80   
81    /** Maps local proof line labels to local line number Integers. */
82    private Map label2line;
83   
84    /** Rule version we support. */
85    private final VersionSet supported;
86   
87    /** These preconditions apply. This is a conjunction with 0 to n elements. */
88    private ElementList conditions;
89   
90    /** Rule existence checker. */
91    private RuleChecker checker;
92   
93    /**
94    * Constructor.
95    */
 
96  87 toggle public ProofChecker2Impl() {
97  87 supported = new VersionSet();
98  87 supported.add("0.01.00");
99  87 supported.add("0.02.00");
100    }
101   
 
102  0 toggle public LogicalCheckExceptionList checkRule(final Rule rule,
103    final ModuleContext context, final RuleChecker checker,
104    final ReferenceResolver resolver) {
105  0 exceptions = new LogicalCheckExceptionList();
106  0 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
107  0 if (rule.getVersion() == null || !supported.contains(rule.getVersion())) {
108  0 final ProofCheckException ex = new ProofCheckException(
109    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
110    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey
111    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
112    context);
113  0 exceptions.add(ex);
114    }
115  0 return exceptions;
116    }
117   
 
118  37 toggle public LogicalCheckExceptionList checkProof(final Element formula,
119    final FormalProofLineList proof,
120    final RuleChecker checker,
121    final ModuleContext moduleContext,
122    final ReferenceResolver resolver) {
123  37 final DefaultElementList con = new DefaultElementList(
124    Operators.CONJUNCTION_OPERATOR);
125    // we have no conditions, so we add an empty condition
126  37 return checkProof(con, formula, proof, checker, moduleContext, resolver);
127    }
128   
 
129  87 toggle private LogicalCheckExceptionList checkProof(final ElementList conditions, final Element formula,
130    final FormalProofLineList proof,
131    final RuleChecker checker,
132    final ModuleContext moduleContext,
133    final ReferenceResolver resolver) {
134  87 this.conditions = conditions;
135  87 this.proof = proof;
136  87 this.checker = checker;
137  87 this.resolver = resolver;
138  87 this.moduleContext = moduleContext;
139    // use copy constructor for changing context
140  87 currentContext = new ModuleContext(moduleContext);
141  87 exceptions = new LogicalCheckExceptionList();
142  87 final String context = moduleContext.getLocationWithinModule();
143  87 lineProved = new boolean[proof.size()];
144  87 label2line = new HashMap();
145  532 for (int i = 0; i < proof.size(); i++) {
146  445 boolean ok = true;
147  445 setLocationWithinModule(context + ".get(" + i + ")");
148  445 final FormalProofLine line = proof.get(i);
149  445 if (line == null || line.getFormula() == null
150    || line.getFormula().getElement() == null) {
151  0 ok = false;
152  0 handleProofCheckException(
153    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
154    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
155    getCurrentContext());
156  0 continue;
157    }
158  445 setLocationWithinModule(context + ".get(" + i + ").getReason()");
159  445 final Reason reason = line.getReason();
160  445 if (reason == null) {
161  0 ok = false;
162  0 handleProofCheckException(
163    BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
164    BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
165    getCurrentContext());
166  0 continue;
167    }
168  445 if (line.getLabel() != null && line.getLabel().length() > 0) {
169  445 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
170  445 addLocalLineLabel(i, line.getLabel());
171    }
172   
173    // check if the formula together with the conditions is well formed
174  445 if (hasConditions()) {
175  126 setLocationWithinModule(context + ".get(" + i + ").getFormula.getElement()");
176  126 ElementList full = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
177  126 if (conditions.size() > 1) {
178  51 full.add(conditions);
179    } else {
180  75 full.add(conditions.getElement(0));
181    }
182  126 full.add(line.getFormula().getElement());
183  126 FormulaChecker checkWf = new FormulaCheckerImpl(); // TODO 20110612 m31: use factory?
184  126 final LogicalCheckExceptionList list = checkWf.checkFormula(full, getCurrentContext());
185  126 if (list.size() > 0) {
186  0 ok = false;
187  0 handleProofCheckException(
188    BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_CODE,
189    BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT
190    + list.get(0).getMessage(),
191    getCurrentContext());
192  0 continue;
193    }
194    }
195   
196    // check if only defined rules are used
197    // TODO 20110316 m31: this is a dirty trick to get the context of the reason
198    // perhaps we can solve this more elegantly?
199  445 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
200  445 if (getReason.endsWith("Vo")) {
201  445 getReason = getReason.substring(0, getReason.length() - 2) + "()";
202  445 setLocationWithinModule(context + ".get(" + i + ").getReason()"
203    + getReason);
204    // System.out.println(getCurrentContext());
205    }
206  445 if (reason instanceof Add) {
207  88 ok = check((Add) reason, i, line.getFormula().getElement());
208  357 } else if (reason instanceof Rename) {
209  5 ok = check((Rename) reason, i, line.getFormula().getElement());
210  352 } else if (reason instanceof ModusPonens) {
211  134 ok = check((ModusPonens) reason, i, line.getFormula().getElement());
212  218 } else if (reason instanceof SubstFree) {
213  4 ok = check((SubstFree) reason, i, line.getFormula().getElement());
214  214 } else if (reason instanceof SubstPred) {
215  160 ok = check((SubstPred) reason, i, line.getFormula().getElement());
216  54 } else if (reason instanceof SubstFunc) {
217  0 ok = check((SubstFunc) reason, i, line.getFormula().getElement());
218  54 } else if (reason instanceof Universal) {
219  4 ok = check((Universal) reason, i, line.getFormula().getElement());
220  50 } else if (reason instanceof Existential) {
221  0 ok = check((Existential) reason, i, line.getFormula().getElement());
222  50 } else if (reason instanceof ConditionalProof) {
223  50 setLocationWithinModule(context + ".get(" + i + ")");
224  50 ok = check((ConditionalProof) reason, i, line.getFormula().getElement());
225    } else {
226  0 ok = false;
227  0 handleProofCheckException(
228    BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
229    BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
230    + reason.getName(),
231    getCurrentContext());
232    }
233  445 lineProved[i] = ok;
234    // check if last proof line is identical with proposition formula
235  445 if (i == proof.size() - 1) {
236  87 if (!formula.equals(line.getFormula().getElement())) {
237  1 handleProofCheckException(
238    BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
239    BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT,
240    getModuleContextOfProofLineFormula(i));
241    }
242    }
243    }
244  87 return exceptions;
245    }
246   
 
247  445 toggle private void addLocalLineLabel(final int i, final String label) {
248  445 if (label != null && label.length() > 0) {
249  445 final Integer n = (Integer) label2line.get(label);
250  445 if (n != null) {
251  0 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
252    moduleContext.getLocationWithinModule() + ".get("
253    + label2line.get(label)
254    + ").getLabel()");
255  0 handleProofCheckException(
256    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
257    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
258    + label,
259    getCurrentContext(),
260    lc);
261    } else {
262  445 if (isLocalProofLineReference(label)) {
263  0 handleProofCheckException(
264    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
265    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
266    + label,
267    getCurrentContext(),
268    resolver.getReferenceContext(label));
269    // System.out.println("we hava label already: " + label);
270    // ProofFinderUtility.println(getNormalizedLocalProofLineReference(label));
271    }
272    }
273    // System.out.println("adding label: " + label);
274  445 label2line.put(label, new Integer(i));
275    }
276    }
277   
 
278  88 toggle private boolean check(final Add add, final int i, final Element element) {
279  88 final String context = currentContext.getLocationWithinModule();
280  88 boolean ok = true;
281  88 if (add.getReference() == null) {
282  0 ok = false;
283  0 setLocationWithinModule(context + ".getReference()");
284  0 handleProofCheckException(
285    BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
286    BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
287    getCurrentContext());
288  0 return ok;
289    }
290  88 if (!resolver.isProvedFormula(add.getReference())) {
291  0 ok = false;
292  0 setLocationWithinModule(context + ".getReference()");
293  0 handleProofCheckException(
294    BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
295    BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
296    + add.getReference(),
297    getCurrentContext());
298  0 return ok;
299    }
300  88 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
301  88 final Element current = resolver.getNormalizedFormula(element);
302  88 if (!EqualsUtility.equals(expected, current)) {
303  0 ok = false;
304  0 handleProofCheckException(
305    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
306    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
307    + add.getReference(),
308    getDiffModuleContextOfProofLineFormula(i, expected));
309  0 return ok;
310    }
311  88 final RuleKey defined = checker.getRule(add.getName());
312  88 if (defined == null) {
313  0 ok = false;
314  0 handleProofCheckException(
315    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
316    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
317    + add.getName(),
318    getCurrentContext());
319  0 return ok;
320  88 } else if (!supported.contains(defined.getVersion())) {
321  0 ok = false;
322  0 handleProofCheckException(
323    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
324    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
325    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
326    getCurrentContext());
327  0 return ok;
328  88 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
329  0 ok = false;
330  0 handleProofCheckException(
331    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
332    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
333    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
334    getCurrentContext());
335  0 return ok;
336    }
337  88 return ok;
338    }
339   
 
340  5 toggle private boolean check(final Rename rename, final int i, final Element element) {
341  5 final String context = currentContext.getLocationWithinModule();
342  5 boolean ok = true;
343  5 final Element f = getNormalizedLocalProofLineReference(rename.getReference());
344  5 if (f == null) {
345  0 ok = false;
346  0 setLocationWithinModule(context + ".getReference()");
347  0 handleProofCheckException(
348    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
349    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
350    + rename.getReference(),
351    getCurrentContext());
352    } else {
353  5 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
354    rename.getOriginalSubjectVariable(),
355    rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
356    new Enumerator());
357  5 final Element current = resolver.getNormalizedFormula(element);
358  5 if (!EqualsUtility.equals(expected, current)) {
359  0 ok = false;
360  0 handleProofCheckException(
361    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
362    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
363    + rename.getReference(),
364    getDiffModuleContextOfProofLineFormula(i, expected));
365    } else {
366  5 ok = true;
367    }
368    }
369  5 final RuleKey defined = checker.getRule(rename.getName());
370  5 if (defined == null) {
371  0 ok = false;
372  0 handleProofCheckException(
373    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
374    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
375    + rename.getName(),
376    getCurrentContext());
377  0 return ok;
378  5 } else if (!supported.contains(defined.getVersion())) {
379  0 ok = false;
380  0 handleProofCheckException(
381    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
382    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
383    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
384    getCurrentContext());
385  0 return ok;
386  5 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
387  0 ok = false;
388  0 handleProofCheckException(
389    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
390    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
391    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
392    getCurrentContext());
393  0 return ok;
394    }
395  5 return ok;
396    }
397   
 
398  4 toggle private boolean check(final SubstFree substFree, final int i, final Element element) {
399  4 final String context = currentContext.getLocationWithinModule();
400  4 boolean ok = true;
401  4 final Element f = getNormalizedLocalProofLineReference(substFree.getReference());
402  4 if (f == null) {
403  0 ok = false;
404  0 setLocationWithinModule(context + ".getReference()");
405  0 handleProofCheckException(
406    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
407    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
408    + substFree.getReference(),
409    getCurrentContext());
410    } else {
411  4 final Element current = resolver.getNormalizedFormula(element);
412  4 final Element expected = f.replace(substFree.getSubjectVariable(),
413    resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
414  4 if (!EqualsUtility.equals(current, expected)) {
415  0 ok = false;
416  0 handleProofCheckException(
417    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
418    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
419    + substFree.getReference(),
420    getDiffModuleContextOfProofLineFormula(i, expected));
421  0 return ok;
422    }
423    }
424    // check precondition: subject variable doesn't occur in a precondition
425  4 if (FormulaUtility.containsOperatorVariable(conditions, substFree.getSubjectVariable())) {
426  0 ok = false;
427  0 setLocationWithinModule(context + ".getSubstituteFormula()");
428  0 handleProofCheckException(
429    BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
430    BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
431    getCurrentContext());
432  0 return ok;
433    }
434  4 final RuleKey defined = checker.getRule(substFree.getName());
435  4 if (defined == null) {
436  0 ok = false;
437  0 handleProofCheckException(
438    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
439    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
440    + substFree.getName(),
441    getCurrentContext());
442  0 return ok;
443  4 } else if (!supported.contains(defined.getVersion())) {
444  0 ok = false;
445  0 handleProofCheckException(
446    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
447    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
448    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
449    getCurrentContext());
450  0 return ok;
451  4 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
452  0 ok = false;
453  0 handleProofCheckException(
454    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
455    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
456    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
457    getCurrentContext());
458  0 return ok;
459    }
460  4 return ok;
461    }
462   
 
463  160 toggle private boolean check(final SubstPred substPred, final int i, final Element element) {
464  160 final String context = currentContext.getLocationWithinModule();
465  160 boolean ok = true;
466  160 final Element alpha = getNormalizedLocalProofLineReference(substPred.getReference());
467  160 if (alpha == null) {
468  0 ok = false;
469  0 setLocationWithinModule(context + ".getReference()");
470  0 handleProofCheckException(
471    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
472    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
473    + substPred.getReference(),
474    getCurrentContext());
475  0 return ok;
476    }
477  160 final Element current = resolver.getNormalizedFormula(element);
478  160 if (substPred.getSubstituteFormula() == null) {
479  0 ok = false;
480  0 handleProofCheckException(
481    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
482    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
483    getCurrentContext());
484  0 return ok;
485    }
486  160 final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
487  160 final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
488  160 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
489  160 if (!EqualsUtility.equals(current, expected)) {
490  0 ok = false;
491  0 handleProofCheckException(
492    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
493    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
494    + substPred.getReference(),
495    getDiffModuleContextOfProofLineFormula(i, expected));
496  0 return ok;
497    }
498    // check precondition: predicate variable p must have n pairwise different free subject
499    // variables as arguments
500  160 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
501  160 if (predFree.size() != p.getList().size() - 1) {
502  0 ok = false;
503  0 setLocationWithinModule(context + ".getPredicateVariable()");
504  0 handleProofCheckException(
505    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
506    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
507    getDiffModuleContextOfProofLineFormula(i, expected));
508  0 return ok;
509    }
510  164 for (int j = 1; j < p.getList().size(); j++) {
511  4 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
512  0 ok = false;
513  0 setLocationWithinModule(context + ".getPredicateVariable()");
514  0 handleProofCheckException(
515    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
516    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
517    getCurrentContext());
518  0 return ok;
519    }
520    }
521    // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
522    // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
523  160 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
524  160 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
525  160 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
526  0 ok = false;
527  0 setLocationWithinModule(context + ".getSubstituteFormula()");
528  0 handleProofCheckException(
529    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
530    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
531    getCurrentContext());
532  0 return ok;
533    }
534    // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
535    // no bound variable of $\beta(x_1, \ldots, x_n)$
536  160 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
537  160 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
538  0 ok = false;
539  0 setLocationWithinModule(context + ".getSubstituteFormula()");
540  0 handleProofCheckException(
541    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
542    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
543    getCurrentContext());
544  0 return ok;
545    }
546    // check precondition: $\sigma(...)$ dosn't occur in a precondition
547  160 if (FormulaUtility.containsOperatorVariable(conditions, p)) {
548  0 ok = false;
549  0 setLocationWithinModule(context + ".getPredicateVariable()");
550  0 handleProofCheckException(
551    BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
552    BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
553    getCurrentContext());
554  0 return ok;
555    }
556    // check precondition: resulting formula is well formed was already done by well formed
557    // checker
558   
559  160 final RuleKey defined = checker.getRule(substPred.getName());
560  160 if (defined == null) {
561  0 ok = false;
562  0 handleProofCheckException(
563    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
564    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
565    + substPred.getName(),
566    getCurrentContext());
567  0 return ok;
568  160 } else if (!supported.contains(defined.getVersion())) {
569  0 ok = false;
570  0 handleProofCheckException(
571    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
572    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
573    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
574    getCurrentContext());
575  0 return ok;
576  160 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
577  0 ok = false;
578  0 handleProofCheckException(
579    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
580    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
581    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
582    getCurrentContext());
583  0 return ok;
584    }
585  160 return ok;
586    }
587   
 
588  0 toggle private boolean check(final SubstFunc substFunc, final int i, final Element element) {
589  0 final String context = currentContext.getLocationWithinModule();
590  0 boolean ok = true;
591  0 final Element alpha = getNormalizedLocalProofLineReference(substFunc.getReference());
592  0 if (alpha == null) {
593  0 ok = false;
594  0 setLocationWithinModule(context + ".getReference()");
595  0 handleProofCheckException(
596    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
597    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
598    + substFunc.getReference(),
599    getCurrentContext());
600  0 return ok;
601    }
602  0 final Element current = resolver.getNormalizedFormula(element);
603  0 if (substFunc.getSubstituteTerm() == null) {
604  0 ok = false;
605  0 handleProofCheckException(
606    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
607    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
608    getCurrentContext());
609  0 return ok;
610    }
611  0 final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
612  0 final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
613  0 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
614  0 if (!EqualsUtility.equals(current, expected)) {
615  0 ok = false;
616  0 handleProofCheckException(
617    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
618    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
619    + substFunc.getReference(),
620    getDiffModuleContextOfProofLineFormula(i, expected));
621  0 return ok;
622    }
623    // check precondition: function variable $\sigma$ must have n pairwise different free
624    // subject variables as arguments
625  0 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
626  0 if (funcFree.size() != sigma.getList().size() - 1) {
627  0 ok = false;
628  0 setLocationWithinModule(context + ".getPredicateVariable()");
629  0 handleProofCheckException(
630    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
631    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
632    getDiffModuleContextOfProofLineFormula(i, expected));
633  0 return ok;
634    }
635  0 for (int j = 1; j < sigma.getList().size(); j++) {
636  0 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
637  0 ok = false;
638  0 setLocationWithinModule(context + ".getPredicateVariable()");
639  0 handleProofCheckException(
640    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
641    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
642    getCurrentContext());
643  0 return ok;
644    }
645    }
646    // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
647    // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
648  0 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
649  0 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
650  0 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
651  0 ok = false;
652  0 setLocationWithinModule(context + ".getSubstituteFormula()");
653  0 handleProofCheckException(
654    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
655    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
656    getCurrentContext());
657  0 return ok;
658    }
659    // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
660    // contains no bound variable of $\tau(x_1, \ldots, x_n)$
661  0 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
662  0 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
663  0 ok = false;
664  0 setLocationWithinModule(context + ".getSubstituteFormula()");
665  0 handleProofCheckException(
666    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
667    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
668    getCurrentContext());
669  0 return ok;
670    }
671    // check precondition: $\sigma(...)$ dosn't occur in a precondition
672  0 if (FormulaUtility.containsOperatorVariable(conditions, sigma)) {
673  0 ok = false;
674  0 setLocationWithinModule(context + ".getPredicateVariable()");
675  0 handleProofCheckException(
676    BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
677    BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
678    getCurrentContext());
679  0 return ok;
680    }
681    // check precondition: resulting formula is well formed was already done by well formed
682    // checker
683   
684  0 final RuleKey defined = checker.getRule(substFunc.getName());
685  0 if (defined == null) {
686  0 ok = false;
687  0 handleProofCheckException(
688    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
689    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
690    + substFunc.getName(),
691    getCurrentContext());
692  0 return ok;
693  0 } else if (!supported.contains(defined.getVersion())) {
694  0 ok = false;
695  0 handleProofCheckException(
696    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
697    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
698    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
699    getCurrentContext());
700  0 return ok;
701  0 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
702  0 ok = false;
703  0 handleProofCheckException(
704    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
705    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
706    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
707    getCurrentContext());
708  0 return ok;
709    }
710  0 return ok;
711    }
712   
 
713  134 toggle private boolean check(final ModusPonens mp, final int i, final Element element) {
714  134 final String context = currentContext.getLocationWithinModule();
715  134 boolean ok = true;
716  134 final Element f1 = getNormalizedLocalProofLineReference(mp.getReference1());
717  134 if (f1 == null) {
718  0 ok = false;
719  0 setLocationWithinModule(context + ".getReference1()");
720  0 handleProofCheckException(
721    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
722    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
723    + mp.getReference1(),
724    getCurrentContext());
725    }
726  134 final Element f2 = getNormalizedLocalProofLineReference(mp.getReference2());
727  134 if (f2 == null) {
728  0 ok = false;
729  0 setLocationWithinModule(context + ".getReference2()");
730  0 handleProofCheckException(
731    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
732    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
733    + mp.getReference2(),
734    getCurrentContext());
735    }
736  134 if (ok) {
737  134 final Element current = getNormalizedFormula(element);
738  134 if (!FormulaUtility.isImplication(f1)) {
739  0 ok = false;
740  0 setLocationWithinModule(context + ".getReference1()");
741  0 handleProofCheckException(
742    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
743    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
744    + mp.getReference1(),
745    getCurrentContext());
746  134 } else if (!f2.equals(f1.getList().getElement(0))) {
747  0 ok = false;
748  0 setLocationWithinModule(context + ".getReference2()");
749  0 handleProofCheckException(
750    BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
751    BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
752    + mp.getReference2(),
753    getCurrentContext(),
754    resolver.getReferenceContext(mp.getReference1()));
755  134 } else if (!current.equals(f1.getList().getElement(1))) {
756  0 ok = false;
757  0 setLocationWithinModule(context + ".getReference1()");
758  0 handleProofCheckException(
759    BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
760    BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
761    + mp.getReference1(),
762    getCurrentContext(),
763    resolver.getReferenceContext(mp.getReference1()));
764    } else {
765  134 ok = true;
766    }
767    }
768  134 final RuleKey defined = checker.getRule(mp.getName());
769  134 if (defined == null) {
770  0 ok = false;
771  0 handleProofCheckException(
772    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
773    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
774    + mp.getName(),
775    getCurrentContext());
776  0 return ok;
777  134 } else if (!supported.contains(defined.getVersion())) {
778  0 ok = false;
779  0 handleProofCheckException(
780    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
781    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
782    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
783    getCurrentContext());
784  0 return ok;
785  134 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
786  0 ok = false;
787  0 handleProofCheckException(
788    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
789    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
790    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
791    getCurrentContext());
792  0 return ok;
793    }
794  134 return ok;
795    }
796   
 
797  4 toggle private boolean check(final Universal universal, final int i, final Element element) {
798  4 final String context = currentContext.getLocationWithinModule();
799  4 boolean ok = true;
800  4 final Element reference = getNormalizedLocalProofLineReference(universal.getReference());
801  4 if (reference == null) {
802  0 ok = false;
803  0 setLocationWithinModule(context + ".getReference()");
804  0 handleProofCheckException(
805    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
806    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
807    + universal.getReference(),
808    getCurrentContext());
809    // } else if (!lineProved[n.intValue()]) {
810    // ok = false;
811    // setLocationWithinModule(context + ".getReference()");
812    // handleProofCheckException(
813    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
814    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
815    // + universal.getReference(),
816    // getCurrentContext());
817    } else {
818  4 final Element current = getNormalizedFormula(element);
819  4 if (!FormulaUtility.isImplication(current)) {
820  0 ok = false;
821  0 setLocationWithinModule(context + ".getReference()");
822  0 handleProofCheckException(
823    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
824    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
825    + universal.getReference(),
826    getCurrentContext());
827  0 return ok;
828    }
829  4 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
830  0 ok = false;
831  0 setLocationWithinModule(context + ".getSubjectVariable()");
832  0 handleProofCheckException(
833    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
834    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
835    getCurrentContext());
836  0 return ok;
837    }
838  4 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
839  4 expected.add(reference.getList().getElement(0));
840  4 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
841  4 uni.add(universal.getSubjectVariable());
842  4 uni.add(reference.getList().getElement(1));
843  4 expected.add(uni);
844    // System.out.print("Expected: ");
845    // ProofFinderUtility.println(expected);
846    // System.out.print("Current : ");
847    // ProofFinderUtility.println(current);
848  4 if (!EqualsUtility.equals(current, expected)) {
849  0 ok = false;
850  0 handleProofCheckException(
851    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
852    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
853    + universal.getReference(),
854    getDiffModuleContextOfProofLineFormula(i, expected));
855  0 return ok;
856    }
857    }
858  4 final RuleKey defined = checker.getRule(universal.getName());
859  4 if (defined == null) {
860  0 ok = false;
861  0 handleProofCheckException(
862    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
863    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
864    + universal.getName(),
865    getCurrentContext());
866  0 return ok;
867  4 } else if (!supported.contains(defined.getVersion())) {
868  0 ok = false;
869  0 handleProofCheckException(
870    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
871    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
872    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
873    getCurrentContext());
874  0 return ok;
875  4 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
876  0 ok = false;
877  0 handleProofCheckException(
878    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
879    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
880    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
881    getCurrentContext());
882  0 return ok;
883    }
884  4 return ok;
885    }
886   
 
887  0 toggle private boolean check(final Existential existential, final int i, final Element element) {
888  0 final String context = currentContext.getLocationWithinModule();
889  0 boolean ok = true;
890  0 final Element reference = getNormalizedLocalProofLineReference(existential.getReference());
891  0 if (reference == null) {
892  0 ok = false;
893  0 setLocationWithinModule(context + ".getReference()");
894  0 handleProofCheckException(
895    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
896    BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
897    + existential.getReference(),
898    getCurrentContext());
899    // } else if (!lineProved[n.intValue()]) {
900    // ok = false;
901    // setLocationWithinModule(context + ".getReference()");
902    // handleProofCheckException(
903    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
904    // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
905    // + existential.getReference(),
906    // getCurrentContext());
907    } else {
908  0 final Element current = getNormalizedFormula(element);
909  0 if (!FormulaUtility.isImplication(current)) {
910  0 ok = false;
911  0 setLocationWithinModule(context + ".getReference()");
912  0 handleProofCheckException(
913    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
914    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
915    + existential.getReference(),
916    getCurrentContext());
917  0 return ok;
918    }
919  0 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
920  0 ok = false;
921  0 setLocationWithinModule(context + ".getSubjectVariable()");
922  0 handleProofCheckException(
923    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
924    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
925    getCurrentContext());
926  0 return ok;
927    }
928  0 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
929  0 final ElementList exi = new DefaultElementList(
930    Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
931  0 exi.add(existential.getSubjectVariable());
932  0 exi.add(reference.getList().getElement(0));
933  0 expected.add(exi);
934  0 expected.add((reference.getList().getElement(1)));
935  0 if (!EqualsUtility.equals(current, expected)) {
936  0 ok = false;
937  0 handleProofCheckException(
938    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
939    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
940    + existential.getReference(),
941    getDiffModuleContextOfProofLineFormula(i, expected));
942  0 return ok;
943    }
944    }
945  0 final RuleKey defined = checker.getRule(existential.getName());
946  0 if (defined == null) {
947  0 ok = false;
948  0 handleProofCheckException(
949    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
950    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
951    + existential.getName(),
952    getCurrentContext());
953  0 return ok;
954  0 } else if (!supported.contains(defined.getVersion())) {
955  0 ok = false;
956  0 handleProofCheckException(
957    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
958    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
959    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
960    getCurrentContext());
961  0 return ok;
962  0 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
963  0 ok = false;
964  0 handleProofCheckException(
965    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
966    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
967    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
968    getCurrentContext());
969  0 return ok;
970    }
971  0 return ok;
972    }
973   
 
974  50 toggle private boolean check(final ConditionalProof cp, final int i, final Element element) {
975  50 final ModuleAddress address = currentContext.getModuleLocation();
976  50 final String context = currentContext.getLocationWithinModule();
977    // System.out.println(getCurrentContext());
978  50 boolean ok = true;
979  50 if (cp.getHypothesis() == null || cp.getHypothesis().getFormula() == null
980    || cp.getHypothesis().getFormula().getElement() == null) {
981  0 ok = false;
982  0 setLocationWithinModule(context + ".getHypothesis()");
983  0 handleProofCheckException(
984    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
985    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
986    getCurrentContext());
987  0 return ok;
988    }
989  50 if (cp.getFormalProofLineList() == null || cp.getFormalProofLineList().size() <= 0) {
990  0 ok = false;
991  0 setLocationWithinModule(context + ".getFormalProofLineList()");
992  0 handleProofCheckException(
993    BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE,
994    BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT,
995    getCurrentContext());
996  0 return ok;
997    }
998  50 final ReferenceResolver newResolver = new ReferenceResolver() {
999   
 
1000  365 toggle public Element getNormalizedFormula(final Element formula) {
1001  365 return ProofChecker2Impl.this.getNormalizedFormula(formula);
1002    }
1003   
 
1004  7 toggle public Element getNormalizedReferenceFormula(final String reference) {
1005    // System.out.println("Looking for " + reference);
1006  7 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1007  0 return resolver.getNormalizedFormula(cp.getHypothesis().getFormula()
1008    .getElement());
1009    }
1010  7 return ProofChecker2Impl.this.getNormalizedReferenceFormula(reference);
1011    }
1012   
 
1013  7 toggle public boolean isProvedFormula(final String reference) {
1014  7 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1015  0 return true;
1016    }
1017  7 return ProofChecker2Impl.this.isProvedFormula(reference);
1018    }
1019   
 
1020  191 toggle public boolean isLocalProofLineReference(final String reference) {
1021  191 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1022  0 return true;
1023    }
1024  191 return ProofChecker2Impl.this.isLocalProofLineReference(reference);
1025    }
1026   
 
1027  0 toggle public ModuleContext getReferenceContext(final String reference) {
1028  0 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1029  0 return new ModuleContext(address, context
1030    + ".getHypothesis().getLabel()");
1031    }
1032  0 return ProofChecker2Impl.this.getReferenceContext(reference);
1033    }
1034   
 
1035  168 toggle public Element getNormalizedLocalProofLineReference(final String reference) {
1036    // System.out.println("\t resolver looks for " + reference);
1037  168 if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1038    // System.out.println("\t resolver found local " + reference);
1039  62 return resolver.getNormalizedFormula(
1040    cp.getHypothesis().getFormula().getElement());
1041    }
1042  106 return ProofChecker2Impl.this.getNormalizedLocalProofLineReference(reference);
1043    }
1044   
1045    };
1046  50 final int last = cp.getFormalProofLineList().size() - 1;
1047  50 setLocationWithinModule(context + ".getFormalProofLineList().get(" + last + ")");
1048  50 final FormalProofLine line = cp.getFormalProofLineList().get(last);
1049  50 if (line == null || line.getFormula() == null
1050    || line.getFormula().getElement() == null) {
1051  0 ok = false;
1052  0 handleProofCheckException(
1053    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1054    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1055    getCurrentContext());
1056  0 return ok;
1057    }
1058  50 final Element lastFormula = resolver.getNormalizedFormula(line.getFormula().getElement());
1059  50 final ElementList newConditions = (ElementList) conditions.copy();
1060    // add hypothesis as new condition
1061  50 newConditions.add(cp.getHypothesis().getFormula().getElement());
1062  50 setLocationWithinModule(context + ".getFormalProofLineList()");
1063  50 final LogicalCheckExceptionList eList = (new ProofChecker2Impl()).checkProof(
1064    newConditions, lastFormula, cp.getFormalProofLineList(), checker, getCurrentContext(),
1065    newResolver);
1066  50 exceptions.add(eList);
1067  50 ok = eList.size() == 0;
1068  50 setLocationWithinModule(context + ".getConclusion()");
1069  50 if (cp.getConclusion() == null || cp.getConclusion().getFormula() == null
1070    || cp.getConclusion().getFormula().getElement() == null) {
1071  0 ok = false;
1072  0 handleProofCheckException(
1073    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1074    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1075    getCurrentContext());
1076  0 return ok;
1077    }
1078  50 final Element c = resolver.getNormalizedFormula(cp.getConclusion().getFormula().getElement());
1079  50 setLocationWithinModule(context + ".getConclusion().getFormula().getElement()");
1080  50 if (!FormulaUtility.isImplication(c)) {
1081  0 ok = false;
1082  0 handleProofCheckException(
1083    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
1084    BasicProofErrors.IMPLICATION_EXPECTED_TEXT,
1085    getCurrentContext());
1086  0 return ok;
1087    }
1088  50 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
1089  50 expected.add(cp.getHypothesis().getFormula().getElement());
1090  50 expected.add(lastFormula);
1091    // System.out.println("expected: ");
1092    // ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
1093  50 if (!EqualsUtility.equals(cp.getConclusion().getFormula().getElement(), expected)) {
1094    // System.out.println("found: ");
1095    // ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
1096  0 ok = false;
1097  0 handleProofCheckException(
1098    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_CODE,
1099    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_TEXT,
1100    getDiffModuleContextOfProofLineFormula(i, expected));
1101  0 return ok;
1102    }
1103  50 final RuleKey defined = checker.getRule(cp.getName());
1104  50 if (defined == null) {
1105  0 ok = false;
1106  0 handleProofCheckException(
1107    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
1108    BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
1109    + cp.getName(),
1110    getCurrentContext());
1111  0 return ok;
1112  50 } else if (!supported.contains(defined.getVersion())) {
1113  0 ok = false;
1114  0 handleProofCheckException(
1115    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
1116    BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
1117    + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
1118    getCurrentContext());
1119  0 return ok;
1120  50 } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
1121  0 ok = false;
1122  0 handleProofCheckException(
1123    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
1124    BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
1125    + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
1126    getCurrentContext());
1127  0 return ok;
1128    }
1129  50 return ok;
1130    }
1131   
 
1132  1 toggle private ModuleContext getModuleContextOfProofLineFormula(final int i) {
1133  1 if (proof.get(i) instanceof ConditionalProof) {
1134  0 return new ModuleContext(moduleContext.getModuleLocation(),
1135    moduleContext.getLocationWithinModule() + ".get(" + i
1136    + ").getConclusion().getFormula().getElement()");
1137    }
1138  1 return new ModuleContext(moduleContext.getModuleLocation(),
1139    moduleContext.getLocationWithinModule() + ".get(" + i
1140    + ").getFormula().getElement()");
1141    }
1142   
 
1143  0 toggle private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
1144    final Element expected) {
1145  0 final String diff = FormulaUtility.getDifferenceLocation(
1146    proof.get(i).getFormula().getElement(), expected);
1147  0 if (proof.get(i) instanceof ConditionalProof) {
1148  0 return new ModuleContext(moduleContext.getModuleLocation(),
1149    moduleContext.getLocationWithinModule() + ".get(" + i
1150    + ").getConclusion().getFormula().getElement()" + diff);
1151    }
1152  0 return new ModuleContext(moduleContext.getModuleLocation(),
1153    moduleContext.getLocationWithinModule() + ".get(" + i
1154    + ").getFormula().getElement()" + diff);
1155    }
1156   
1157    /**
1158    * Have we any conditions. If yes we are within an conditional proof argument.
1159    *
1160    * @return Do we have conditions?
1161    */
 
1162  890 toggle private boolean hasConditions() {
1163  890 return conditions.size() > 0;
1164    }
1165   
 
1166  379 toggle private Element getNormalizedProofLine(final Integer n) {
1167  379 if (n == null) {
1168  0 return null;
1169    }
1170  379 int i = n.intValue();
1171  379 if (i < 0 || i >= proof.size()) {
1172  0 return null;
1173    }
1174  379 return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
1175    }
1176   
1177    /**
1178    * Add new {@link ProofCheckException} to exception list.
1179    *
1180    * @param code Error code.
1181    * @param msg Error message.
1182    * @param context Error context.
1183    */
 
1184  1 toggle private void handleProofCheckException(final int code, final String msg,
1185    final ModuleContext context) {
1186    // System.out.println(context);
1187    // System.setProperty("qedeq.test.xmlLocationFailures", "true");
1188  1 final ProofCheckException ex = new ProofCheckException(code, msg, context);
1189  1 exceptions.add(ex);
1190    }
1191   
1192    /**
1193    * Add new {@link ProofCheckException} to exception list.
1194    *
1195    * @param code Error code.
1196    * @param msg Error message.
1197    * @param context Error context.
1198    * @param referenceContext Reference context.
1199    */
 
1200  0 toggle private void handleProofCheckException(final int code, final String msg,
1201    final ModuleContext context, final ModuleContext referenceContext) {
1202    // System.out.println(context);
1203    // System.setProperty("qedeq.test.xmlLocationFailures", "true");
1204  0 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
1205    referenceContext);
1206  0 exceptions.add(ex);
1207    }
1208   
1209    /**
1210    * Get current context within original.
1211    *
1212    * @return Current context.
1213    */
 
1214  4790 toggle protected final ModuleContext getCurrentContext() {
1215  4790 return currentContext;
1216    }
1217   
1218    /**
1219    * Set location information where are we within the original module.
1220    *
1221    * @param locationWithinModule Location within module.
1222    */
 
1223  927 toggle protected void setLocationWithinModule(final String locationWithinModule) {
1224  927 getCurrentContext().setLocationWithinModule(locationWithinModule);
1225    }
1226   
 
1227  7 toggle public boolean isProvedFormula(final String reference) {
1228  7 if (label2line.containsKey(reference)) {
1229  0 return lineProved[((Integer) label2line.get(reference)).intValue()];
1230    }
1231  7 return resolver.isProvedFormula(reference);
1232    }
1233   
 
1234  7 toggle public Element getNormalizedReferenceFormula(final String reference) {
1235    // System.out.println("looking for " + reference);
1236  7 if (label2line.containsKey(reference)) {
1237    // System.out.println("found in local " + reference);
1238  0 return getNormalizedProofLine((Integer) label2line.get(reference));
1239    }
1240    // System.out.println("not found in local " + reference);
1241  7 return resolver.getNormalizedReferenceFormula(reference);
1242    }
1243   
 
1244  503 toggle public Element getNormalizedFormula(final Element element) {
1245  503 return resolver.getNormalizedFormula(element);
1246    }
1247   
 
1248  636 toggle public boolean isLocalProofLineReference(final String reference) {
1249  636 if (label2line.containsKey(reference)) {
1250  0 return true;
1251    }
1252  636 return resolver.isLocalProofLineReference(reference);
1253    }
1254   
 
1255  547 toggle public Element getNormalizedLocalProofLineReference(final String reference) {
1256    // System.out.println("\t resolver looks for " + reference);
1257  547 if (label2line.containsKey(reference)) {
1258    // System.out.println("\t resolver found local " + reference);
1259  379 return getNormalizedProofLine((Integer) label2line.get(reference));
1260    }
1261    // System.out.println("\t resolver asks super resolver for " + reference);
1262  168 final Element result = resolver.getNormalizedLocalProofLineReference(reference);
1263    // if (result == null) {
1264    // System.out.println("\t super resolver didn't find " + reference);
1265    // } else {
1266    // System.out.println("\t super resolver found " + reference);
1267    // }
1268  168 return result;
1269    }
1270   
 
1271  0 toggle public ModuleContext getReferenceContext(final String reference) {
1272  0 if (label2line.containsKey(reference)) {
1273  0 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
1274    moduleContext.getLocationWithinModule() + ".get("
1275    + label2line.get(reference)
1276    + ").getLabel()");
1277  0 return lc;
1278    }
1279  0 return resolver.getReferenceContext(reference);
1280    }
1281   
1282    }