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, useparseQDimacsOutput(String)- Author:
 - Anna Gessler
 
 
- 
- 
Nested Class Summary
Nested Classes Modifier and Type Class Description static classQdimacsParser.AnswerPossible answers that solvers can find for a given QDIMACS problem. 
- 
Constructor Summary
Constructors Constructor Description QdimacsParser() 
- 
Method Summary
Modifier and Type Method Description PlBeliefSetparseBeliefBase(java.io.Reader reader)Parses the given reader into a belief base of the given type.QdimacsParser.AnswerparseQDimacsOutput(java.lang.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 
 - 
 
 - 
 
- 
- 
Method Detail
- 
parseBeliefBase
public PlBeliefSet parseBeliefBase(java.io.Reader reader) throws java.io.IOException, ParserException
Description copied from class:ParserParses the given reader into a belief base of the given type.- Overrides:
 parseBeliefBasein classDimacsParser- 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
 
 
 - 
 
 -