dratify 0.1.4
“Check DRAT/DRUP proofs of unsatisfiability inside your Python process. Zero dependencies, optional Rust accelerator.”
Source contains low-bit mask syntaxSource references XOR syntax
SHA-2568f786a10b07c8e3ed4bd91400ce7b638d92efee6cfd0736fa3d319929410fb5a
MaleculeH₂(CmF)
Evidence
1# SPDX-License-Identifier: Apache-2.0
2# Copyright (c) 2026 Carlo Perassi. Licensed under the Apache License 2.0.
3"""Clause and formula containers, plus DIMACS CNF input/output.
4
5Two distinct objects live here and they are …
8:28… ause. Mutable, carries the two watched literals in
9 slots 0 and 1, and holds the learnt-clause bookkeeping (LBD, activity,
10 deletion mark). Never used for storage or I/O.
11
12``CNF``
13 An immutable-ish *formula*: a variable count plus a list of clauses, each a
14 tuple of internal literals. This is what the parser produces, what the
15 encoders build, what the proof checker consumes and w …
44:20… seen``) carry no meaning here: they exist because
45 `cdclkit <https://github.com/carlok/cdclkit>`_ imports this class for its
46 solver, which maintains the watch invariant that if the clause is not
47 satisfied at a lower level, ``lits[0]`` and ``lits[1]`` are either
48 …
147:5… if l in seen:
148 continue
149 if (l ^ 1) in seen:
150 return False # tautology
151 seen.add(l)
152 out.append(l)
153 v = l >> 1
154 …
242:20… getvalue()
243
244 def save(self, path: str) -> None:
245 with open(path, "w", encoding="ascii") as fh:
246 write_dimacs(self, fh)
247
248 def __repr__(self) -> str: # pragma: no cover - debugging aid
249 return f" …
No evidence locations were recorded for this file. Raw result