Package net.sf.tweety.logics.qbf.parser

Class QbfParser

java.lang.Object

net.sf.tweety.commons.Parser<PlBeliefSet,PlFormula>

net.sf.tweety.logics.pl.parser.PlParser

net.sf.tweety.logics.qbf.parser.QbfParser

public class QbfParser
extends PlParser

This class implements a parser for quantified boolean formulas. The BNF for a qbf belief set is given by (starting symbol is KB)

KB ::== VARDECLAR FORMULAS
VARDECLAR ::== "{" (VARIABLENAME ("," VARIABLENAME)*)? "}"
FORMULAS ::== FORMULA ( "\n" FORMULA )*
FORMULA ::== VARIABLENAME | "(" FORMULA ")" | FORMULA ">>" FORMULA | FORMULA "||" FORMULA | FORMULA "=>" FORMULA | FORMULA "<=>" FORMULA | "!" FORMULA | "+" | "-" | "forall" VARIABLENAME ":" "(" FORMULA ")" | "exists" VARIABLENAME ":" "(" FORMULA ")" |

VARIABLENAME is a sequence of characters excluding |,&,!,(,),=,<,> and whitespace characters.

Author:

Anna Gessler, Matthias Thimm

Field Summary

Fields

Modifier and Type	Field	Description
private PlSignature	variables	Keeps track of variables defined.

Constructor Summary

Constructors

Constructor	Description
QbfParser()

Method Summary

Modifier and Type	Method	Description
private void	consumeToken(java.util.Stack<java.lang.Object> stack, int c)	This method reads one token from the given reader and appropriately constructs a propositional formula from the stream.
PlBeliefSet	parseBeliefBase(java.io.Reader reader)	Parses the given reader into a belief base of the given type.
private PlFormula	parseEquivalence(java.util.List<java.lang.Object> l)
PlFormula	parseFormula(java.io.Reader reader)	Parses the given reader into a formula of the given type.
private PlFormula	parseImplication(java.util.List<java.lang.Object> l)
private PlFormula	parseQuantification(java.util.List<java.lang.Object> l)	Parses a quantification

Methods inherited from class net.sf.tweety.logics.pl.parser.PlParser

parseDisjunction

Methods inherited from class net.sf.tweety.commons.Parser

isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile

Methods inherited from class java.lang.Object

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

Field Detail

variables

private PlSignature variables

Keeps track of variables defined.

Constructor Detail

QbfParser

public QbfParser()

Method Detail

parseBeliefBase

public PlBeliefSet parseBeliefBase(java.io.Reader reader)
                            throws ParserException

Description copied from class: Parser

Parses the given reader into a belief base of the given type.

Overrides:

parseBeliefBase in class PlParser

Parameters:

reader - a reader

Returns:

a belief base

Throws:

ParserException - some parsing exceptions may be added here.

parseFormula

public PlFormula parseFormula(java.io.Reader reader)
                       throws ParserException

Description copied from class: Parser

Parses the given reader into a formula of the given type.

Overrides:

parseFormula in class PlParser

Parameters:

reader - a reader

Returns:

a formula

Throws:

ParserException - some parsing exceptions may be added here.

consumeToken

private void consumeToken(java.util.Stack<java.lang.Object> stack,
                          int c)
                   throws ParserException

This method reads one token from the given reader and appropriately constructs a propositional formula from the stream.

Parameters:

stack - a stack used for monitoring the read items.

c - a token from a stream.

Throws:

ParserException - in case of parser errors.

parseQuantification

private PlFormula parseQuantification(java.util.List<java.lang.Object> l)

Parses a quantification

Parameters:

l - list of terms

Returns:

the formula

parseEquivalence

private PlFormula parseEquivalence(java.util.List<java.lang.Object> l)

parseImplication

private PlFormula parseImplication(java.util.List<java.lang.Object> l)