|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
FormulaUtility | Line # 33 | 215 | 144 | 72.7% |
0.7270408
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||
(74) | |||
Result | |||
0.6020408
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin | 1 PASS | |
0.5739796
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin2 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin2 | 1 PASS | |
0.5739796
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin3 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin3 | 1 PASS | |
0.50510204
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin2 org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPlugin2 | 1 PASS | |
0.50510204
|
org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPluginFast org.qedeq.kernel.bo.service.logic.SimpleProofFinderPluginTest.testPluginFast | 1 PASS | |
0.4744898
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin | 1 PASS | |
0.46173468
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck6 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck6 | 1 PASS | |
0.4234694
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind | 1 PASS | |
0.4234694
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind2 org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind2 | 1 PASS | |
0.4234694
|
org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind3 org.qedeq.kernel.bo.logic.proof.finder.ProofFinderImplTest.testFind3 | 1 PASS | |
0.40561223
|
org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin4 org.qedeq.kernel.bo.service.logic.FormalProofCheckerPluginTest.testPlugin4 | 1 PASS | |
0.37244898
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck4 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck4 | 1 PASS | |
0.37244898
|
org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck1 org.qedeq.kernel.bo.logic.proof.checker.ProofCheckerTest.testCheck1 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative04 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative04 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript1 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript1 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript1 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript1 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative04 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative04 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1b org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1b | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq5 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq5 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.heuristic.DynamicHeuristicCheckerPluginTest.testQedeqSampleScript1 org.qedeq.kernel.bo.service.heuristic.DynamicHeuristicCheckerPluginTest.testQedeqSampleScript1 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript2 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqSetTheoryScript2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive04 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive04 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v2 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegativeGeneration2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v1 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L001_v1 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L003 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L003 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration1 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_05 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_05 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq4 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq4 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerTest.testCheckModule org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerTest.testCheckModule | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3b org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3b | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03b org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive03b | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration2 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative06 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration4 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration4 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript2 org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPluginTest.testQedeqLogicScript2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative08 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 org.qedeq.kernel.bo.latex.GenerateLatexTest.testGeneration2 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq6 org.qedeq.kernel.bo.service.control.QedeqBoFactoryTest.testCreateStringQedeq6 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_07 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_07 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_06 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_06 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive02 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive02 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative03 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative03 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative05 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_08 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_08 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3 org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 org.qedeq.kernel.bo.latex.GenerateLatexTest.testNegative07 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L002 org.qedeq.kernel.bo.service.latex.Qedeq2LatexTest.testQ2L002 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative03 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative03 | 1 PASS | |
0.1734694
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive01 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testPositive01 | 1 PASS | |
0.16836734
|
org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative02 org.qedeq.kernel.bo.service.logic.QedeqBoFormalLogicCheckerDirectTest.testNegative02 | 1 PASS | |
0.16836734
|
org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative02 org.qedeq.kernel.bo.logic.wf.FormulaCheckerContextTest.testNegative02 | 1 PASS | |
0.15306123
|
org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceOperatorVariableTest.test_Positive01 org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceOperatorVariableTest.test_Positive01 | 1 PASS | |
0.1377551
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_02 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_02 | 1 PASS | |
0.1377551
|
org.qedeq.kernel.xml.parser.CharsetParserTest.testParse1 org.qedeq.kernel.xml.parser.CharsetParserTest.testParse1 | 1 PASS | |
0.1377551
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_04 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_04 | 1 PASS | |
0.1377551
|
org.qedeq.kernel.xml.parser.CharsetParserTest.testParse2 org.qedeq.kernel.xml.parser.CharsetParserTest.testParse2 | 1 PASS | |
0.1377551
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_09 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_09 | 1 PASS | |
0.1377551
|
org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_03 org.qedeq.kernel.bo.service.control.ModuleConstantsExistenceCheckerTest.testModuleConstantsExistenceChecker_03 | 1 PASS | |
0.12244898
|
org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive04 org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive04 | 1 PASS | |
0.12244898
|
org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive02 org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive02 | 1 PASS | |
0.11989796
|
org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive01 org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive01 | 1 PASS | |
0.11734694
|
org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive03 org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive03 | 1 PASS | |
0.11734694
|
org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive05 org.qedeq.kernel.bo.logic.common.FormulaUtilityReplaceSubjectVariableQuantifierTest.testClassTermPositive05 | 1 PASS | |
0.10714286
|
org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3c org.qedeq.kernel.bo.service.unicode.GenerateUtf8Test.testGeneration3c | 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.logic.common; | |
17 | ||
18 | import org.qedeq.base.utility.Enumerator; | |
19 | import org.qedeq.base.utility.EqualsUtility; | |
20 | import org.qedeq.kernel.se.base.list.Atom; | |
21 | import org.qedeq.kernel.se.base.list.Element; | |
22 | import org.qedeq.kernel.se.base.list.ElementList; | |
23 | import org.qedeq.kernel.se.dto.list.DefaultAtom; | |
24 | import org.qedeq.kernel.se.dto.list.DefaultElementList; | |
25 | import org.qedeq.kernel.se.dto.list.ElementSet; | |
26 | ||
27 | ||
28 | /** | |
29 | * Some useful static methods for formulas and terms. | |
30 | * | |
31 | * @author Michael Meyling | |
32 | */ | |
33 | public final class FormulaUtility implements Operators { | |
34 | ||
35 | /** | |
36 | * Constructor. | |
37 | * | |
38 | */ | |
39 | 0 | private FormulaUtility() { |
40 | // nothing to do here | |
41 | } | |
42 | ||
43 | /** | |
44 | * Is {@link Element} a subject variable? | |
45 | * | |
46 | * @param element Element to look onto. | |
47 | * @return Is it a subject variable? | |
48 | */ | |
49 | 1560011 | public static final boolean isSubjectVariable(final Element element) { |
50 | 1560011 | if (element == null || !element.isList() || element.getList() == null) { |
51 | 878927 | return false; |
52 | } | |
53 | 681084 | final ElementList list = element.getList(); |
54 | 681084 | if (list.getOperator().equals(SUBJECT_VARIABLE)) { |
55 | 240054 | if (list.size() != 1) { |
56 | 0 | return false; |
57 | } | |
58 | 240054 | final Element first = element.getList().getElement(0); |
59 | 240054 | if (first == null || !first.isAtom() || first.getAtom() == null) { |
60 | 0 | return false; |
61 | } | |
62 | 240054 | final Atom atom = first.getAtom(); |
63 | 240054 | if (atom.getString() == null || atom.getAtom().getString() == null |
64 | || atom.getString().length() == 0) { | |
65 | 0 | return false; |
66 | } | |
67 | } else { | |
68 | 441030 | return false; |
69 | } | |
70 | 240054 | return true; |
71 | } | |
72 | ||
73 | /** | |
74 | * Is {@link Element} a predicate variable? | |
75 | * | |
76 | * @param element Element to look onto. | |
77 | * @return Is it a predicate variable? | |
78 | */ | |
79 | 35 | public static final boolean isPredicateVariable(final Element element) { |
80 | 35 | return isOperator(PREDICATE_VARIABLE, element); |
81 | } | |
82 | ||
83 | /** | |
84 | * Is {@link Element} a proposition variable? | |
85 | * | |
86 | * @param element Element to look onto. | |
87 | * @return Is it a proposition variable? | |
88 | */ | |
89 | 109415 | public static final boolean isPropositionVariable(final Element element) { |
90 | 109415 | return isOperator(PREDICATE_VARIABLE, element) && element.getList().size() <= 1; |
91 | } | |
92 | ||
93 | /** | |
94 | * Is {@link Element} a function variable? | |
95 | * | |
96 | * @param element Element to look onto. | |
97 | * @return Is it a function variable? | |
98 | */ | |
99 | 0 | public static final boolean isFunctionVariable(final Element element) { |
100 | 0 | return isOperator(FUNCTION_VARIABLE, element); |
101 | } | |
102 | ||
103 | /** | |
104 | * Is {@link Element} a predicate constant? | |
105 | * | |
106 | * @param element Element to look onto. | |
107 | * @return Is it a predicate constant? | |
108 | */ | |
109 | 15902 | public static final boolean isPredicateConstant(final Element element) { |
110 | 15902 | return isOperator(PREDICATE_CONSTANT, element); |
111 | } | |
112 | ||
113 | /** | |
114 | * Is {@link Element} a function constant? | |
115 | * | |
116 | * @param element Element to look onto. | |
117 | * @return Is it a function constant? | |
118 | */ | |
119 | 15889 | public static final boolean isFunctionConstant(final Element element) { |
120 | 15889 | return isOperator(FUNCTION_CONSTANT, element); |
121 | } | |
122 | ||
123 | /** | |
124 | * Is the given element an list with given operator and has as first element an non empty | |
125 | * string atom? | |
126 | * | |
127 | * @param operator Operator. | |
128 | * @param element Check this element. | |
129 | * @return Check successful? | |
130 | */ | |
131 | 141241 | public static boolean isOperator(final String operator, |
132 | final Element element) { | |
133 | 141241 | return isOperator(operator, element, 0); |
134 | } | |
135 | ||
136 | /** | |
137 | * Is the given element an list with given operator and has as first element an non empty | |
138 | * string atom? | |
139 | * | |
140 | * @param operator Operator. | |
141 | * @param element Check this element. | |
142 | * @param minArguments Minimum number of arguments (beside the first string atom). | |
143 | * @return Check successful? | |
144 | */ | |
145 | 141241 | private static boolean isOperator(final String operator, |
146 | final Element element, final int minArguments) { | |
147 | 141241 | if (element == null || !element.isList() || element.getList() == null) { |
148 | 60 | return false; |
149 | } | |
150 | 141181 | final ElementList list = element.getList(); |
151 | 141181 | if (list.getOperator().equals(operator)) { |
152 | 58544 | if (list.size() < 1 + minArguments) { |
153 | 0 | return false; |
154 | } | |
155 | 58544 | final Element first = element.getList().getElement(0); |
156 | 58544 | if (first == null || !first.isAtom() || first.getAtom() == null) { |
157 | 0 | return false; |
158 | } | |
159 | 58544 | final Atom atom = first.getAtom(); |
160 | 58544 | if (atom.getString() == null || atom.getAtom().getString() == null |
161 | || atom.getString().length() == 0) { | |
162 | 0 | return false; |
163 | } | |
164 | } else { | |
165 | 82637 | return false; |
166 | } | |
167 | 58544 | return true; |
168 | } | |
169 | ||
170 | /** | |
171 | * Return all free subject variables of an element. | |
172 | * | |
173 | * @param element Work on this element. | |
174 | * @return All free subject variables. | |
175 | */ | |
176 | 701848 | public static final ElementSet getFreeSubjectVariables(final Element element) { |
177 | 701848 | final ElementSet free = new ElementSet(); |
178 | 701848 | if (isSubjectVariable(element)) { |
179 | 184280 | free.add(element); |
180 | 517568 | } else if (element.isList()) { |
181 | 303699 | final ElementList list = element.getList(); |
182 | 303699 | if (isBindingOperator(list)) { |
183 | 49304 | for (int i = 1; i < list.size(); i++) { |
184 | 24970 | free.union(getFreeSubjectVariables(list.getElement(i))); |
185 | } | |
186 | 24334 | free.remove(list.getElement(0)); |
187 | } else { | |
188 | 768986 | for (int i = 0; i < list.size(); i++) { |
189 | 489621 | free.union(getFreeSubjectVariables(list.getElement(i))); |
190 | } | |
191 | } | |
192 | } | |
193 | 701848 | return free; |
194 | } | |
195 | ||
196 | /** | |
197 | * Return all bound subject variables of an element. | |
198 | * | |
199 | * @param element Work on this element. | |
200 | * @return All bound subject variables. | |
201 | */ | |
202 | 999248 | public static final ElementSet getBoundSubjectVariables(final Element element) { |
203 | 999248 | final ElementSet bound = new ElementSet(); |
204 | 999248 | if (element.isList()) { |
205 | 548306 | ElementList list = element.getList(); |
206 | // if operator is quantifier or class term | |
207 | 548306 | if (isBindingOperator(list)) { |
208 | // add subject variable to bound list | |
209 | 26162 | bound.add(list.getElement(0)); |
210 | // add all bound variables of sub-elements | |
211 | 53043 | for (int i = 1; i < list.size(); i++) { |
212 | 26881 | bound.union(getBoundSubjectVariables( |
213 | list.getElement(i))); | |
214 | } | |
215 | } else { | |
216 | // add all bound variables of sub-elements | |
217 | 1293525 | for (int i = 0; i < list.size(); i++) { |
218 | 771381 | bound.union(getBoundSubjectVariables(list.getElement(i))); |
219 | } | |
220 | } | |
221 | } | |
222 | 999248 | return bound; |
223 | } | |
224 | ||
225 | /** | |
226 | * Return all subject variables of an element. | |
227 | * | |
228 | * @param element Work on this element. | |
229 | * @return All subject variables. | |
230 | */ | |
231 | 632 | public static final ElementSet getSubjectVariables(final Element element) { |
232 | 632 | final ElementSet all = new ElementSet(); |
233 | 632 | if (isSubjectVariable(element)) { |
234 | 54 | all.add(element); |
235 | 578 | } else if (element.isList()) { |
236 | 578 | final ElementList list = element.getList(); |
237 | 632 | for (int i = 1; i < list.size(); i++) { |
238 | 54 | all.union(getSubjectVariables(list.getElement(i))); |
239 | } | |
240 | } | |
241 | 632 | return all; |
242 | } | |
243 | ||
244 | /** | |
245 | * Return all predicate variables of an element. The arguments are normalized to subject | |
246 | * variables "x_1", "x_2" and so on. | |
247 | * | |
248 | * @param element Work on this element. | |
249 | * @return All predicate variables of that formula. | |
250 | */ | |
251 | 0 | public static final ElementSet getPredicateVariables(final Element element) { |
252 | 0 | final ElementSet all = new ElementSet(); |
253 | 0 | if (isPredicateVariable(element)) { |
254 | 0 | final ElementList pred = element.getList(); |
255 | 0 | final DefaultElementList normalized = new DefaultElementList(pred.getOperator()); |
256 | 0 | normalized.add(pred.getElement(0)); |
257 | 0 | for (int i = 1; i < pred.size(); i++) { |
258 | 0 | normalized.add(createSubjectVariable("x_" + i)); |
259 | } | |
260 | 0 | all.add(normalized); |
261 | 0 | } else if (element.isList()) { |
262 | 0 | final ElementList list = element.getList(); |
263 | 0 | for (int i = 0; i < list.size(); i++) { |
264 | 0 | all.union(getPredicateVariables(list.getElement(i))); |
265 | } | |
266 | } | |
267 | 0 | return all; |
268 | } | |
269 | ||
270 | /** | |
271 | * Return all proposition variables of an element. That are predicate variables with | |
272 | * arity zero. | |
273 | * | |
274 | * @param element Work on this element. | |
275 | * @return All proposition variables of that formula. | |
276 | */ | |
277 | 109415 | public static final ElementSet getPropositionVariables(final Element element) { |
278 | 109415 | final ElementSet all = new ElementSet(); |
279 | 109415 | if (isPropositionVariable(element)) { |
280 | 58498 | all.add(element); |
281 | 50917 | } else if (element.isList()) { |
282 | 50857 | final ElementList list = element.getList(); |
283 | 152535 | for (int i = 0; i < list.size(); i++) { |
284 | 101678 | all.union(getPropositionVariables(list.getElement(i))); |
285 | } | |
286 | } | |
287 | 109415 | return all; |
288 | } | |
289 | ||
290 | /** | |
291 | * Return all part formulas of an element. | |
292 | * | |
293 | * @param element Work on this element. | |
294 | * @return All part formulas of that element. | |
295 | */ | |
296 | 35 | public static final ElementSet getPartFormulas(final Element element) { |
297 | 35 | final ElementSet all = new ElementSet(); |
298 | 35 | if (element == null || element.isAtom()) { |
299 | 0 | return all; |
300 | } | |
301 | 35 | final ElementList list = element.getList(); |
302 | 35 | if (isPredicateVariable(list)) { |
303 | 22 | all.add(element); |
304 | 13 | } else if (isPredicateConstant(list)) { |
305 | 0 | all.add(list); |
306 | 13 | } else if (Operators.CONJUNCTION_OPERATOR.equals(list.getOperator()) |
307 | || Operators.DISJUNCTION_OPERATOR.equals(list.getOperator()) | |
308 | || Operators.NEGATION_OPERATOR.equals(list.getOperator()) | |
309 | || Operators.IMPLICATION_OPERATOR.equals(list.getOperator()) | |
310 | || Operators.EQUIVALENCE_OPERATOR.equals(list.getOperator()) | |
311 | ) { | |
312 | 13 | all.add(list); |
313 | 39 | for (int i = 0; i < list.size(); i++) { |
314 | 26 | all.union(getPartFormulas(list.getElement(i))); |
315 | } | |
316 | 0 | } else if (isBindingOperator(list)) { |
317 | 0 | all.add(list); |
318 | 0 | for (int i = 0; i < list.size(); i++) { |
319 | 0 | all.union(getPartFormulas(list.getElement(i))); |
320 | } | |
321 | 0 | } else if (isSubjectVariable(list)) { |
322 | // this is no formula | |
323 | 0 | } else if (isFunctionVariable(list)) { |
324 | // this is no formula | |
325 | 0 | } else if (isFunctionConstant(list)) { |
326 | // this is no formula | |
327 | } else { | |
328 | 0 | for (int i = 0; i < list.size(); i++) { |
329 | 0 | all.union(getPartFormulas(list.getElement(i))); |
330 | } | |
331 | } | |
332 | 35 | return all; |
333 | } | |
334 | ||
335 | /** | |
336 | * Has the given list an operator that binds a subject variable? | |
337 | * | |
338 | * @param list Check for this operator. | |
339 | * @return Has it an binding operator with subject variable? | |
340 | */ | |
341 | 852428 | public static boolean isBindingOperator(final ElementList list) { |
342 | 852428 | final String operator = list.getOperator(); |
343 | 852428 | if (operator == null || list.size() <= 0 || !isSubjectVariable(list.getElement(0))) { |
344 | 801806 | return false; |
345 | } | |
346 | 50622 | return operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR) |
347 | || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR) | |
348 | || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR) | |
349 | || operator.equals(CLASS_OP); | |
350 | } | |
351 | ||
352 | /** | |
353 | * Get relative context of the first difference between the given elements. | |
354 | * | |
355 | * @param first First element. | |
356 | * @param second Second element. | |
357 | * @return Relative path (beginning with ".") of first difference. | |
358 | */ | |
359 | 18 | public static String getDifferenceLocation(final Element first, final Element second) { |
360 | 18 | final StringBuffer diff = new StringBuffer(); |
361 | 18 | equal(diff, first, second); |
362 | 18 | return diff.toString(); |
363 | } | |
364 | ||
365 | /** | |
366 | * Is there any difference between the two elements? If so, the context has the difference | |
367 | * position. | |
368 | * | |
369 | * @param firstContext Context (might be relative) for first element. | |
370 | * @param first First element. | |
371 | * @param second Second element. | |
372 | * @return Are both elements equal? | |
373 | */ | |
374 | 185 | private static boolean equal(final StringBuffer firstContext, |
375 | final Element first, final Element second) { | |
376 | 185 | if (first == null) { |
377 | 0 | return second == null; |
378 | } | |
379 | 185 | if (second == null) { |
380 | 0 | return false; |
381 | } | |
382 | 185 | if (first.isAtom()) { |
383 | 66 | if (!second.isAtom()) { |
384 | 0 | return false; |
385 | } | |
386 | 66 | return EqualsUtility.equals(first.getAtom().getString(), second.getAtom().getString()); |
387 | } | |
388 | 119 | if (second.isAtom()) { |
389 | 0 | return false; |
390 | } | |
391 | 119 | if (!EqualsUtility.equals(first.getList().getOperator(), second.getList().getOperator())) { |
392 | 6 | return false; |
393 | } | |
394 | 113 | if (first.getList().size() != second.getList().size()) { |
395 | 2 | return false; |
396 | } | |
397 | 230 | for (int i = 0; i < first.getList().size(); i++) { |
398 | 167 | final int length = firstContext.length(); |
399 | 167 | firstContext.append(".getList().getElement(" + i + ")"); |
400 | 167 | if (!equal(firstContext, first.getList().getElement(i), |
401 | second.getList().getElement(i))) { | |
402 | 48 | return false; |
403 | } | |
404 | 119 | firstContext.setLength(length); |
405 | } | |
406 | 63 | return true; |
407 | } | |
408 | ||
409 | /** | |
410 | * Replace bound subject variables at given occurrence by another one. | |
411 | * If goal occurrence number is below number of occurrences within the formula nothing is | |
412 | * changed. Original parts are used, so don't modify the formulas directly. | |
413 | * | |
414 | * @param originalSubjectVariable Replace this subject variable. | |
415 | * @param replacementSubjectVariable By this subject variable. | |
416 | * @param formulaElement This is the formula we work on. | |
417 | * @param occurrenceGoal This is the binding occurrence number. | |
418 | * @param occurreneCurrent Counter how much occurrences we already had. | |
419 | * @return Formula with replaced subject variables. | |
420 | */ | |
421 | 681 | public static Element replaceSubjectVariableQuantifier(final Element originalSubjectVariable, |
422 | final Element replacementSubjectVariable, final Element formulaElement, | |
423 | final int occurrenceGoal, final Enumerator occurreneCurrent) { | |
424 | 681 | if (formulaElement.isAtom()) { |
425 | 243 | return formulaElement; |
426 | } | |
427 | 438 | final ElementList formula = formulaElement.getList(); |
428 | 438 | if (occurreneCurrent.getNumber() > occurrenceGoal) { |
429 | 15 | return formula.copy(); |
430 | } | |
431 | 423 | final ElementList result = new DefaultElementList(formula.getOperator()); |
432 | 423 | if (isBindingOperator(formula) |
433 | && formula.getElement(0).equals(originalSubjectVariable)) { | |
434 | 56 | occurreneCurrent.increaseNumber(); |
435 | // System.out.println("found: " + occurreneCurrent); | |
436 | 56 | if (occurrenceGoal == occurreneCurrent.getNumber()) { |
437 | // System.out.println("match: " + occurrenceGoal); | |
438 | 43 | return formula.replace(originalSubjectVariable, |
439 | replacementSubjectVariable); | |
440 | } | |
441 | } | |
442 | 1007 | for (int i = 0; i < formula.size(); i++) { |
443 | 627 | result.add(replaceSubjectVariableQuantifier(originalSubjectVariable, |
444 | replacementSubjectVariable, formula.getElement(i), occurrenceGoal, | |
445 | occurreneCurrent)); | |
446 | } | |
447 | 380 | return result; |
448 | } | |
449 | ||
450 | /** | |
451 | * Replace function or predicate variable by given term or formula. Old parts are not copied | |
452 | * but taken directly - so don't modify the formulas! | |
453 | * | |
454 | * @param formula Formula we want the replacement take place. | |
455 | * @param operatorVariable Predicate variable or function variable with only subject | |
456 | * variables as arguments. | |
457 | * @param replacement Replacement formula or term with matching subject variables. | |
458 | * <code>operatorVariable</code> might have some subject variables | |
459 | * that are not in <code>replacement</code> and vice versa. | |
460 | * @return Formula where operatorVariable was replaced. | |
461 | */ | |
462 | 75877 | public static Element replaceOperatorVariable(final Element formula, |
463 | final Element operatorVariable, final Element replacement) { | |
464 | 75877 | if (formula == null || operatorVariable == null || replacement == null |
465 | || formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) { | |
466 | 3 | return formula; |
467 | } | |
468 | 75874 | final ElementList f = formula.getList(); |
469 | 75874 | final ElementList ov = operatorVariable.getList(); |
470 | 75874 | final ElementList r = replacement.getList(); |
471 | // check elementary preconditions | |
472 | // System.out.println("ov.size=" + ov.size()); | |
473 | 75874 | if (f.size() < 1 || ov.size() < 1) { |
474 | // System.out.println("failed elementary conditions"); | |
475 | 0 | return formula; |
476 | } | |
477 | // construct replacement formula with meta variables | |
478 | 75874 | Element rn = r; |
479 | 75907 | for (int i = 1; i < ov.size(); i++) { |
480 | 33 | rn = rn.replace(ov.getElement(i), createMeta(ov.getElement(i))); |
481 | } | |
482 | 75874 | return replaceOperatorVariableMeta(formula, operatorVariable, rn); |
483 | } | |
484 | ||
485 | /** | |
486 | * Replace function or predicate variable by given term or formula. Original parts are used - | |
487 | * so don't modify them! | |
488 | * | |
489 | * @param formula Formula we want the replacement take place. | |
490 | * @param operatorVariable Predicate variable or function variable with only subject | |
491 | * variables as arguments. | |
492 | * @param replacement Replacement formula or term with meta variables instead of | |
493 | * subject variables to replace (matching | |
494 | * <code>operatorVariable</code>). | |
495 | * @return Formula where operatorVariable was replaced. | |
496 | */ | |
497 | 1460058 | private static Element replaceOperatorVariableMeta(final Element formula, |
498 | final Element operatorVariable, final Element replacement) { | |
499 | 1460058 | if (formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) { |
500 | 358440 | return formula; |
501 | } | |
502 | 1101618 | final ElementList f = formula.getList(); |
503 | 1101618 | final ElementList ov = operatorVariable.getList(); |
504 | 1101618 | final ElementList r = replacement.getList(); |
505 | 1101618 | if (f.size() < 1 || ov.size() < 1) { |
506 | 0 | return formula.copy(); |
507 | } | |
508 | 1101618 | ElementList result; |
509 | 1101618 | if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size() |
510 | && f.getElement(0).equals(ov.getElement(0))) { | |
511 | // replace meta variables by matching entries | |
512 | 230419 | result = r; |
513 | 230481 | for (int i = 1; i < ov.size(); i++) { |
514 | 62 | result = (ElementList) result.replace(createMeta(ov.getElement(i)), |
515 | replaceOperatorVariableMeta(f.getElement(i), operatorVariable, replacement)); | |
516 | } | |
517 | } else { | |
518 | 871199 | result = new DefaultElementList(f.getOperator()); |
519 | 2255321 | for (int i = 0; i < f.size(); i++) { |
520 | 1384122 | result.add(replaceOperatorVariableMeta(f.getElement(i), operatorVariable, |
521 | replacement)); | |
522 | } | |
523 | } | |
524 | 1101618 | return result; |
525 | } | |
526 | ||
527 | /** | |
528 | * Checks if a given term or formula contains a given function or predicate variable with same | |
529 | * size. | |
530 | * | |
531 | * @param formula Formula we want the replacement take place. | |
532 | * @param operatorVariable Predicate variable or function variable with only subject | |
533 | * variables as arguments. | |
534 | * @return Do we have any occurrence? | |
535 | */ | |
536 | 164 | public static boolean containsOperatorVariable(final Element formula, |
537 | final Element operatorVariable) { | |
538 | 164 | if (formula == null || formula.isAtom() || operatorVariable == null |
539 | || operatorVariable.isAtom()) { | |
540 | 0 | return false; |
541 | } | |
542 | 164 | final ElementList f = formula.getList(); |
543 | 164 | final ElementList ov = operatorVariable.getList(); |
544 | 164 | if (f.size() < 1 || ov.size() < 1) { |
545 | 164 | return f.equals(ov); |
546 | } | |
547 | 0 | if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size() |
548 | && f.getElement(0).equals(ov.getElement(0))) { | |
549 | 0 | return true; |
550 | } | |
551 | 0 | for (int i = 0; i < f.size(); i++) { |
552 | 0 | if (containsOperatorVariable(f.getElement(i), operatorVariable)) { |
553 | 0 | return true; |
554 | } | |
555 | } | |
556 | 0 | return false; |
557 | } | |
558 | ||
559 | /** | |
560 | * Test if operator occurrence in formula matches always to a formula that contains no subject | |
561 | * variable that is in the given ElementSet of bound subject variables.. | |
562 | * | |
563 | * @param formula Formula we want to test the condition. | |
564 | * @param operatorVariable Predicate variable or function variable with only subject | |
565 | * variables as arguments. | |
566 | * @param bound Set of subject variables that are tabu. | |
567 | * @return Formula test was successful. | |
568 | */ | |
569 | 4123 | public static boolean testOperatorVariable(final Element formula, |
570 | final Element operatorVariable, final ElementSet bound) { | |
571 | 4123 | if (formula.isAtom() || operatorVariable.isAtom()) { |
572 | 1140 | return true; |
573 | } | |
574 | 2983 | final ElementList f = formula.getList(); |
575 | 2983 | final ElementList ov = operatorVariable.getList(); |
576 | 2983 | if (f.size() < 1 || ov.size() < 1) { |
577 | 0 | return true; |
578 | } | |
579 | 2983 | boolean ok = true; |
580 | 2983 | if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size() |
581 | && f.getElement(0).equals(ov.getElement(0))) { | |
582 | 578 | if (!getSubjectVariables(f).intersection(bound).isEmpty()) { |
583 | 0 | return false; |
584 | } | |
585 | } else { | |
586 | 6238 | for (int i = 0; ok && i < f.size(); i++) { |
587 | 3833 | ok = testOperatorVariable(f.getElement(i), operatorVariable, bound); |
588 | } | |
589 | } | |
590 | 2983 | return ok; |
591 | } | |
592 | ||
593 | /** | |
594 | * Is the given formula a simple implication like A => B. | |
595 | * | |
596 | * @param formula Check this formula. | |
597 | * @return Is the formula a simple implication? | |
598 | */ | |
599 | 25552187 | public static boolean isImplication(final Element formula) { |
600 | 25552187 | if (formula.isAtom()) { |
601 | 0 | return false; |
602 | } | |
603 | 25552187 | final ElementList f = formula.getList(); |
604 | 25552187 | return Operators.IMPLICATION_OPERATOR.equals(f.getList().getOperator()) |
605 | && f.getList().size() == 2; | |
606 | } | |
607 | ||
608 | /** | |
609 | * Create meta variable for subject variable. | |
610 | * | |
611 | * @param subjectVariable Subject variable, we want to have a meta variable for. | |
612 | * @return Resulting meta variable. If we didn't got a subject variable we just | |
613 | * return the original. | |
614 | */ | |
615 | 95 | public static Element createMeta(final Element subjectVariable) { |
616 | 95 | if (!isSubjectVariable(subjectVariable)) { |
617 | 0 | return subjectVariable; |
618 | } | |
619 | 95 | final DefaultElementList result = new DefaultElementList(META_VARIABLE); |
620 | 95 | result.add(subjectVariable.getList().getElement(0)); |
621 | 95 | return result; |
622 | } | |
623 | ||
624 | /** | |
625 | * Create subject variable out of variable name. | |
626 | * | |
627 | * @param subjectVariableName Subject variable name. | |
628 | * @return Resulting subject variable. | |
629 | */ | |
630 | 0 | public static Element createSubjectVariable(final String subjectVariableName) { |
631 | 0 | final DefaultElementList result = new DefaultElementList(SUBJECT_VARIABLE); |
632 | 0 | result.add(new DefaultAtom(subjectVariableName)); |
633 | 0 | return result; |
634 | } | |
635 | ||
636 | /** | |
637 | * Create predicate variable out of variable name with no further arguments. | |
638 | * | |
639 | * @param predicateVariableName Predicate variable name. | |
640 | * @return Resulting predicate variable. | |
641 | */ | |
642 | 0 | public static Element createPredicateVariable(final String predicateVariableName) { |
643 | 0 | final DefaultElementList result = new DefaultElementList(PREDICATE_VARIABLE); |
644 | 0 | result.add(new DefaultAtom(predicateVariableName)); |
645 | 0 | return result; |
646 | } | |
647 | ||
648 | } |
|