Package org.tweetyproject.logics.qbf.parser

Class QdimacsParser

java.lang.Object

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

org.tweetyproject.logics.pl.parser.DimacsParser

org.tweetyproject.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(Reader reader)	Parses the given reader into a belief base of the given type.
QdimacsParser.Answer	parseQDimacsOutput(String output)	Parses the answer from a given QDIMACS output file.

Methods inherited from class org.tweetyproject.logics.pl.parser.DimacsParser

parseFormula, setSignature

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

QdimacsParser

public QdimacsParser()

Method Details

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.

Overrides:

parseBeliefBase in class DimacsParser

Parameters:

reader - a reader

Returns:

a belief base

Throws:

IOException - if some IO issue occurred.

ParserException - some parsing exceptions may be added here.

parseQDimacsOutput

public QdimacsParser.Answer parseQDimacsOutput(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