Kirk Rader  1.0-SNAPSHOT
Classes | Public Member Functions | Static Public Member Functions | Private Member Functions | Static Private Member Functions | Static Private Attributes | List of all members
us.rader.tt.formula.Formula Class Referenceabstract

A formula of the monadic predicate calculus. More...

Inheritance diagram for us.rader.tt.formula.Formula:
Inheritance graph

Classes

class  ColumnComparator
 Comparator used to sort the columns in a truth table. More...
 

Public Member Functions

abstract boolean evaluate (Map< Expression, Boolean > values)
 Evaluate this formula according to its truth table assuming the given values for its primitive terms. More...
 
final String toDigraph (final int indent) throws IOException
 
final void toDigraph (final PrintStream stream, final int indent)
 Write this formula's syntax tree as a Graphviz digraph. More...
 
final String toTruthTable (final int indent) throws IOException
 
final void toTruthTable (final PrintStream stream, final int indent) throws IOException
 Print this formula's truth table in LaTeX format to the given output stream. More...
 
- Public Member Functions inherited from us.rader.tt.formula.Expression
final boolean equals (final Object obj)
 Base equality on the string representation of a formula. More...
 
abstract Set< ExpressiongetNodes ()
 
abstract Set< ExpressiongetTerminalNodes ()
 
final int hashCode ()
 Base the hash code on the string representation of a formula. More...
 
abstract Expression replaceVariable (Variable boundVariable, Expression factor)
 Replace boundVariable with factor everywhere in this Expression. More...
 
final String toLaTeX () throws IOException
 
abstract void toLaTeX (PrintStream stream)
 Print the LaTeX representation of this object to the given stream. More...
 
- Public Member Functions inherited from us.rader.tt.formula.Graphable
void printDigraph (PrintStream stream, int indent)
 Print the Graphviz nodes and edges for this object to the given stream. More...
 

Static Public Member Functions

static Formula parseFormula (final BufferedReader reader) throws IOException
 Parse the next Formula from the given buffered input stream. More...
 
static Formula parseFormula (final InputStream stream) throws IOException
 Parse the next Formula from the given input stream. More...
 
static Formula parseFormula (final String formula) throws IOException
 Parse the the given term. More...
 
- Static Public Member Functions inherited from us.rader.tt.formula.Expression
static Expression parseFactor (final BufferedReader reader) throws IOException
 Parse the next Expression from the given buffered input stream. More...
 
static Expression parseFactor (final InputStream stream) throws IOException
 Parse the next Expression from the given buffered input stream. More...
 
static Expression parseFactor (final String factor) throws IOException
 Parse the next Expression from the given buffered input stream. More...
 

Private Member Functions

List< Map< Expression, Boolean > > getValues ()
 Return the sequence of values to pass to evaluate in order to compute the truth table for this Formula. More...
 
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. More...
 

Static Private Member Functions

static void expect (final BufferedReader reader, final String expected) throws IOException
 Consume the specified characters. More...
 
static Connective newConnective (final String operator, final Formula operand1, final Formula operand2)
 Parse the next SymbolicNode from the given input stream. More...
 
static Connective parseConnective (final BufferedReader reader) throws IOException
 Parse the next Connective from the given buffered input stream. More...
 
static Identity parseIdentity (final BufferedReader reader) throws IOException
 Parse the next Identity from the given buffered input stream. More...
 
static String parseOperator (final BufferedReader reader, final int c) throws IOException
 Parse the next operator symbol for the current Connective being parsed. More...
 
static Formula parseOtherFormula (final BufferedReader reader, final int c) throws IOException
 Useless helper for parseFormula. More...
 
static Formula parseSymbolicNode (final BufferedReader reader, final int c) throws IOException
 Parse the next SymbolicNode from the given input stream. More...
 

Static Private Attributes

static final int GRAPH_INDENTATION = 3
 Number of spaces to indent each line in a DOT graph or digraph. More...
 
static final String ENCODING = "UTF-8"
 Text encoding for files and streams. More...
 

Additional Inherited Members

- Protected Member Functions inherited from us.rader.tt.formula.Expression
 Expression ()
 Initialize nodeName. More...
 
- Static Protected Member Functions inherited from us.rader.tt.formula.Expression
static Expression parseVariableBindingOperator (final BufferedReader reader, final Class<? extends VariableBindingOperator > type, final char terminator) throws IOException
 Parse the next VariableBindingOperator or Description from the given buffered input stream. More...
 
static void printIndentation (final PrintStream stream, final int indent)
 Print the specified number of spaces to the given stream. More...
 
static int skipWhitespace (final BufferedReader reader) throws IOException
 Discard white space from the given buffered input stream. More...
 
- Protected Attributes inherited from us.rader.tt.formula.Expression
String nodeName
 Graphviz digraph node name. More...
 
- Static Package Functions inherited from us.rader.tt.formula.Expression
 [static initializer]
 

Detailed Description

A formula of the monadic predicate calculus.

Note that the LaTeX output generated by toLaTeX assumes the following preamble:

    \usepackage{graphicx}
    \usepackage{natded}
    \usepackage{amssymb}
    \newcommand{\lognot}{\mathord{\sim}}
    \newcommand{\uq}{\mathord{\bigwedge}}
    \newcommand{\eq}{\mathord{\bigvee}}
    \newcommand{\riota}{\mathrm{\rotatebox[origin=c]{180}{$\iota$}}}

Definition at line 51 of file Formula.java.

Member Function Documentation

◆ evaluate()

abstract boolean us.rader.tt.formula.Formula.evaluate ( Map< Expression, Boolean >  values)
abstract

Evaluate this formula according to its truth table assuming the given values for its primitive terms.

Parameters
valuesMapping of truth values for the primitive terms in this formula.
Returns
The truth value of this formula.

Referenced by us.rader.tt.formula.test.ConditionalTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.NegationTest.evaluateFalseTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.ConditionalTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.evaluateTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.ConditionalTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.NegationTest.evaluateTrueTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateTrueTrueTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateTrueTrueTest(), us.rader.tt.formula.test.ConditionalTest.evaluateTrueTrueTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateTrueTrueTest(), us.rader.tt.formula.Formula.parseSymbolicNode(), and us.rader.tt.formula.Formula.printTruthTableRow().

◆ expect()

static void us.rader.tt.formula.Formula.expect ( final BufferedReader  reader,
final String  expected 
) throws IOException
staticprivate

Consume the specified characters.

This simply checks to see that the next sequence of characters in the buffered input stream matches the expected string and discards them.

Parameters
readerThe buffered input stream.
expectedThe expected string.
Exceptions
IOExceptionThrown if an I/O error occurs.

Definition at line 206 of file Formula.java.

Referenced by us.rader.tt.formula.Formula.parseOperator().

207  {
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  }

◆ getValues()

List<Map<Expression, Boolean> > us.rader.tt.formula.Formula.getValues ( )
private

Return the sequence of values to pass to evaluate in order to compute the truth table for this Formula.

Note that the resulting list must be sorted using the same comparator as that used by toTruthTable,

Returns
The values.
See also
toTruthTable

Definition at line 668 of file Formula.java.

References us.rader.tt.formula.Expression.getTerminalNodes().

Referenced by us.rader.tt.formula.Formula.toTruthTable().

668  {
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  }
abstract Set< Expression > getTerminalNodes()

◆ newConnective()

static Connective us.rader.tt.formula.Formula.newConnective ( final String  operator,
final Formula  operand1,
final Formula  operand2 
)
staticprivate

Parse the next SymbolicNode from the given input stream.

Parameters
operatorThe operator's symbol.
operand1The first operand.
operand2The second operand.
Returns
The Connective

Definition at line 246 of file Formula.java.

Referenced by us.rader.tt.formula.Formula.parseConnective().

247  {
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  }

◆ parseConnective()

static Connective us.rader.tt.formula.Formula.parseConnective ( final BufferedReader  reader) throws IOException
staticprivate

Parse the next Connective from the given buffered input stream.

Parameters
readerThe buffered input stream.
Returns
The Connective
Exceptions
IOExceptionThrown if an I/O error occurs.

Definition at line 285 of file Formula.java.

References us.rader.tt.formula.Formula.newConnective(), us.rader.tt.formula.Formula.parseFormula(), us.rader.tt.formula.Formula.parseOperator(), and us.rader.tt.formula.Expression.skipWhitespace().

Referenced by us.rader.tt.formula.Formula.parseOtherFormula().

286  {
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  }
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 Formula parseFormula(final BufferedReader reader)
Parse the next Formula from the given buffered input stream.
Definition: Formula.java:112
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

◆ parseFormula() [1/3]

static Formula us.rader.tt.formula.Formula.parseFormula ( final BufferedReader  reader) throws IOException
static

Parse the next Formula from the given buffered input stream.

Parameters
readerThe buffered input stream.
Returns
The Formula
Exceptions
IOExceptionThrown if an I/O error occurs.

Definition at line 112 of file Formula.java.

References us.rader.tt.formula.Formula.parseIdentity(), us.rader.tt.formula.Formula.parseOtherFormula(), us.rader.tt.formula.Formula.parseSymbolicNode(), and us.rader.tt.formula.Expression.skipWhitespace().

Referenced by us.rader.tt.formula.test.ConditionalTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateFalseFalseTest(), us.rader.tt.formula.test.NegationTest.evaluateFalseTest(), us.rader.tt.formula.test.ConditionalTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateFalseTrueTest(), us.rader.tt.formula.test.ExistentialGeneralizationTest.evaluateTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.evaluateTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.ConditionalTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateTrueFalseTest(), us.rader.tt.formula.test.NegationTest.evaluateTrueTest(), us.rader.tt.formula.test.DisjunctionTest.evaluateTrueTrueTest(), us.rader.tt.formula.test.ConditionalTest.evaluateTrueTrueTest(), us.rader.tt.formula.test.ConjunctionTest.evaluateTrueTrueTest(), us.rader.tt.formula.test.BiconditionalTest.evaluateTrueTrueTest(), us.rader.tt.formula.test.ExistentialGeneralizationTest.instantiateTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.instantiateTest(), us.rader.tt.formula.test.IdentityTest.missingEqualsTest(), us.rader.tt.formula.test.ExpressionTest.parseBadBoundVariableTest(), us.rader.tt.formula.test.FormulaTest.parseBadFirstCharacterTest(), us.rader.tt.formula.test.FormulaTest.parseBadOperatorTest(), us.rader.tt.formula.Formula.parseConnective(), us.rader.tt.formula.test.FormulaTest.parseEmptyTest(), us.rader.tt.formula.Formula.parseFormula(), us.rader.tt.formula.test.DescriptionTest.parseFormulaTest(), us.rader.tt.formula.test.ExpressionTest.parseMismatchedDelimitersTest(), us.rader.tt.formula.test.ExpressionTest.parseMissingBoundVariableTest(), us.rader.tt.formula.test.FormulaTest.parseMissingFirstOperandTest(), us.rader.tt.formula.test.FormulaTest.parseMissingOperatorTest(), us.rader.tt.formula.test.FormulaTest.parseMissingParenthesisTest(), us.rader.tt.formula.Formula.parseOtherFormula(), us.rader.tt.formula.test.BiconditionalTest.parseUnexpectedEndTest(), us.rader.tt.formula.test.BiconditionalTest.parseUnexpectedTerminatorTest(), us.rader.tt.formula.Expression.parseVariableBindingOperator(), us.rader.tt.formula.test.BiconditionalTest.parseWellFormedTest(), us.rader.tt.formula.test.SentenceTest.replaceVariableTest(), us.rader.tt.formula.test.IdentityTest.replaceVariableTest(), us.rader.tt.formula.test.NegationTest.replaceVariableTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.replaceVariableTest(), us.rader.tt.formula.test.ExistentialGeneralizationTest.replaceVariableTest(), us.rader.tt.formula.test.DisjunctionTest.replaceVariableTest(), us.rader.tt.formula.test.ConditionalTest.replaceVariableTest(), us.rader.tt.formula.test.ConjunctionTest.replaceVariableTest(), us.rader.tt.formula.test.BiconditionalTest.replaceVariableTest(), us.rader.tt.formula.test.IdentityTest.toDigraphTest(), us.rader.tt.formula.test.NegationTest.toDigraphTest(), us.rader.tt.formula.test.ExistentialGeneralizationTest.toDigraphTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.toDigraphTest(), us.rader.tt.formula.test.ConjunctionTest.toDigraphTest(), us.rader.tt.formula.test.ConditionalTest.toDigraphTest(), us.rader.tt.formula.test.DisjunctionTest.toDigraphTest(), us.rader.tt.formula.test.BiconditionalTest.toDigraphTest(), us.rader.tt.formula.test.IdentityTest.toTruthTableTest(), us.rader.tt.formula.test.NegationTest.toTruthTableTest(), us.rader.tt.formula.test.ExistentialGeneralizationTest.toTruthTableTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.toTruthTableTest(), us.rader.tt.formula.test.ConditionalTest.toTruthTableTest(), us.rader.tt.formula.test.ConjunctionTest.toTruthTableTest(), us.rader.tt.formula.test.DisjunctionTest.toTruthTableTest(), us.rader.tt.formula.test.BiconditionalTest.toTruthTableTest(), and us.rader.tt.app.TT.tt().

113  {
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  }
static Formula parseSymbolicNode(final BufferedReader reader, final int c)
Parse the next SymbolicNode from the given input stream.
Definition: Formula.java:460
static int skipWhitespace(final BufferedReader reader)
Discard white space from the given buffered input stream.
static Formula parseOtherFormula(final BufferedReader reader, final int c)
Useless helper for parseFormula.
Definition: Formula.java:411
static Identity parseIdentity(final BufferedReader reader)
Parse the next Identity from the given buffered input stream.
Definition: Formula.java:323

◆ parseFormula() [2/3]

static Formula us.rader.tt.formula.Formula.parseFormula ( final InputStream  stream) throws IOException
static

Parse the next Formula from the given input stream.

Parameters
streamThe input stream.
Returns
The Formula
Exceptions
IOExceptionThrown if an I/O error occurs.
See also
parseFormula

Definition at line 153 of file Formula.java.

References us.rader.tt.formula.Formula.parseFormula().

154  {
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  }
static Formula parseFormula(final BufferedReader reader)
Parse the next Formula from the given buffered input stream.
Definition: Formula.java:112
static final String ENCODING
Text encoding for files and streams.
Definition: Formula.java:99

◆ parseFormula() [3/3]

static Formula us.rader.tt.formula.Formula.parseFormula ( final String  formula) throws IOException
static

Parse the the given term.

Parameters
formulaThe well-formed formula.
Returns
The Formula
Exceptions
IOExceptionThrown if an I/O error occurs.
See also
parseFormula

Definition at line 180 of file Formula.java.

References us.rader.tt.formula.Formula.parseFormula().

181  {
182 
183  try (ByteArrayInputStream stream = new ByteArrayInputStream(
184  formula.getBytes(ENCODING))) {
185 
186  return parseFormula(stream);
187 
188  }
189  }
static Formula parseFormula(final BufferedReader reader)
Parse the next Formula from the given buffered input stream.
Definition: Formula.java:112
static final String ENCODING
Text encoding for files and streams.
Definition: Formula.java:99

◆ parseIdentity()

static Identity us.rader.tt.formula.Formula.parseIdentity ( final BufferedReader  reader) throws IOException
staticprivate

Parse the next Identity from the given buffered input stream.

Parameters
readerThe buffered input stream.
Returns
The Identity
Exceptions
IOExceptionThrown if an I/O error occurs.

Definition at line 323 of file Formula.java.

References us.rader.tt.formula.Expression.parseFactor(), and us.rader.tt.formula.Expression.skipWhitespace().

Referenced by us.rader.tt.formula.Formula.parseFormula().

324  {
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  }
Expression()
Initialize nodeName.
static int skipWhitespace(final BufferedReader reader)
Discard white space from the given buffered input stream.
static Expression parseFactor(final BufferedReader reader)
Parse the next Expression from the given buffered input stream.

◆ parseOperator()

static String us.rader.tt.formula.Formula.parseOperator ( final BufferedReader  reader,
final int  c 
) throws IOException
staticprivate

Parse the next operator symbol for the current Connective being parsed.

Parameters
readerThe buffered input stream.
cThe character most recently read from the input stream.
Returns
The Formula
Exceptions
IOExceptionThrown if an I/O error occurs.

Definition at line 356 of file Formula.java.

References us.rader.tt.formula.Formula.expect().

Referenced by us.rader.tt.formula.Formula.parseConnective().

357  {
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  }
static void expect(final BufferedReader reader, final String expected)
Consume the specified characters.
Definition: Formula.java:206

◆ parseOtherFormula()

static Formula us.rader.tt.formula.Formula.parseOtherFormula ( final BufferedReader  reader,
final int  c 
) throws IOException
staticprivate

Useless helper for parseFormula.

Only exists to shut up an ill-advised SonarQube rule.

Parameters
readerThe buffered input stream.
cThe character most recently read from the input stream.
Returns
The Formula
Exceptions
IOExceptionThrown if an I/O error occurs.

Definition at line 411 of file Formula.java.

References us.rader.tt.formula.Formula.parseConnective(), us.rader.tt.formula.Formula.parseFormula(), and us.rader.tt.formula.Expression.parseVariableBindingOperator().

Referenced by us.rader.tt.formula.Formula.parseFormula().

412  {
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  }
static Formula parseFormula(final BufferedReader reader)
Parse the next Formula from the given buffered input stream.
Definition: Formula.java:112
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

◆ parseSymbolicNode()

static Formula us.rader.tt.formula.Formula.parseSymbolicNode ( final BufferedReader  reader,
final int  c 
) throws IOException
staticprivate

Parse the next SymbolicNode from the given input stream.

Parameters
readerThe input stream.
cThe upper case letter.
Returns
The Formula
Exceptions
IOExceptionThrown if an I/O error occurs.
See also
parseFormula

Definition at line 460 of file Formula.java.

References us.rader.tt.formula.Formula.evaluate(), us.rader.tt.formula.Expression.parseFactor(), and us.rader.tt.formula.Expression.skipWhitespace().

Referenced by us.rader.tt.formula.Formula.parseFormula().

461  {
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  }
static int skipWhitespace(final BufferedReader reader)
Discard white space from the given buffered input stream.
static Expression parseFactor(final BufferedReader reader)
Parse the next Expression from the given buffered input stream.

◆ printTruthTableRow()

void us.rader.tt.formula.Formula.printTruthTableRow ( final PrintStream  stream,
final List< Expression nodes,
final Map< Expression, Boolean >  values,
final int  indent 
)
private

Print one row of the truth table for this formula.

Parameters
streamThe output stream.
nodesThe truth table columns.
valuesThe map of truth values for the terminal nodes in the row to print.
indentThe number of spaces to indent.

Definition at line 713 of file Formula.java.

References us.rader.tt.formula.Formula.evaluate(), and us.rader.tt.formula.Expression.printIndentation().

Referenced by us.rader.tt.formula.Formula.toTruthTable().

715  {
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  }
Expression()
Initialize nodeName.
static void printIndentation(final PrintStream stream, final int indent)
Print the specified number of spaces to the given stream.

◆ toDigraph() [1/2]

final String us.rader.tt.formula.Formula.toDigraph ( final int  indent) throws IOException
Returns
Output generated by a call to toDigraph
Parameters
indentThe number of spaces to indent each line of output.
Exceptions
IOExceptionThrown if an I/O error occurs.

Definition at line 505 of file Formula.java.

References us.rader.tt.formula.Formula.ENCODING.

Referenced by us.rader.tt.formula.test.IdentityTest.toDigraphTest(), us.rader.tt.formula.test.NegationTest.toDigraphTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.toDigraphTest(), us.rader.tt.formula.test.ExistentialGeneralizationTest.toDigraphTest(), us.rader.tt.formula.test.ConditionalTest.toDigraphTest(), us.rader.tt.formula.test.DisjunctionTest.toDigraphTest(), us.rader.tt.formula.test.ConjunctionTest.toDigraphTest(), us.rader.tt.formula.test.BiconditionalTest.toDigraphTest(), and us.rader.tt.app.TT.tt().

505  {
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  }
final String toDigraph(final int indent)
Definition: Formula.java:505
static final String ENCODING
Text encoding for files and streams.
Definition: Formula.java:99

◆ toDigraph() [2/2]

final void us.rader.tt.formula.Formula.toDigraph ( final PrintStream  stream,
final int  indent 
)

Write this formula's syntax tree as a Graphviz digraph.

Parameters
streamThe print stream.
indentThe number of spaces to indent each line of output.

Definition at line 529 of file Formula.java.

References us.rader.tt.formula.Graphable.printDigraph(), and us.rader.tt.formula.Expression.printIndentation().

529  {
530 
531  printIndentation(stream, indent);
532  stream.println("digraph {");
533  printDigraph(stream, indent + GRAPH_INDENTATION);
534  printIndentation(stream, indent);
535  stream.println("}");
536 
537  }
void printDigraph(PrintStream stream, int indent)
Print the Graphviz nodes and edges for this object to the given stream.
static final int GRAPH_INDENTATION
Number of spaces to indent each line in a DOT graph or digraph.
Definition: Formula.java:94
static void printIndentation(final PrintStream stream, final int indent)
Print the specified number of spaces to the given stream.

◆ toTruthTable() [1/2]

final String us.rader.tt.formula.Formula.toTruthTable ( final int  indent) throws IOException
Parameters
indentThe number of spaces to indent each line.
Returns
The truth table for this formula in LaTeX format.
Exceptions
IOExceptionThrown if an I/O error occurs.
See also
toTruthTable

Definition at line 550 of file Formula.java.

References us.rader.tt.formula.Formula.ENCODING.

Referenced by us.rader.tt.formula.test.IdentityTest.missingEqualsTest(), us.rader.tt.formula.test.IdentityTest.toTruthTableTest(), us.rader.tt.formula.test.NegationTest.toTruthTableTest(), us.rader.tt.formula.test.UniversalGeneralizationTest.toTruthTableTest(), us.rader.tt.formula.test.ExistentialGeneralizationTest.toTruthTableTest(), us.rader.tt.formula.test.ConditionalTest.toTruthTableTest(), us.rader.tt.formula.test.DisjunctionTest.toTruthTableTest(), us.rader.tt.formula.test.ConjunctionTest.toTruthTableTest(), us.rader.tt.formula.test.BiconditionalTest.toTruthTableTest(), and us.rader.tt.app.TT.tt().

550  {
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  }
final String toTruthTable(final int indent)
Definition: Formula.java:550
static final String ENCODING
Text encoding for files and streams.
Definition: Formula.java:99

◆ toTruthTable() [2/2]

final void us.rader.tt.formula.Formula.toTruthTable ( final PrintStream  stream,
final int  indent 
) throws IOException

Print this formula's truth table in LaTeX format to the given output stream.

Note that the columns are sorted using ColumnComparator which, in turn, relies on Expression#nodeName.

Parameters
streamThe output stream.
indentThe number of psaces to indent each line.
Exceptions
IOExceptionThrown if an I/O error occurs.
See also
ColumnComparator
evaluate
getValues

Definition at line 585 of file Formula.java.

References us.rader.tt.formula.Expression.getNodes(), us.rader.tt.formula.Expression.getTerminalNodes(), us.rader.tt.formula.Formula.getValues(), us.rader.tt.formula.Expression.printIndentation(), and us.rader.tt.formula.Formula.printTruthTableRow().

586  {
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  }
Expression()
Initialize nodeName.
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
abstract Set< Expression > getNodes()
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 void printIndentation(final PrintStream stream, final int indent)
Print the specified number of spaces to the given stream.
abstract Set< Expression > getTerminalNodes()

Member Data Documentation

◆ ENCODING

final String us.rader.tt.formula.Formula.ENCODING = "UTF-8"
staticprivate

Text encoding for files and streams.

Definition at line 99 of file Formula.java.

Referenced by us.rader.tt.formula.Formula.toDigraph(), and us.rader.tt.formula.Formula.toTruthTable().

◆ GRAPH_INDENTATION

final int us.rader.tt.formula.Formula.GRAPH_INDENTATION = 3
staticprivate

Number of spaces to indent each line in a DOT graph or digraph.

This pointless constant is used simply to shut up an ill-advised SonarQube rule.

Definition at line 94 of file Formula.java.


The documentation for this class was generated from the following file: