de.uni_tuebingen.sfb.lichtenstein.binarytrees
Class LispToMonaParser

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.binarytrees.LispToMonaParser

All Implemented Interfaces:

FormulaParser

public class LispToMonaParser
extends Object
implements FormulaParser

A formula in fsq’s lisp-like format, which can parse itself into the required format.

Author:

Stephan Kepser , Hendrik Maryns

Field Summary

Fields inherited from interface de.uni_tuebingen.sfb.lichtenstein.binarytrees.FormulaParser

CATEGORY, CONJUNCTION, CONTAINMENT, DISJUNCTION, DOMINANCE, EQUALITY, FIRST_ORDER_EXISTENTIAL, FIRST_ORDER_UNIVERSAL, FUNCTION, IMMEDIATE_DOMINANCE, IMMEDIATE_PRECEDENCE, IMPLICATION, LEMMA, MORPHOLOGY, NEGATION, PRECEDENCE, PROPER_DOMINANCE, SECOND_ORDER_EXISTENTIAL, SECOND_ORDER_UNIVERSAL, SENTENCE, WORD

Constructor Summary

LispToMonaParser(String formula, Map<String,String> predicates)
Create a new Formula Parser which outputs Mona code for the given formula.

Method Summary

de.uni_tuebingen.sfb.lichtenstein.binarytrees.DString	getNextSubformula()
de.uni_tuebingen.sfb.lichtenstein.binarytrees.DString	getToken()
String	parse() Parse the formula.
String	parseConjunction()
String	parseContainment(String contained, String container)
String	parseDisjunction()
String	parseEquality(String var1, String var2)
String	parseFirstOrderExistentialQuantification()
String	parseFirstOrderUniversalQuantification()
String	parseImmediateDominance(String parent, String child)
String	parseImplication()
String	parseNegation()
String	parsePrecedence(String first, String second)
String	parsePredicate(String node, String predicate)
String	parseProperDominance(String ancestor, String descendant)
String	parseSecondOrderExistentialQantification()
String	parseSecondOrderUniversalQuantification()
String	randomVarName() Create a random variable name.
String	toString() Just return the underlying formula string.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

LispToMonaParser

public LispToMonaParser(String formula,
                        Map<String,String> predicates)

Create a new Formula Parser which outputs Mona code for the given formula.

Parameters:

formula - The formula to parse.

predicates - The list of predicates that occur in the formula.

Method Detail

getToken

public de.uni_tuebingen.sfb.lichtenstein.binarytrees.DString getToken()
                                                               throws LispFormulaParseException

Throws:

LispFormulaParseException

getNextSubformula

public de.uni_tuebingen.sfb.lichtenstein.binarytrees.DString getNextSubformula()
                                                                        throws LispFormulaParseException

Throws:

LispFormulaParseException

randomVarName

public String randomVarName()

Create a random variable name. This is important for not having different variables with the same name in the Mona file.

Postcondition:

The varNumber is increased by one. | new.varNumber == varNumber + 1

Returns:

A variable name that has not been used yet.

parse

public String parse()
             throws LispFormulaParseException

Parse the formula.

Specified by:

parse in interface FormulaParser

Throws:

LispFormulaParseException - [CAN] If the formula has an incorrect syntax.

parseImmediateDominance

public String parseImmediateDominance(String parent,
                                      String child)

parseProperDominance

public String parseProperDominance(String ancestor,
                                   String descendant)

parsePrecedence

public String parsePrecedence(String first,
                              String second)

parseEquality

public String parseEquality(String var1,
                            String var2)

parsePredicate

public String parsePredicate(String node,
                             String predicate)

parseContainment

public String parseContainment(String contained,
                               String container)

parseNegation

public String parseNegation()
                     throws LispFormulaParseException

Throws:

LispFormulaParseException

parseConjunction

public String parseConjunction()
                        throws LispFormulaParseException

Throws:

LispFormulaParseException

parseDisjunction

public String parseDisjunction()
                        throws LispFormulaParseException

Throws:

LispFormulaParseException

parseImplication

public String parseImplication()
                        throws LispFormulaParseException

Throws:

LispFormulaParseException

parseFirstOrderExistentialQuantification

public String parseFirstOrderExistentialQuantification()
                                                throws LispFormulaParseException

Throws:

LispFormulaParseException

parseFirstOrderUniversalQuantification

public String parseFirstOrderUniversalQuantification()
                                              throws LispFormulaParseException

Throws:

LispFormulaParseException

parseSecondOrderExistentialQantification

public String parseSecondOrderExistentialQantification()
                                                throws LispFormulaParseException

Throws:

LispFormulaParseException

parseSecondOrderUniversalQuantification

public String parseSecondOrderUniversalQuantification()
                                               throws LispFormulaParseException

Throws:

LispFormulaParseException

toString

public String toString()

Just return the underlying formula string.

Overrides:

toString in class Object