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."],[[["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"]]
