Package net.sf.tweety.logics.ml.writer
Class SPASSWriter
- java.lang.Object
-
- net.sf.tweety.logics.ml.writer.SPASSWriter
-
public class SPASSWriter extends java.lang.Object
This class prints single first-order modal logic formulas and knowledge bases to the SPASS format.A SPASS input file consists of the following parts:
- Description: Contains meta-information about the problem, i.e. name, author, satisfiability
- Symbols: Signature declaration
- Axioms: a list of formulas
- Conjectures: a list of formulas
- Author:
- Anna Gessler
- See Also:
SPASSMlReasoner
-
-
Field Summary
Fields Modifier and Type Field Description (package private) java.io.Writer
writer
Output is redirected to this writer.
-
Constructor Summary
Constructors Constructor Description SPASSWriter()
Creates a new SPASSWriter.SPASSWriter(java.io.Writer writer)
Creates a new SPASSWriter.
-
Method Summary
Modifier and Type Method Description void
close()
private java.lang.String
printDescription()
Generates a generic description part for a SPASS problem file.private java.lang.String
printFormula(RelationalFormula f)
private java.lang.String
printFormulas(MlBeliefSet kb, RelationalFormula formula)
Prints the axioms declaration and conjectures declaration for a SPASS input file.void
printProblem(MlBeliefSet kb, RelationalFormula formula)
Prints the contents of a SPASS problem file for a given knowledge base and a formula.private java.lang.String
printSignature(FolSignature signature)
Prints the symbols declaration for a SPASS input file.
-
-
-
Method Detail
-
printProblem
public void printProblem(MlBeliefSet kb, RelationalFormula formula) throws ParserException, java.io.IOException
Prints the contents of a SPASS problem file for a given knowledge base and a formula.- Parameters:
kb
- a knowledge baseformula
- a relational formula- Throws:
ParserException
- if parsing failsjava.io.IOException
- if an IO issue occurs.
-
printDescription
private java.lang.String printDescription()
Generates a generic description part for a SPASS problem file.- Returns:
- a string containing the description part
-
printSignature
private java.lang.String printSignature(FolSignature signature)
Prints the symbols declaration for a SPASS input file. First-order quantifiers and operators are do not need to be declared. All declared symbols have to be different from each other.- Parameters:
signature
- FolSignature of the problem- Returns:
- a string containing the signature declaration
-
printFormulas
private java.lang.String printFormulas(MlBeliefSet kb, RelationalFormula formula)
Prints the axioms declaration and conjectures declaration for a SPASS input file. All formulas must be closed.- Parameters:
kb
- a knowledge base of relational formulas that will be used as the axioms declarationsformula
- a formula that will be used as the conjectures declaration- Returns:
- a string containing the axioms and conjectures declaration
- See Also:
- https://webspass.spass-prover.org/help/spass-input-syntax15.pdf
-
printFormula
private java.lang.String printFormula(RelationalFormula f)
-
close
public void close() throws java.io.IOException
- Throws:
java.io.IOException
-
-