Class Lrat.LratInferredClause.RatInfo

java.lang.Object
com.google.protobuf.AbstractMessageLite
com.google.protobuf.AbstractMessage
com.google.protobuf.GeneratedMessage
operations_research.sat.Lrat.LratInferredClause.RatInfo
All Implemented Interfaces:
com.google.protobuf.Message, com.google.protobuf.MessageLite, com.google.protobuf.MessageLiteOrBuilder, com.google.protobuf.MessageOrBuilder, Serializable, Lrat.LratInferredClause.RatInfoOrBuilder
Enclosing class:
Lrat.LratInferredClause
public static final class Lrat.LratInferredClause.RatInfo extends com.google.protobuf.GeneratedMessage implements Lrat.LratInferredClause.RatInfoOrBuilder
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.
Protobuf type operations_research.sat.LratInferredClause.RatInfo
See Also:

  • Field Details

    • RESOLVANT_ID_FIELD_NUMBER

      public static final int RESOLVANT_ID_FIELD_NUMBER
      See Also:

    • UNIT_IDS_FIELD_NUMBER

      public static final int UNIT_IDS_FIELD_NUMBER
      See Also:

  • Method Details

    • getDescriptor

      public static final com.google.protobuf.Descriptors.Descriptor getDescriptor()

    • internalGetFieldAccessorTable

      protected com.google.protobuf.GeneratedMessage.FieldAccessorTable internalGetFieldAccessorTable()
      Specified by:
      internalGetFieldAccessorTable in class com.google.protobuf.GeneratedMessage

    • hasResolvantId

      public boolean hasResolvantId()
      optional int64 resolvant_id = 1;
      Specified by:
      hasResolvantId in interface Lrat.LratInferredClause.RatInfoOrBuilder
      Returns:
      Whether the resolvantId field is set.

    • getResolvantId

      public long getResolvantId()
      optional int64 resolvant_id = 1;
      Specified by:
      getResolvantId in interface Lrat.LratInferredClause.RatInfoOrBuilder
      Returns:
      The resolvantId.

    • getUnitIdsList

      public List<Long> getUnitIdsList()
      repeated int64 unit_ids = 2 [packed = true];
      Specified by:
      getUnitIdsList in interface Lrat.LratInferredClause.RatInfoOrBuilder
      Returns:
      A list containing the unitIds.

    • getUnitIdsCount

      public int getUnitIdsCount()
      repeated int64 unit_ids = 2 [packed = true];
      Specified by:
      getUnitIdsCount in interface Lrat.LratInferredClause.RatInfoOrBuilder
      Returns:
      The count of unitIds.

    • getUnitIds

      public long getUnitIds(int index)
      repeated int64 unit_ids = 2 [packed = true];
      Specified by:
      getUnitIds in interface Lrat.LratInferredClause.RatInfoOrBuilder
      Parameters:
      index - The index of the element to return.
      Returns:
      The unitIds at the given index.

    • isInitialized

      public final boolean isInitialized()
      Specified by:
      isInitialized in interface com.google.protobuf.MessageLiteOrBuilder
      Overrides:
      isInitialized in class com.google.protobuf.GeneratedMessage

    • writeTo

      public void writeTo(com.google.protobuf.CodedOutputStream output) throws IOException
      Specified by:
      writeTo in interface com.google.protobuf.MessageLite
      Overrides:
      writeTo in class com.google.protobuf.GeneratedMessage
      Throws:
      IOException

    • getSerializedSize

      public int getSerializedSize()
      Specified by:
      getSerializedSize in interface com.google.protobuf.MessageLite
      Overrides:
      getSerializedSize in class com.google.protobuf.GeneratedMessage

    • equals

      public boolean equals(Object obj)
      Specified by:
      equals in interface com.google.protobuf.Message
      Overrides:
      equals in class com.google.protobuf.AbstractMessage

    • hashCode

      public int hashCode()
      Specified by:
      hashCode in interface com.google.protobuf.Message
      Overrides:
      hashCode in class com.google.protobuf.AbstractMessage

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(ByteBuffer data) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(ByteBuffer data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(com.google.protobuf.ByteString data) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(com.google.protobuf.ByteString data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(byte[] data) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(byte[] data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(InputStream input) throws IOException
      Throws:
      IOException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws IOException
      Throws:
      IOException

    • parseDelimitedFrom

      public static Lrat.LratInferredClause.RatInfo parseDelimitedFrom(InputStream input) throws IOException
      Throws:
      IOException

    • parseDelimitedFrom

      public static Lrat.LratInferredClause.RatInfo parseDelimitedFrom(InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws IOException
      Throws:
      IOException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(com.google.protobuf.CodedInputStream input) throws IOException
      Throws:
      IOException

    • parseFrom

      public static Lrat.LratInferredClause.RatInfo parseFrom(com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws IOException
      Throws:
      IOException

    • newBuilderForType

      public Lrat.LratInferredClause.RatInfo.Builder newBuilderForType()
      Specified by:
      newBuilderForType in interface com.google.protobuf.Message
      Specified by:
      newBuilderForType in interface com.google.protobuf.MessageLite

    • newBuilder

      public static Lrat.LratInferredClause.RatInfo.Builder newBuilder()

    • newBuilder

      public static Lrat.LratInferredClause.RatInfo.Builder newBuilder(Lrat.LratInferredClause.RatInfo prototype)

    • toBuilder

      public Lrat.LratInferredClause.RatInfo.Builder toBuilder()
      Specified by:
      toBuilder in interface com.google.protobuf.Message
      Specified by:
      toBuilder in interface com.google.protobuf.MessageLite

    • newBuilderForType

      protected Lrat.LratInferredClause.RatInfo.Builder newBuilderForType(com.google.protobuf.AbstractMessage.BuilderParent parent)
      Overrides:
      newBuilderForType in class com.google.protobuf.AbstractMessage

    • getDefaultInstance

      public static Lrat.LratInferredClause.RatInfo getDefaultInstance()

    • parser

      public static com.google.protobuf.Parser<Lrat.LratInferredClause.RatInfo> parser()

    • getParserForType

      public com.google.protobuf.Parser<Lrat.LratInferredClause.RatInfo> getParserForType()
      Specified by:
      getParserForType in interface com.google.protobuf.Message
      Specified by:
      getParserForType in interface com.google.protobuf.MessageLite
      Overrides:
      getParserForType in class com.google.protobuf.GeneratedMessage

    • getDefaultInstanceForType

      public Lrat.LratInferredClause.RatInfo getDefaultInstanceForType()
      Specified by:
      getDefaultInstanceForType in interface com.google.protobuf.MessageLiteOrBuilder
      Specified by:
      getDefaultInstanceForType in interface com.google.protobuf.MessageOrBuilder