diff options
Diffstat (limited to 'src/proof/dimacs.h')
-rw-r--r-- | src/proof/dimacs.h | 69 |
1 files changed, 0 insertions, 69 deletions
diff --git a/src/proof/dimacs.h b/src/proof/dimacs.h deleted file mode 100644 index 405b33208..000000000 --- a/src/proof/dimacs.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file dimacs.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/deserialization for SAT problems as DIMACS - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__PROOF__DIMACS_H -#define CVC4__PROOF__DIMACS_H - -#include <iosfwd> -#include <memory> -#include <unordered_map> - -#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::unordered_map<ClauseId, prop::SatClause>& clauses, - const std::vector<ClauseId>& usedIndices); - -std::vector<prop::SatClause> parseDimacs(std::istream& i); - -} // namespace proof -} // namespace CVC4 - -#endif // CVC4__PROOF__DIMACS_H |