Class SPASSWriter


  • public class SPASSWriter
    extends java.lang.Object
    This class prints single first-order 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
    SPASS attempts to prove that the conjunction of all axioms implies the disjunction of all conjectures.
    Author:
    Anna Gessler
    See Also:
    SpassFolReasoner
    • 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​(FolBeliefSet kb, RelationalFormula formula)
      Prints the axioms declaration and conjectures declaration for a SPASS input file.
      void printProblem​(FolBeliefSet 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.
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Field Detail

      • writer

        final java.io.Writer writer
        Output is redirected to this writer.
    • Constructor Detail

      • SPASSWriter

        public SPASSWriter​(java.io.Writer writer)
        Creates a new SPASSWriter.
        Parameters:
        writer - Output is redirected to this writer.
      • SPASSWriter

        public SPASSWriter()
        Creates a new SPASSWriter.
    • Method Detail

      • printProblem

        public void printProblem​(FolBeliefSet 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 base
        formula - a relational formula
        Throws:
        ParserException - if parsing fails
        java.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​(FolBeliefSet 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 declarations
        formula - 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
      • close

        public void close()
                   throws java.io.IOException
        Throws:
        java.io.IOException