Class QdimacsWriter

java.lang.Object
org.tweetyproject.logics.qbf.writer.QdimacsWriter
public class QdimacsWriter extends Object
Converts belief bases to QDIMACS format and prints them.

Notes:
- Currently only works for belief bases that have only quantifiers in the left portion of each formula and have only unquantified formulas in the right portion of each formula.
- The right portion of the formulas does not need to be in any special form (it will be converted to cnf).
Author:
Anna Gessler

  • Field Details

    • DISABLE_PREAMBLE_ZERO

      public boolean DISABLE_PREAMBLE_ZERO
      Removes zero at the end of the problem line (workaround for some solvers).

    • special_formula_flag

      public Boolean special_formula_flag
      Will be set to true/false if the input can be simplified to a tautology/contradiction. Used in some of the solver wrappers to immediately return true/false instead of calling the solver in case of a tautology/contradiction.

  • Constructor Details

    • QdimacsWriter

      public QdimacsWriter(Writer writer)
      Creates a new QDIMACS writer.
      Parameters:
      writer - a writer

    • QdimacsWriter

      public QdimacsWriter()
      Creates a new QDIMACS writer.

  • Method Details

    • printBase

      public String printBase(PlBeliefSet kb) throws IOException
      Return Kb in string format
      Parameters:
      kb - a kb
      Returns:
      kb in string format
      Throws:
      IOException - error

    • printVariables

      public String printVariables(Set<Proposition> vars, Map<Proposition,Integer> mappings)
      Prints the variable mappings for a given set of propositions. The method generates a string containing the corresponding integer mappings for each proposition in the provided set, using the mappings from the provided map.
      Parameters:
      vars - The set of propositions whose mappings are to be printed.
      mappings - A map that associates each proposition with an integer value.
      Returns:
      A string containing the integer mappings of the propositions, separated by spaces.

    • close

      public void close() throws IOException
      Closes the underlying writer resource. This method should be called when all writing operations are complete to ensure that all resources are properly released.
      Throws:
      IOException - If an I/O error occurs during closing the writer.