"""
@generated by mypy-protobuf.  Do not edit manually!
isort:skip_file
Protocol buffer to encode a Boolean satisfiability/optimization problem."""

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 LinearBooleanConstraint(google.protobuf.message.Message):
    """A linear Boolean constraint which is a bounded sum of linear terms. Each term
    beeing a literal times an integer coefficient. If we assume that a literal
    takes the value 1 if it is true and 0 otherwise, the constraint is:
      lower_bound <= ... + coefficients[i] * literals[i] + ... <= upper_bound
    """

    DESCRIPTOR: google.protobuf.descriptor.Descriptor

    LITERALS_FIELD_NUMBER: builtins.int
    COEFFICIENTS_FIELD_NUMBER: builtins.int
    LOWER_BOUND_FIELD_NUMBER: builtins.int
    UPPER_BOUND_FIELD_NUMBER: builtins.int
    NAME_FIELD_NUMBER: builtins.int
    lower_bound: builtins.int
    """Optional lower (resp. upper) bound of the constraint. If not present, it
    means that the constraint is not bounded in this direction. The bounds
    are INCLUSIVE.
    """
    upper_bound: builtins.int
    name: builtins.str
    """The name of this constraint."""
    @property
    def literals(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]:
        """Linear terms involved in this constraint.

        literals[i] is the signed representation of the i-th literal of the
        constraint and coefficients[i] its coefficients. The signed representation
        is as follow: for a 0-based variable index x, (x + 1) represents the
        variable x and -(x + 1) represents its negation.

        Note that the same variable shouldn't appear twice and that zero
        coefficients are not allowed.
        """

    @property
    def coefficients(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: ...
    def __init__(
        self,
        *,
        literals: collections.abc.Iterable[builtins.int] | None = ...,
        coefficients: collections.abc.Iterable[builtins.int] | None = ...,
        lower_bound: builtins.int | None = ...,
        upper_bound: builtins.int | None = ...,
        name: builtins.str | None = ...,
    ) -> None: ...
    _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["lower_bound", b"lower_bound", "name", b"name", "upper_bound", b"upper_bound"]
    def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ...
    _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["coefficients", b"coefficients", "literals", b"literals", "lower_bound", b"lower_bound", "name", b"name", "upper_bound", b"upper_bound"]
    def ClearField(self, field_name: _ClearFieldArgType) -> None: ...

Global___LinearBooleanConstraint: typing_extensions.TypeAlias = LinearBooleanConstraint

@typing.final
class LinearObjective(google.protobuf.message.Message):
    """The objective of an optimization problem."""

    DESCRIPTOR: google.protobuf.descriptor.Descriptor

    LITERALS_FIELD_NUMBER: builtins.int
    COEFFICIENTS_FIELD_NUMBER: builtins.int
    OFFSET_FIELD_NUMBER: builtins.int
    SCALING_FACTOR_FIELD_NUMBER: builtins.int
    offset: builtins.float
    """For a given variable assignment, the "real" problem objective value is
    'scaling_factor * (minimization_objective + offset)' where
    'minimization_objective is the one defined just above.

    Note that this is not what we minimize, but it is what we display.
    In particular if scaling_factor is negative, then the "real" problem is
    a maximization problem, even if the "internal" objective is minimized.
    """
    scaling_factor: builtins.float
    @property
    def literals(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]:
        """The goal is always to minimize the linear Boolean formula defined by these
        two fields: sum_i literal_i * coefficient_i where literal_i is 1 iff
        literal_i is true in a given assignment.

        Note that the same variable shouldn't appear twice and that zero
        coefficients are not allowed.
        """

    @property
    def coefficients(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: ...
    def __init__(
        self,
        *,
        literals: collections.abc.Iterable[builtins.int] | None = ...,
        coefficients: collections.abc.Iterable[builtins.int] | None = ...,
        offset: builtins.float | None = ...,
        scaling_factor: builtins.float | None = ...,
    ) -> None: ...
    _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["offset", b"offset", "scaling_factor", b"scaling_factor"]
    def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ...
    _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["coefficients", b"coefficients", "literals", b"literals", "offset", b"offset", "scaling_factor", b"scaling_factor"]
    def ClearField(self, field_name: _ClearFieldArgType) -> None: ...

Global___LinearObjective: typing_extensions.TypeAlias = LinearObjective

@typing.final
class BooleanAssignment(google.protobuf.message.Message):
    """Stores an assignment of variables as a list of true literals using their
    signed representation. There will be at most one literal per variable. The
    literals will be sorted by increasing variable index. The assignment may be
    partial in the sense that some variables may not appear and thus not be
    assigned.
    """

    DESCRIPTOR: google.protobuf.descriptor.Descriptor

    LITERALS_FIELD_NUMBER: builtins.int
    @property
    def literals(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.int]: ...
    def __init__(
        self,
        *,
        literals: collections.abc.Iterable[builtins.int] | None = ...,
    ) -> None: ...
    _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["literals", b"literals"]
    def ClearField(self, field_name: _ClearFieldArgType) -> None: ...

Global___BooleanAssignment: typing_extensions.TypeAlias = BooleanAssignment

@typing.final
class LinearBooleanProblem(google.protobuf.message.Message):
    """A linear Boolean problem."""

    DESCRIPTOR: google.protobuf.descriptor.Descriptor

    NAME_FIELD_NUMBER: builtins.int
    NUM_VARIABLES_FIELD_NUMBER: builtins.int
    CONSTRAINTS_FIELD_NUMBER: builtins.int
    OBJECTIVE_FIELD_NUMBER: builtins.int
    VAR_NAMES_FIELD_NUMBER: builtins.int
    ASSIGNMENT_FIELD_NUMBER: builtins.int
    ORIGINAL_NUM_VARIABLES_FIELD_NUMBER: builtins.int
    name: builtins.str
    """The name of the problem."""
    num_variables: builtins.int
    """The number of variables in the problem.
    All the signed representation of the problem literals must be in
    [-num_variables, num_variables], excluding 0.
    """
    original_num_variables: builtins.int
    """Hack: When converting a wcnf formulat to a LinearBooleanProblem, extra
    variables need to be created. This stores the number of variables in the
    original problem (which are in one to one correspondence with the first
    variables of this problem).
    """
    @property
    def constraints(self) -> google.protobuf.internal.containers.RepeatedCompositeFieldContainer[Global___LinearBooleanConstraint]:
        """The constraints of the problem."""

    @property
    def objective(self) -> Global___LinearObjective:
        """The objective of the problem.
        If left empty, we just have a satisfiability problem.
        """

    @property
    def var_names(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.str]:
        """The names of the problem variables. The variables index are 0-based and
        var_names[i] will be the name of the i-th variable which correspond to
        literals +(i + 1) or -(i + 1). This is optional and can be left empty.
        """

    @property
    def assignment(self) -> Global___BooleanAssignment:
        """Stores an assignment of the problem variables. That may be an initial
        feasible solution, just a partial assignment or the optimal solution.
        """

    def __init__(
        self,
        *,
        name: builtins.str | None = ...,
        num_variables: builtins.int | None = ...,
        constraints: collections.abc.Iterable[Global___LinearBooleanConstraint] | None = ...,
        objective: Global___LinearObjective | None = ...,
        var_names: collections.abc.Iterable[builtins.str] | None = ...,
        assignment: Global___BooleanAssignment | None = ...,
        original_num_variables: builtins.int | None = ...,
    ) -> None: ...
    _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["assignment", b"assignment", "name", b"name", "num_variables", b"num_variables", "objective", b"objective", "original_num_variables", b"original_num_variables"]
    def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ...
    _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["assignment", b"assignment", "constraints", b"constraints", "name", b"name", "num_variables", b"num_variables", "objective", b"objective", "original_num_variables", b"original_num_variables", "var_names", b"var_names"]
    def ClearField(self, field_name: _ClearFieldArgType) -> None: ...

Global___LinearBooleanProblem: typing_extensions.TypeAlias = LinearBooleanProblem