View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">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  
16  package org.qedeq.kernel.bo.logic.proof.finder;
17  
18  import org.qedeq.base.utility.EqualsUtility;
19  import org.qedeq.kernel.se.base.list.Element;
20  import org.qedeq.kernel.se.base.module.SubstPred;
21  
22  
23  /**
24   * Usage of rule for substitute predicate variable.
25   *
26   * @author  Michael Meyling
27   */
28  public class SubstPredBo implements SubstPred {
29  
30      /** Reference to previously proven formula. */
31      private int n;
32  
33      /** Function variable that will be substituted. */
34      private Element predicateVariable;
35  
36      /** Replacement formula. */
37      private Element substituteFormula;
38  
39      /**
40       * Constructs an reason.
41       *
42       * @param   n                           Reference to a valid formula.
43       * @param   predicateVariable           Predicate variable that will be substituted.
44       * @param   substituteFormula           Replacement formula.
45       */
46  
47      public SubstPredBo(final int n, final Element predicateVariable,
48              final Element substituteFormula) {
49          this.n = n;
50          this.predicateVariable = predicateVariable;
51          this.substituteFormula = substituteFormula;
52      }
53  
54      public SubstPred getSubstPred() {
55          return this;
56      }
57  
58      public String getReference() {
59          return "" + n;
60      }
61  
62      /**
63       * Set formula reference.
64       *
65       * @param   n   Reference to formula.
66       */
67      public void setN(final int n) {
68          this.n = n;
69      }
70  
71      /**
72       * Get formula reference.
73       *
74       * @return  Reference to formula.
75       */
76      public int getN() {
77          return n;
78      }
79  
80      public String[] getReferences() {
81          return new String[] {getReference()};
82      }
83  
84      public Element getPredicateVariable() {
85          return predicateVariable;
86      }
87  
88      public Element getSubstituteFormula() {
89          return substituteFormula;
90      }
91  
92      public String getName() {
93          return "SubstPred";
94      }
95  
96      public boolean equals(final Object obj) {
97          if (!(obj instanceof SubstPred)) {
98              return false;
99          }
100         final SubstPred other = (SubstPred) obj;
101         return EqualsUtility.equals(getReference(), other.getReference())
102             && EqualsUtility.equals(predicateVariable, other.getPredicateVariable())
103             && EqualsUtility.equals(substituteFormula, other.getSubstituteFormula());
104     }
105 
106     public int hashCode() {
107         return getReference().hashCode()
108             ^ (2 ^ getPredicateVariable().hashCode())
109             ^ (3 ^ getSubstituteFormula().hashCode());
110     }
111 
112     public String toString() {
113         StringBuffer result = new StringBuffer();
114         result.append("SubstPred");
115         result.append(" (");
116         result.append(getReference());
117         if (getPredicateVariable() != null) {
118             result.append(", ");
119             result.append(getPredicateVariable());
120         }
121         if (getSubstituteFormula() != null) {
122             result.append("by ");
123             result.append(getSubstituteFormula());
124         }
125         result.append(")");
126         return result.toString();
127     }
128 
129 }