C++ Reference: class File
Note: This documentation is automatically generated.
| Method |
AddClause | Return type: void Arguments: absl::Span<const Literal> clause Writes a new clause to the DRAT output. Note that the RAT property is only
checked on the first literal.
|
DeleteClause | Return type: void Arguments: absl::Span<const Literal> clause Writes a "deletion" information about a clause that has been added before
to the DRAT output. Note that it is also possible to delete a clause from
the problem.
|
DratWriter | Arguments: bool in_binary_format, File* output |
~DratWriter | |
Except as otherwise noted, the content of this page is licensed under the Creative Commons Attribution 4.0 License, and code samples are licensed under the Apache 2.0 License. For details, see the Google Developers Site Policies. Java is a registered trademark of Oracle and/or its affiliates.
Last updated 2024-08-06 UTC.
[null,null,["Last updated 2024-08-06 UTC."],[[["The `DratWriter` class facilitates writing clauses and deletion information to a DRAT output, enabling proof logging and verification in SAT solving."],["It provides methods like `AddClause` and `DeleteClause` to manipulate clauses within the DRAT output."],["`DratWriter` can be initialized to output in binary format and accepts a `File` object for writing."]]],["The `DratWriter` class manages interactions with a DRAT output. Key actions include `AddClause`, which writes a new clause to the DRAT output, checking the RAT property on the first literal. `DeleteClause` writes a deletion notice for a previously added clause, allowing clauses to be removed. The `DratWriter` constructor initializes the writer, accepting a boolean for binary format and a `File*` output. The `~DratWriter` is the destructor for this class.\n"]]
