Package org.tweetyproject.logics.qbf.writer

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 Summary

Fields

Modifier and Type	Field	Description
boolean	DISABLE_PREAMBLE_ZERO	Removes zero at the end of the problem line (workaround for some solvers).
Boolean	special_formula_flag	Will be set to true/false if the input can be simplified to a tautology/contradiction.

Constructor Summary

Constructors

Constructor	Description
QdimacsWriter()	Creates a new QDIMACS writer.
QdimacsWriter(Writer writer)	Creates a new QDIMACS writer.

Method Summary

Modifier and Type	Method	Description
void	close()	Closes the underlying writer resource.
String	printBase(PlBeliefSet kb)	Return Kb in string format
String	printVariables(Set<Proposition> vars, Map<Proposition,Integer> mappings)	Prints the variable mappings for a given set of propositions.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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.