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.
[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["\u003cp\u003eThe \u003ccode\u003eDratWriter\u003c/code\u003e class facilitates writing clauses and deletion information to a DRAT output, enabling proof logging and verification in SAT solving.\u003c/p\u003e\n"],["\u003cp\u003eIt provides methods like \u003ccode\u003eAddClause\u003c/code\u003e and \u003ccode\u003eDeleteClause\u003c/code\u003e to manipulate clauses within the DRAT output.\u003c/p\u003e\n"],["\u003cp\u003e\u003ccode\u003eDratWriter\u003c/code\u003e can be initialized to output in binary format and accepts a \u003ccode\u003eFile\u003c/code\u003e object for writing.\u003c/p\u003e\n"]]],["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"],null,["# File\n\nC++ Reference: class File\n=========================\n\n\nNote: This documentation is automatically generated.\n\n| Method ||\n|----------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|\n| [`AddClause`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_writer.h#L44) | Return type: `void ` Arguments: `absl::Span\u003cconst Literal\u003e clause` Writes a new clause to the DRAT output. Note that the RAT property is only checked on the first literal. |\n| [`DeleteClause`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_writer.h#L49) | Return type: `void ` Arguments: `absl::Span\u003cconst Literal\u003e 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. |\n| [`DratWriter`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_writer.h#L38) | \u003cbr /\u003e Arguments: `bool in_binary_format, File* output` \u003cbr /\u003e |\n| [`~DratWriter`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_writer.h#L40) | \u003cbr /\u003e |"]]
