diff options
Diffstat (limited to 'src/proof/dimacs_printer.h')
-rw-r--r-- | src/proof/dimacs_printer.h | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs_printer.h new file mode 100644 index 000000000..d11adea3f --- /dev/null +++ b/src/proof/dimacs_printer.h @@ -0,0 +1,66 @@ +/********************* */ +/*! \file dimacs_printer.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief DIMACS SAT Problem Format + ** + ** Defines serialization for SAT problems as DIMACS + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__DIMACS_PRINTER_H +#define __CVC4__PROOF__DIMACS_PRINTER_H + +#include <iosfwd> +#include <memory> + +#include "proof/clause_id.h" +#include "prop/sat_solver_types.h" + +namespace CVC4 { +namespace proof { + +/** + * Prints the literal as a (+) or (-) int + * Not operator<< b/c that represents negation as ~ + * + * @param o where to print + * @param l the literal to print + * + * @return the original stream + */ +std::ostream& textOut(std::ostream& o, const prop::SatLiteral& l); + +/** + * Prints the clause as a space-separated list of ints + * Not operator<< b/c that represents literal negation as ~ + * + * @param o where to print + * @param c the clause to print + * + * @return the original stream + */ +std::ostream& textOut(std::ostream& o, const prop::SatClause& c); + +/** + * Prints a CNF formula in DIMACS format + * + * @param o where to print to + * @param usedClauses the CNF formula + */ +void printDimacs( + std::ostream& o, + const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses); + +} // namespace proof +} // namespace CVC4 + +#endif // __CVC4__PROOF__DIMACS_PRINTER_H |