Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
40   175   29   2.35
20   100   0.73   17
17     1.71  
1    
 
  ConditionalProofVo       Line # 35 40 29 100% 1.0
 
  (10)
 
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.se.dto.module;
17   
18    import org.apache.commons.lang.ArrayUtils;
19    import org.qedeq.base.utility.EqualsUtility;
20    import org.qedeq.kernel.se.base.module.Conclusion;
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.Formula;
24    import org.qedeq.kernel.se.base.module.Hypothesis;
25    import org.qedeq.kernel.se.base.module.Reason;
26   
27   
28    /**
29    * Usage of conditional proof method. If you can derive the proposition A out of
30    * the assumed formulas then the following formula is true:
31    * conjunction of the assumed formulas implies A.
32    *
33    * @author Michael Meyling
34    */
 
35    public class ConditionalProofVo implements ConditionalProof {
36   
37    /** Hypothesis. */
38    private Hypothesis hypothesis;
39   
40    /** Proof lines term. */
41    private FormalProofLineList formalProofLineList;
42   
43    /** Conclusion. */
44    private Conclusion conclusion;
45   
46    /**
47    * Constructs an reason.
48    *
49    * @param hypothesis Free subject variable that will be replaced.
50    * @param proofLines Bound subject variable that will be substituted.
51    * @param conclusion Conclusion.
52    */
 
53  454 toggle public ConditionalProofVo(final Hypothesis hypothesis, final FormalProofLineList proofLines,
54    final Conclusion conclusion) {
55  454 this.hypothesis = hypothesis;
56  454 this.formalProofLineList = proofLines;
57  454 this.conclusion = conclusion;
58    }
59   
60    /**
61    * Default constructor.
62    */
 
63  509 toggle public ConditionalProofVo() {
64    // nothing to do
65    }
66   
 
67  30 toggle public ConditionalProof getConditionalProof() {
68  30 return this;
69    }
70   
 
71  35815 toggle public Hypothesis getHypothesis() {
72  35815 return hypothesis;
73    }
74   
75    /**
76    * Set hypothesis.
77    *
78    * @param hypothesis Reference to formula.
79    */
 
80  470 toggle public void setHypothesis(final Hypothesis hypothesis) {
81  470 this.hypothesis = hypothesis;
82    }
83   
 
84  1 toggle public String[] getReferences() {
85  1 return ArrayUtils.EMPTY_STRING_ARRAY;
86    }
87   
88    /**
89    * Set formal proof lines.
90    *
91    * @param list Proof lines that might use hypothesis.
92    */
 
93  466 toggle public void setFormalProofLineList(final FormalProofLineList list) {
94  466 this.formalProofLineList = list;
95    }
96   
 
97  40042 toggle public FormalProofLineList getFormalProofLineList() {
98  40042 return formalProofLineList;
99    }
100   
 
101  22484 toggle public Conclusion getConclusion() {
102  22484 return conclusion;
103    }
104   
105    /**
106    * Set conclusion.
107    *
108    * @param conclusion New derived formula.
109    */
 
110  474 toggle public void setConclusion(final Conclusion conclusion) {
111  474 this.conclusion = conclusion;
112    }
113   
 
114  1075 toggle public Formula getFormula() {
115  1075 if (conclusion == null) {
116  1 return null;
117    }
118  1074 return conclusion.getFormula();
119    }
120   
 
121  3146 toggle public String getLabel() {
122  3146 if (conclusion == null) {
123  1 return null;
124    }
125  3145 return conclusion.getLabel();
126    }
127   
 
128  293 toggle public String getName() {
129  293 return "CP";
130    }
131   
 
132  3013 toggle public Reason getReason() {
133  3013 return this;
134    }
135   
 
136  47 toggle public boolean equals(final Object obj) {
137  47 if (!(obj instanceof ConditionalProofVo)) {
138  5 return false;
139    }
140  42 final ConditionalProofVo other = (ConditionalProofVo) obj;
141  42 return EqualsUtility.equals(hypothesis, other.hypothesis)
142    && EqualsUtility.equals(formalProofLineList, other.formalProofLineList)
143    && EqualsUtility.equals(conclusion, other.conclusion);
144    }
145   
 
146  58 toggle public int hashCode() {
147  58 return (hypothesis != null ? hypothesis.hashCode() : 0)
148  58 ^ (formalProofLineList != null ? 2 ^ formalProofLineList.hashCode() : 0)
149  58 ^ (conclusion != null ? 4 ^ conclusion.hashCode() : 0);
150    }
151   
 
152  42 toggle public String toString() {
153  42 StringBuffer result = new StringBuffer();
154  42 result.append(getName());
155  42 if (hypothesis != null || formalProofLineList != null || conclusion != null) {
156  28 result.append(" (");
157  28 if (hypothesis != null) {
158  18 result.append("\n");
159  18 result.append(hypothesis);
160    }
161  28 if (formalProofLineList != null) {
162  16 result.append("\n");
163  16 result.append(formalProofLineList);
164    }
165  28 if (conclusion != null) {
166  26 result.append("\n");
167  26 result.append(conclusion);
168    }
169  28 result.append("\n");
170  28 result.append(")");
171    }
172  42 return result.toString();
173    }
174   
175    }