Kirk Rader  1.0-SNAPSHOT
Formula.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.BufferedReader;
20 import java.io.ByteArrayInputStream;
21 import java.io.ByteArrayOutputStream;
22 import java.io.IOException;
23 import java.io.InputStream;
24 import java.io.InputStreamReader;
25 import java.io.PrintStream;
26 import java.util.ArrayList;
27 import java.util.Collections;
28 import java.util.Comparator;
29 import java.util.HashMap;
30 import java.util.LinkedList;
31 import java.util.List;
32 import java.util.Map;
33 import java.util.Set;
34 
35 /**
36  * A formula of the monadic predicate calculus.
37  *
38  * Note that the LaTeX output generated by {@link #toLaTeX} assumes the
39  * following preamble:
40  *
41  * <pre>
42  * \\usepackage{graphicx}
43  * \\usepackage{natded}
44  * \\usepackage{amssymb}
45  * \\newcommand{\\lognot}{\\mathord{\\sim}}
46  * \\newcommand{\\uq}{\\mathord{\\bigwedge}}
47  * \\newcommand{\\eq}{\\mathord{\\bigvee}}
48  * \\newcommand{\\riota}{\\mathrm{\\rotatebox[origin=c]{180}{$\\iota$}}}
49  * </pre>
50  */
51 public abstract class Formula extends Expression {
52 
53  /**
54  * `Comparator` used to sort the columns in a truth table.
55  *
56  * Note: SonarQube issue suppressed because this private comparator will
57  * never be used in a serializable context.
58  *
59  * @see Formula#toTruthTable
60  * @see Formula#getValues
61  */
62  private static final class ColumnComparator
63  implements Comparator<Expression> { // NOSONAR
64 
65  /**
66  * Sort expressions by their node names.
67  *
68  * This works because:
69  *
70  * 1. Constituent nodes of an expression are parsed self-recursively and
71  * in left-to-right order.
72  *
73  * 2. the logic for generating {@link Expression#nodeName} results in
74  * monotonically increasing names according to
75  * `String.compareTo(String)`.
76  *
77  * This comparator will need to be re-written if either of those
78  * assumptions are invalidated by subsequent code changes.
79  */
80  @Override
81  public int compare(final Expression o1, final Expression o2) {
82 
83  return o1.nodeName.compareTo(o2.nodeName);
84 
85  }
86  }
87 
88  /**
89  * Number of spaces to indent each line in a DOT graph or digraph.
90  *
91  * This pointless constant is used simply to shut up an ill-advised
92  * SonarQube rule.
93  */
94  private static final int GRAPH_INDENTATION = 3;
95 
96  /**
97  * Text encoding for files and streams.
98  */
99  private static final String ENCODING = "UTF-8";
100 
101  /**
102  * Parse the next {@link Formula} from the given buffered input stream.
103  *
104  * @param reader
105  * The buffered input stream.
106  *
107  * @return The {@link Formula}
108  *
109  * @throws IOException
110  * Thrown if an I/O error occurs.
111  */
112  public static Formula parseFormula(final BufferedReader reader)
113  throws IOException {
114 
115  final int c = skipWhitespace(reader);
116 
117  if (c == -1) {
118 
119  throw new SyntaxError("unexpected end of input");
120 
121  }
122 
123  if (c == ':' || Character.isLowerCase(c)) {
124 
125  reader.reset();
126  return parseIdentity(reader);
127 
128  }
129 
130  if (Character.isUpperCase(c)) {
131 
132  return parseSymbolicNode(reader, c);
133 
134  }
135 
136  return parseOtherFormula(reader, c);
137 
138  }
139 
140  /**
141  * Parse the next {@link Formula} from the given input stream.
142  *
143  * @param stream
144  * The input stream.
145  *
146  * @return The {@link Formula}
147  *
148  * @throws IOException
149  * Thrown if an I/O error occurs.
150  *
151  * @see #parseFormula
152  */
153  public static Formula parseFormula(final InputStream stream)
154  throws IOException {
155 
156  try (InputStreamReader streamReader = new InputStreamReader(stream,
157  ENCODING)) {
158 
159  try (BufferedReader reader = new BufferedReader(streamReader)) {
160 
161  return parseFormula(reader);
162 
163  }
164  }
165  }
166 
167  /**
168  * Parse the the given term.
169  *
170  * @param formula
171  * The well-formed formula.
172  *
173  * @return The {@link Formula}
174  *
175  * @throws IOException
176  * Thrown if an I/O error occurs.
177  *
178  * @see #parseFormula
179  */
180  public static Formula parseFormula(final String formula)
181  throws IOException {
182 
183  try (ByteArrayInputStream stream = new ByteArrayInputStream(
184  formula.getBytes(ENCODING))) {
185 
186  return parseFormula(stream);
187 
188  }
189  }
190 
191  /**
192  * Consume the specified characters.
193  *
194  * This simply checks to see that the next sequence of characters in the
195  * buffered input stream matches the expected string and discards them.
196  *
197  * @param reader
198  * The buffered input stream.
199  *
200  * @param expected
201  * The expected string.
202  *
203  * @throws IOException
204  * Thrown if an I/O error occurs.
205  */
206  private static void expect(final BufferedReader reader,
207  final String expected) throws IOException {
208 
209  final int length = expected.length();
210  reader.mark(length);
211  final char[] buffer = new char[length];
212  final int actualLength = reader.read(buffer, 0, length);
213 
214  if (actualLength != length) {
215 
216  throw new SyntaxError(String.format(
217  "unexpected end of input parsing \"%s\"", expected));
218 
219  }
220 
221  final String actualString = new String(buffer);
222 
223  if (!expected.equals(actualString)) {
224 
225  reader.reset();
226  throw new SyntaxError(String.format("expected \"%s\", got \"%s\"",
227  expected, actualString));
228 
229  }
230  }
231 
232  /**
233  * Parse the next {@link SymbolicNode} from the given input stream.
234  *
235  * @param operator
236  * The operator's symbol.
237  *
238  * @param operand1
239  * The first operand.
240  *
241  * @param operand2
242  * The second operand.
243  *
244  * @return The {@link Connective}
245  */
246  private static Connective newConnective(final String operator,
247  final Formula operand1, final Formula operand2) {
248 
249  switch (operator) {
250 
251  case "&":
252 
253  return new Conjunction(operand1, operand2);
254 
255  case "|":
256 
257  return new Disjunction(operand1, operand2);
258 
259  case "->":
260 
261  return new Conditional(operand1, operand2);
262 
263  case "<->":
264 
265  return new Biconditional(operand1, operand2);
266 
267  default:
268 
269  throw new IllegalStateException("reached unreachable code!");
270 
271  }
272  }
273 
274  /**
275  * Parse the next {@link Connective} from the given buffered input stream.
276  *
277  * @param reader
278  * The buffered input stream.
279  *
280  * @return The {@link Connective}
281  *
282  * @throws IOException
283  * Thrown if an I/O error occurs.
284  */
285  private static Connective parseConnective(final BufferedReader reader)
286  throws IOException {
287 
288  final Formula operand1 = parseFormula(reader);
289  int c = skipWhitespace(reader);
290 
291  if (c == -1) {
292 
293  throw new SyntaxError(
294  "unexpected end of input while parsing connective");
295 
296  }
297 
298  final String operator = parseOperator(reader, c);
299  final Formula operand2 = parseFormula(reader);
300  c = skipWhitespace(reader);
301 
302  if (c != ')') {
303 
304  throw new SyntaxError(
305  String.format("missing ')' after %s", operator));
306 
307  }
308 
309  return newConnective(operator, operand1, operand2);
310  }
311 
312  /**
313  * Parse the next {@link Identity} from the given buffered input stream.
314  *
315  * @param reader
316  * The buffered input stream.
317  *
318  * @return The {@link Identity}
319  *
320  * @throws IOException
321  * Thrown if an I/O error occurs.
322  */
323  private static Identity parseIdentity(final BufferedReader reader)
324  throws IOException {
325 
326  final Expression factor1 = parseFactor(reader);
327  final int c = skipWhitespace(reader);
328 
329  if (c != '=') {
330 
331  throw new SyntaxError(String.format("expected '=', got '%s'",
332  Character.toString((char) c)));
333 
334  }
335 
336  final Expression factor2 = parseFactor(reader);
337  return new Identity(factor1, factor2);
338 
339  }
340 
341  /**
342  * Parse the next operator symbol for the current {@link Connective} being
343  * parsed.
344  *
345  * @param reader
346  * The buffered input stream.
347  *
348  * @param c
349  * The character most recently read from the input stream.
350  *
351  * @return The {@link Formula}
352  *
353  * @throws IOException
354  * Thrown if an I/O error occurs.
355  */
356  private static String parseOperator(final BufferedReader reader,
357  final int c) throws IOException {
358 
359  String operator;
360 
361  switch (c) {
362 
363  case '&':
364 
365  operator = "&";
366  break;
367 
368  case '|':
369 
370  operator = "|";
371  break;
372 
373  case '-':
374 
375  expect(reader, ">");
376  operator = "->";
377  break;
378 
379  case '<':
380 
381  expect(reader, "->");
382  operator = "<->";
383  break;
384 
385  default:
386 
387  throw new SyntaxError(String.format(
388  "invalid character for connective, \"%s\"",
389  Character.toString((char) c)));
390 
391  }
392  return operator;
393  }
394 
395  /**
396  * Useless helper for {@link #parseFormula}.
397  *
398  * Only exists to shut up an ill-advised SonarQube rule.
399  *
400  * @param reader
401  * The buffered input stream.
402  *
403  * @param c
404  * The character most recently read from the input stream.
405  *
406  * @return The {@link Formula}
407  *
408  * @throws IOException
409  * Thrown if an I/O error occurs.
410  */
411  private static Formula parseOtherFormula(final BufferedReader reader,
412  final int c) throws IOException {
413 
414  switch (c) {
415 
416  case '{':
417 
418  return (Formula) parseVariableBindingOperator(reader,
419  UniversalGeneralization.class, '}');
420 
421  case '[':
422 
423  return (Formula) parseVariableBindingOperator(reader,
424  ExistentialGeneralization.class, ']');
425 
426  case '(':
427 
428  return parseConnective(reader);
429 
430  case '~':
431 
432  return new Negation(parseFormula(reader));
433 
434  default:
435 
436  reader.reset();
437  throw new SyntaxError(
438  String.format("Invalid initial character \"%s\"",
439  Character.toString((char) c)));
440 
441  }
442  }
443 
444  /**
445  * Parse the next {@link SymbolicNode} from the given input stream.
446  *
447  * @param reader
448  * The input stream.
449  *
450  * @param c
451  * The upper case letter.
452  *
453  * @return The {@link Formula}
454  *
455  * @throws IOException
456  * Thrown if an I/O error occurs.
457  *
458  * @see #parseFormula
459  */
460  private static Formula parseSymbolicNode(final BufferedReader reader,
461  final int c) throws IOException {
462 
463  final int f = skipWhitespace(reader);
464 
465  if (f == -1) {
466 
467  return new Sentence(Character.toString((char) c));
468 
469  }
470 
471  if (f == ':' || Character.isLowerCase((char) f)) {
472 
473  reader.reset();
474  return new Predicate(Character.toString((char) c),
475  parseFactor(reader));
476 
477  }
478 
479  reader.reset();
480  return new Sentence(Character.toString((char) c));
481 
482  }
483 
484  /**
485  * Evaluate this formula according to its truth table assuming the given
486  * values for its primitive terms.
487  *
488  * @param values
489  * Mapping of truth values for the primitive terms in this
490  * formula.
491  *
492  * @return The truth value of this formula.
493  */
494  public abstract boolean evaluate(Map<Expression, Boolean> values);
495 
496  /**
497  * @return Output generated by a call to {@link #toDigraph}
498  *
499  * @param indent
500  * The number of spaces to indent each line of output.
501  *
502  * @throws IOException
503  * Thrown if an I/O error occurs.
504  */
505  public final String toDigraph(final int indent) throws IOException {
506 
507  try (ByteArrayOutputStream stream = new ByteArrayOutputStream()) {
508 
509  try (PrintStream printStream = new PrintStream(stream, false,
510  ENCODING)) {
511 
512  toDigraph(printStream, indent);
513  printStream.flush();
514  return new String(stream.toByteArray(), ENCODING);
515 
516  }
517  }
518  }
519 
520  /**
521  * Write this formula's syntax tree as a Graphviz digraph.
522  *
523  * @param stream
524  * The print stream.
525  *
526  * @param indent
527  * The number of spaces to indent each line of output.
528  */
529  public final void toDigraph(final PrintStream stream, final int indent) {
530 
531  printIndentation(stream, indent);
532  stream.println("digraph {");
533  printDigraph(stream, indent + GRAPH_INDENTATION);
534  printIndentation(stream, indent);
535  stream.println("}");
536 
537  }
538 
539  /**
540  * @param indent
541  * The number of spaces to indent each line.
542  *
543  * @return The truth table for this formula in LaTeX format.
544  *
545  * @throws IOException
546  * Thrown if an I/O error occurs.
547  *
548  * @see #toTruthTable
549  */
550  public final String toTruthTable(final int indent) throws IOException {
551 
552  try (ByteArrayOutputStream stream = new ByteArrayOutputStream()) {
553 
554  try (PrintStream printStream = new PrintStream(stream, false,
555  ENCODING)) {
556 
557  toTruthTable(printStream, indent);
558  stream.flush();
559  return new String(stream.toByteArray(), ENCODING);
560 
561  }
562  }
563  }
564 
565  /**
566  * Print this formula's truth table in LaTeX format to the given output
567  * stream.
568  *
569  * Note that the columns are sorted using {@link ColumnComparator} which, in
570  * turn, relies on {@link Expression#nodeName}.
571  *
572  * @param stream
573  * The output stream.
574  *
575  * @param indent
576  * The number of psaces to indent each line.
577  *
578  * @throws IOException
579  * Thrown if an I/O error occurs.
580  *
581  * @see ColumnComparator
582  * @see #evaluate
583  * @see #getValues
584  */
585  public final void toTruthTable(final PrintStream stream, final int indent)
586  throws IOException {
587 
588  final List<Map<Expression, Boolean>> values = getValues();
589  final List<Expression> nodes = new ArrayList<>();
590  nodes.addAll(getNodes());
591  Collections.sort(nodes, new ColumnComparator());
592  printIndentation(stream, indent);
593  stream.print("\\begin{array}{");
594  final int columns = nodes.size();
595  boolean first = true;
596 
597  for (int count = 0; count < columns; ++count) {
598 
599  if (count == columns - 1) {
600 
601  stream.print("|");
602 
603  }
604 
605  stream.print("c");
606 
607  }
608 
609  stream.println("}");
610 
611  for (final Expression column : nodes) {
612 
613  if (first) {
614 
615  printIndentation(stream, indent);
616  first = false;
617 
618  } else {
619 
620  stream.print(" & ");
621 
622  }
623 
624  stream.print(column.toLaTeX());
625 
626  }
627 
628  stream.println(" \\\\");
629  stream.println("\\hline \\\\");
630 
631  final Set<Expression> terminalNodes = getTerminalNodes();
632  final int rows = 1 << terminalNodes.size();
633  first = true;
634 
635  for (int row = 0; row < rows; ++row) {
636 
637  if (first) {
638 
639  first = false;
640 
641  } else {
642 
643  stream.println(" \\\\");
644 
645  }
646 
647  printTruthTableRow(stream, nodes, values.get(row), indent);
648 
649  }
650 
651  stream.println();
652  printIndentation(stream, indent);
653  stream.println("\\end{array}");
654 
655  }
656 
657  /**
658  * Return the sequence of values to pass to {@link #evaluate} in order to
659  * compute the truth table for this {@link Formula}.
660  *
661  * Note that the resulting list must be sorted using the same comparator as
662  * that used by {@link #toTruthTable},
663  *
664  * @return The values.
665  *
666  * @see #toTruthTable
667  */
668  private List<Map<Expression, Boolean>> getValues() {
669 
670  final List<Expression> terminalNodes = new ArrayList<>();
671  terminalNodes.addAll(getTerminalNodes());
672  Collections.sort(terminalNodes, new ColumnComparator());
673  final int columns = terminalNodes.size();
674  final int rows = 1 << columns;
675  final List<Map<Expression, Boolean>> values = new LinkedList<>();
676  final int highBit = columns - 1;
677 
678  for (int row = 0; row < rows; ++row) {
679 
680  final Map<Expression, Boolean> map = new HashMap<>();
681  values.add(map);
682 
683  for (int column = 0; column < columns; ++column) {
684 
685  final int bitPosition = highBit - column;
686  final int bitMask = 1 << bitPosition;
687  final int bit = row & bitMask;
688  map.put(terminalNodes.get(column), 0 == bit);
689 
690  }
691  }
692 
693  return values;
694 
695  }
696 
697  /**
698  * Print one row of the truth table for this formula.
699  *
700  * @param stream
701  * The output stream.
702  *
703  * @param nodes
704  * The truth table columns.
705  *
706  * @param values
707  * The map of truth values for the terminal nodes in the row to
708  * print.
709  *
710  * @param indent
711  * The number of spaces to indent.
712  */
713  private void printTruthTableRow(final PrintStream stream,
714  final List<Expression> nodes, final Map<Expression, Boolean> values,
715  final int indent) {
716 
717  boolean first = true;
718 
719  for (final Expression term : nodes) {
720 
721  final Formula formula = (Formula) term;
722 
723  if (first) {
724 
725  printIndentation(stream, indent);
726  first = false;
727 
728  } else {
729 
730  stream.print(" & ");
731 
732  }
733 
734  stream.print(formula.evaluate(values) ? "T" : "F");
735 
736  }
737  }
738 
739 }
void printDigraph(PrintStream stream, int indent)
Print the Graphviz nodes and edges for this object to the given stream.
String nodeName
Graphviz digraph node name.
Definition: Expression.java:90
Comparator used to sort the columns in a truth table.
Definition: Formula.java:62
void printTruthTableRow(final PrintStream stream, final List< Expression > nodes, final Map< Expression, Boolean > values, final int indent)
Print one row of the truth table for this formula.
Definition: Formula.java:713
static Formula parseSymbolicNode(final BufferedReader reader, final int c)
Parse the next SymbolicNode from the given input stream.
Definition: Formula.java:460
static String parseOperator(final BufferedReader reader, final int c)
Parse the next operator symbol for the current Connective being parsed.
Definition: Formula.java:356
static int skipWhitespace(final BufferedReader reader)
Discard white space from the given buffered input stream.
static void expect(final BufferedReader reader, final String expected)
Consume the specified characters.
Definition: Formula.java:206
An atomic sentence represented by an upper-case letter (P, Q etc.).
Definition: Sentence.java:22
static Expression parseFactor(final BufferedReader reader)
Parse the next Expression from the given buffered input stream.
abstract Set< Expression > getNodes()
final String toDigraph(final int indent)
Definition: Formula.java:505
final String toTruthTable(final int indent)
Definition: Formula.java:550
static Formula parseFormula(final BufferedReader reader)
Parse the next Formula from the given buffered input stream.
Definition: Formula.java:112
static Formula parseFormula(final String formula)
Parse the the given term.
Definition: Formula.java:180
final void toTruthTable(final PrintStream stream, final int indent)
Print this formula&#39;s truth table in LaTeX format to the given output stream.
Definition: Formula.java:585
abstract boolean evaluate(Map< Expression, Boolean > values)
Evaluate this formula according to its truth table assuming the given values for its primitive terms...
"Inclusive or" operator.
static final int GRAPH_INDENTATION
Number of spaces to indent each line in a DOT graph or digraph.
Definition: Formula.java:94
static Formula parseFormula(final InputStream stream)
Parse the next Formula from the given input stream.
Definition: Formula.java:153
final void toDigraph(final PrintStream stream, final int indent)
Write this formula&#39;s syntax tree as a Graphviz digraph.
Definition: Formula.java:529
Objects with unique Graphviz node names.
Definition: Expression.java:32
static Formula parseOtherFormula(final BufferedReader reader, final int c)
Useless helper for parseFormula.
Definition: Formula.java:411
int compare(final Expression o1, final Expression o2)
Sort expressions by their node names.
Definition: Formula.java:81
static Expression parseVariableBindingOperator(final BufferedReader reader, final Class<? extends VariableBindingOperator > type, final char terminator)
Parse the next VariableBindingOperator or Description from the given buffered input stream...
static Connective parseConnective(final BufferedReader reader)
Parse the next Connective from the given buffered input stream.
Definition: Formula.java:285
"Equivalence" operator.
Exception thrown when a syntax error is detected while parsing an Expression.
Definition: Expression.java:41
A formula of the monadic predicate calculus.
Definition: Formula.java:51
static Identity parseIdentity(final BufferedReader reader)
Parse the next Identity from the given buffered input stream.
Definition: Formula.java:323
List< Map< Expression, Boolean > > getValues()
Return the sequence of values to pass to evaluate in order to compute the truth table for this Formul...
Definition: Formula.java:668
static Connective newConnective(final String operator, final Formula operand1, final Formula operand2)
Parse the next SymbolicNode from the given input stream.
Definition: Formula.java:246
static final String ENCODING
Text encoding for files and streams.
Definition: Formula.java:99
static void printIndentation(final PrintStream stream, final int indent)
Print the specified number of spaces to the given stream.
abstract Set< Expression > getTerminalNodes()