Package org.tweetyproject.logics.qbf.parser

Class QCirParser

java.lang.Object

org.tweetyproject.commons.Parser<PlBeliefSet,PlFormula>

org.tweetyproject.logics.qbf.parser.QCirParser

public class QCirParser
extends Parser<PlBeliefSet,PlFormula>

This class implements a parser for the QCIR (Quantified CIRcuit) format. See http://www.qbflib.org/qcir.pdf for more information.
The BNF for a QCir file is given by (starting symbol is QCIR-FILE):

QCIR-FILE ::== FORMAT-ID QBLOCK-STMT OUTPUT-STMT (GATE-STMT)*
FORMAT-ID ::== "#QCIR-G14" [INTEGER] "\n"
QBLOCK-STMT ::== ["free(" VAR-LIST ")\n"] QBLOCK-QUANT*
QBLOCK-QUANT ::== QUANT "(" VAR-LIST ")"\n"
VAR-LIST ::== (VAR,)* VAR
LIT-LIST ::== (LIT,)* LIT
OUTPUT-STMT ::== "output(" LIT ")\n"
GATE-STMT ::== GVAR "=" "and" "(" LIT-LIST ")" | GVAR "=" "or" "(" LIT-LIST ")" | GVAR "=" "xor(" LIT "," LIT ")" | GVAR "=" "ite(" LIT "," LIT "," LIT ")" | GVAR = QUANT "(" VAR-LIST ";" LIT ")"
QUANT ::== "exists" | "forall"
LIT ::== VAR | "-" VAR | GVAR | "-" GVAR

ite stands for if-then-else.
INTEGER are integer numbers.
VAR and GVAR are sequences of characters of symbols from {a,...,z,A,...,Z,0,...,9,_}.
Additionally, lines starting with "#" (comments) will be ignored.

Author:

Anna Gessler

Constructor Summary

Constructors

Constructor	Description
QCirParser()	Default

Method Summary

Modifier and Type	Method	Description
PlFormula	getOutputVariable()	Return the output gate of this QCir problem.
PlBeliefSet	parseBeliefBase(Reader reader)	Parses the given reader into a belief base of the given type.
PlFormula	parseFormula(Reader reader)	Parses the given reader into a formula of the given type.

Methods inherited from class org.tweetyproject.commons.Parser

isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile, parseListOfBeliefBases, parseListOfBeliefBases, parseListOfBeliefBasesFromFile, parseListOfBeliefBasesFromFile

Methods inherited from class java.lang.Object

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

Constructor Details

QCirParser

public QCirParser()

Default

Method Details

getOutputVariable

public PlFormula getOutputVariable()

Return the output gate of this QCir problem.

Returns:

the output gate of this QCir problem.

parseBeliefBase

public PlBeliefSet parseBeliefBase(Reader reader)
                            throws IOException,
ParserException

Description copied from class: Parser

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

Specified by:

parseBeliefBase in class Parser<PlBeliefSet,PlFormula>

Parameters:

reader - a reader

Returns:

a belief base

Throws:

IOException - if some IO issue occurred.

ParserException - some parsing exceptions may be added here.

parseFormula

public PlFormula parseFormula(Reader reader)
                       throws IOException,
ParserException

Description copied from class: Parser

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

Specified by:

parseFormula in class Parser<PlBeliefSet,PlFormula>

Parameters:

reader - a reader

Returns:

a formula

Throws:

IOException - if some IO issue occurred.

ParserException - some parsing exceptions may be added here.