Kirk Rader  1.0-SNAPSHOT
VariableBindingOperator.java
Go to the documentation of this file.
1 /*
2  * Copyright 2016 Kirk Rader
3  *
4  * Licensed under the Apache License, Version 2.0 (the "License");
5  * you may not use this file except in compliance with the License.
6  * You may obtain a copy of the License at
7  *
8  * http://www.apache.org/licenses/LICENSE-2.0
9  *
10  * Unless required by applicable law or agreed to in writing, software
11  * distributed under the License is distributed on an "AS IS" BASIS,
12  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13  * See the License for the specific language governing permissions and
14  * limitations under the License.
15  */
16 
17 package us.rader.tt.formula;
18 
19 import java.io.PrintStream;
20 import java.util.Map;
21 import java.util.Set;
22 
23 /**
24  * Generalization.
25  */
26 public abstract class VariableBindingOperator extends Operator {
27 
28  /**
29  * The variable bound by this operator.
30  */
31  protected Variable variable;
32 
33  /**
34  * Initialize {@link #variable} and {@link Operator}.
35  *
36  * @param variable
37  * {@link #variable}
38  *
39  * @param operand
40  * Formula in which {@link #variable} is bound.
41  */
42  protected VariableBindingOperator(final Variable variable, final Formula operand) {
43 
44  super(operand);
45  this.variable = variable;
46 
47  }
48 
49  /**
50  * @see Formula#evaluate
51  */
52  @Override
53  public final boolean evaluate(final Map<Expression, Boolean> values) {
54 
55  throw new IllegalArgumentException("Variable binding operators cannot be evaluated");
56 
57  }
58 
59  /**
60  * @see Expression#getTerminalNodes
61  */
62  @Override
63  public Set<Expression> getTerminalNodes() {
64 
65  final Set<Expression> terminalNodes = super.getTerminalNodes();
66  terminalNodes.addAll(variable.getTerminalNodes());
67  return terminalNodes;
68 
69  }
70 
71  /**
72  * Return the {@link Formula} that results from instantiating this operator.
73  *
74  * @param factor
75  * The new free value for this operator's bound variable.
76  *
77  * @return The instantiated {@link Formula}.
78  */
79  public final Formula instantiate(final Expression factor) {
80 
81  return (Formula) operands.get(0).replaceVariable(variable, factor);
82 
83  }
84 
85  /**
86  * @see Graphable#printDigraph
87  */
88  @Override
89  public void printDigraph(final PrintStream stream, final int indent) {
90 
91  super.printDigraph(stream, indent);
92  printIndentation(stream, indent);
93  stream.print(nodeName);
94  stream.print(" [ label=\"");
95  stream.print(getOperator());
96  stream.println("\" ]");
97  stream.print(nodeName);
98  stream.print(" -> ");
99  stream.println(operands.get(0).nodeName);
100 
101  }
102 
103  /**
104  * @see Formula#toLaTeX
105  */
106  @Override
107  public final void toLaTeX(final PrintStream stream) {
108 
109  printLaTeXOperator(stream);
110  operands.get(0).toLaTeX(stream);
111 
112  }
113 
114  /**
115  * @return String representation of this formula.
116  */
117  @Override
118  public final String toString() {
119 
120  return getOperator() + operands.get(0).toString();
121 
122  }
123 
124 }
abstract String getOperator()
String nodeName
Graphviz digraph node name.
Definition: Expression.java:90
final void toLaTeX(final PrintStream stream)
A variable (lower-case alphabetic character) of the monadic predicate calculus.
Definition: Variable.java:27
abstract void printLaTeXOperator(PrintStream stream)
final boolean evaluate(final Map< Expression, Boolean > values)
List< Formula > operands
The connective&#39;s operands.
Definition: Operator.java:33
Objects with unique Graphviz node names.
Definition: Expression.java:32
final Formula instantiate(final Expression factor)
Return the Formula that results from instantiating this operator.
Set< Expression > getTerminalNodes()
Definition: Variable.java:58
A formula of the monadic predicate calculus.
Definition: Formula.java:51
A non-terminal Formula of the monadic predicate calculus.
Definition: Operator.java:28
void printDigraph(final PrintStream stream, final int indent)
Variable variable
The variable bound by this operator.
VariableBindingOperator(final Variable variable, final Formula operand)
Initialize variable and Operator.
static void printIndentation(final PrintStream stream, final int indent)
Print the specified number of spaces to the given stream.