EMMA Coverage Report (generated Fri Feb 14 08:28:31 UTC 2014)
[all classes][org.qedeq.kernel.bo.logic.proof.checker]

COVERAGE SUMMARY FOR SOURCE FILE [ProofChecker1Impl.java]

nameclass, %method, %block, %line, %
ProofChecker1Impl.java100% (1/1)95%  (18/19)67%  (1505/2238)68%  (265/387)

COVERAGE BREAKDOWN BY CLASS AND METHOD

nameclass, %method, %block, %line, %
     
class ProofChecker1Impl100% (1/1)95%  (18/19)67%  (1505/2238)68%  (265/387)
checkRule (Rule, ModuleContext, RuleChecker, ReferenceResolver): LogicalCheck... 0%   (0/1)0%   (0/52)0%   (0/6)
check (Existential, int, Element): boolean 100% (1/1)48%  (102/213)59%  (23/39)
check (SubstFunc, int, Element): boolean 100% (1/1)55%  (158/286)55%  (30/55)
check (SubstPred, int, Element): boolean 100% (1/1)59%  (168/286)60%  (33/55)
check (ModusPonens, int, Element): boolean 100% (1/1)62%  (156/250)69%  (27/39)
check (Add, int, Element): boolean 100% (1/1)63%  (94/150)68%  (19/28)
check (Universal, int, Element): boolean 100% (1/1)70%  (147/211)74%  (29/39)
check (SubstFree, int, Element): boolean 100% (1/1)74%  (101/137)75%  (18/24)
check (Rename, int, Element): boolean 100% (1/1)74%  (104/140)75%  (18/24)
getNormalizedProofLine (Integer): Element 100% (1/1)78%  (7/9)67%  (2/3)
getNormalizedProofLine (int): Element 100% (1/1)89%  (17/19)67%  (2/3)
checkProof (Element, FormalProofLineList, RuleChecker, ModuleContext, Referen... 100% (1/1)91%  (355/389)86%  (49/57)
ProofChecker1Impl (): void 100% (1/1)100% (9/9)100% (3/3)
getCurrentContext (): ModuleContext 100% (1/1)100% (3/3)100% (1/1)
getDiffModuleContextOfProofLineFormula (int, Element): ModuleContext 100% (1/1)100% (32/32)100% (2/2)
getModuleContextOfProofLineFormula (int): ModuleContext 100% (1/1)100% (21/21)100% (1/1)
handleProofCheckException (int, String, ModuleContext): void 100% (1/1)100% (12/12)100% (3/3)
handleProofCheckException (int, String, ModuleContext, ModuleContext): void 100% (1/1)100% (14/14)100% (3/3)
setLocationWithinModule (String): void 100% (1/1)100% (5/5)100% (2/2)

1/* This file is part of the project "Hilbert II" - http://www.qedeq.org
2 *
3 * Copyright 2000-2014,  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 
16package org.qedeq.kernel.bo.logic.proof.checker;
17 
18import java.util.HashMap;
19import java.util.Map;
20 
21import org.qedeq.base.io.Version;
22import org.qedeq.base.utility.Enumerator;
23import org.qedeq.base.utility.EqualsUtility;
24import org.qedeq.base.utility.StringUtility;
25import org.qedeq.kernel.bo.logic.common.FormulaUtility;
26import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
27import org.qedeq.kernel.bo.logic.common.Operators;
28import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
29import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
30import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
31import org.qedeq.kernel.se.base.list.Element;
32import org.qedeq.kernel.se.base.list.ElementList;
33import org.qedeq.kernel.se.base.module.Add;
34import org.qedeq.kernel.se.base.module.Existential;
35import org.qedeq.kernel.se.base.module.FormalProofLine;
36import org.qedeq.kernel.se.base.module.FormalProofLineList;
37import org.qedeq.kernel.se.base.module.ModusPonens;
38import org.qedeq.kernel.se.base.module.Reason;
39import org.qedeq.kernel.se.base.module.Rename;
40import org.qedeq.kernel.se.base.module.Rule;
41import org.qedeq.kernel.se.base.module.SubstFree;
42import org.qedeq.kernel.se.base.module.SubstFunc;
43import org.qedeq.kernel.se.base.module.SubstPred;
44import org.qedeq.kernel.se.base.module.Universal;
45import org.qedeq.kernel.se.common.ModuleContext;
46import org.qedeq.kernel.se.common.RuleKey;
47import org.qedeq.kernel.se.dto.list.DefaultElementList;
48import org.qedeq.kernel.se.dto.list.ElementSet;
49 
50 
51/**
52 * Formal proof checker for basic rules.
53 *
54 * @author  Michael Meyling
55 */
56public 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    public ProofChecker1Impl() {
90        this.ruleVersion = new Version("0.01.00");
91    }
92 
93    public LogicalCheckExceptionList checkRule(final Rule rule,
94            final ModuleContext context, final RuleChecker checker,
95            final ReferenceResolver resolver) {
96        exceptions = new LogicalCheckExceptionList();
97        final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
98        if (rule.getVersion() == null || !ruleVersion.equals(rule.getVersion())) {
99            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            exceptions.add(ex);
105        }
106        return exceptions;
107    }
108 
109    public LogicalCheckExceptionList checkProof(final Element formula,
110            final FormalProofLineList proof,
111            final RuleChecker checker,
112            final ModuleContext moduleContext,
113            final ReferenceResolver resolver) {
114        this.proof = proof;
115        this.resolver = resolver;
116        this.moduleContext = moduleContext;
117        this.checker = checker;
118        // use copy constructor for changing context
119        currentContext = new ModuleContext(moduleContext);
120        exceptions = new LogicalCheckExceptionList();
121        final String context = moduleContext.getLocationWithinModule();
122        lineProved = new boolean[proof.size()];
123        label2line = new HashMap();
124        for (int i = 0; i < proof.size(); i++) {
125            boolean ok = true;
126            setLocationWithinModule(context + ".get("  + i + ")");
127            final FormalProofLine line = proof.get(i);
128            if (line == null || line.getFormula() == null
129                    || line.getFormula().getElement() == null) {
130                ok = false;
131                handleProofCheckException(
132                    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
133                    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
134                    getCurrentContext());
135                continue;
136            }
137            setLocationWithinModule(context + ".get(" + i + ").getReason()");
138            final Reason reason = line.getReason();
139            if (reason == null) {
140                ok = false;
141                handleProofCheckException(
142                    BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
143                    BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
144                    getCurrentContext());
145                continue;
146            }
147            if (line.getLabel() != null && line.getLabel().length() > 0) {
148                final Integer n = (Integer) label2line.get(line.getLabel());
149                if (n != null) {
150                    final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
151                        moduleContext.getLocationWithinModule() + ".get("
152                        + label2line.get(line.getLabel())
153                        + ").getLabel()");
154                    setLocationWithinModule(context + ".get("  + i + ").getLabel()");
155                    handleProofCheckException(
156                        BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
157                        BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
158                        + line.getLabel(),
159                        getCurrentContext(),
160                        lc);
161                }
162                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            String getReason = ".get" + StringUtility.getClassName(reason.getClass());
168            if (getReason.endsWith("Vo")) {
169                getReason = getReason.substring(0, getReason.length() - 2) + "()";
170                setLocationWithinModule(context + ".get("  + i + ").getReason()"
171                    + getReason);
172            }
173            if (reason instanceof Add) {
174                ok = check((Add) reason, i, line.getFormula().getElement());
175            } else if (reason instanceof Rename) {
176                ok = check((Rename) reason, i, line.getFormula().getElement());
177            } else if (reason instanceof ModusPonens) {
178                ok = check((ModusPonens) reason, i, line.getFormula().getElement());
179            } else if (reason instanceof SubstFree) {
180                ok = check((SubstFree) reason, i, line.getFormula().getElement());
181            } else if (reason instanceof SubstPred) {
182                ok = check((SubstPred) reason, i, line.getFormula().getElement());
183            } else if (reason instanceof SubstFunc) {
184                ok = check((SubstFunc) reason, i, line.getFormula().getElement());
185            } else if (reason instanceof Universal) {
186                ok = check((Universal) reason, i, line.getFormula().getElement());
187            } else if (reason instanceof Existential) {
188                ok = check((Existential) reason, i, line.getFormula().getElement());
189            } else {
190                ok = false;
191                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            lineProved[i] = ok;
198            // check if last proof line is identical with proposition formula
199            if (i == proof.size() - 1) {
200                if (!formula.equals(line.getFormula().getElement())) {
201                    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        return exceptions;
210    }
211 
212    private boolean check(final Add add, final int i, final Element element) {
213        final String context = currentContext.getLocationWithinModule();
214        boolean ok = true;
215        if (add.getReference() == null) {
216            ok = false;
217            setLocationWithinModule(context + ".getReference()");
218            handleProofCheckException(
219                BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
220                BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
221                getCurrentContext());
222            return ok;
223        }
224        if (!resolver.isProvedFormula(add.getReference())) {
225            ok = false;
226            setLocationWithinModule(context + ".getReference()");
227            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            return ok;
233        }
234        final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
235        final Element current = resolver.getNormalizedFormula(element);
236        if (!EqualsUtility.equals(expected, current)) {
237            ok = false;
238            handleProofCheckException(
239                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
240                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
241                + add.getReference(),
242                getDiffModuleContextOfProofLineFormula(i, expected));
243            return ok;
244        }
245        final RuleKey defined = checker.getRule(add.getName());
246        if (defined == null) {
247            ok = false;
248            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            return ok;
254        } else if (!ruleVersion.equals(defined.getVersion())) {
255            ok = false;
256            handleProofCheckException(
257                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
258                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
259                getCurrentContext());
260            return ok;
261        }
262        return ok;
263    }
264 
265    private boolean check(final Rename rename, final int i, final Element element) {
266        final String context = currentContext.getLocationWithinModule();
267        boolean ok = true;
268        final Integer n = (Integer) label2line.get(rename.getReference());
269        if (n == null) {
270            ok = false;
271            setLocationWithinModule(context + ".getReference()");
272            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            final Element f = getNormalizedProofLine(n);
287            final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
288                rename.getOriginalSubjectVariable(),
289                rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
290                new Enumerator());
291            final Element current = resolver.getNormalizedFormula(element);
292            if (!EqualsUtility.equals(expected, current)) {
293                ok = false;
294                handleProofCheckException(
295                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
296                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
297                    + rename.getReference(),
298                    getDiffModuleContextOfProofLineFormula(i, expected));
299            } else {
300                ok = true;
301            }
302        }
303        final RuleKey defined = checker.getRule(rename.getName());
304        if (defined == null) {
305            ok = false;
306            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            return ok;
312        } else if (!ruleVersion.equals(defined.getVersion())) {
313            ok = false;
314            handleProofCheckException(
315                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
316                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
317                getCurrentContext());
318            return ok;
319        }
320        return ok;
321    }
322 
323    private boolean check(final SubstFree substFree, final int i, final Element element) {
324        final String context = currentContext.getLocationWithinModule();
325        boolean ok = true;
326        final Integer n = (Integer) label2line.get(substFree.getReference());
327        if (n == null) {
328            ok = false;
329            setLocationWithinModule(context + ".getReference()");
330            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            final Element f = getNormalizedProofLine(n);
345            final Element current = resolver.getNormalizedFormula(element);
346            final Element expected = f.replace(substFree.getSubjectVariable(),
347                resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
348            if (!EqualsUtility.equals(current, expected)) {
349                ok = false;
350                handleProofCheckException(
351                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
352                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
353                    + substFree.getReference(),
354                    getDiffModuleContextOfProofLineFormula(i, expected));
355                return ok;
356            }
357        }
358        final RuleKey defined = checker.getRule(substFree.getName());
359        if (defined == null) {
360            ok = false;
361            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            return ok;
367        } else if (!ruleVersion.equals(defined.getVersion())) {
368            ok = false;
369            handleProofCheckException(
370                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
371                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
372                getCurrentContext());
373            return ok;
374        }
375        return ok;
376    }
377 
378    private boolean check(final SubstPred substPred, final int i, final Element element) {
379        final String context = currentContext.getLocationWithinModule();
380        boolean ok = true;
381        final Integer n = (Integer) label2line.get(substPred.getReference());
382        if (n == null) {
383            ok = false;
384            setLocationWithinModule(context + ".getReference()");
385            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            final Element alpha = getNormalizedProofLine(n);
400            final Element current = resolver.getNormalizedFormula(element);
401            if (substPred.getSubstituteFormula() == null) {
402                ok = false;
403                handleProofCheckException(
404                    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
405                    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
406                    getCurrentContext());
407                return ok;
408            }
409            final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
410            final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
411            final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
412            if (!EqualsUtility.equals(current, expected)) {
413                ok = false;
414                handleProofCheckException(
415                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
416                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
417                    + substPred.getReference(),
418                    getDiffModuleContextOfProofLineFormula(i, expected));
419                return ok;
420            }
421            // check precondition: predicate variable p must have n pairwise different free subject
422            // variables as arguments
423            final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
424            if (predFree.size() != p.getList().size() - 1) {
425                ok = false;
426                setLocationWithinModule(context + ".getPredicateVariable()");
427                handleProofCheckException(
428                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
429                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
430                    getDiffModuleContextOfProofLineFormula(i, expected));
431                return ok;
432            }
433            for (int j = 1; j < p.getList().size(); j++) {
434                if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
435                    ok = false;
436                    setLocationWithinModule(context + ".getPredicateVariable()");
437                    handleProofCheckException(
438                        BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
439                        BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
440                        getCurrentContext());
441                    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            final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
447            final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
448            if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
449                ok = false;
450                setLocationWithinModule(context + ".getSubstituteFormula()");
451                handleProofCheckException(
452                    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
453                    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
454                    getCurrentContext());
455                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            final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
460            if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
461                ok = false;
462                setLocationWithinModule(context + ".getSubstituteFormula()");
463                handleProofCheckException(
464                    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
465                    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
466                    getCurrentContext());
467                return ok;
468            }
469            // check precondition: resulting formula is well formed was already done by well formed
470            // checker
471        }
472        final RuleKey defined = checker.getRule(substPred.getName());
473        if (defined == null) {
474            ok = false;
475            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            return ok;
481        } else if (!ruleVersion.equals(defined.getVersion())) {
482            ok = false;
483            handleProofCheckException(
484                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
485                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
486                getCurrentContext());
487            return ok;
488        }
489        return ok;
490    }
491 
492    private boolean check(final SubstFunc substFunc, final int i, final Element element) {
493        final String context = currentContext.getLocationWithinModule();
494        boolean ok = true;
495        final Integer n = (Integer) label2line.get(substFunc.getReference());
496        if (n == null) {
497            ok = false;
498            setLocationWithinModule(context + ".getReference()");
499            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            final Element alpha = getNormalizedProofLine(n);
514            final Element current = resolver.getNormalizedFormula(element);
515            if (substFunc.getSubstituteTerm() == null) {
516                ok = false;
517                handleProofCheckException(
518                    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
519                    BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
520                    getCurrentContext());
521                return ok;
522            }
523            final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
524            final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
525            final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
526            if (!EqualsUtility.equals(current, expected)) {
527                ok = false;
528                handleProofCheckException(
529                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
530                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
531                    + substFunc.getReference(),
532                    getDiffModuleContextOfProofLineFormula(i, expected));
533                return ok;
534            }
535            // check precondition: function variable $\sigma$ must have n pairwise different free
536            // subject variables as arguments
537            final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
538            if (funcFree.size() != sigma.getList().size() - 1) {
539                ok = false;
540                setLocationWithinModule(context + ".getPredicateVariable()");
541                handleProofCheckException(
542                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
543                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
544                    getDiffModuleContextOfProofLineFormula(i, expected));
545                return ok;
546            }
547            for (int j = 1; j < sigma.getList().size(); j++) {
548                if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
549                    ok = false;
550                    setLocationWithinModule(context + ".getPredicateVariable()");
551                    handleProofCheckException(
552                        BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
553                        BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
554                        getCurrentContext());
555                    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            final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
561            final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
562            if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
563                ok = false;
564                setLocationWithinModule(context + ".getSubstituteFormula()");
565                handleProofCheckException(
566                    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
567                    BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
568                    getCurrentContext());
569                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            final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
574            if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
575                ok = false;
576                setLocationWithinModule(context + ".getSubstituteFormula()");
577                handleProofCheckException(
578                    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
579                    BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
580                    getCurrentContext());
581                return ok;
582            }
583            // check precondition: resulting formula is well formed was already done by well formed
584            // checker
585        }
586        final RuleKey defined = checker.getRule(substFunc.getName());
587        if (defined == null) {
588            ok = false;
589            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            return ok;
595        } else if (!ruleVersion.equals(defined.getVersion())) {
596            ok = false;
597            handleProofCheckException(
598                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
599                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
600                getCurrentContext());
601            return ok;
602        }
603        return ok;
604    }
605 
606    private boolean check(final ModusPonens mp, final int i, final Element element) {
607        final String context = currentContext.getLocationWithinModule();
608        boolean ok = true;
609        final Integer n1 = (Integer) label2line.get(mp.getReference1());
610        if (n1 == null) {
611            ok = false;
612            setLocationWithinModule(context + ".getReference1()");
613            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        final Integer n2 = (Integer) label2line.get(mp.getReference2());
628        if (n2 == null) {
629            ok = false;
630            setLocationWithinModule(context + ".getReference2()");
631            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        if (ok) {
646            final Element f1 = getNormalizedProofLine(n1);
647            final Element f2 = getNormalizedProofLine(n2);
648            final Element current = getNormalizedProofLine(i);
649            if (!FormulaUtility.isImplication(f1)) {
650                ok = false;
651                setLocationWithinModule(context + ".getReference1()");
652                handleProofCheckException(
653                    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
654                    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
655                    + mp.getReference1(),
656                    getCurrentContext());
657            } else if (!f2.equals(f1.getList().getElement(0))) {
658                ok = false;
659                setLocationWithinModule(context + ".getReference2()");
660                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            } else if (!current.equals(f1.getList().getElement(1))) {
667                ok = false;
668                setLocationWithinModule(context + ".getReference1()");
669                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                ok = true;
677            }
678        }
679        final RuleKey defined = checker.getRule(mp.getName());
680        if (defined == null) {
681            ok = false;
682            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            return ok;
688        } else if (!ruleVersion.equals(defined.getVersion())) {
689            ok = false;
690            handleProofCheckException(
691                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
692                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
693                getCurrentContext());
694            return ok;
695        }
696        return ok;
697    }
698 
699    private boolean check(final Universal universal, final int i, final Element element) {
700        final String context = currentContext.getLocationWithinModule();
701        boolean ok = true;
702        final Integer n = (Integer) label2line.get(universal.getReference());
703        if (n == null) {
704            ok = false;
705            setLocationWithinModule(context + ".getReference()");
706            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            final Element f = getNormalizedProofLine(n);
721            final Element current = resolver.getNormalizedFormula(element);
722            if (!FormulaUtility.isImplication(f)) {
723                ok = false;
724                setLocationWithinModule(context + ".getReference()");
725                handleProofCheckException(
726                    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
727                    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
728                    + universal.getReference(),
729                    getCurrentContext());
730                return ok;
731            }
732            if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
733                ok = false;
734                setLocationWithinModule(context + ".getSubjectVariable()");
735                handleProofCheckException(
736                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
737                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
738                    getCurrentContext());
739                return ok;
740            }
741            final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
742            expected.add((f.getList().getElement(0)));
743            final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
744            uni.add(universal.getSubjectVariable());
745            uni.add(f.getList().getElement(1));
746            expected.add(uni);
747            if (!EqualsUtility.equals(current, expected)) {
748                ok = false;
749                handleProofCheckException(
750                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
751                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
752                    + universal.getReference(),
753                    getDiffModuleContextOfProofLineFormula(i, expected));
754                return ok;
755            }
756        }
757        final RuleKey defined = checker.getRule(universal.getName());
758        if (defined == null) {
759            ok = false;
760            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            return ok;
766        } else if (!ruleVersion.equals(defined.getVersion())) {
767            ok = false;
768            handleProofCheckException(
769                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
770                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
771                getCurrentContext());
772            return ok;
773        }
774        return ok;
775    }
776 
777    private boolean check(final Existential existential, final int i, final Element element) {
778        final String context = currentContext.getLocationWithinModule();
779        boolean ok = true;
780        final Integer n = (Integer) label2line.get(existential.getReference());
781        if (n == null) {
782            ok = false;
783            setLocationWithinModule(context + ".getReference()");
784            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            final Element f = getNormalizedProofLine(n);
799            final Element current = resolver.getNormalizedFormula(element);
800            if (!FormulaUtility.isImplication(f)) {
801                ok = false;
802                setLocationWithinModule(context + ".getReference()");
803                handleProofCheckException(
804                    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
805                    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
806                    + existential.getReference(),
807                    getCurrentContext());
808                return ok;
809            }
810            if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
811                ok = false;
812                setLocationWithinModule(context + ".getSubjectVariable()");
813                handleProofCheckException(
814                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
815                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
816                    getCurrentContext());
817                return ok;
818            }
819            final DefaultElementList expected = new DefaultElementList(f.getList().getOperator());
820            final ElementList exi = new DefaultElementList(
821                Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
822            exi.add(existential.getSubjectVariable());
823            exi.add(f.getList().getElement(0));
824            expected.add(exi);
825            expected.add((f.getList().getElement(1)));
826            if (!EqualsUtility.equals(current, expected)) {
827                ok = false;
828                handleProofCheckException(
829                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
830                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
831                    + existential.getReference(),
832                    getDiffModuleContextOfProofLineFormula(i, expected));
833                return ok;
834            }
835        }
836        final RuleKey defined = checker.getRule(existential.getName());
837        if (defined == null) {
838            ok = false;
839            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            return ok;
845        } else if (!ruleVersion.equals(defined.getVersion())) {
846            ok = false;
847            handleProofCheckException(
848                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
849                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
850                getCurrentContext());
851            return ok;
852        }
853        return ok;
854    }
855 
856    private ModuleContext getModuleContextOfProofLineFormula(final int i) {
857        return new ModuleContext(moduleContext.getModuleLocation(),
858            moduleContext.getLocationWithinModule() + ".get(" + i
859            + ").getFormula().getElement()");
860    }
861 
862    private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
863            final Element expected) {
864        final String diff = FormulaUtility.getDifferenceLocation(
865            proof.get(i).getFormula().getElement(),  expected);
866        return new ModuleContext(moduleContext.getModuleLocation(),
867            moduleContext.getLocationWithinModule() + ".get(" + i
868            + ").getFormula().getElement()" + diff);
869    }
870 
871    private Element getNormalizedProofLine(final Integer n) {
872        if (n == null) {
873            return null;
874        }
875        return getNormalizedProofLine(n.intValue());
876    }
877 
878    private Element getNormalizedProofLine(final int i) {
879        if (i < 0 || i >= proof.size()) {
880            return null;
881        }
882        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    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        final ProofCheckException ex = new ProofCheckException(code, msg, context);
897        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    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        final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
913            referenceContext);
914        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    protected void setLocationWithinModule(final String locationWithinModule) {
923        getCurrentContext().setLocationWithinModule(locationWithinModule);
924    }
925 
926    /**
927     * Get current context within original.
928     *
929     * @return  Current context.
930     */
931    protected final ModuleContext getCurrentContext() {
932        return currentContext;
933    }
934 
935 
936}

[all classes][org.qedeq.kernel.bo.logic.proof.checker]
EMMA 2.1.5320 (stable) (C) Vladimir Roubtsov