""" @generated by mypy-protobuf. Do not edit manually! isort:skip_file Proto used to store LRAT proofs (https://arxiv.org/abs/1612.02353) with some extensions to support multi-threading (with one output file per file). This proto is only used internally to store partial proofs on disk before merging them. It can be changed without backward compatibility, and should not be used directly by users. LINT: LEGACY_NAMES """ import builtins import collections.abc import google.protobuf.descriptor import google.protobuf.internal.containers import google.protobuf.message import sys import typing if sys.version_info >= (3, 10): import typing as typing_extensions else: import typing_extensions DESCRIPTOR: google.protobuf.descriptor.FileDescriptor @typing.final class LratImportedClause(google.protobuf.message.Message): """A clause imported from the input problem, or from another worker.""" DESCRIPTOR: google.protobuf.descriptor.Descriptor CLAUSE_ID_FIELD_NUMBER: builtins.int LITERALS_FIELD_NUMBER: builtins.int clause_id: builtins.int @property def literals(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: ... def __init__( self, *, clause_id: builtins.int | None = ..., literals: collections.abc.Iterable[builtins.int] | None = ..., ) -> None: ... _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["clause_id", b"clause_id"] def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ... _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["clause_id", b"clause_id", "literals", b"literals"] def ClearField(self, field_name: _ClearFieldArgType) -> None: ... Global___LratImportedClause: typing_extensions.TypeAlias = LratImportedClause @typing.final class LratInferredClause(google.protobuf.message.Message): """An LRAT inferred clause.""" DESCRIPTOR: google.protobuf.descriptor.Descriptor @typing.final class RatInfo(google.protobuf.message.Message): """If `rat_infos` is empty, the last `unit_ids` clause must become empty after unit propagation. If the last `unit_ids` clause does not become empty by unit propagation, then `rat_infos` must contain all the clauses which contain the negation of the first `literals` (called the pivot 'p') -- and no other clauses. Moreover, for each r in `rat_infos`, all the `r.unit_ids` clauses must become unit and eventually empty if all the literals of the `r.resolvant_id` clause (minus ~p), plus those in `literals`, are assumed to be false (this list must be in unit propagation order; verification stops at the first empty clause). See LratChecker for more details. """ DESCRIPTOR: google.protobuf.descriptor.Descriptor RESOLVANT_ID_FIELD_NUMBER: builtins.int UNIT_IDS_FIELD_NUMBER: builtins.int resolvant_id: builtins.int @property def unit_ids(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: ... def __init__( self, *, resolvant_id: builtins.int | None = ..., unit_ids: collections.abc.Iterable[builtins.int] | None = ..., ) -> None: ... _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["resolvant_id", b"resolvant_id"] def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ... _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["resolvant_id", b"resolvant_id", "unit_ids", b"unit_ids"] def ClearField(self, field_name: _ClearFieldArgType) -> None: ... CLAUSE_ID_FIELD_NUMBER: builtins.int LITERALS_FIELD_NUMBER: builtins.int UNIT_IDS_FIELD_NUMBER: builtins.int RAT_INFOS_FIELD_NUMBER: builtins.int EXPORTED_FIELD_NUMBER: builtins.int clause_id: builtins.int exported: builtins.bool """Whether the clause must be exported, so that other workers can import it (a clause cannot be imported if it is not previously exported). This is not needed for unary and binary clauses, which are always exported. """ @property def literals(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: """Literals are represented with LiteralIndex values.""" @property def unit_ids(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: """Clauses which become unit and possibly empty if all the `literals` are assumed to be false (verification stops at the first empty clause). This list must be in unit propagation order. See LratChecker for more details. """ @property def rat_infos(self) -> google.protobuf.internal.containers.RepeatedCompositeFieldContainer[Global___LratInferredClause.RatInfo]: ... def __init__( self, *, clause_id: builtins.int | None = ..., literals: collections.abc.Iterable[builtins.int] | None = ..., unit_ids: collections.abc.Iterable[builtins.int] | None = ..., rat_infos: collections.abc.Iterable[Global___LratInferredClause.RatInfo] | None = ..., exported: builtins.bool | None = ..., ) -> None: ... _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["clause_id", b"clause_id", "exported", b"exported"] def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ... _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["clause_id", b"clause_id", "exported", b"exported", "literals", b"literals", "rat_infos", b"rat_infos", "unit_ids", b"unit_ids"] def ClearField(self, field_name: _ClearFieldArgType) -> None: ... Global___LratInferredClause: typing_extensions.TypeAlias = LratInferredClause @typing.final class LratExportedClause(google.protobuf.message.Message): """A clause to export, so that it can be imported from any worker. This is not needed for unary and binary clauses, which are always exported. """ DESCRIPTOR: google.protobuf.descriptor.Descriptor CLAUSE_ID_FIELD_NUMBER: builtins.int LITERALS_FIELD_NUMBER: builtins.int clause_id: builtins.int @property def literals(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: ... def __init__( self, *, clause_id: builtins.int | None = ..., literals: collections.abc.Iterable[builtins.int] | None = ..., ) -> None: ... _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["clause_id", b"clause_id"] def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ... _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["clause_id", b"clause_id", "literals", b"literals"] def ClearField(self, field_name: _ClearFieldArgType) -> None: ... Global___LratExportedClause: typing_extensions.TypeAlias = LratExportedClause @typing.final class LratDeletedClauses(google.protobuf.message.Message): """A list of clauses to delete.""" DESCRIPTOR: google.protobuf.descriptor.Descriptor CLAUSE_IDS_FIELD_NUMBER: builtins.int @property def clause_ids(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: """IDs of the imported or inferred clauses to delete. A deleted clause can no longer be used to infer clauses. """ def __init__( self, *, clause_ids: collections.abc.Iterable[builtins.int] | None = ..., ) -> None: ... _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["clause_ids", b"clause_ids"] def ClearField(self, field_name: _ClearFieldArgType) -> None: ... Global___LratDeletedClauses: typing_extensions.TypeAlias = LratDeletedClauses @typing.final class LratProofStep(google.protobuf.message.Message): """An LRAT UNSAT proof is a sequence of steps, starting from imported clauses and ending with the empty clause. At each step new clauses can be inferred from previous ones (with an explicit proof), or imported from another proof built by another thread. A proof step can also delete clauses which are no longer needed, or export a clause for other workers to import. Each clause is identified by a unique clause ID. """ DESCRIPTOR: google.protobuf.descriptor.Descriptor IMPORTED_CLAUSE_FIELD_NUMBER: builtins.int INFERRED_CLAUSE_FIELD_NUMBER: builtins.int EXPORTED_CLAUSE_FIELD_NUMBER: builtins.int DELETED_CLAUSES_FIELD_NUMBER: builtins.int @property def imported_clause(self) -> Global___LratImportedClause: ... @property def inferred_clause(self) -> Global___LratInferredClause: ... @property def exported_clause(self) -> Global___LratExportedClause: ... @property def deleted_clauses(self) -> Global___LratDeletedClauses: ... def __init__( self, *, imported_clause: Global___LratImportedClause | None = ..., inferred_clause: Global___LratInferredClause | None = ..., exported_clause: Global___LratExportedClause | None = ..., deleted_clauses: Global___LratDeletedClauses | None = ..., ) -> None: ... _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["deleted_clauses", b"deleted_clauses", "exported_clause", b"exported_clause", "imported_clause", b"imported_clause", "inferred_clause", b"inferred_clause", "step", b"step"] def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ... _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["deleted_clauses", b"deleted_clauses", "exported_clause", b"exported_clause", "imported_clause", b"imported_clause", "inferred_clause", b"inferred_clause", "step", b"step"] def ClearField(self, field_name: _ClearFieldArgType) -> None: ... _WhichOneofReturnType_step: typing_extensions.TypeAlias = typing.Literal["imported_clause", "inferred_clause", "exported_clause", "deleted_clauses"] _WhichOneofArgType_step: typing_extensions.TypeAlias = typing.Literal["step", b"step"] def WhichOneof(self, oneof_group: _WhichOneofArgType_step) -> _WhichOneofReturnType_step | None: ... Global___LratProofStep: typing_extensions.TypeAlias = LratProofStep