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

Class 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

    • Field Detail

      • gate_variables

        private java.util.Map<java.lang.String,​PlFormula> gate_variables
        Keeps track of the formulas that are assigned to specific gate variables.

      • forall_quantified_variables

        private PlSignature forall_quantified_variables
        Keeps track of universally quantified variables.

      • exists_quantified_variables

        private PlSignature exists_quantified_variables
        Keeps track of existentially quantified variables.

      • output

        private Proposition output
        The name of the output gate variable of the problem.

    • Constructor Detail

      • QCirParser

        public QCirParser()

    • Method Detail

      • getOutputVariable

        public PlFormula getOutputVariable()
        Returns:
        the output gate of this QCir problem.

      • parseBeliefBase

        public PlBeliefSet parseBeliefBase​(java.io.Reader reader)
                            throws java.io.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:
        java.io.IOException - if some IO issue occurred.
        ParserException - some parsing exceptions may be added here.

      • parseQuantifierBlock

        private void parseQuantifierBlock​(java.lang.String s)
        Parses the quantifier block at the beginning of the file. The free variables declaration is ignored as free variables are not currently saved in this parser.
        Parameters:
        s - string containing the quantifier block

      • parseFormula

        public PlFormula parseFormula​(java.io.Reader reader)
                       throws java.io.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:
        java.io.IOException - if some IO issue occurred.
        ParserException - some parsing exceptions may be added here.

      • parseGateFormula

        private PlFormula parseGateFormula​(java.lang.String formula)
        This method parses a gate formula, meaning a conjunction, disjunction, quantification, xor-construct or if-then-else-construct.
        Parameters:
        formula - the input formula as a String
        Returns:
        the parsed quantified boolean formula

      • parseLiteral

        private PlFormula parseLiteral​(java.lang.String literal,
                               boolean parseGateVariables)
        Parses variables and their negations.
        Parameters:
        literal - the input variable as a string
        parseGateVariables - if set to true, gate variables are also parsed, meaning they are replaced with the formulas that they represent.
        Returns:
        the parsed quantified boolean formula

      • parseAssociativeFormula

        private PlFormula parseAssociativeFormula​(java.lang.String prefix,
                                          java.lang.String innerFormula)
        Parses an associative formula, i.e. a conjunction or disjunction.
        Parameters:
        prefix - the full formula with its prefix "and" or "or"
        innerFormula - the inner formula without the prefix or parentheses
        Returns:
        the parsed quantified boolean formula

      • parseQuantification

        private PlFormula parseQuantification​(java.lang.String prefix,
                                      java.lang.String innerFormula)
        Parses a quantified formula.
        Parameters:
        prefix - the full formula with its prefix "forall" or "exists"
        innerFormula - the inner formula without the prefix or parentheses
        Returns:
        the parsed quantified boolean formula

      • parseIfThenElse

        private PlFormula parseIfThenElse​(java.lang.String innerFormula)
        Parses an if-then-else construct.
        Parameters:
        innerFormula - the inner formula without the "ite" prefix or parentheses
        Returns:
        the parsed quantified boolean formula

      • parseXor

        private PlFormula parseXor​(java.lang.String innerFormula)
        Parses an xor construct.
        Parameters:
        innerFormula - the inner formula without the "xor" prefix or parentheses
        Returns:
        the parsed quantified boolean formula