"""
@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
