SubstFreeVo.java
001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002  *
003  * Copyright 2000-2011,  Michael Meyling <mime@qedeq.org>.
004  *
005  * "Hilbert II" is free software; you can redistribute
006  * it and/or modify it under the terms of the GNU General Public
007  * License as published by the Free Software Foundation; either
008  * version 2 of the License, or (at your option) any later version.
009  *
010  * This program is distributed in the hope that it will be useful,
011  * but WITHOUT ANY WARRANTY; without even the implied warranty of
012  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013  * GNU General Public License for more details.
014  */
015 
016 package org.qedeq.kernel.se.dto.module;
017 
018 import org.qedeq.base.utility.EqualsUtility;
019 import org.qedeq.kernel.se.base.list.Element;
020 import org.qedeq.kernel.se.base.module.SubstFree;
021 
022 
023 /**
024  * Usage of rule for substitute free subject variable.
025  *
026  @author  Michael Meyling
027  */
028 public class SubstFreeVo implements SubstFree {
029 
030     /** Reference to previously proven formula. */
031     private String reference;
032 
033     /** Free subject variable that will be replaced. */
034     private Element subjectVariable;
035 
036     /** Replacement term. */
037     private Element substituteTerm;
038 
039     /**
040      * Constructs an reason.
041      *
042      @param   reference                   Reference to a valid formula.
043      @param   subjectVariable             Bound subject variable that will be substituted.
044      @param   substituteTerm              Replacement term.
045      */
046 
047     public SubstFreeVo(final String reference, final Element subjectVariable,
048             final Element substituteTerm) {
049         this.reference = reference;
050         this.subjectVariable = subjectVariable;
051         this.substituteTerm = substituteTerm;
052     }
053 
054     /**
055      * Default constructor.
056      */
057     public SubstFreeVo() {
058         // nothing to do
059     }
060 
061     public String getReference() {
062         return reference;
063     }
064 
065     /**
066      * Set formula reference.
067      *
068      @param   reference   Reference to formula.
069      */
070     public void setReference(final String reference) {
071         this.reference = reference;
072     }
073 
074     public String[] getReferences() {
075         if (reference == null || reference.length() == 0) {
076             return new String[] {};
077         else {
078             return new String[] {reference };
079         }
080     }
081 
082     public Element getSubjectVariable() {
083         return subjectVariable;
084     }
085 
086     /**
087      * Get subject variable that will be substituted.
088      *
089      @param   subjectVariable Subject variable that will be replaced.
090      */
091     public void setSubjectVariable(final Element subjectVariable) {
092         this.subjectVariable = subjectVariable;
093     }
094 
095     public Element getSubstituteTerm() {
096         return substituteTerm;
097     }
098 
099     /**
100      * Set substitution term.
101      *
102      @param   substituteTerm  New term.
103      */
104     public void setSubstituteTerm(final Element substituteTerm) {
105         this.substituteTerm = substituteTerm;
106     }
107 
108     public String getName() {
109         return "SubstFree";
110     }
111 
112     public boolean equals(final Object obj) {
113         if (!(obj instanceof SubstFreeVo)) {
114             return false;
115         }
116         final SubstFreeVo other = (SubstFreeVoobj;
117         return EqualsUtility.equals(reference, other.reference)
118             && EqualsUtility.equals(subjectVariable, other.subjectVariable)
119             && EqualsUtility.equals(substituteTerm, other.substituteTerm);
120     }
121 
122     public int hashCode() {
123         return (reference != null ? reference.hashCode() 0)
124             (subjectVariable != null ^ subjectVariable.hashCode() 0)
125             (substituteTerm != null ^ substituteTerm.hashCode() 0);
126     }
127 
128     public String toString() {
129         StringBuffer result = new StringBuffer();
130         result.append("SubstFunc");
131         if (reference != null || subjectVariable != null
132                 || substituteTerm != null) {
133             result.append(" (");
134             boolean w = false;
135             if (reference != null) {
136                 result.append(reference);
137                 w = true;
138             }
139             if (subjectVariable != null) {
140                 if (w) {
141                     result.append(", ");
142                 }
143                 result.append(subjectVariable);
144                 w = true;
145             }
146             if (substituteTerm != null) {
147                 if (w) {
148                     result.append(", ");
149                 }
150                 result.append("by ");
151                 result.append(substituteTerm);
152                 w = true;
153             }
154             result.append(")");
155         }
156         return result.toString();
157     }
158 
159 }