Class QdimacsParser


  • public class QdimacsParser
    extends DimacsParser
    This class implements a parser for the QDIMACS input format. It is an extension of the DIMACS format used in sat solver competitions. See http://www.qbflib.org/qdimacs.html for more information.

    The BNF for a QDIMACS input file is given by (starting symbol is QDIMACS-FILE):

    QDIMACS-FILE ::== PREAMBLE PREFIX MATRIX
    PREAMBLE ::== "p" "cnf" PNUM PNUM "\n"
    PREFIX ::== [QUANT_SETS]
    QUANT_SETS ::== QUANT_SET QUANT_SETS | QUANT_SET
    QUANT_SET ::== QUANTIFIER ATOM_SET "0\n"
    QUANTIFIER ::== "e" | "a"
    ATOM_SET ::== PNUM ATOM_SET | PNUM
    MATRIX ::== CLAUSE_LIST
    CLAUSE_LIST ::== CLAUSE CLAUSE_LIST | CLAUSE
    CLAUSE ::== LITERAL CLAUSE | LITERAL "0\n"

    Lines starting with "c" and consisting of non-special-ASCII characters (comments) are ignored.
    LITERAL is a signed integer != 0.
    PNUM is a signed integer > 0.
    The two numbers in PREAMBLE specify the number of variables and the number of clauses.

    To parse QDIMACS output files, use parseQDimacsOutput(String)
    Author:
    Anna Gessler
    • Constructor Detail

      • QdimacsParser

        public QdimacsParser()
    • Method Detail

      • 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.
        Overrides:
        parseBeliefBase in class DimacsParser
        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.
      • parseQDimacsOutput

        public QdimacsParser.Answer parseQDimacsOutput​(java.lang.String output)
        Parses the answer from a given QDIMACS output file. The rest of the file is ignored.
        Parameters:
        output - string containing a QDIMACS output file
        Returns:
        either SAT, UNSAT or UNKNOWN