1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief DIMACS SAT Problem Format
14 ** Defines serialization for SAT problems as DIMACS
17 #include "proof/dimacs.h"
19 #include "base/check.h"
26 // Prints the literal as a (+) or (-) int
27 // Not operator<< b/c that represents negation as ~
28 std::ostream
& textOut(std::ostream
& o
, const prop::SatLiteral
& l
)
34 return o
<< l
.getSatVariable() + 1;
37 // Prints the clause as a space-separated list of ints
38 // Not operator<< b/c that represents negation as ~
39 std::ostream
& textOut(std::ostream
& o
, const prop::SatClause
& c
)
41 for (const auto& l
: c
)
48 void printDimacs(std::ostream
& o
,
49 const std::unordered_map
<ClauseId
, prop::SatClause
>& clauses
,
50 const std::vector
<ClauseId
>& usedIndices
)
53 for (const ClauseId i
: usedIndices
)
55 const prop::SatClause
& c
= clauses
.at(i
);
56 for (const auto& l
: c
)
58 if (l
.getSatVariable() + 1 > maxVar
)
60 maxVar
= l
.getSatVariable() + 1;
64 o
<< "p cnf " << maxVar
<< " " << usedIndices
.size() << '\n';
65 for (const ClauseId i
: usedIndices
)
67 const prop::SatClause
& c
= clauses
.at(i
);
68 for (const auto& l
: c
)
74 o
<< l
.getSatVariable() + 1 << " ";
80 std::vector
<prop::SatClause
> parseDimacs(std::istream
& in
)
98 Assert(nClauses
>= 0);
100 std::vector
<prop::SatClause
> cnf
;
101 for (uint64_t i
= 0; i
< nClauses
; ++i
)
109 cnf
.back().emplace_back(std::abs(lit
) - 1, lit
< 0);
111 Assert(static_cast<uint64_t>(std::abs(lit
)) <= nVars
);