|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
KernelNodeBo | Line # 37 | 64 | 39 | 76.2% |
0.76229507
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||
(77) | |||
Result | |||
0.647541
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin4 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin4 | 1 PASS | |
0.57377046
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin2 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin2 | 1 PASS | |
0.57377046
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin | 1 PASS | |
0.57377046
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin2 org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin2 | 1 PASS | |
0.57377046
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPluginFast org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPluginFast | 1 PASS | |
0.5409836
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin | 1 PASS | |
0.5409836
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin3 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin3 | 1 PASS | |
0.5081967
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration | 1 PASS | |
0.5081967
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration | 1 PASS | |
0.4918033
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1b org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1b | 1 PASS | |
0.36885247
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 | 1 PASS | |
0.36885247
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 | 1 PASS | |
0.36885247
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 | 1 PASS | |
0.36885247
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3b org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3b | 1 PASS | |
0.36885247
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3c org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3c | 1 PASS | |
0.36885247
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 | 1 PASS | |
0.20491803
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration4 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration4 | 1 PASS | |
0.16393442
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1 | 1 PASS | |
0.10655738
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L003 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L003 | 1 PASS | |
0.09016393
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck6 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck6 | 1 PASS | |
0.09016393
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind | 1 PASS | |
0.09016393
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind2 org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind2 | 1 PASS | |
0.09016393
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck4 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck4 | 1 PASS | |
0.09016393
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck1 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck1 | 1 PASS | |
0.09016393
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind3 org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind3 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative04 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative04 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript1 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript1 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_02 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_02 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_10 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_10 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript1 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript1 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_11 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_11 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative04 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative04 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative02 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative02 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq5 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq5 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.heuristic.DynamicHeuristicCheckerPluginTest.testQedeqSampleScript1 org.qedeq.kernel.bo.service.heuristic.DynamicHeuristicCheckerPluginTest.testQedeqSampleScript1 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.xml.parser.CharsetParserTest.testParse1 org.qedeq.kernel.xml.parser.CharsetParserTest.testParse1 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_13 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_13 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript2 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript2 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive04 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive04 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v2 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v2 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative02 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative02 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v1 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v1 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_04 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_04 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_01 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_01 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_05 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_05 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq4 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq4 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerTest.testCheckModule org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerTest.testCheckModule | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03b org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03b | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration2 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration2 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.xml.parser.CharsetParserTest.testParse2 org.qedeq.kernel.xml.parser.CharsetParserTest.testParse2 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_12 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_12 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_09 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_09 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript2 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript2 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq6 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq6 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_07 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_07 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_06 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_06 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive02 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive02 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative03 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative03 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_03 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_03 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_08 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_08 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L002 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L002 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive01 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive01 | 1 PASS | |
0.07377049
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative03 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative03 | 1 PASS | |
0.040983606
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 | 1 PASS | |
0.040983606
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative02 | 1 PASS | |
0.040983606
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq1 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq1 | 1 PASS | |
0.040983606
|
org.qedeq.kernel.xml.dao.GenerateXmlTest.testGeneration org.qedeq.kernel.xml.dao.GenerateXmlTest.testGeneration | 1 PASS | |
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.module; | |
17 | ||
18 | import org.qedeq.kernel.bo.common.NodeBo; | |
19 | import org.qedeq.kernel.bo.common.QedeqBo; | |
20 | import org.qedeq.kernel.se.base.list.Element; | |
21 | import org.qedeq.kernel.se.base.module.ConditionalProof; | |
22 | import org.qedeq.kernel.se.base.module.FormalProofLineList; | |
23 | import org.qedeq.kernel.se.base.module.FormalProofList; | |
24 | import org.qedeq.kernel.se.base.module.NodeType; | |
25 | import org.qedeq.kernel.se.base.module.Proposition; | |
26 | import org.qedeq.kernel.se.base.module.Reason; | |
27 | import org.qedeq.kernel.se.common.CheckLevel; | |
28 | import org.qedeq.kernel.se.common.ModuleContext; | |
29 | import org.qedeq.kernel.se.dto.module.NodeVo; | |
30 | import org.qedeq.kernel.se.visitor.QedeqNumbers; | |
31 | ||
32 | /** | |
33 | * Business object for node access. | |
34 | * | |
35 | * @author Michael Meyling | |
36 | */ | |
37 | public class KernelNodeBo implements NodeBo, CheckLevel { | |
38 | ||
39 | /** The plain node data. */ | |
40 | private final NodeVo node; | |
41 | ||
42 | /** The module context the node is within. */ | |
43 | private final ModuleContext context; | |
44 | ||
45 | /** Parent module the node is within. */ | |
46 | private final KernelQedeqBo qedeq; | |
47 | ||
48 | /** Herein are the results of various counters for the node. */ | |
49 | private final QedeqNumbers data; | |
50 | ||
51 | /** Are all formal formulas of this node well formed. | |
52 | * See {@link CheckLevel} for value format. */ | |
53 | private int wellFormedCheck = UNCHECKED; | |
54 | ||
55 | /** Is this node been successfully formally proved at least once. | |
56 | * See {@link CheckLevel} for value format. */ | |
57 | private int provedCheck = UNCHECKED; | |
58 | ||
59 | ||
60 | /** | |
61 | * Constructor. | |
62 | * | |
63 | * @param node The plain node data. | |
64 | * @param context The module context the node is within. | |
65 | * @param qedeq Parent module the node is within. | |
66 | * @param data Herein are the results of various counters for the node. | |
67 | */ | |
68 | 18958 | public KernelNodeBo(final NodeVo node, final ModuleContext context, final KernelQedeqBo qedeq, |
69 | final QedeqNumbers data) { | |
70 | 18958 | this.node = node; |
71 | 18958 | this.context = new ModuleContext(context); |
72 | 18958 | this.qedeq = qedeq; |
73 | 18958 | this.data = new QedeqNumbers(data); |
74 | } | |
75 | ||
76 | /** | |
77 | * Get plain node data. | |
78 | * | |
79 | * @return The plain node data. | |
80 | */ | |
81 | 12997 | public NodeVo getNodeVo() { |
82 | 12997 | return node; |
83 | } | |
84 | ||
85 | /** | |
86 | * Get module context the node is within. | |
87 | * | |
88 | * @return The module context the node is within. | |
89 | */ | |
90 | 0 | public ModuleContext getModuleContext() { |
91 | 0 | return context; |
92 | } | |
93 | ||
94 | /** | |
95 | * Get parent module the node is within. | |
96 | * | |
97 | * @return Parent module the node is within. | |
98 | */ | |
99 | 0 | public QedeqBo getParentQedeqBo() { |
100 | 0 | return qedeq; |
101 | } | |
102 | ||
103 | /** | |
104 | * Get parent module the node is within. | |
105 | * | |
106 | * @return Parent module the node is within. | |
107 | */ | |
108 | 157 | public KernelQedeqBo getQedeqBo() { |
109 | 157 | return qedeq; |
110 | } | |
111 | ||
112 | /** | |
113 | * Get the results of various counters for the node. | |
114 | * | |
115 | * @return Herein are the results of various counters for the node. | |
116 | */ | |
117 | 1325 | public QedeqNumbers getNumbers() { |
118 | 1325 | return data; |
119 | } | |
120 | ||
121 | /** | |
122 | * // FIXME 20110316 m31: we have to solve the uniqueness problem if we have several formal proofs | |
123 | * Is the given name a proof line label within this node? | |
124 | * | |
125 | * @param label Look if this node is a proposition that contains this label name. | |
126 | * @return Answer. | |
127 | */ | |
128 | 4759 | public boolean isProofLineLabel(final String label) { |
129 | 4759 | if (label == null || label.length() == 0) { |
130 | 0 | return false; |
131 | } | |
132 | 4759 | final Proposition theorem = getNodeVo().getNodeType().getProposition(); |
133 | 4759 | if (theorem == null) { |
134 | 150 | return false; |
135 | } | |
136 | 4609 | final FormalProofList proofs = theorem.getFormalProofList(); |
137 | 4609 | if (proofs == null) { |
138 | 504 | return false; |
139 | } | |
140 | // iterate through all formal proofs | |
141 | 5240 | for (int i = 0; i < proofs.size(); i++) { |
142 | 4105 | final FormalProofLineList list = proofs.get(i).getFormalProofLineList(); |
143 | 4105 | if (hasProofLineLabel(label, list)) { |
144 | 2970 | return true; |
145 | } | |
146 | } | |
147 | // nowhere found: | |
148 | 1135 | return false; |
149 | } | |
150 | ||
151 | 6637 | private boolean hasProofLineLabel(final String label, final FormalProofLineList list) { |
152 | 6637 | if (list == null) { |
153 | 0 | return false; |
154 | } | |
155 | 40249 | for (int j = 0; j < list.size(); j++) { |
156 | 37470 | if (label.equals(list.get(j).getLabel())) { |
157 | 2598 | return true; |
158 | } | |
159 | 34872 | final Reason reason = list.get(j).getReason(); |
160 | 34872 | if (reason instanceof ConditionalProof) { |
161 | 2904 | final ConditionalProof conditionalProof = (ConditionalProof) reason; |
162 | 2904 | if (conditionalProof.getHypothesis() != null) { |
163 | 2904 | if (label.equals(conditionalProof.getHypothesis().getLabel())) { |
164 | 372 | return true; |
165 | } | |
166 | } | |
167 | 2532 | final FormalProofLineList list2 = conditionalProof.getFormalProofLineList(); |
168 | 2532 | if (hasProofLineLabel(label, list2)) { |
169 | 888 | return true; |
170 | } | |
171 | } | |
172 | } | |
173 | 2779 | return false; |
174 | } | |
175 | ||
176 | /** | |
177 | * Set proved parameter. See {@link #isWellFormed()}. | |
178 | * | |
179 | * @param wellFormedCheck Node well formed state. | |
180 | * See {@link CheckLevel} for parameter format. | |
181 | */ | |
182 | 20171 | public void setWellFormed(final int wellFormedCheck) { |
183 | 20171 | this.wellFormedCheck = wellFormedCheck; |
184 | } | |
185 | ||
186 | 140 | public boolean isWellFormed() { |
187 | 140 | return wellFormedCheck >= SUCCESS; |
188 | } | |
189 | ||
190 | 11761 | public boolean isNotWellFormed() { |
191 | 11761 | return wellFormedCheck < SUCCESS && wellFormedCheck > UNCHECKED; |
192 | } | |
193 | ||
194 | /** | |
195 | * Set proved parameter. See {@link #isProved()}. | |
196 | * | |
197 | * @param provedCheck Node proved state. | |
198 | * See {@link CheckLevel} for parameter format. | |
199 | */ | |
200 | 548 | public void setProved(final int provedCheck) { |
201 | 548 | this.provedCheck = provedCheck; |
202 | } | |
203 | ||
204 | 944 | public boolean isProved() { |
205 | 944 | return provedCheck >= SUCCESS; |
206 | } | |
207 | ||
208 | 81 | public boolean isNotProved() { |
209 | 81 | return provedCheck < SUCCESS && provedCheck > UNCHECKED; |
210 | } | |
211 | ||
212 | 314 | public boolean hasFormula() { |
213 | 314 | return null != getFormula(); |
214 | } | |
215 | ||
216 | 492 | public Element getFormula() { |
217 | 492 | if (getNodeVo() == null || getNodeVo().getNodeType() == null) { |
218 | 0 | return null; |
219 | } | |
220 | 492 | final NodeType nodeType = getNodeVo().getNodeType(); |
221 | 492 | if (nodeType.getProposition() != null) { |
222 | 55 | if (nodeType.getProposition().getFormula() != null) { |
223 | 55 | return nodeType.getProposition().getFormula().getElement(); |
224 | } | |
225 | 0 | return null; |
226 | 437 | } else if (nodeType.getPredicateDefinition() != null) { |
227 | 0 | if (nodeType.getPredicateDefinition().getFormula() != null) { |
228 | 0 | return nodeType.getPredicateDefinition().getFormula().getElement(); |
229 | } | |
230 | 0 | return null; |
231 | 437 | } else if (nodeType.getFunctionDefinition() != null) { |
232 | 0 | if (nodeType.getFunctionDefinition().getFormula() != null) { |
233 | 0 | return nodeType.getFunctionDefinition().getFormula().getElement(); |
234 | } | |
235 | 0 | return null; |
236 | 437 | } else if (nodeType.getAxiom() != null) { |
237 | 437 | if (nodeType.getAxiom().getFormula() != null) { |
238 | 437 | return nodeType.getAxiom().getFormula().getElement(); |
239 | } | |
240 | 0 | return null; |
241 | } | |
242 | 0 | return null; |
243 | } | |
244 | } |
|