Class Lrat.LratProofStep

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

  • Field Details

    • IMPORTED_CLAUSE_FIELD_NUMBER

      public static final int IMPORTED_CLAUSE_FIELD_NUMBER
      See Also:

    • INFERRED_CLAUSE_FIELD_NUMBER

      public static final int INFERRED_CLAUSE_FIELD_NUMBER
      See Also:

    • EXPORTED_CLAUSE_FIELD_NUMBER

      public static final int EXPORTED_CLAUSE_FIELD_NUMBER
      See Also:

    • DELETED_CLAUSES_FIELD_NUMBER

      public static final int DELETED_CLAUSES_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

    • getStepCase

      public Lrat.LratProofStep.StepCase getStepCase()
      Specified by:
      getStepCase in interface Lrat.LratProofStepOrBuilder

    • hasImportedClause

      public boolean hasImportedClause()
      .operations_research.sat.LratImportedClause imported_clause = 1;
      Specified by:
      hasImportedClause in interface Lrat.LratProofStepOrBuilder
      Returns:
      Whether the importedClause field is set.

    • getImportedClause

      public Lrat.LratImportedClause getImportedClause()
      .operations_research.sat.LratImportedClause imported_clause = 1;
      Specified by:
      getImportedClause in interface Lrat.LratProofStepOrBuilder
      Returns:
      The importedClause.

    • getImportedClauseOrBuilder

      public Lrat.LratImportedClauseOrBuilder getImportedClauseOrBuilder()
      .operations_research.sat.LratImportedClause imported_clause = 1;
      Specified by:
      getImportedClauseOrBuilder in interface Lrat.LratProofStepOrBuilder

    • hasInferredClause

      public boolean hasInferredClause()
      .operations_research.sat.LratInferredClause inferred_clause = 2;
      Specified by:
      hasInferredClause in interface Lrat.LratProofStepOrBuilder
      Returns:
      Whether the inferredClause field is set.

    • getInferredClause

      public Lrat.LratInferredClause getInferredClause()
      .operations_research.sat.LratInferredClause inferred_clause = 2;
      Specified by:
      getInferredClause in interface Lrat.LratProofStepOrBuilder
      Returns:
      The inferredClause.

    • getInferredClauseOrBuilder

      public Lrat.LratInferredClauseOrBuilder getInferredClauseOrBuilder()
      .operations_research.sat.LratInferredClause inferred_clause = 2;
      Specified by:
      getInferredClauseOrBuilder in interface Lrat.LratProofStepOrBuilder

    • hasExportedClause

      public boolean hasExportedClause()
      .operations_research.sat.LratExportedClause exported_clause = 3;
      Specified by:
      hasExportedClause in interface Lrat.LratProofStepOrBuilder
      Returns:
      Whether the exportedClause field is set.

    • getExportedClause

      public Lrat.LratExportedClause getExportedClause()
      .operations_research.sat.LratExportedClause exported_clause = 3;
      Specified by:
      getExportedClause in interface Lrat.LratProofStepOrBuilder
      Returns:
      The exportedClause.

    • getExportedClauseOrBuilder

      public Lrat.LratExportedClauseOrBuilder getExportedClauseOrBuilder()
      .operations_research.sat.LratExportedClause exported_clause = 3;
      Specified by:
      getExportedClauseOrBuilder in interface Lrat.LratProofStepOrBuilder

    • hasDeletedClauses

      public boolean hasDeletedClauses()
      .operations_research.sat.LratDeletedClauses deleted_clauses = 4;
      Specified by:
      hasDeletedClauses in interface Lrat.LratProofStepOrBuilder
      Returns:
      Whether the deletedClauses field is set.

    • getDeletedClauses

      public Lrat.LratDeletedClauses getDeletedClauses()
      .operations_research.sat.LratDeletedClauses deleted_clauses = 4;
      Specified by:
      getDeletedClauses in interface Lrat.LratProofStepOrBuilder
      Returns:
      The deletedClauses.

    • getDeletedClausesOrBuilder

      public Lrat.LratDeletedClausesOrBuilder getDeletedClausesOrBuilder()
      .operations_research.sat.LratDeletedClauses deleted_clauses = 4;
      Specified by:
      getDeletedClausesOrBuilder in interface Lrat.LratProofStepOrBuilder

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

    • parseFrom

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

    • parseFrom

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

    • parseFrom

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

    • parseFrom

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

    • parseFrom

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

    • parseFrom

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

    • parseDelimitedFrom

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

    • parseDelimitedFrom

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

    • parseFrom

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

    • parseFrom

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

    • newBuilderForType

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

    • newBuilder

      public static Lrat.LratProofStep.Builder newBuilder()

    • newBuilder

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

    • toBuilder

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

    • newBuilderForType

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

    • getDefaultInstance

      public static Lrat.LratProofStep getDefaultInstance()

    • parser

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

    • getParserForType

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