QdimacsParser

java.lang.Object
- net.sf.tweety.commons.Parser<PlBeliefSet,PlFormula>
- - net.sf.tweety.logics.pl.parser.DimacsParser
  - - net.sf.tweety.logics.qbf.parser.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

Nested Class Summary

Nested Classes
Modifier and Type Class Description

static class QdimacsParser.Answer
Possible answers that solvers can find for a given QDIMACS problem.

Constructor Summary

Constructors
Constructor Description

QdimacsParser()

Method Summary

Modifier and Type	Method	Description
`PlBeliefSet`	`parseBeliefBase(java.io.Reader reader)`	Parses the given reader into a belief base of the given type.
`QdimacsParser.Answer`	`parseQDimacsOutput(java.lang.String output)`	Parses the answer from a given QDIMACS output file.

Methods inherited from class net.sf.tweety.logics.pl.parser.DimacsParser
parseFormula, setSignature

Methods inherited from class net.sf.tweety.commons.Parser
isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- 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