Class QbfParser

java.lang.Object

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