Class Lrat.LratInferredClause

java.lang.Object
com.google.protobuf.AbstractMessageLite
com.google.protobuf.AbstractMessage
com.google.protobuf.GeneratedMessage
operations_research.sat.Lrat.LratInferredClause
All Implemented Interfaces:
com.google.protobuf.Message, com.google.protobuf.MessageLite, com.google.protobuf.MessageLiteOrBuilder, com.google.protobuf.MessageOrBuilder, Serializable, Lrat.LratInferredClauseOrBuilder
Enclosing class:
Lrat
public static final class Lrat.LratInferredClause extends com.google.protobuf.GeneratedMessage implements Lrat.LratInferredClauseOrBuilder
An LRAT inferred clause.
Protobuf type operations_research.sat.LratInferredClause
See Also:

  • Field Details

  • 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

    • hasClauseId

      public boolean hasClauseId()
      optional int64 clause_id = 1;
      Specified by:
      hasClauseId in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      Whether the clauseId field is set.

    • getClauseId

      public long getClauseId()
      optional int64 clause_id = 1;
      Specified by:
      getClauseId in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      The clauseId.

    • getLiteralsList

      public List<Integer> getLiteralsList()
      Literals are represented with LiteralIndex values.
      repeated int32 literals = 2 [packed = true];
      Specified by:
      getLiteralsList in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      A list containing the literals.

    • getLiteralsCount

      public int getLiteralsCount()
      Literals are represented with LiteralIndex values.
      repeated int32 literals = 2 [packed = true];
      Specified by:
      getLiteralsCount in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      The count of literals.

    • getLiterals

      public int getLiterals(int index)
      Literals are represented with LiteralIndex values.
      repeated int32 literals = 2 [packed = true];
      Specified by:
      getLiterals in interface Lrat.LratInferredClauseOrBuilder
      Parameters:
      index - The index of the element to return.
      Returns:
      The literals at the given index.

    • getUnitIdsList

      public List<Long> getUnitIdsList()
      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.
      repeated int64 unit_ids = 3 [packed = true];
      Specified by:
      getUnitIdsList in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      A list containing the unitIds.

    • getUnitIdsCount

      public int getUnitIdsCount()
      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.
      repeated int64 unit_ids = 3 [packed = true];
      Specified by:
      getUnitIdsCount in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      The count of unitIds.

    • getUnitIds

      public long getUnitIds(int index)
      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.
      repeated int64 unit_ids = 3 [packed = true];
      Specified by:
      getUnitIds in interface Lrat.LratInferredClauseOrBuilder
      Parameters:
      index - The index of the element to return.
      Returns:
      The unitIds at the given index.

    • getRatInfosList

      public List<Lrat.LratInferredClause.RatInfo> getRatInfosList()
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
      Specified by:
      getRatInfosList in interface Lrat.LratInferredClauseOrBuilder

    • getRatInfosOrBuilderList

      public List<? extends Lrat.LratInferredClause.RatInfoOrBuilder> getRatInfosOrBuilderList()
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
      Specified by:
      getRatInfosOrBuilderList in interface Lrat.LratInferredClauseOrBuilder

    • getRatInfosCount

      public int getRatInfosCount()
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
      Specified by:
      getRatInfosCount in interface Lrat.LratInferredClauseOrBuilder

    • getRatInfos

      public Lrat.LratInferredClause.RatInfo getRatInfos(int index)
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
      Specified by:
      getRatInfos in interface Lrat.LratInferredClauseOrBuilder

    • getRatInfosOrBuilder

      public Lrat.LratInferredClause.RatInfoOrBuilder getRatInfosOrBuilder(int index)
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
      Specified by:
      getRatInfosOrBuilder in interface Lrat.LratInferredClauseOrBuilder

    • hasExported

      public boolean hasExported()
      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.
      optional bool exported = 5;
      Specified by:
      hasExported in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      Whether the exported field is set.

    • getExported

      public boolean getExported()
      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.
      optional bool exported = 5;
      Specified by:
      getExported in interface Lrat.LratInferredClauseOrBuilder
      Returns:
      The exported.

    • 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 parseFrom(ByteBuffer data) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

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

    • parseFrom

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

    • parseFrom

      public static Lrat.LratInferredClause 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 parseFrom(byte[] data) throws com.google.protobuf.InvalidProtocolBufferException
      Throws:
      com.google.protobuf.InvalidProtocolBufferException

    • parseFrom

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

    • parseFrom

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

    • parseFrom

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

    • parseDelimitedFrom

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

    • parseDelimitedFrom

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

    • parseFrom

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

    • parseFrom

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

    • newBuilderForType

      public Lrat.LratInferredClause.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.Builder newBuilder()

    • newBuilder

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

    • toBuilder

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

    • newBuilderForType

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

    • getDefaultInstance

      public static Lrat.LratInferredClause getDefaultInstance()

    • parser

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

    • getParserForType

      public com.google.protobuf.Parser<Lrat.LratInferredClause> 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 getDefaultInstanceForType()
      Specified by:
      getDefaultInstanceForType in interface com.google.protobuf.MessageLiteOrBuilder
      Specified by:
      getDefaultInstanceForType in interface com.google.protobuf.MessageOrBuilder