Proof processing (pyqbf.proof)#

List of classes#

QratType

Contains all available types for the QRAT lemmas

QratLemma

Class for storing a QRAT-Lemma

QratProof

Class for manipulating QRAT-proofs.

Module description#

This module provides classes and methods for manipulation and handling of proofs for QBFs

At the moment, we only support QRAT [1].

Module details#

class pyqbf.proof.QratLemma(type: ~pyqbf.proof.QratType = QratType.QRATA, clause: list[int] = <factory>, pivot: int = 0)#

Class for storing a QRAT-Lemma

Variables:

  • types (QratType) – type of the lemma

  • clause (list[int]) – clause information of the lemma

class pyqbf.proof.QratProof(from_file=None, from_fp=None, from_string=None)#

Class for manipulating QRAT-proofs. It can be used for creating formulas, reading them from a file, or writing them to a file.

Parameters:

  • from_file (str) – a QRAT filename to read from

  • from_fp (SupportsRead[str]) – a file pointer to read from

  • from_string (str) – a string storing a PCNF formula in QDIMACS format

Variables:

  • lemmas (list[int]) – list of proof-lemmas

  • comments (list[str]) – Comments encountered during parsing

add(lemma_type, clause)#

Adds a lemma of the specified type to the proof.

Parameters:

  • lemma_type (QratType) – type of the lemma

  • clause (list[int]) – clause learnt by the lemma

>>> proof = QratProof(from_file="/path/to/proof.qrat")
>>> proof.add(QratType.QRATA, [1, 2])
>>> proof.add(QratType.QRATE, [1, 2])
>>> proof.add(QratType.QRATU, [2, 1])
from_file(fname)#

Read a QRAT-proof from a file

Parameters:

fname (str) – file path to the file

>>> proof = QratProof()
>>> proof.from_file("/path/to/proof.qrat")
from_fp(fp)#

Read a QRAT-proof from a file pointer

Parameters:

fp (SupportsRead[str]) – file pointer to file containing the proof

>>> proof = QratProof()
>>> with open("/path/to/proof.qrat", "r") as fp:
...     proof.from_fp(fp)
from_string(text)#

Read a QRAT-proof from a string

Parameters:

text (str) – string containing the proof

>>> proof = QratProof()
>>> proof.from_string("1 2 0\nd 3 4 0\nu 6 2 0")
to_file(fname, with_comments=False)#

Writes the current state of the object in QRAT encoding to a file.

Parameters:

fname (str) – file path to the file

Usage example:

>>> proof = QratProof(from_file="/path/to/proof.qrat")
>>> proof.to_file("/path/to/target1.qrat")
>>> proof.to_file("/path/to/target2.qrat", with_comments=True)
to_fp(fp, with_comments=False)#

Writes the current state of the object in QRAT encoding to a filepointer.

param fp:

file pointer to target

type fp:

SupportsRead[str]

Usage example:

>>> proof = QratProof(from_file="/path/to/proof.qrat")
>>> with open("/path/to/target1.qrat", "w") as fp:
...     proof.to_fp(fp)
>>> with open("/path/to/target2.qrat", "w") as fp:
...     proof.to_fp(fp, with_comments=True)
to_string(with_comments=False)#

Return the current state of the object in QRAT encoding.

Returns:

a QRAT representation of the formula

Return type:

str

Usage example:

>>> proof = QratProof(from_file="/path/to/proof.qrat")
>>> print(proof.comments)
["clause addition", "universal reduction"]
>>> print(proof.to_string())
1 2 0
u 2 1 0
>>> print(proof.to_string(with_comments=True))
1 2 0 clause addition
u 2 1 0 universal reduction
class pyqbf.proof.QratType(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)#

Contains all available types for the QRAT lemmas