Documentation
¶
Overview ¶
Package io gathers readers and writers for formulas in different formats in LogicNG.
To write a formula to a file, you can use the
io.WriteFormula(fac, "filename", formula)
To read the file again, simply use
read, err := io.ReadFormula(fac, "filename")
Index ¶
- func ReadDimacs(fac f.Factory, filename string, prefix ...string) (*[]f.Formula, error)
- func ReadDimacsFile(fac f.Factory, file *os.File, prefix ...string) (*[]f.Formula, error)
- func ReadFormula(fac f.Factory, filename string) (f.Formula, error)
- func ReadFormulaFile(fac f.Factory, file *os.File) (f.Formula, error)
- func ReadFormulas(fac f.Factory, filename string) ([]f.Formula, error)
- func ReadFormulasFile(fac f.Factory, file *os.File) ([]f.Formula, error)
- func WriteDimacs(fac f.Factory, filename string, formula f.Formula) (map[f.Variable]int, error)
- func WriteDimacsToFile(fac f.Factory, file *os.File, formula f.Formula) (map[f.Variable]int, error)
- func WriteDimacsToWriter(fac f.Factory, writer io.Writer, formula f.Formula) (map[f.Variable]int, error)
- func WriteFormula(fac f.Factory, filename string, formula f.Formula, splitAnd ...bool) error
- func WriteFormulaToFile(fac f.Factory, file *os.File, formula f.Formula, splitAnd ...bool) error
- func WriteFormulaToWriter(fac f.Factory, writer io.Writer, formula f.Formula, splitAnd ...bool) error
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ReadDimacs ¶
ReadDimacs reads a CNF from the given filename in Dimacs format. The optional prefix parameter is used to generate the variable names. The default value is `v` therefore variable v1, v2, ... will be generated from the input problem. Returns the CNF as a list of clauses and an optional error if there was a problem reading the file.
func ReadDimacsFile ¶
ReadDimacsFile reads a CNF from the given file in Dimacs format. The optional prefix parameter is used to generate the variable names. The default value is `v` therefore variable v1, v2, ... will be generated from the input problem. Returns the CNF as a list of clauses and an optional error if there was a problem reading the file.
func ReadFormula ¶
ReadFormula reads a formula from the given file. If the file contains more than one line, the conjunction of all lines is returned. Returns the formula and an optional error if there was a problem reading the file.
func ReadFormulaFile ¶
ReadFormulaFile reads a formula from the given file. If the file contains more than one line, the conjunction of all lines is returned. Returns the formula and an optional error if there was a problem reading the file.
func ReadFormulas ¶
ReadFormulas reads a list of formulas from the given file. Each line in the file is one formula in the result. Returns the list of formulas ad an optional error if there was a problem reading the file.
func ReadFormulasFile ¶
ReadFormulasFile reads a list of formulas from the given file. Each line in the file is one formula in the result. Returns the list of formulas ad an optional error if there was a problem reading the file.
func WriteDimacs ¶
WriteDimacs writes the given formula in CNF to a file with the given filename in the http://www.satcompetition.org/2009/format-benchmarks2009.html. Returns a mapping from each variable of the original problem to its index in the CNF file an optional error if there was a problem writing the file or the formula was not in CNF.
func WriteDimacsToFile ¶
WriteDimacsToFile writes the given formula in CNF to the given file in the http://www.satcompetition.org/2009/format-benchmarks2009.html. Returns a mapping from each variable of the original problem to its index in the CNF file an optional error if there was a problem writing the file or the formula was not in CNF.
func WriteDimacsToWriter ¶
func WriteDimacsToWriter(fac f.Factory, writer io.Writer, formula f.Formula) (map[f.Variable]int, error)
WriteDimacsToWriter writes the given formula to the given writer in the http://www.satcompetition.org/2009/format-benchmarks2009.html. Returns a mapping from each variable of the original problem to its index in the CNF file an optional error if there was a problem writing to the writer.
func WriteFormula ¶
WriteFormula writes the given formula to a file with the given filename. The flag splitAnd indicates whether - if the formula is a conjunction - the single operands should be written to different lines without a conjoining operator. Returns an error if there was a problem writing the file.
func WriteFormulaToFile ¶
WriteFormulaToFile writes the given formula to the given file. The flag splitAnd indicates whether - if the formula is a conjunction - the single operands should be written to different lines without a conjoining operator. Returns an error if there was a problem writing the file.
func WriteFormulaToWriter ¶
func WriteFormulaToWriter(fac f.Factory, writer io.Writer, formula f.Formula, splitAnd ...bool) error
WriteFormulaToWriter writes the given formula to the given writer. The flag splitAnd indicates whether - if the formula is a conjunction - the single operands should be written to different lines without a conjoining operator. Returns an error if there was a problem writing the writer.
Types ¶
This section is empty.
Source Files