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