Lrat.java

Go to the documentation of this file.

// Generated by the protocol buffer compiler.  DO NOT EDIT!
// NO CHECKED-IN PROTOBUF GENCODE
// source: ortools/sat/lrat.proto
// Protobuf Java Version: 4.33.1
 
package operations_research.sat;
 
@com.google.protobuf.Generated
public final class Lrat extends com.google.protobuf.GeneratedFile {
  private Lrat() {}
  static {
    com.google.protobuf.RuntimeVersion.validateProtobufGencodeVersion(
      com.google.protobuf.RuntimeVersion.RuntimeDomain.PUBLIC,
      /* major= */ 4,
      /* minor= */ 33,
      /* patch= */ 1,
      /* suffix= */ "",
      "Lrat");
  }
  public static void registerAllExtensions(
      com.google.protobuf.ExtensionRegistryLite registry) {
  }
 
  public static void registerAllExtensions(
      com.google.protobuf.ExtensionRegistry registry) {
    registerAllExtensions(
        (com.google.protobuf.ExtensionRegistryLite) registry);
  }
  public interface LratImportedClauseOrBuilder extends
      // @@protoc_insertion_point(interface_extends:operations_research.sat.LratImportedClause)
      com.google.protobuf.MessageOrBuilder {

    boolean hasClauseId();
    long getClauseId();

    java.util.List<java.lang.Integer> getLiteralsList();
    int getLiteralsCount();
    int getLiterals(int index);
  }

  public static final class LratImportedClause extends
      com.google.protobuf.GeneratedMessage implements
      // @@protoc_insertion_point(message_implements:operations_research.sat.LratImportedClause)
      LratImportedClauseOrBuilder {
  private static final long serialVersionUID = 0L;
    static {
      com.google.protobuf.RuntimeVersion.validateProtobufGencodeVersion(
        com.google.protobuf.RuntimeVersion.RuntimeDomain.PUBLIC,
        /* major= */ 4,
        /* minor= */ 33,
        /* patch= */ 1,
        /* suffix= */ "",
        "LratImportedClause");
    }
    // Use LratImportedClause.newBuilder() to construct.
    private LratImportedClause(com.google.protobuf.GeneratedMessage.Builder<?> builder) {
      super(builder);
    }
    private LratImportedClause() {
      literals_ = emptyIntList();
    }
 
    public static final com.google.protobuf.Descriptors.Descriptor
        getDescriptor() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratImportedClause_descriptor;
    }
 
    @java.lang.Override
    protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
        internalGetFieldAccessorTable() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratImportedClause_fieldAccessorTable
          .ensureFieldAccessorsInitialized(
              operations_research.sat.Lrat.LratImportedClause.class, operations_research.sat.Lrat.LratImportedClause.Builder.class);
    }
 
    private int bitField0_;
    public static final int CLAUSE_ID_FIELD_NUMBER = 1;
    private long clauseId_ = 0L;
    @java.lang.Override
    public boolean hasClauseId() {
      return ((bitField0_ & 0x00000001) != 0);
    }

    @java.lang.Override
    public long getClauseId() {
      return clauseId_;
    }
 
    public static final int LITERALS_FIELD_NUMBER = 2;
    @SuppressWarnings("serial")
    private com.google.protobuf.Internal.IntList literals_ =
        emptyIntList();
    @java.lang.Override
    public java.util.List<java.lang.Integer>
        getLiteralsList() {
      return literals_;
    }

    public int getLiteralsCount() {
      return literals_.size();
    }

    public int getLiterals(int index) {
      return literals_.getInt(index);
    }
    private int literalsMemoizedSerializedSize = -1;
 
    private byte memoizedIsInitialized = -1;
    @java.lang.Override
    public final boolean isInitialized() {
      byte isInitialized = memoizedIsInitialized;
      if (isInitialized == 1) return true;
      if (isInitialized == 0) return false;
 
      memoizedIsInitialized = 1;
      return true;
    }
 
    @java.lang.Override
    public void writeTo(com.google.protobuf.CodedOutputStream output)
                        throws java.io.IOException {
      getSerializedSize();
      if (((bitField0_ & 0x00000001) != 0)) {
        output.writeInt64(1, clauseId_);
      }
      if (getLiteralsList().size() > 0) {
        output.writeUInt32NoTag(18);
        output.writeUInt32NoTag(literalsMemoizedSerializedSize);
      }
      for (int i = 0; i < literals_.size(); i++) {
        output.writeInt32NoTag(literals_.getInt(i));
      }
      getUnknownFields().writeTo(output);
    }
 
    @java.lang.Override
    public int getSerializedSize() {
      int size = memoizedSize;
      if (size != -1) return size;
 
      size = 0;
      if (((bitField0_ & 0x00000001) != 0)) {
        size += com.google.protobuf.CodedOutputStream
          .computeInt64Size(1, clauseId_);
      }
      {
        int dataSize = 0;
        for (int i = 0; i < literals_.size(); i++) {
          dataSize += com.google.protobuf.CodedOutputStream
            .computeInt32SizeNoTag(literals_.getInt(i));
        }
        size += dataSize;
        if (!getLiteralsList().isEmpty()) {
          size += 1;
          size += com.google.protobuf.CodedOutputStream
              .computeInt32SizeNoTag(dataSize);
        }
        literalsMemoizedSerializedSize = dataSize;
      }
      size += getUnknownFields().getSerializedSize();
      memoizedSize = size;
      return size;
    }
 
    @java.lang.Override
    public boolean equals(final java.lang.Object obj) {
      if (obj == this) {
       return true;
      }
      if (!(obj instanceof operations_research.sat.Lrat.LratImportedClause)) {
        return super.equals(obj);
      }
      operations_research.sat.Lrat.LratImportedClause other = (operations_research.sat.Lrat.LratImportedClause) obj;
 
      if (hasClauseId() != other.hasClauseId()) return false;
      if (hasClauseId()) {
        if (getClauseId()
            != other.getClauseId()) return false;
      }
      if (!getLiteralsList()
          .equals(other.getLiteralsList())) return false;
      if (!getUnknownFields().equals(other.getUnknownFields())) return false;
      return true;
    }
 
    @java.lang.Override
    public int hashCode() {
      if (memoizedHashCode != 0) {
        return memoizedHashCode;
      }
      int hash = 41;
      hash = (19 * hash) + getDescriptor().hashCode();
      if (hasClauseId()) {
        hash = (37 * hash) + CLAUSE_ID_FIELD_NUMBER;
        hash = (53 * hash) + com.google.protobuf.Internal.hashLong(
            getClauseId());
      }
      if (getLiteralsCount() > 0) {
        hash = (37 * hash) + LITERALS_FIELD_NUMBER;
        hash = (53 * hash) + getLiteralsList().hashCode();
      }
      hash = (29 * hash) + getUnknownFields().hashCode();
      memoizedHashCode = hash;
      return hash;
    }
 
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        java.nio.ByteBuffer data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        java.nio.ByteBuffer data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        com.google.protobuf.ByteString data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        com.google.protobuf.ByteString data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(byte[] data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        byte[] data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    public static operations_research.sat.Lrat.LratImportedClause parseDelimitedFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input);
    }
 
    public static operations_research.sat.Lrat.LratImportedClause parseDelimitedFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        com.google.protobuf.CodedInputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratImportedClause parseFrom(
        com.google.protobuf.CodedInputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    @java.lang.Override
    public Builder newBuilderForType() { return newBuilder(); }
    public static Builder newBuilder() {
      return DEFAULT_INSTANCE.toBuilder();
    }
    public static Builder newBuilder(operations_research.sat.Lrat.LratImportedClause prototype) {
      return DEFAULT_INSTANCE.toBuilder().mergeFrom(prototype);
    }
    @java.lang.Override
    public Builder toBuilder() {
      return this == DEFAULT_INSTANCE
          ? new Builder() : new Builder().mergeFrom(this);
    }
 
    @java.lang.Override
    protected Builder newBuilderForType(
        com.google.protobuf.GeneratedMessage.BuilderParent parent) {
      Builder builder = new Builder(parent);
      return builder;
    }

    public static final class Builder extends
        com.google.protobuf.GeneratedMessage.Builder<Builder> implements
        // @@protoc_insertion_point(builder_implements:operations_research.sat.LratImportedClause)
        operations_research.sat.Lrat.LratImportedClauseOrBuilder {
      public static final com.google.protobuf.Descriptors.Descriptor
          getDescriptor() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratImportedClause_descriptor;
      }
 
      @java.lang.Override
      protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
          internalGetFieldAccessorTable() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratImportedClause_fieldAccessorTable
            .ensureFieldAccessorsInitialized(
                operations_research.sat.Lrat.LratImportedClause.class, operations_research.sat.Lrat.LratImportedClause.Builder.class);
      }
 
      // Construct using operations_research.sat.Lrat.LratImportedClause.newBuilder()
      private Builder() {
 
      }
 
      private Builder(
          com.google.protobuf.GeneratedMessage.BuilderParent parent) {
        super(parent);
 
      }
      @java.lang.Override
      public Builder clear() {
        super.clear();
        bitField0_ = 0;
        clauseId_ = 0L;
        literals_ = emptyIntList();
        return this;
      }
 
      @java.lang.Override
      public com.google.protobuf.Descriptors.Descriptor
          getDescriptorForType() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratImportedClause_descriptor;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratImportedClause getDefaultInstanceForType() {
        return operations_research.sat.Lrat.LratImportedClause.getDefaultInstance();
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratImportedClause build() {
        operations_research.sat.Lrat.LratImportedClause result = buildPartial();
        if (!result.isInitialized()) {
          throw newUninitializedMessageException(result);
        }
        return result;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratImportedClause buildPartial() {
        operations_research.sat.Lrat.LratImportedClause result = new operations_research.sat.Lrat.LratImportedClause(this);
        if (bitField0_ != 0) { buildPartial0(result); }
        onBuilt();
        return result;
      }
 
      private void buildPartial0(operations_research.sat.Lrat.LratImportedClause result) {
        int from_bitField0_ = bitField0_;
        int to_bitField0_ = 0;
        if (((from_bitField0_ & 0x00000001) != 0)) {
          result.clauseId_ = clauseId_;
          to_bitField0_ |= 0x00000001;
        }
        if (((from_bitField0_ & 0x00000002) != 0)) {
          literals_.makeImmutable();
          result.literals_ = literals_;
        }
        result.bitField0_ |= to_bitField0_;
      }
 
      @java.lang.Override
      public Builder mergeFrom(com.google.protobuf.Message other) {
        if (other instanceof operations_research.sat.Lrat.LratImportedClause) {
          return mergeFrom((operations_research.sat.Lrat.LratImportedClause)other);
        } else {
          super.mergeFrom(other);
          return this;
        }
      }
 
      public Builder mergeFrom(operations_research.sat.Lrat.LratImportedClause other) {
        if (other == operations_research.sat.Lrat.LratImportedClause.getDefaultInstance()) return this;
        if (other.hasClauseId()) {
          setClauseId(other.getClauseId());
        }
        if (!other.literals_.isEmpty()) {
          if (literals_.isEmpty()) {
            literals_ = other.literals_;
            literals_.makeImmutable();
            bitField0_ |= 0x00000002;
          } else {
            ensureLiteralsIsMutable();
            literals_.addAll(other.literals_);
          }
          onChanged();
        }
        this.mergeUnknownFields(other.getUnknownFields());
        onChanged();
        return this;
      }
 
      @java.lang.Override
      public final boolean isInitialized() {
        return true;
      }
 
      @java.lang.Override
      public Builder mergeFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        if (extensionRegistry == null) {
          throw new java.lang.NullPointerException();
        }
        try {
          boolean done = false;
          while (!done) {
            int tag = input.readTag();
            switch (tag) {
              case 0:
                done = true;
                break;
              case 8: {
                clauseId_ = input.readInt64();
                bitField0_ |= 0x00000001;
                break;
              } // case 8
              case 16: {
                int v = input.readInt32();
                ensureLiteralsIsMutable();
                literals_.addInt(v);
                break;
              } // case 16
              case 18: {
                int length = input.readRawVarint32();
                int limit = input.pushLimit(length);
                ensureLiteralsIsMutable();
                while (input.getBytesUntilLimit() > 0) {
                  literals_.addInt(input.readInt32());
                }
                input.popLimit(limit);
                break;
              } // case 18
              default: {
                if (!super.parseUnknownField(input, extensionRegistry, tag)) {
                  done = true; // was an endgroup tag
                }
                break;
              } // default:
            } // switch (tag)
          } // while (!done)
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.unwrapIOException();
        } finally {
          onChanged();
        } // finally
        return this;
      }
      private int bitField0_;
 
      private long clauseId_ ;
      @java.lang.Override
      public boolean hasClauseId() {
        return ((bitField0_ & 0x00000001) != 0);
      }

      @java.lang.Override
      public long getClauseId() {
        return clauseId_;
      }

      public Builder setClauseId(long value) {
 
        clauseId_ = value;
        bitField0_ |= 0x00000001;
        onChanged();
        return this;
      }

      public Builder clearClauseId() {
        bitField0_ = (bitField0_ & ~0x00000001);
        clauseId_ = 0L;
        onChanged();
        return this;
      }
 
      private com.google.protobuf.Internal.IntList literals_ = emptyIntList();
      private void ensureLiteralsIsMutable() {
        if (!literals_.isModifiable()) {
          literals_ = makeMutableCopy(literals_);
        }
        bitField0_ |= 0x00000002;
      }
      public java.util.List<java.lang.Integer>
          getLiteralsList() {
        literals_.makeImmutable();
        return literals_;
      }

      public int getLiteralsCount() {
        return literals_.size();
      }

      public int getLiterals(int index) {
        return literals_.getInt(index);
      }

      public Builder setLiterals(
          int index, int value) {
 
        ensureLiteralsIsMutable();
        literals_.setInt(index, value);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder addLiterals(int value) {
 
        ensureLiteralsIsMutable();
        literals_.addInt(value);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder addAllLiterals(
          java.lang.Iterable<? extends java.lang.Integer> values) {
        ensureLiteralsIsMutable();
        com.google.protobuf.AbstractMessageLite.Builder.addAll(
            values, literals_);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder clearLiterals() {
        literals_ = emptyIntList();
        bitField0_ = (bitField0_ & ~0x00000002);
        onChanged();
        return this;
      }
 
      // @@protoc_insertion_point(builder_scope:operations_research.sat.LratImportedClause)
    }
 
    // @@protoc_insertion_point(class_scope:operations_research.sat.LratImportedClause)
    private static final operations_research.sat.Lrat.LratImportedClause DEFAULT_INSTANCE;
    static {
      DEFAULT_INSTANCE = new operations_research.sat.Lrat.LratImportedClause();
    }
 
    public static operations_research.sat.Lrat.LratImportedClause getDefaultInstance() {
      return DEFAULT_INSTANCE;
    }
 
    private static final com.google.protobuf.Parser<LratImportedClause>
        PARSER = new com.google.protobuf.AbstractParser<LratImportedClause>() {
      @java.lang.Override
      public LratImportedClause parsePartialFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        Builder builder = newBuilder();
        try {
          builder.mergeFrom(input, extensionRegistry);
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.setUnfinishedMessage(builder.buildPartial());
        } catch (com.google.protobuf.UninitializedMessageException e) {
          throw e.asInvalidProtocolBufferException().setUnfinishedMessage(builder.buildPartial());
        } catch (java.io.IOException e) {
          throw new com.google.protobuf.InvalidProtocolBufferException(e)
              .setUnfinishedMessage(builder.buildPartial());
        }
        return builder.buildPartial();
      }
    };
 
    public static com.google.protobuf.Parser<LratImportedClause> parser() {
      return PARSER;
    }
 
    @java.lang.Override
    public com.google.protobuf.Parser<LratImportedClause> getParserForType() {
      return PARSER;
    }
 
    @java.lang.Override
    public operations_research.sat.Lrat.LratImportedClause getDefaultInstanceForType() {
      return DEFAULT_INSTANCE;
    }
 
  }
 
  public interface LratInferredClauseOrBuilder extends
      // @@protoc_insertion_point(interface_extends:operations_research.sat.LratInferredClause)
      com.google.protobuf.MessageOrBuilder {

    boolean hasClauseId();
    long getClauseId();

    java.util.List<java.lang.Integer> getLiteralsList();
    int getLiteralsCount();
    int getLiterals(int index);

    java.util.List<java.lang.Long> getUnitIdsList();
    int getUnitIdsCount();
    long getUnitIds(int index);

    java.util.List<operations_research.sat.Lrat.LratInferredClause.RatInfo> 
        getRatInfosList();
    operations_research.sat.Lrat.LratInferredClause.RatInfo getRatInfos(int index);
    int getRatInfosCount();
    java.util.List<? extends operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder> 
        getRatInfosOrBuilderList();
    operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder getRatInfosOrBuilder(
        int index);

    boolean hasExported();
    boolean getExported();
  }

  public static final class LratInferredClause extends
      com.google.protobuf.GeneratedMessage implements
      // @@protoc_insertion_point(message_implements:operations_research.sat.LratInferredClause)
      LratInferredClauseOrBuilder {
  private static final long serialVersionUID = 0L;
    static {
      com.google.protobuf.RuntimeVersion.validateProtobufGencodeVersion(
        com.google.protobuf.RuntimeVersion.RuntimeDomain.PUBLIC,
        /* major= */ 4,
        /* minor= */ 33,
        /* patch= */ 1,
        /* suffix= */ "",
        "LratInferredClause");
    }
    // Use LratInferredClause.newBuilder() to construct.
    private LratInferredClause(com.google.protobuf.GeneratedMessage.Builder<?> builder) {
      super(builder);
    }
    private LratInferredClause() {
      literals_ = emptyIntList();
      unitIds_ = emptyLongList();
      ratInfos_ = java.util.Collections.emptyList();
    }
 
    public static final com.google.protobuf.Descriptors.Descriptor
        getDescriptor() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_descriptor;
    }
 
    @java.lang.Override
    protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
        internalGetFieldAccessorTable() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_fieldAccessorTable
          .ensureFieldAccessorsInitialized(
              operations_research.sat.Lrat.LratInferredClause.class, operations_research.sat.Lrat.LratInferredClause.Builder.class);
    }
 
    public interface RatInfoOrBuilder extends
        // @@protoc_insertion_point(interface_extends:operations_research.sat.LratInferredClause.RatInfo)
        com.google.protobuf.MessageOrBuilder {

      boolean hasResolvantId();
      long getResolvantId();

      java.util.List<java.lang.Long> getUnitIdsList();
      int getUnitIdsCount();
      long getUnitIds(int index);
    }

    public static final class RatInfo extends
        com.google.protobuf.GeneratedMessage implements
        // @@protoc_insertion_point(message_implements:operations_research.sat.LratInferredClause.RatInfo)
        RatInfoOrBuilder {
    private static final long serialVersionUID = 0L;
      static {
        com.google.protobuf.RuntimeVersion.validateProtobufGencodeVersion(
          com.google.protobuf.RuntimeVersion.RuntimeDomain.PUBLIC,
          /* major= */ 4,
          /* minor= */ 33,
          /* patch= */ 1,
          /* suffix= */ "",
          "RatInfo");
      }
      // Use RatInfo.newBuilder() to construct.
      private RatInfo(com.google.protobuf.GeneratedMessage.Builder<?> builder) {
        super(builder);
      }
      private RatInfo() {
        unitIds_ = emptyLongList();
      }
 
      public static final com.google.protobuf.Descriptors.Descriptor
          getDescriptor() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_RatInfo_descriptor;
      }
 
      @java.lang.Override
      protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
          internalGetFieldAccessorTable() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_RatInfo_fieldAccessorTable
            .ensureFieldAccessorsInitialized(
                operations_research.sat.Lrat.LratInferredClause.RatInfo.class, operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.class);
      }
 
      private int bitField0_;
      public static final int RESOLVANT_ID_FIELD_NUMBER = 1;
      private long resolvantId_ = 0L;
      @java.lang.Override
      public boolean hasResolvantId() {
        return ((bitField0_ & 0x00000001) != 0);
      }

      @java.lang.Override
      public long getResolvantId() {
        return resolvantId_;
      }
 
      public static final int UNIT_IDS_FIELD_NUMBER = 2;
      @SuppressWarnings("serial")
      private com.google.protobuf.Internal.LongList unitIds_ =
          emptyLongList();
      @java.lang.Override
      public java.util.List<java.lang.Long>
          getUnitIdsList() {
        return unitIds_;
      }

      public int getUnitIdsCount() {
        return unitIds_.size();
      }

      public long getUnitIds(int index) {
        return unitIds_.getLong(index);
      }
      private int unitIdsMemoizedSerializedSize = -1;
 
      private byte memoizedIsInitialized = -1;
      @java.lang.Override
      public final boolean isInitialized() {
        byte isInitialized = memoizedIsInitialized;
        if (isInitialized == 1) return true;
        if (isInitialized == 0) return false;
 
        memoizedIsInitialized = 1;
        return true;
      }
 
      @java.lang.Override
      public void writeTo(com.google.protobuf.CodedOutputStream output)
                          throws java.io.IOException {
        getSerializedSize();
        if (((bitField0_ & 0x00000001) != 0)) {
          output.writeInt64(1, resolvantId_);
        }
        if (getUnitIdsList().size() > 0) {
          output.writeUInt32NoTag(18);
          output.writeUInt32NoTag(unitIdsMemoizedSerializedSize);
        }
        for (int i = 0; i < unitIds_.size(); i++) {
          output.writeInt64NoTag(unitIds_.getLong(i));
        }
        getUnknownFields().writeTo(output);
      }
 
      @java.lang.Override
      public int getSerializedSize() {
        int size = memoizedSize;
        if (size != -1) return size;
 
        size = 0;
        if (((bitField0_ & 0x00000001) != 0)) {
          size += com.google.protobuf.CodedOutputStream
            .computeInt64Size(1, resolvantId_);
        }
        {
          int dataSize = 0;
          for (int i = 0; i < unitIds_.size(); i++) {
            dataSize += com.google.protobuf.CodedOutputStream
              .computeInt64SizeNoTag(unitIds_.getLong(i));
          }
          size += dataSize;
          if (!getUnitIdsList().isEmpty()) {
            size += 1;
            size += com.google.protobuf.CodedOutputStream
                .computeInt32SizeNoTag(dataSize);
          }
          unitIdsMemoizedSerializedSize = dataSize;
        }
        size += getUnknownFields().getSerializedSize();
        memoizedSize = size;
        return size;
      }
 
      @java.lang.Override
      public boolean equals(final java.lang.Object obj) {
        if (obj == this) {
         return true;
        }
        if (!(obj instanceof operations_research.sat.Lrat.LratInferredClause.RatInfo)) {
          return super.equals(obj);
        }
        operations_research.sat.Lrat.LratInferredClause.RatInfo other = (operations_research.sat.Lrat.LratInferredClause.RatInfo) obj;
 
        if (hasResolvantId() != other.hasResolvantId()) return false;
        if (hasResolvantId()) {
          if (getResolvantId()
              != other.getResolvantId()) return false;
        }
        if (!getUnitIdsList()
            .equals(other.getUnitIdsList())) return false;
        if (!getUnknownFields().equals(other.getUnknownFields())) return false;
        return true;
      }
 
      @java.lang.Override
      public int hashCode() {
        if (memoizedHashCode != 0) {
          return memoizedHashCode;
        }
        int hash = 41;
        hash = (19 * hash) + getDescriptor().hashCode();
        if (hasResolvantId()) {
          hash = (37 * hash) + RESOLVANT_ID_FIELD_NUMBER;
          hash = (53 * hash) + com.google.protobuf.Internal.hashLong(
              getResolvantId());
        }
        if (getUnitIdsCount() > 0) {
          hash = (37 * hash) + UNIT_IDS_FIELD_NUMBER;
          hash = (53 * hash) + getUnitIdsList().hashCode();
        }
        hash = (29 * hash) + getUnknownFields().hashCode();
        memoizedHashCode = hash;
        return hash;
      }
 
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          java.nio.ByteBuffer data)
          throws com.google.protobuf.InvalidProtocolBufferException {
        return PARSER.parseFrom(data);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          java.nio.ByteBuffer data,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        return PARSER.parseFrom(data, extensionRegistry);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          com.google.protobuf.ByteString data)
          throws com.google.protobuf.InvalidProtocolBufferException {
        return PARSER.parseFrom(data);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          com.google.protobuf.ByteString data,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        return PARSER.parseFrom(data, extensionRegistry);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(byte[] data)
          throws com.google.protobuf.InvalidProtocolBufferException {
        return PARSER.parseFrom(data);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          byte[] data,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        return PARSER.parseFrom(data, extensionRegistry);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(java.io.InputStream input)
          throws java.io.IOException {
        return com.google.protobuf.GeneratedMessage
            .parseWithIOException(PARSER, input);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          java.io.InputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        return com.google.protobuf.GeneratedMessage
            .parseWithIOException(PARSER, input, extensionRegistry);
      }
 
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseDelimitedFrom(java.io.InputStream input)
          throws java.io.IOException {
        return com.google.protobuf.GeneratedMessage
            .parseDelimitedWithIOException(PARSER, input);
      }
 
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseDelimitedFrom(
          java.io.InputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        return com.google.protobuf.GeneratedMessage
            .parseDelimitedWithIOException(PARSER, input, extensionRegistry);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          com.google.protobuf.CodedInputStream input)
          throws java.io.IOException {
        return com.google.protobuf.GeneratedMessage
            .parseWithIOException(PARSER, input);
      }
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        return com.google.protobuf.GeneratedMessage
            .parseWithIOException(PARSER, input, extensionRegistry);
      }
 
      @java.lang.Override
      public Builder newBuilderForType() { return newBuilder(); }
      public static Builder newBuilder() {
        return DEFAULT_INSTANCE.toBuilder();
      }
      public static Builder newBuilder(operations_research.sat.Lrat.LratInferredClause.RatInfo prototype) {
        return DEFAULT_INSTANCE.toBuilder().mergeFrom(prototype);
      }
      @java.lang.Override
      public Builder toBuilder() {
        return this == DEFAULT_INSTANCE
            ? new Builder() : new Builder().mergeFrom(this);
      }
 
      @java.lang.Override
      protected Builder newBuilderForType(
          com.google.protobuf.GeneratedMessage.BuilderParent parent) {
        Builder builder = new Builder(parent);
        return builder;
      }

      public static final class Builder extends
          com.google.protobuf.GeneratedMessage.Builder<Builder> implements
          // @@protoc_insertion_point(builder_implements:operations_research.sat.LratInferredClause.RatInfo)
          operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder {
        public static final com.google.protobuf.Descriptors.Descriptor
            getDescriptor() {
          return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_RatInfo_descriptor;
        }
 
        @java.lang.Override
        protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
            internalGetFieldAccessorTable() {
          return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_RatInfo_fieldAccessorTable
              .ensureFieldAccessorsInitialized(
                  operations_research.sat.Lrat.LratInferredClause.RatInfo.class, operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.class);
        }
 
        // Construct using operations_research.sat.Lrat.LratInferredClause.RatInfo.newBuilder()
        private Builder() {
 
        }
 
        private Builder(
            com.google.protobuf.GeneratedMessage.BuilderParent parent) {
          super(parent);
 
        }
        @java.lang.Override
        public Builder clear() {
          super.clear();
          bitField0_ = 0;
          resolvantId_ = 0L;
          unitIds_ = emptyLongList();
          return this;
        }
 
        @java.lang.Override
        public com.google.protobuf.Descriptors.Descriptor
            getDescriptorForType() {
          return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_RatInfo_descriptor;
        }
 
        @java.lang.Override
        public operations_research.sat.Lrat.LratInferredClause.RatInfo getDefaultInstanceForType() {
          return operations_research.sat.Lrat.LratInferredClause.RatInfo.getDefaultInstance();
        }
 
        @java.lang.Override
        public operations_research.sat.Lrat.LratInferredClause.RatInfo build() {
          operations_research.sat.Lrat.LratInferredClause.RatInfo result = buildPartial();
          if (!result.isInitialized()) {
            throw newUninitializedMessageException(result);
          }
          return result;
        }
 
        @java.lang.Override
        public operations_research.sat.Lrat.LratInferredClause.RatInfo buildPartial() {
          operations_research.sat.Lrat.LratInferredClause.RatInfo result = new operations_research.sat.Lrat.LratInferredClause.RatInfo(this);
          if (bitField0_ != 0) { buildPartial0(result); }
          onBuilt();
          return result;
        }
 
        private void buildPartial0(operations_research.sat.Lrat.LratInferredClause.RatInfo result) {
          int from_bitField0_ = bitField0_;
          int to_bitField0_ = 0;
          if (((from_bitField0_ & 0x00000001) != 0)) {
            result.resolvantId_ = resolvantId_;
            to_bitField0_ |= 0x00000001;
          }
          if (((from_bitField0_ & 0x00000002) != 0)) {
            unitIds_.makeImmutable();
            result.unitIds_ = unitIds_;
          }
          result.bitField0_ |= to_bitField0_;
        }
 
        @java.lang.Override
        public Builder mergeFrom(com.google.protobuf.Message other) {
          if (other instanceof operations_research.sat.Lrat.LratInferredClause.RatInfo) {
            return mergeFrom((operations_research.sat.Lrat.LratInferredClause.RatInfo)other);
          } else {
            super.mergeFrom(other);
            return this;
          }
        }
 
        public Builder mergeFrom(operations_research.sat.Lrat.LratInferredClause.RatInfo other) {
          if (other == operations_research.sat.Lrat.LratInferredClause.RatInfo.getDefaultInstance()) return this;
          if (other.hasResolvantId()) {
            setResolvantId(other.getResolvantId());
          }
          if (!other.unitIds_.isEmpty()) {
            if (unitIds_.isEmpty()) {
              unitIds_ = other.unitIds_;
              unitIds_.makeImmutable();
              bitField0_ |= 0x00000002;
            } else {
              ensureUnitIdsIsMutable();
              unitIds_.addAll(other.unitIds_);
            }
            onChanged();
          }
          this.mergeUnknownFields(other.getUnknownFields());
          onChanged();
          return this;
        }
 
        @java.lang.Override
        public final boolean isInitialized() {
          return true;
        }
 
        @java.lang.Override
        public Builder mergeFrom(
            com.google.protobuf.CodedInputStream input,
            com.google.protobuf.ExtensionRegistryLite extensionRegistry)
            throws java.io.IOException {
          if (extensionRegistry == null) {
            throw new java.lang.NullPointerException();
          }
          try {
            boolean done = false;
            while (!done) {
              int tag = input.readTag();
              switch (tag) {
                case 0:
                  done = true;
                  break;
                case 8: {
                  resolvantId_ = input.readInt64();
                  bitField0_ |= 0x00000001;
                  break;
                } // case 8
                case 16: {
                  long v = input.readInt64();
                  ensureUnitIdsIsMutable();
                  unitIds_.addLong(v);
                  break;
                } // case 16
                case 18: {
                  int length = input.readRawVarint32();
                  int limit = input.pushLimit(length);
                  ensureUnitIdsIsMutable();
                  while (input.getBytesUntilLimit() > 0) {
                    unitIds_.addLong(input.readInt64());
                  }
                  input.popLimit(limit);
                  break;
                } // case 18
                default: {
                  if (!super.parseUnknownField(input, extensionRegistry, tag)) {
                    done = true; // was an endgroup tag
                  }
                  break;
                } // default:
              } // switch (tag)
            } // while (!done)
          } catch (com.google.protobuf.InvalidProtocolBufferException e) {
            throw e.unwrapIOException();
          } finally {
            onChanged();
          } // finally
          return this;
        }
        private int bitField0_;
 
        private long resolvantId_ ;
        @java.lang.Override
        public boolean hasResolvantId() {
          return ((bitField0_ & 0x00000001) != 0);
        }

        @java.lang.Override
        public long getResolvantId() {
          return resolvantId_;
        }

        public Builder setResolvantId(long value) {
 
          resolvantId_ = value;
          bitField0_ |= 0x00000001;
          onChanged();
          return this;
        }

        public Builder clearResolvantId() {
          bitField0_ = (bitField0_ & ~0x00000001);
          resolvantId_ = 0L;
          onChanged();
          return this;
        }
 
        private com.google.protobuf.Internal.LongList unitIds_ = emptyLongList();
        private void ensureUnitIdsIsMutable() {
          if (!unitIds_.isModifiable()) {
            unitIds_ = makeMutableCopy(unitIds_);
          }
          bitField0_ |= 0x00000002;
        }
        public java.util.List<java.lang.Long>
            getUnitIdsList() {
          unitIds_.makeImmutable();
          return unitIds_;
        }

        public int getUnitIdsCount() {
          return unitIds_.size();
        }

        public long getUnitIds(int index) {
          return unitIds_.getLong(index);
        }

        public Builder setUnitIds(
            int index, long value) {
 
          ensureUnitIdsIsMutable();
          unitIds_.setLong(index, value);
          bitField0_ |= 0x00000002;
          onChanged();
          return this;
        }

        public Builder addUnitIds(long value) {
 
          ensureUnitIdsIsMutable();
          unitIds_.addLong(value);
          bitField0_ |= 0x00000002;
          onChanged();
          return this;
        }

        public Builder addAllUnitIds(
            java.lang.Iterable<? extends java.lang.Long> values) {
          ensureUnitIdsIsMutable();
          com.google.protobuf.AbstractMessageLite.Builder.addAll(
              values, unitIds_);
          bitField0_ |= 0x00000002;
          onChanged();
          return this;
        }

        public Builder clearUnitIds() {
          unitIds_ = emptyLongList();
          bitField0_ = (bitField0_ & ~0x00000002);
          onChanged();
          return this;
        }
 
        // @@protoc_insertion_point(builder_scope:operations_research.sat.LratInferredClause.RatInfo)
      }
 
      // @@protoc_insertion_point(class_scope:operations_research.sat.LratInferredClause.RatInfo)
      private static final operations_research.sat.Lrat.LratInferredClause.RatInfo DEFAULT_INSTANCE;
      static {
        DEFAULT_INSTANCE = new operations_research.sat.Lrat.LratInferredClause.RatInfo();
      }
 
      public static operations_research.sat.Lrat.LratInferredClause.RatInfo getDefaultInstance() {
        return DEFAULT_INSTANCE;
      }
 
      private static final com.google.protobuf.Parser<RatInfo>
          PARSER = new com.google.protobuf.AbstractParser<RatInfo>() {
        @java.lang.Override
        public RatInfo parsePartialFrom(
            com.google.protobuf.CodedInputStream input,
            com.google.protobuf.ExtensionRegistryLite extensionRegistry)
            throws com.google.protobuf.InvalidProtocolBufferException {
          Builder builder = newBuilder();
          try {
            builder.mergeFrom(input, extensionRegistry);
          } catch (com.google.protobuf.InvalidProtocolBufferException e) {
            throw e.setUnfinishedMessage(builder.buildPartial());
          } catch (com.google.protobuf.UninitializedMessageException e) {
            throw e.asInvalidProtocolBufferException().setUnfinishedMessage(builder.buildPartial());
          } catch (java.io.IOException e) {
            throw new com.google.protobuf.InvalidProtocolBufferException(e)
                .setUnfinishedMessage(builder.buildPartial());
          }
          return builder.buildPartial();
        }
      };
 
      public static com.google.protobuf.Parser<RatInfo> parser() {
        return PARSER;
      }
 
      @java.lang.Override
      public com.google.protobuf.Parser<RatInfo> getParserForType() {
        return PARSER;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratInferredClause.RatInfo getDefaultInstanceForType() {
        return DEFAULT_INSTANCE;
      }
 
    }
 
    private int bitField0_;
    public static final int CLAUSE_ID_FIELD_NUMBER = 1;
    private long clauseId_ = 0L;
    @java.lang.Override
    public boolean hasClauseId() {
      return ((bitField0_ & 0x00000001) != 0);
    }

    @java.lang.Override
    public long getClauseId() {
      return clauseId_;
    }
 
    public static final int LITERALS_FIELD_NUMBER = 2;
    @SuppressWarnings("serial")
    private com.google.protobuf.Internal.IntList literals_ =
        emptyIntList();
    @java.lang.Override
    public java.util.List<java.lang.Integer>
        getLiteralsList() {
      return literals_;
    }

    public int getLiteralsCount() {
      return literals_.size();
    }

    public int getLiterals(int index) {
      return literals_.getInt(index);
    }
    private int literalsMemoizedSerializedSize = -1;
 
    public static final int UNIT_IDS_FIELD_NUMBER = 3;
    @SuppressWarnings("serial")
    private com.google.protobuf.Internal.LongList unitIds_ =
        emptyLongList();
    @java.lang.Override
    public java.util.List<java.lang.Long>
        getUnitIdsList() {
      return unitIds_;
    }

    public int getUnitIdsCount() {
      return unitIds_.size();
    }

    public long getUnitIds(int index) {
      return unitIds_.getLong(index);
    }
    private int unitIdsMemoizedSerializedSize = -1;
 
    public static final int RAT_INFOS_FIELD_NUMBER = 4;
    @SuppressWarnings("serial")
    private java.util.List<operations_research.sat.Lrat.LratInferredClause.RatInfo> ratInfos_;
    @java.lang.Override
    public java.util.List<operations_research.sat.Lrat.LratInferredClause.RatInfo> getRatInfosList() {
      return ratInfos_;
    }

    @java.lang.Override
    public java.util.List<? extends operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder> 
        getRatInfosOrBuilderList() {
      return ratInfos_;
    }

    @java.lang.Override
    public int getRatInfosCount() {
      return ratInfos_.size();
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratInferredClause.RatInfo getRatInfos(int index) {
      return ratInfos_.get(index);
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder getRatInfosOrBuilder(
        int index) {
      return ratInfos_.get(index);
    }
 
    public static final int EXPORTED_FIELD_NUMBER = 5;
    private boolean exported_ = false;
    @java.lang.Override
    public boolean hasExported() {
      return ((bitField0_ & 0x00000002) != 0);
    }

    @java.lang.Override
    public boolean getExported() {
      return exported_;
    }
 
    private byte memoizedIsInitialized = -1;
    @java.lang.Override
    public final boolean isInitialized() {
      byte isInitialized = memoizedIsInitialized;
      if (isInitialized == 1) return true;
      if (isInitialized == 0) return false;
 
      memoizedIsInitialized = 1;
      return true;
    }
 
    @java.lang.Override
    public void writeTo(com.google.protobuf.CodedOutputStream output)
                        throws java.io.IOException {
      getSerializedSize();
      if (((bitField0_ & 0x00000001) != 0)) {
        output.writeInt64(1, clauseId_);
      }
      if (getLiteralsList().size() > 0) {
        output.writeUInt32NoTag(18);
        output.writeUInt32NoTag(literalsMemoizedSerializedSize);
      }
      for (int i = 0; i < literals_.size(); i++) {
        output.writeInt32NoTag(literals_.getInt(i));
      }
      if (getUnitIdsList().size() > 0) {
        output.writeUInt32NoTag(26);
        output.writeUInt32NoTag(unitIdsMemoizedSerializedSize);
      }
      for (int i = 0; i < unitIds_.size(); i++) {
        output.writeInt64NoTag(unitIds_.getLong(i));
      }
      for (int i = 0; i < ratInfos_.size(); i++) {
        output.writeMessage(4, ratInfos_.get(i));
      }
      if (((bitField0_ & 0x00000002) != 0)) {
        output.writeBool(5, exported_);
      }
      getUnknownFields().writeTo(output);
    }
 
    @java.lang.Override
    public int getSerializedSize() {
      int size = memoizedSize;
      if (size != -1) return size;
 
      size = 0;
      if (((bitField0_ & 0x00000001) != 0)) {
        size += com.google.protobuf.CodedOutputStream
          .computeInt64Size(1, clauseId_);
      }
      {
        int dataSize = 0;
        for (int i = 0; i < literals_.size(); i++) {
          dataSize += com.google.protobuf.CodedOutputStream
            .computeInt32SizeNoTag(literals_.getInt(i));
        }
        size += dataSize;
        if (!getLiteralsList().isEmpty()) {
          size += 1;
          size += com.google.protobuf.CodedOutputStream
              .computeInt32SizeNoTag(dataSize);
        }
        literalsMemoizedSerializedSize = dataSize;
      }
      {
        int dataSize = 0;
        for (int i = 0; i < unitIds_.size(); i++) {
          dataSize += com.google.protobuf.CodedOutputStream
            .computeInt64SizeNoTag(unitIds_.getLong(i));
        }
        size += dataSize;
        if (!getUnitIdsList().isEmpty()) {
          size += 1;
          size += com.google.protobuf.CodedOutputStream
              .computeInt32SizeNoTag(dataSize);
        }
        unitIdsMemoizedSerializedSize = dataSize;
      }
      for (int i = 0; i < ratInfos_.size(); i++) {
        size += com.google.protobuf.CodedOutputStream
          .computeMessageSize(4, ratInfos_.get(i));
      }
      if (((bitField0_ & 0x00000002) != 0)) {
        size += com.google.protobuf.CodedOutputStream
          .computeBoolSize(5, exported_);
      }
      size += getUnknownFields().getSerializedSize();
      memoizedSize = size;
      return size;
    }
 
    @java.lang.Override
    public boolean equals(final java.lang.Object obj) {
      if (obj == this) {
       return true;
      }
      if (!(obj instanceof operations_research.sat.Lrat.LratInferredClause)) {
        return super.equals(obj);
      }
      operations_research.sat.Lrat.LratInferredClause other = (operations_research.sat.Lrat.LratInferredClause) obj;
 
      if (hasClauseId() != other.hasClauseId()) return false;
      if (hasClauseId()) {
        if (getClauseId()
            != other.getClauseId()) return false;
      }
      if (!getLiteralsList()
          .equals(other.getLiteralsList())) return false;
      if (!getUnitIdsList()
          .equals(other.getUnitIdsList())) return false;
      if (!getRatInfosList()
          .equals(other.getRatInfosList())) return false;
      if (hasExported() != other.hasExported()) return false;
      if (hasExported()) {
        if (getExported()
            != other.getExported()) return false;
      }
      if (!getUnknownFields().equals(other.getUnknownFields())) return false;
      return true;
    }
 
    @java.lang.Override
    public int hashCode() {
      if (memoizedHashCode != 0) {
        return memoizedHashCode;
      }
      int hash = 41;
      hash = (19 * hash) + getDescriptor().hashCode();
      if (hasClauseId()) {
        hash = (37 * hash) + CLAUSE_ID_FIELD_NUMBER;
        hash = (53 * hash) + com.google.protobuf.Internal.hashLong(
            getClauseId());
      }
      if (getLiteralsCount() > 0) {
        hash = (37 * hash) + LITERALS_FIELD_NUMBER;
        hash = (53 * hash) + getLiteralsList().hashCode();
      }
      if (getUnitIdsCount() > 0) {
        hash = (37 * hash) + UNIT_IDS_FIELD_NUMBER;
        hash = (53 * hash) + getUnitIdsList().hashCode();
      }
      if (getRatInfosCount() > 0) {
        hash = (37 * hash) + RAT_INFOS_FIELD_NUMBER;
        hash = (53 * hash) + getRatInfosList().hashCode();
      }
      if (hasExported()) {
        hash = (37 * hash) + EXPORTED_FIELD_NUMBER;
        hash = (53 * hash) + com.google.protobuf.Internal.hashBoolean(
            getExported());
      }
      hash = (29 * hash) + getUnknownFields().hashCode();
      memoizedHashCode = hash;
      return hash;
    }
 
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        java.nio.ByteBuffer data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        java.nio.ByteBuffer data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        com.google.protobuf.ByteString data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        com.google.protobuf.ByteString data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(byte[] data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        byte[] data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    public static operations_research.sat.Lrat.LratInferredClause parseDelimitedFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input);
    }
 
    public static operations_research.sat.Lrat.LratInferredClause parseDelimitedFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        com.google.protobuf.CodedInputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratInferredClause parseFrom(
        com.google.protobuf.CodedInputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    @java.lang.Override
    public Builder newBuilderForType() { return newBuilder(); }
    public static Builder newBuilder() {
      return DEFAULT_INSTANCE.toBuilder();
    }
    public static Builder newBuilder(operations_research.sat.Lrat.LratInferredClause prototype) {
      return DEFAULT_INSTANCE.toBuilder().mergeFrom(prototype);
    }
    @java.lang.Override
    public Builder toBuilder() {
      return this == DEFAULT_INSTANCE
          ? new Builder() : new Builder().mergeFrom(this);
    }
 
    @java.lang.Override
    protected Builder newBuilderForType(
        com.google.protobuf.GeneratedMessage.BuilderParent parent) {
      Builder builder = new Builder(parent);
      return builder;
    }

    public static final class Builder extends
        com.google.protobuf.GeneratedMessage.Builder<Builder> implements
        // @@protoc_insertion_point(builder_implements:operations_research.sat.LratInferredClause)
        operations_research.sat.Lrat.LratInferredClauseOrBuilder {
      public static final com.google.protobuf.Descriptors.Descriptor
          getDescriptor() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_descriptor;
      }
 
      @java.lang.Override
      protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
          internalGetFieldAccessorTable() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_fieldAccessorTable
            .ensureFieldAccessorsInitialized(
                operations_research.sat.Lrat.LratInferredClause.class, operations_research.sat.Lrat.LratInferredClause.Builder.class);
      }
 
      // Construct using operations_research.sat.Lrat.LratInferredClause.newBuilder()
      private Builder() {
 
      }
 
      private Builder(
          com.google.protobuf.GeneratedMessage.BuilderParent parent) {
        super(parent);
 
      }
      @java.lang.Override
      public Builder clear() {
        super.clear();
        bitField0_ = 0;
        clauseId_ = 0L;
        literals_ = emptyIntList();
        unitIds_ = emptyLongList();
        if (ratInfosBuilder_ == null) {
          ratInfos_ = java.util.Collections.emptyList();
        } else {
          ratInfos_ = null;
          ratInfosBuilder_.clear();
        }
        bitField0_ = (bitField0_ & ~0x00000008);
        exported_ = false;
        return this;
      }
 
      @java.lang.Override
      public com.google.protobuf.Descriptors.Descriptor
          getDescriptorForType() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratInferredClause_descriptor;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratInferredClause getDefaultInstanceForType() {
        return operations_research.sat.Lrat.LratInferredClause.getDefaultInstance();
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratInferredClause build() {
        operations_research.sat.Lrat.LratInferredClause result = buildPartial();
        if (!result.isInitialized()) {
          throw newUninitializedMessageException(result);
        }
        return result;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratInferredClause buildPartial() {
        operations_research.sat.Lrat.LratInferredClause result = new operations_research.sat.Lrat.LratInferredClause(this);
        buildPartialRepeatedFields(result);
        if (bitField0_ != 0) { buildPartial0(result); }
        onBuilt();
        return result;
      }
 
      private void buildPartialRepeatedFields(operations_research.sat.Lrat.LratInferredClause result) {
        if (ratInfosBuilder_ == null) {
          if (((bitField0_ & 0x00000008) != 0)) {
            ratInfos_ = java.util.Collections.unmodifiableList(ratInfos_);
            bitField0_ = (bitField0_ & ~0x00000008);
          }
          result.ratInfos_ = ratInfos_;
        } else {
          result.ratInfos_ = ratInfosBuilder_.build();
        }
      }
 
      private void buildPartial0(operations_research.sat.Lrat.LratInferredClause result) {
        int from_bitField0_ = bitField0_;
        int to_bitField0_ = 0;
        if (((from_bitField0_ & 0x00000001) != 0)) {
          result.clauseId_ = clauseId_;
          to_bitField0_ |= 0x00000001;
        }
        if (((from_bitField0_ & 0x00000002) != 0)) {
          literals_.makeImmutable();
          result.literals_ = literals_;
        }
        if (((from_bitField0_ & 0x00000004) != 0)) {
          unitIds_.makeImmutable();
          result.unitIds_ = unitIds_;
        }
        if (((from_bitField0_ & 0x00000010) != 0)) {
          result.exported_ = exported_;
          to_bitField0_ |= 0x00000002;
        }
        result.bitField0_ |= to_bitField0_;
      }
 
      @java.lang.Override
      public Builder mergeFrom(com.google.protobuf.Message other) {
        if (other instanceof operations_research.sat.Lrat.LratInferredClause) {
          return mergeFrom((operations_research.sat.Lrat.LratInferredClause)other);
        } else {
          super.mergeFrom(other);
          return this;
        }
      }
 
      public Builder mergeFrom(operations_research.sat.Lrat.LratInferredClause other) {
        if (other == operations_research.sat.Lrat.LratInferredClause.getDefaultInstance()) return this;
        if (other.hasClauseId()) {
          setClauseId(other.getClauseId());
        }
        if (!other.literals_.isEmpty()) {
          if (literals_.isEmpty()) {
            literals_ = other.literals_;
            literals_.makeImmutable();
            bitField0_ |= 0x00000002;
          } else {
            ensureLiteralsIsMutable();
            literals_.addAll(other.literals_);
          }
          onChanged();
        }
        if (!other.unitIds_.isEmpty()) {
          if (unitIds_.isEmpty()) {
            unitIds_ = other.unitIds_;
            unitIds_.makeImmutable();
            bitField0_ |= 0x00000004;
          } else {
            ensureUnitIdsIsMutable();
            unitIds_.addAll(other.unitIds_);
          }
          onChanged();
        }
        if (ratInfosBuilder_ == null) {
          if (!other.ratInfos_.isEmpty()) {
            if (ratInfos_.isEmpty()) {
              ratInfos_ = other.ratInfos_;
              bitField0_ = (bitField0_ & ~0x00000008);
            } else {
              ensureRatInfosIsMutable();
              ratInfos_.addAll(other.ratInfos_);
            }
            onChanged();
          }
        } else {
          if (!other.ratInfos_.isEmpty()) {
            if (ratInfosBuilder_.isEmpty()) {
              ratInfosBuilder_.dispose();
              ratInfosBuilder_ = null;
              ratInfos_ = other.ratInfos_;
              bitField0_ = (bitField0_ & ~0x00000008);
              ratInfosBuilder_ = 
                com.google.protobuf.GeneratedMessage.alwaysUseFieldBuilders ?
                   internalGetRatInfosFieldBuilder() : null;
            } else {
              ratInfosBuilder_.addAllMessages(other.ratInfos_);
            }
          }
        }
        if (other.hasExported()) {
          setExported(other.getExported());
        }
        this.mergeUnknownFields(other.getUnknownFields());
        onChanged();
        return this;
      }
 
      @java.lang.Override
      public final boolean isInitialized() {
        return true;
      }
 
      @java.lang.Override
      public Builder mergeFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        if (extensionRegistry == null) {
          throw new java.lang.NullPointerException();
        }
        try {
          boolean done = false;
          while (!done) {
            int tag = input.readTag();
            switch (tag) {
              case 0:
                done = true;
                break;
              case 8: {
                clauseId_ = input.readInt64();
                bitField0_ |= 0x00000001;
                break;
              } // case 8
              case 16: {
                int v = input.readInt32();
                ensureLiteralsIsMutable();
                literals_.addInt(v);
                break;
              } // case 16
              case 18: {
                int length = input.readRawVarint32();
                int limit = input.pushLimit(length);
                ensureLiteralsIsMutable();
                while (input.getBytesUntilLimit() > 0) {
                  literals_.addInt(input.readInt32());
                }
                input.popLimit(limit);
                break;
              } // case 18
              case 24: {
                long v = input.readInt64();
                ensureUnitIdsIsMutable();
                unitIds_.addLong(v);
                break;
              } // case 24
              case 26: {
                int length = input.readRawVarint32();
                int limit = input.pushLimit(length);
                ensureUnitIdsIsMutable();
                while (input.getBytesUntilLimit() > 0) {
                  unitIds_.addLong(input.readInt64());
                }
                input.popLimit(limit);
                break;
              } // case 26
              case 34: {
                operations_research.sat.Lrat.LratInferredClause.RatInfo m =
                    input.readMessage(
                        operations_research.sat.Lrat.LratInferredClause.RatInfo.parser(),
                        extensionRegistry);
                if (ratInfosBuilder_ == null) {
                  ensureRatInfosIsMutable();
                  ratInfos_.add(m);
                } else {
                  ratInfosBuilder_.addMessage(m);
                }
                break;
              } // case 34
              case 40: {
                exported_ = input.readBool();
                bitField0_ |= 0x00000010;
                break;
              } // case 40
              default: {
                if (!super.parseUnknownField(input, extensionRegistry, tag)) {
                  done = true; // was an endgroup tag
                }
                break;
              } // default:
            } // switch (tag)
          } // while (!done)
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.unwrapIOException();
        } finally {
          onChanged();
        } // finally
        return this;
      }
      private int bitField0_;
 
      private long clauseId_ ;
      @java.lang.Override
      public boolean hasClauseId() {
        return ((bitField0_ & 0x00000001) != 0);
      }

      @java.lang.Override
      public long getClauseId() {
        return clauseId_;
      }

      public Builder setClauseId(long value) {
 
        clauseId_ = value;
        bitField0_ |= 0x00000001;
        onChanged();
        return this;
      }

      public Builder clearClauseId() {
        bitField0_ = (bitField0_ & ~0x00000001);
        clauseId_ = 0L;
        onChanged();
        return this;
      }
 
      private com.google.protobuf.Internal.IntList literals_ = emptyIntList();
      private void ensureLiteralsIsMutable() {
        if (!literals_.isModifiable()) {
          literals_ = makeMutableCopy(literals_);
        }
        bitField0_ |= 0x00000002;
      }
      public java.util.List<java.lang.Integer>
          getLiteralsList() {
        literals_.makeImmutable();
        return literals_;
      }

      public int getLiteralsCount() {
        return literals_.size();
      }

      public int getLiterals(int index) {
        return literals_.getInt(index);
      }

      public Builder setLiterals(
          int index, int value) {
 
        ensureLiteralsIsMutable();
        literals_.setInt(index, value);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder addLiterals(int value) {
 
        ensureLiteralsIsMutable();
        literals_.addInt(value);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder addAllLiterals(
          java.lang.Iterable<? extends java.lang.Integer> values) {
        ensureLiteralsIsMutable();
        com.google.protobuf.AbstractMessageLite.Builder.addAll(
            values, literals_);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder clearLiterals() {
        literals_ = emptyIntList();
        bitField0_ = (bitField0_ & ~0x00000002);
        onChanged();
        return this;
      }
 
      private com.google.protobuf.Internal.LongList unitIds_ = emptyLongList();
      private void ensureUnitIdsIsMutable() {
        if (!unitIds_.isModifiable()) {
          unitIds_ = makeMutableCopy(unitIds_);
        }
        bitField0_ |= 0x00000004;
      }
      public java.util.List<java.lang.Long>
          getUnitIdsList() {
        unitIds_.makeImmutable();
        return unitIds_;
      }

      public int getUnitIdsCount() {
        return unitIds_.size();
      }

      public long getUnitIds(int index) {
        return unitIds_.getLong(index);
      }

      public Builder setUnitIds(
          int index, long value) {
 
        ensureUnitIdsIsMutable();
        unitIds_.setLong(index, value);
        bitField0_ |= 0x00000004;
        onChanged();
        return this;
      }

      public Builder addUnitIds(long value) {
 
        ensureUnitIdsIsMutable();
        unitIds_.addLong(value);
        bitField0_ |= 0x00000004;
        onChanged();
        return this;
      }

      public Builder addAllUnitIds(
          java.lang.Iterable<? extends java.lang.Long> values) {
        ensureUnitIdsIsMutable();
        com.google.protobuf.AbstractMessageLite.Builder.addAll(
            values, unitIds_);
        bitField0_ |= 0x00000004;
        onChanged();
        return this;
      }

      public Builder clearUnitIds() {
        unitIds_ = emptyLongList();
        bitField0_ = (bitField0_ & ~0x00000004);
        onChanged();
        return this;
      }
 
      private java.util.List<operations_research.sat.Lrat.LratInferredClause.RatInfo> ratInfos_ =
        java.util.Collections.emptyList();
      private void ensureRatInfosIsMutable() {
        if (!((bitField0_ & 0x00000008) != 0)) {
          ratInfos_ = new java.util.ArrayList<operations_research.sat.Lrat.LratInferredClause.RatInfo>(ratInfos_);
          bitField0_ |= 0x00000008;
         }
      }
 
      private com.google.protobuf.RepeatedFieldBuilder<
          operations_research.sat.Lrat.LratInferredClause.RatInfo, operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder, operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder> ratInfosBuilder_;

      public java.util.List<operations_research.sat.Lrat.LratInferredClause.RatInfo> getRatInfosList() {
        if (ratInfosBuilder_ == null) {
          return java.util.Collections.unmodifiableList(ratInfos_);
        } else {
          return ratInfosBuilder_.getMessageList();
        }
      }

      public int getRatInfosCount() {
        if (ratInfosBuilder_ == null) {
          return ratInfos_.size();
        } else {
          return ratInfosBuilder_.getCount();
        }
      }

      public operations_research.sat.Lrat.LratInferredClause.RatInfo getRatInfos(int index) {
        if (ratInfosBuilder_ == null) {
          return ratInfos_.get(index);
        } else {
          return ratInfosBuilder_.getMessage(index);
        }
      }

      public Builder setRatInfos(
          int index, operations_research.sat.Lrat.LratInferredClause.RatInfo value) {
        if (ratInfosBuilder_ == null) {
          if (value == null) {
            throw new NullPointerException();
          }
          ensureRatInfosIsMutable();
          ratInfos_.set(index, value);
          onChanged();
        } else {
          ratInfosBuilder_.setMessage(index, value);
        }
        return this;
      }

      public Builder setRatInfos(
          int index, operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder builderForValue) {
        if (ratInfosBuilder_ == null) {
          ensureRatInfosIsMutable();
          ratInfos_.set(index, builderForValue.build());
          onChanged();
        } else {
          ratInfosBuilder_.setMessage(index, builderForValue.build());
        }
        return this;
      }

      public Builder addRatInfos(operations_research.sat.Lrat.LratInferredClause.RatInfo value) {
        if (ratInfosBuilder_ == null) {
          if (value == null) {
            throw new NullPointerException();
          }
          ensureRatInfosIsMutable();
          ratInfos_.add(value);
          onChanged();
        } else {
          ratInfosBuilder_.addMessage(value);
        }
        return this;
      }

      public Builder addRatInfos(
          int index, operations_research.sat.Lrat.LratInferredClause.RatInfo value) {
        if (ratInfosBuilder_ == null) {
          if (value == null) {
            throw new NullPointerException();
          }
          ensureRatInfosIsMutable();
          ratInfos_.add(index, value);
          onChanged();
        } else {
          ratInfosBuilder_.addMessage(index, value);
        }
        return this;
      }

      public Builder addRatInfos(
          operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder builderForValue) {
        if (ratInfosBuilder_ == null) {
          ensureRatInfosIsMutable();
          ratInfos_.add(builderForValue.build());
          onChanged();
        } else {
          ratInfosBuilder_.addMessage(builderForValue.build());
        }
        return this;
      }

      public Builder addRatInfos(
          int index, operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder builderForValue) {
        if (ratInfosBuilder_ == null) {
          ensureRatInfosIsMutable();
          ratInfos_.add(index, builderForValue.build());
          onChanged();
        } else {
          ratInfosBuilder_.addMessage(index, builderForValue.build());
        }
        return this;
      }

      public Builder addAllRatInfos(
          java.lang.Iterable<? extends operations_research.sat.Lrat.LratInferredClause.RatInfo> values) {
        if (ratInfosBuilder_ == null) {
          ensureRatInfosIsMutable();
          com.google.protobuf.AbstractMessageLite.Builder.addAll(
              values, ratInfos_);
          onChanged();
        } else {
          ratInfosBuilder_.addAllMessages(values);
        }
        return this;
      }

      public Builder clearRatInfos() {
        if (ratInfosBuilder_ == null) {
          ratInfos_ = java.util.Collections.emptyList();
          bitField0_ = (bitField0_ & ~0x00000008);
          onChanged();
        } else {
          ratInfosBuilder_.clear();
        }
        return this;
      }

      public Builder removeRatInfos(int index) {
        if (ratInfosBuilder_ == null) {
          ensureRatInfosIsMutable();
          ratInfos_.remove(index);
          onChanged();
        } else {
          ratInfosBuilder_.remove(index);
        }
        return this;
      }

      public operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder getRatInfosBuilder(
          int index) {
        return internalGetRatInfosFieldBuilder().getBuilder(index);
      }

      public operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder getRatInfosOrBuilder(
          int index) {
        if (ratInfosBuilder_ == null) {
          return ratInfos_.get(index);  } else {
          return ratInfosBuilder_.getMessageOrBuilder(index);
        }
      }

      public java.util.List<? extends operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder> 
           getRatInfosOrBuilderList() {
        if (ratInfosBuilder_ != null) {
          return ratInfosBuilder_.getMessageOrBuilderList();
        } else {
          return java.util.Collections.unmodifiableList(ratInfos_);
        }
      }

      public operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder addRatInfosBuilder() {
        return internalGetRatInfosFieldBuilder().addBuilder(
            operations_research.sat.Lrat.LratInferredClause.RatInfo.getDefaultInstance());
      }

      public operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder addRatInfosBuilder(
          int index) {
        return internalGetRatInfosFieldBuilder().addBuilder(
            index, operations_research.sat.Lrat.LratInferredClause.RatInfo.getDefaultInstance());
      }

      public java.util.List<operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder> 
           getRatInfosBuilderList() {
        return internalGetRatInfosFieldBuilder().getBuilderList();
      }
      private com.google.protobuf.RepeatedFieldBuilder<
          operations_research.sat.Lrat.LratInferredClause.RatInfo, operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder, operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder> 
          internalGetRatInfosFieldBuilder() {
        if (ratInfosBuilder_ == null) {
          ratInfosBuilder_ = new com.google.protobuf.RepeatedFieldBuilder<
              operations_research.sat.Lrat.LratInferredClause.RatInfo, operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder, operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder>(
                  ratInfos_,
                  ((bitField0_ & 0x00000008) != 0),
                  getParentForChildren(),
                  isClean());
          ratInfos_ = null;
        }
        return ratInfosBuilder_;
      }
 
      private boolean exported_ ;
      @java.lang.Override
      public boolean hasExported() {
        return ((bitField0_ & 0x00000010) != 0);
      }

      @java.lang.Override
      public boolean getExported() {
        return exported_;
      }

      public Builder setExported(boolean value) {
 
        exported_ = value;
        bitField0_ |= 0x00000010;
        onChanged();
        return this;
      }

      public Builder clearExported() {
        bitField0_ = (bitField0_ & ~0x00000010);
        exported_ = false;
        onChanged();
        return this;
      }
 
      // @@protoc_insertion_point(builder_scope:operations_research.sat.LratInferredClause)
    }
 
    // @@protoc_insertion_point(class_scope:operations_research.sat.LratInferredClause)
    private static final operations_research.sat.Lrat.LratInferredClause DEFAULT_INSTANCE;
    static {
      DEFAULT_INSTANCE = new operations_research.sat.Lrat.LratInferredClause();
    }
 
    public static operations_research.sat.Lrat.LratInferredClause getDefaultInstance() {
      return DEFAULT_INSTANCE;
    }
 
    private static final com.google.protobuf.Parser<LratInferredClause>
        PARSER = new com.google.protobuf.AbstractParser<LratInferredClause>() {
      @java.lang.Override
      public LratInferredClause parsePartialFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        Builder builder = newBuilder();
        try {
          builder.mergeFrom(input, extensionRegistry);
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.setUnfinishedMessage(builder.buildPartial());
        } catch (com.google.protobuf.UninitializedMessageException e) {
          throw e.asInvalidProtocolBufferException().setUnfinishedMessage(builder.buildPartial());
        } catch (java.io.IOException e) {
          throw new com.google.protobuf.InvalidProtocolBufferException(e)
              .setUnfinishedMessage(builder.buildPartial());
        }
        return builder.buildPartial();
      }
    };
 
    public static com.google.protobuf.Parser<LratInferredClause> parser() {
      return PARSER;
    }
 
    @java.lang.Override
    public com.google.protobuf.Parser<LratInferredClause> getParserForType() {
      return PARSER;
    }
 
    @java.lang.Override
    public operations_research.sat.Lrat.LratInferredClause getDefaultInstanceForType() {
      return DEFAULT_INSTANCE;
    }
 
  }
 
  public interface LratExportedClauseOrBuilder extends
      // @@protoc_insertion_point(interface_extends:operations_research.sat.LratExportedClause)
      com.google.protobuf.MessageOrBuilder {

    boolean hasClauseId();
    long getClauseId();

    java.util.List<java.lang.Integer> getLiteralsList();
    int getLiteralsCount();
    int getLiterals(int index);
  }

  public static final class LratExportedClause extends
      com.google.protobuf.GeneratedMessage implements
      // @@protoc_insertion_point(message_implements:operations_research.sat.LratExportedClause)
      LratExportedClauseOrBuilder {
  private static final long serialVersionUID = 0L;
    static {
      com.google.protobuf.RuntimeVersion.validateProtobufGencodeVersion(
        com.google.protobuf.RuntimeVersion.RuntimeDomain.PUBLIC,
        /* major= */ 4,
        /* minor= */ 33,
        /* patch= */ 1,
        /* suffix= */ "",
        "LratExportedClause");
    }
    // Use LratExportedClause.newBuilder() to construct.
    private LratExportedClause(com.google.protobuf.GeneratedMessage.Builder<?> builder) {
      super(builder);
    }
    private LratExportedClause() {
      literals_ = emptyIntList();
    }
 
    public static final com.google.protobuf.Descriptors.Descriptor
        getDescriptor() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratExportedClause_descriptor;
    }
 
    @java.lang.Override
    protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
        internalGetFieldAccessorTable() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratExportedClause_fieldAccessorTable
          .ensureFieldAccessorsInitialized(
              operations_research.sat.Lrat.LratExportedClause.class, operations_research.sat.Lrat.LratExportedClause.Builder.class);
    }
 
    private int bitField0_;
    public static final int CLAUSE_ID_FIELD_NUMBER = 1;
    private long clauseId_ = 0L;
    @java.lang.Override
    public boolean hasClauseId() {
      return ((bitField0_ & 0x00000001) != 0);
    }

    @java.lang.Override
    public long getClauseId() {
      return clauseId_;
    }
 
    public static final int LITERALS_FIELD_NUMBER = 2;
    @SuppressWarnings("serial")
    private com.google.protobuf.Internal.IntList literals_ =
        emptyIntList();
    @java.lang.Override
    public java.util.List<java.lang.Integer>
        getLiteralsList() {
      return literals_;
    }

    public int getLiteralsCount() {
      return literals_.size();
    }

    public int getLiterals(int index) {
      return literals_.getInt(index);
    }
    private int literalsMemoizedSerializedSize = -1;
 
    private byte memoizedIsInitialized = -1;
    @java.lang.Override
    public final boolean isInitialized() {
      byte isInitialized = memoizedIsInitialized;
      if (isInitialized == 1) return true;
      if (isInitialized == 0) return false;
 
      memoizedIsInitialized = 1;
      return true;
    }
 
    @java.lang.Override
    public void writeTo(com.google.protobuf.CodedOutputStream output)
                        throws java.io.IOException {
      getSerializedSize();
      if (((bitField0_ & 0x00000001) != 0)) {
        output.writeInt64(1, clauseId_);
      }
      if (getLiteralsList().size() > 0) {
        output.writeUInt32NoTag(18);
        output.writeUInt32NoTag(literalsMemoizedSerializedSize);
      }
      for (int i = 0; i < literals_.size(); i++) {
        output.writeInt32NoTag(literals_.getInt(i));
      }
      getUnknownFields().writeTo(output);
    }
 
    @java.lang.Override
    public int getSerializedSize() {
      int size = memoizedSize;
      if (size != -1) return size;
 
      size = 0;
      if (((bitField0_ & 0x00000001) != 0)) {
        size += com.google.protobuf.CodedOutputStream
          .computeInt64Size(1, clauseId_);
      }
      {
        int dataSize = 0;
        for (int i = 0; i < literals_.size(); i++) {
          dataSize += com.google.protobuf.CodedOutputStream
            .computeInt32SizeNoTag(literals_.getInt(i));
        }
        size += dataSize;
        if (!getLiteralsList().isEmpty()) {
          size += 1;
          size += com.google.protobuf.CodedOutputStream
              .computeInt32SizeNoTag(dataSize);
        }
        literalsMemoizedSerializedSize = dataSize;
      }
      size += getUnknownFields().getSerializedSize();
      memoizedSize = size;
      return size;
    }
 
    @java.lang.Override
    public boolean equals(final java.lang.Object obj) {
      if (obj == this) {
       return true;
      }
      if (!(obj instanceof operations_research.sat.Lrat.LratExportedClause)) {
        return super.equals(obj);
      }
      operations_research.sat.Lrat.LratExportedClause other = (operations_research.sat.Lrat.LratExportedClause) obj;
 
      if (hasClauseId() != other.hasClauseId()) return false;
      if (hasClauseId()) {
        if (getClauseId()
            != other.getClauseId()) return false;
      }
      if (!getLiteralsList()
          .equals(other.getLiteralsList())) return false;
      if (!getUnknownFields().equals(other.getUnknownFields())) return false;
      return true;
    }
 
    @java.lang.Override
    public int hashCode() {
      if (memoizedHashCode != 0) {
        return memoizedHashCode;
      }
      int hash = 41;
      hash = (19 * hash) + getDescriptor().hashCode();
      if (hasClauseId()) {
        hash = (37 * hash) + CLAUSE_ID_FIELD_NUMBER;
        hash = (53 * hash) + com.google.protobuf.Internal.hashLong(
            getClauseId());
      }
      if (getLiteralsCount() > 0) {
        hash = (37 * hash) + LITERALS_FIELD_NUMBER;
        hash = (53 * hash) + getLiteralsList().hashCode();
      }
      hash = (29 * hash) + getUnknownFields().hashCode();
      memoizedHashCode = hash;
      return hash;
    }
 
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        java.nio.ByteBuffer data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        java.nio.ByteBuffer data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        com.google.protobuf.ByteString data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        com.google.protobuf.ByteString data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(byte[] data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        byte[] data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    public static operations_research.sat.Lrat.LratExportedClause parseDelimitedFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input);
    }
 
    public static operations_research.sat.Lrat.LratExportedClause parseDelimitedFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        com.google.protobuf.CodedInputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratExportedClause parseFrom(
        com.google.protobuf.CodedInputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    @java.lang.Override
    public Builder newBuilderForType() { return newBuilder(); }
    public static Builder newBuilder() {
      return DEFAULT_INSTANCE.toBuilder();
    }
    public static Builder newBuilder(operations_research.sat.Lrat.LratExportedClause prototype) {
      return DEFAULT_INSTANCE.toBuilder().mergeFrom(prototype);
    }
    @java.lang.Override
    public Builder toBuilder() {
      return this == DEFAULT_INSTANCE
          ? new Builder() : new Builder().mergeFrom(this);
    }
 
    @java.lang.Override
    protected Builder newBuilderForType(
        com.google.protobuf.GeneratedMessage.BuilderParent parent) {
      Builder builder = new Builder(parent);
      return builder;
    }

    public static final class Builder extends
        com.google.protobuf.GeneratedMessage.Builder<Builder> implements
        // @@protoc_insertion_point(builder_implements:operations_research.sat.LratExportedClause)
        operations_research.sat.Lrat.LratExportedClauseOrBuilder {
      public static final com.google.protobuf.Descriptors.Descriptor
          getDescriptor() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratExportedClause_descriptor;
      }
 
      @java.lang.Override
      protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
          internalGetFieldAccessorTable() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratExportedClause_fieldAccessorTable
            .ensureFieldAccessorsInitialized(
                operations_research.sat.Lrat.LratExportedClause.class, operations_research.sat.Lrat.LratExportedClause.Builder.class);
      }
 
      // Construct using operations_research.sat.Lrat.LratExportedClause.newBuilder()
      private Builder() {
 
      }
 
      private Builder(
          com.google.protobuf.GeneratedMessage.BuilderParent parent) {
        super(parent);
 
      }
      @java.lang.Override
      public Builder clear() {
        super.clear();
        bitField0_ = 0;
        clauseId_ = 0L;
        literals_ = emptyIntList();
        return this;
      }
 
      @java.lang.Override
      public com.google.protobuf.Descriptors.Descriptor
          getDescriptorForType() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratExportedClause_descriptor;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratExportedClause getDefaultInstanceForType() {
        return operations_research.sat.Lrat.LratExportedClause.getDefaultInstance();
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratExportedClause build() {
        operations_research.sat.Lrat.LratExportedClause result = buildPartial();
        if (!result.isInitialized()) {
          throw newUninitializedMessageException(result);
        }
        return result;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratExportedClause buildPartial() {
        operations_research.sat.Lrat.LratExportedClause result = new operations_research.sat.Lrat.LratExportedClause(this);
        if (bitField0_ != 0) { buildPartial0(result); }
        onBuilt();
        return result;
      }
 
      private void buildPartial0(operations_research.sat.Lrat.LratExportedClause result) {
        int from_bitField0_ = bitField0_;
        int to_bitField0_ = 0;
        if (((from_bitField0_ & 0x00000001) != 0)) {
          result.clauseId_ = clauseId_;
          to_bitField0_ |= 0x00000001;
        }
        if (((from_bitField0_ & 0x00000002) != 0)) {
          literals_.makeImmutable();
          result.literals_ = literals_;
        }
        result.bitField0_ |= to_bitField0_;
      }
 
      @java.lang.Override
      public Builder mergeFrom(com.google.protobuf.Message other) {
        if (other instanceof operations_research.sat.Lrat.LratExportedClause) {
          return mergeFrom((operations_research.sat.Lrat.LratExportedClause)other);
        } else {
          super.mergeFrom(other);
          return this;
        }
      }
 
      public Builder mergeFrom(operations_research.sat.Lrat.LratExportedClause other) {
        if (other == operations_research.sat.Lrat.LratExportedClause.getDefaultInstance()) return this;
        if (other.hasClauseId()) {
          setClauseId(other.getClauseId());
        }
        if (!other.literals_.isEmpty()) {
          if (literals_.isEmpty()) {
            literals_ = other.literals_;
            literals_.makeImmutable();
            bitField0_ |= 0x00000002;
          } else {
            ensureLiteralsIsMutable();
            literals_.addAll(other.literals_);
          }
          onChanged();
        }
        this.mergeUnknownFields(other.getUnknownFields());
        onChanged();
        return this;
      }
 
      @java.lang.Override
      public final boolean isInitialized() {
        return true;
      }
 
      @java.lang.Override
      public Builder mergeFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        if (extensionRegistry == null) {
          throw new java.lang.NullPointerException();
        }
        try {
          boolean done = false;
          while (!done) {
            int tag = input.readTag();
            switch (tag) {
              case 0:
                done = true;
                break;
              case 8: {
                clauseId_ = input.readInt64();
                bitField0_ |= 0x00000001;
                break;
              } // case 8
              case 16: {
                int v = input.readInt32();
                ensureLiteralsIsMutable();
                literals_.addInt(v);
                break;
              } // case 16
              case 18: {
                int length = input.readRawVarint32();
                int limit = input.pushLimit(length);
                ensureLiteralsIsMutable();
                while (input.getBytesUntilLimit() > 0) {
                  literals_.addInt(input.readInt32());
                }
                input.popLimit(limit);
                break;
              } // case 18
              default: {
                if (!super.parseUnknownField(input, extensionRegistry, tag)) {
                  done = true; // was an endgroup tag
                }
                break;
              } // default:
            } // switch (tag)
          } // while (!done)
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.unwrapIOException();
        } finally {
          onChanged();
        } // finally
        return this;
      }
      private int bitField0_;
 
      private long clauseId_ ;
      @java.lang.Override
      public boolean hasClauseId() {
        return ((bitField0_ & 0x00000001) != 0);
      }

      @java.lang.Override
      public long getClauseId() {
        return clauseId_;
      }

      public Builder setClauseId(long value) {
 
        clauseId_ = value;
        bitField0_ |= 0x00000001;
        onChanged();
        return this;
      }

      public Builder clearClauseId() {
        bitField0_ = (bitField0_ & ~0x00000001);
        clauseId_ = 0L;
        onChanged();
        return this;
      }
 
      private com.google.protobuf.Internal.IntList literals_ = emptyIntList();
      private void ensureLiteralsIsMutable() {
        if (!literals_.isModifiable()) {
          literals_ = makeMutableCopy(literals_);
        }
        bitField0_ |= 0x00000002;
      }
      public java.util.List<java.lang.Integer>
          getLiteralsList() {
        literals_.makeImmutable();
        return literals_;
      }

      public int getLiteralsCount() {
        return literals_.size();
      }

      public int getLiterals(int index) {
        return literals_.getInt(index);
      }

      public Builder setLiterals(
          int index, int value) {
 
        ensureLiteralsIsMutable();
        literals_.setInt(index, value);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder addLiterals(int value) {
 
        ensureLiteralsIsMutable();
        literals_.addInt(value);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder addAllLiterals(
          java.lang.Iterable<? extends java.lang.Integer> values) {
        ensureLiteralsIsMutable();
        com.google.protobuf.AbstractMessageLite.Builder.addAll(
            values, literals_);
        bitField0_ |= 0x00000002;
        onChanged();
        return this;
      }

      public Builder clearLiterals() {
        literals_ = emptyIntList();
        bitField0_ = (bitField0_ & ~0x00000002);
        onChanged();
        return this;
      }
 
      // @@protoc_insertion_point(builder_scope:operations_research.sat.LratExportedClause)
    }
 
    // @@protoc_insertion_point(class_scope:operations_research.sat.LratExportedClause)
    private static final operations_research.sat.Lrat.LratExportedClause DEFAULT_INSTANCE;
    static {
      DEFAULT_INSTANCE = new operations_research.sat.Lrat.LratExportedClause();
    }
 
    public static operations_research.sat.Lrat.LratExportedClause getDefaultInstance() {
      return DEFAULT_INSTANCE;
    }
 
    private static final com.google.protobuf.Parser<LratExportedClause>
        PARSER = new com.google.protobuf.AbstractParser<LratExportedClause>() {
      @java.lang.Override
      public LratExportedClause parsePartialFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        Builder builder = newBuilder();
        try {
          builder.mergeFrom(input, extensionRegistry);
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.setUnfinishedMessage(builder.buildPartial());
        } catch (com.google.protobuf.UninitializedMessageException e) {
          throw e.asInvalidProtocolBufferException().setUnfinishedMessage(builder.buildPartial());
        } catch (java.io.IOException e) {
          throw new com.google.protobuf.InvalidProtocolBufferException(e)
              .setUnfinishedMessage(builder.buildPartial());
        }
        return builder.buildPartial();
      }
    };
 
    public static com.google.protobuf.Parser<LratExportedClause> parser() {
      return PARSER;
    }
 
    @java.lang.Override
    public com.google.protobuf.Parser<LratExportedClause> getParserForType() {
      return PARSER;
    }
 
    @java.lang.Override
    public operations_research.sat.Lrat.LratExportedClause getDefaultInstanceForType() {
      return DEFAULT_INSTANCE;
    }
 
  }
 
  public interface LratDeletedClausesOrBuilder extends
      // @@protoc_insertion_point(interface_extends:operations_research.sat.LratDeletedClauses)
      com.google.protobuf.MessageOrBuilder {

    java.util.List<java.lang.Long> getClauseIdsList();
    int getClauseIdsCount();
    long getClauseIds(int index);
  }

  public static final class LratDeletedClauses extends
      com.google.protobuf.GeneratedMessage implements
      // @@protoc_insertion_point(message_implements:operations_research.sat.LratDeletedClauses)
      LratDeletedClausesOrBuilder {
  private static final long serialVersionUID = 0L;
    static {
      com.google.protobuf.RuntimeVersion.validateProtobufGencodeVersion(
        com.google.protobuf.RuntimeVersion.RuntimeDomain.PUBLIC,
        /* major= */ 4,
        /* minor= */ 33,
        /* patch= */ 1,
        /* suffix= */ "",
        "LratDeletedClauses");
    }
    // Use LratDeletedClauses.newBuilder() to construct.
    private LratDeletedClauses(com.google.protobuf.GeneratedMessage.Builder<?> builder) {
      super(builder);
    }
    private LratDeletedClauses() {
      clauseIds_ = emptyLongList();
    }
 
    public static final com.google.protobuf.Descriptors.Descriptor
        getDescriptor() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratDeletedClauses_descriptor;
    }
 
    @java.lang.Override
    protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
        internalGetFieldAccessorTable() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratDeletedClauses_fieldAccessorTable
          .ensureFieldAccessorsInitialized(
              operations_research.sat.Lrat.LratDeletedClauses.class, operations_research.sat.Lrat.LratDeletedClauses.Builder.class);
    }
 
    public static final int CLAUSE_IDS_FIELD_NUMBER = 1;
    @SuppressWarnings("serial")
    private com.google.protobuf.Internal.LongList clauseIds_ =
        emptyLongList();
    @java.lang.Override
    public java.util.List<java.lang.Long>
        getClauseIdsList() {
      return clauseIds_;
    }

    public int getClauseIdsCount() {
      return clauseIds_.size();
    }

    public long getClauseIds(int index) {
      return clauseIds_.getLong(index);
    }
    private int clauseIdsMemoizedSerializedSize = -1;
 
    private byte memoizedIsInitialized = -1;
    @java.lang.Override
    public final boolean isInitialized() {
      byte isInitialized = memoizedIsInitialized;
      if (isInitialized == 1) return true;
      if (isInitialized == 0) return false;
 
      memoizedIsInitialized = 1;
      return true;
    }
 
    @java.lang.Override
    public void writeTo(com.google.protobuf.CodedOutputStream output)
                        throws java.io.IOException {
      getSerializedSize();
      if (getClauseIdsList().size() > 0) {
        output.writeUInt32NoTag(10);
        output.writeUInt32NoTag(clauseIdsMemoizedSerializedSize);
      }
      for (int i = 0; i < clauseIds_.size(); i++) {
        output.writeInt64NoTag(clauseIds_.getLong(i));
      }
      getUnknownFields().writeTo(output);
    }
 
    @java.lang.Override
    public int getSerializedSize() {
      int size = memoizedSize;
      if (size != -1) return size;
 
      size = 0;
      {
        int dataSize = 0;
        for (int i = 0; i < clauseIds_.size(); i++) {
          dataSize += com.google.protobuf.CodedOutputStream
            .computeInt64SizeNoTag(clauseIds_.getLong(i));
        }
        size += dataSize;
        if (!getClauseIdsList().isEmpty()) {
          size += 1;
          size += com.google.protobuf.CodedOutputStream
              .computeInt32SizeNoTag(dataSize);
        }
        clauseIdsMemoizedSerializedSize = dataSize;
      }
      size += getUnknownFields().getSerializedSize();
      memoizedSize = size;
      return size;
    }
 
    @java.lang.Override
    public boolean equals(final java.lang.Object obj) {
      if (obj == this) {
       return true;
      }
      if (!(obj instanceof operations_research.sat.Lrat.LratDeletedClauses)) {
        return super.equals(obj);
      }
      operations_research.sat.Lrat.LratDeletedClauses other = (operations_research.sat.Lrat.LratDeletedClauses) obj;
 
      if (!getClauseIdsList()
          .equals(other.getClauseIdsList())) return false;
      if (!getUnknownFields().equals(other.getUnknownFields())) return false;
      return true;
    }
 
    @java.lang.Override
    public int hashCode() {
      if (memoizedHashCode != 0) {
        return memoizedHashCode;
      }
      int hash = 41;
      hash = (19 * hash) + getDescriptor().hashCode();
      if (getClauseIdsCount() > 0) {
        hash = (37 * hash) + CLAUSE_IDS_FIELD_NUMBER;
        hash = (53 * hash) + getClauseIdsList().hashCode();
      }
      hash = (29 * hash) + getUnknownFields().hashCode();
      memoizedHashCode = hash;
      return hash;
    }
 
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        java.nio.ByteBuffer data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        java.nio.ByteBuffer data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        com.google.protobuf.ByteString data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        com.google.protobuf.ByteString data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(byte[] data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        byte[] data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    public static operations_research.sat.Lrat.LratDeletedClauses parseDelimitedFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input);
    }
 
    public static operations_research.sat.Lrat.LratDeletedClauses parseDelimitedFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        com.google.protobuf.CodedInputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratDeletedClauses parseFrom(
        com.google.protobuf.CodedInputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    @java.lang.Override
    public Builder newBuilderForType() { return newBuilder(); }
    public static Builder newBuilder() {
      return DEFAULT_INSTANCE.toBuilder();
    }
    public static Builder newBuilder(operations_research.sat.Lrat.LratDeletedClauses prototype) {
      return DEFAULT_INSTANCE.toBuilder().mergeFrom(prototype);
    }
    @java.lang.Override
    public Builder toBuilder() {
      return this == DEFAULT_INSTANCE
          ? new Builder() : new Builder().mergeFrom(this);
    }
 
    @java.lang.Override
    protected Builder newBuilderForType(
        com.google.protobuf.GeneratedMessage.BuilderParent parent) {
      Builder builder = new Builder(parent);
      return builder;
    }

    public static final class Builder extends
        com.google.protobuf.GeneratedMessage.Builder<Builder> implements
        // @@protoc_insertion_point(builder_implements:operations_research.sat.LratDeletedClauses)
        operations_research.sat.Lrat.LratDeletedClausesOrBuilder {
      public static final com.google.protobuf.Descriptors.Descriptor
          getDescriptor() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratDeletedClauses_descriptor;
      }
 
      @java.lang.Override
      protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
          internalGetFieldAccessorTable() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratDeletedClauses_fieldAccessorTable
            .ensureFieldAccessorsInitialized(
                operations_research.sat.Lrat.LratDeletedClauses.class, operations_research.sat.Lrat.LratDeletedClauses.Builder.class);
      }
 
      // Construct using operations_research.sat.Lrat.LratDeletedClauses.newBuilder()
      private Builder() {
 
      }
 
      private Builder(
          com.google.protobuf.GeneratedMessage.BuilderParent parent) {
        super(parent);
 
      }
      @java.lang.Override
      public Builder clear() {
        super.clear();
        bitField0_ = 0;
        clauseIds_ = emptyLongList();
        return this;
      }
 
      @java.lang.Override
      public com.google.protobuf.Descriptors.Descriptor
          getDescriptorForType() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratDeletedClauses_descriptor;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratDeletedClauses getDefaultInstanceForType() {
        return operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance();
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratDeletedClauses build() {
        operations_research.sat.Lrat.LratDeletedClauses result = buildPartial();
        if (!result.isInitialized()) {
          throw newUninitializedMessageException(result);
        }
        return result;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratDeletedClauses buildPartial() {
        operations_research.sat.Lrat.LratDeletedClauses result = new operations_research.sat.Lrat.LratDeletedClauses(this);
        if (bitField0_ != 0) { buildPartial0(result); }
        onBuilt();
        return result;
      }
 
      private void buildPartial0(operations_research.sat.Lrat.LratDeletedClauses result) {
        int from_bitField0_ = bitField0_;
        if (((from_bitField0_ & 0x00000001) != 0)) {
          clauseIds_.makeImmutable();
          result.clauseIds_ = clauseIds_;
        }
      }
 
      @java.lang.Override
      public Builder mergeFrom(com.google.protobuf.Message other) {
        if (other instanceof operations_research.sat.Lrat.LratDeletedClauses) {
          return mergeFrom((operations_research.sat.Lrat.LratDeletedClauses)other);
        } else {
          super.mergeFrom(other);
          return this;
        }
      }
 
      public Builder mergeFrom(operations_research.sat.Lrat.LratDeletedClauses other) {
        if (other == operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance()) return this;
        if (!other.clauseIds_.isEmpty()) {
          if (clauseIds_.isEmpty()) {
            clauseIds_ = other.clauseIds_;
            clauseIds_.makeImmutable();
            bitField0_ |= 0x00000001;
          } else {
            ensureClauseIdsIsMutable();
            clauseIds_.addAll(other.clauseIds_);
          }
          onChanged();
        }
        this.mergeUnknownFields(other.getUnknownFields());
        onChanged();
        return this;
      }
 
      @java.lang.Override
      public final boolean isInitialized() {
        return true;
      }
 
      @java.lang.Override
      public Builder mergeFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        if (extensionRegistry == null) {
          throw new java.lang.NullPointerException();
        }
        try {
          boolean done = false;
          while (!done) {
            int tag = input.readTag();
            switch (tag) {
              case 0:
                done = true;
                break;
              case 8: {
                long v = input.readInt64();
                ensureClauseIdsIsMutable();
                clauseIds_.addLong(v);
                break;
              } // case 8
              case 10: {
                int length = input.readRawVarint32();
                int limit = input.pushLimit(length);
                ensureClauseIdsIsMutable();
                while (input.getBytesUntilLimit() > 0) {
                  clauseIds_.addLong(input.readInt64());
                }
                input.popLimit(limit);
                break;
              } // case 10
              default: {
                if (!super.parseUnknownField(input, extensionRegistry, tag)) {
                  done = true; // was an endgroup tag
                }
                break;
              } // default:
            } // switch (tag)
          } // while (!done)
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.unwrapIOException();
        } finally {
          onChanged();
        } // finally
        return this;
      }
      private int bitField0_;
 
      private com.google.protobuf.Internal.LongList clauseIds_ = emptyLongList();
      private void ensureClauseIdsIsMutable() {
        if (!clauseIds_.isModifiable()) {
          clauseIds_ = makeMutableCopy(clauseIds_);
        }
        bitField0_ |= 0x00000001;
      }
      public java.util.List<java.lang.Long>
          getClauseIdsList() {
        clauseIds_.makeImmutable();
        return clauseIds_;
      }

      public int getClauseIdsCount() {
        return clauseIds_.size();
      }

      public long getClauseIds(int index) {
        return clauseIds_.getLong(index);
      }

      public Builder setClauseIds(
          int index, long value) {
 
        ensureClauseIdsIsMutable();
        clauseIds_.setLong(index, value);
        bitField0_ |= 0x00000001;
        onChanged();
        return this;
      }

      public Builder addClauseIds(long value) {
 
        ensureClauseIdsIsMutable();
        clauseIds_.addLong(value);
        bitField0_ |= 0x00000001;
        onChanged();
        return this;
      }

      public Builder addAllClauseIds(
          java.lang.Iterable<? extends java.lang.Long> values) {
        ensureClauseIdsIsMutable();
        com.google.protobuf.AbstractMessageLite.Builder.addAll(
            values, clauseIds_);
        bitField0_ |= 0x00000001;
        onChanged();
        return this;
      }

      public Builder clearClauseIds() {
        clauseIds_ = emptyLongList();
        bitField0_ = (bitField0_ & ~0x00000001);
        onChanged();
        return this;
      }
 
      // @@protoc_insertion_point(builder_scope:operations_research.sat.LratDeletedClauses)
    }
 
    // @@protoc_insertion_point(class_scope:operations_research.sat.LratDeletedClauses)
    private static final operations_research.sat.Lrat.LratDeletedClauses DEFAULT_INSTANCE;
    static {
      DEFAULT_INSTANCE = new operations_research.sat.Lrat.LratDeletedClauses();
    }
 
    public static operations_research.sat.Lrat.LratDeletedClauses getDefaultInstance() {
      return DEFAULT_INSTANCE;
    }
 
    private static final com.google.protobuf.Parser<LratDeletedClauses>
        PARSER = new com.google.protobuf.AbstractParser<LratDeletedClauses>() {
      @java.lang.Override
      public LratDeletedClauses parsePartialFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        Builder builder = newBuilder();
        try {
          builder.mergeFrom(input, extensionRegistry);
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.setUnfinishedMessage(builder.buildPartial());
        } catch (com.google.protobuf.UninitializedMessageException e) {
          throw e.asInvalidProtocolBufferException().setUnfinishedMessage(builder.buildPartial());
        } catch (java.io.IOException e) {
          throw new com.google.protobuf.InvalidProtocolBufferException(e)
              .setUnfinishedMessage(builder.buildPartial());
        }
        return builder.buildPartial();
      }
    };
 
    public static com.google.protobuf.Parser<LratDeletedClauses> parser() {
      return PARSER;
    }
 
    @java.lang.Override
    public com.google.protobuf.Parser<LratDeletedClauses> getParserForType() {
      return PARSER;
    }
 
    @java.lang.Override
    public operations_research.sat.Lrat.LratDeletedClauses getDefaultInstanceForType() {
      return DEFAULT_INSTANCE;
    }
 
  }
 
  public interface LratProofStepOrBuilder extends
      // @@protoc_insertion_point(interface_extends:operations_research.sat.LratProofStep)
      com.google.protobuf.MessageOrBuilder {

    boolean hasImportedClause();
    operations_research.sat.Lrat.LratImportedClause getImportedClause();
    operations_research.sat.Lrat.LratImportedClauseOrBuilder getImportedClauseOrBuilder();

    boolean hasInferredClause();
    operations_research.sat.Lrat.LratInferredClause getInferredClause();
    operations_research.sat.Lrat.LratInferredClauseOrBuilder getInferredClauseOrBuilder();

    boolean hasExportedClause();
    operations_research.sat.Lrat.LratExportedClause getExportedClause();
    operations_research.sat.Lrat.LratExportedClauseOrBuilder getExportedClauseOrBuilder();

    boolean hasDeletedClauses();
    operations_research.sat.Lrat.LratDeletedClauses getDeletedClauses();
    operations_research.sat.Lrat.LratDeletedClausesOrBuilder getDeletedClausesOrBuilder();
 
    operations_research.sat.Lrat.LratProofStep.StepCase getStepCase();
  }

  public static final class LratProofStep extends
      com.google.protobuf.GeneratedMessage implements
      // @@protoc_insertion_point(message_implements:operations_research.sat.LratProofStep)
      LratProofStepOrBuilder {
  private static final long serialVersionUID = 0L;
    static {
      com.google.protobuf.RuntimeVersion.validateProtobufGencodeVersion(
        com.google.protobuf.RuntimeVersion.RuntimeDomain.PUBLIC,
        /* major= */ 4,
        /* minor= */ 33,
        /* patch= */ 1,
        /* suffix= */ "",
        "LratProofStep");
    }
    // Use LratProofStep.newBuilder() to construct.
    private LratProofStep(com.google.protobuf.GeneratedMessage.Builder<?> builder) {
      super(builder);
    }
    private LratProofStep() {
    }
 
    public static final com.google.protobuf.Descriptors.Descriptor
        getDescriptor() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratProofStep_descriptor;
    }
 
    @java.lang.Override
    protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
        internalGetFieldAccessorTable() {
      return operations_research.sat.Lrat.internal_static_operations_research_sat_LratProofStep_fieldAccessorTable
          .ensureFieldAccessorsInitialized(
              operations_research.sat.Lrat.LratProofStep.class, operations_research.sat.Lrat.LratProofStep.Builder.class);
    }
 
    private int stepCase_ = 0;
    @SuppressWarnings("serial")
    private java.lang.Object step_;
    public enum StepCase
        implements com.google.protobuf.Internal.EnumLite,
            com.google.protobuf.AbstractMessage.InternalOneOfEnum {
      IMPORTED_CLAUSE(1),
      INFERRED_CLAUSE(2),
      EXPORTED_CLAUSE(3),
      DELETED_CLAUSES(4),
      STEP_NOT_SET(0);
      private final int value;
      private StepCase(int value) {
        this.value = value;
      }
      @java.lang.Deprecated
      public static StepCase valueOf(int value) {
        return forNumber(value);
      }
 
      public static StepCase forNumber(int value) {
        switch (value) {
          case 1: return IMPORTED_CLAUSE;
          case 2: return INFERRED_CLAUSE;
          case 3: return EXPORTED_CLAUSE;
          case 4: return DELETED_CLAUSES;
          case 0: return STEP_NOT_SET;
          default: return null;
        }
      }
      public int getNumber() {
        return this.value;
      }
    };
 
    public StepCase
    getStepCase() {
      return StepCase.forNumber(
          stepCase_);
    }
 
    public static final int IMPORTED_CLAUSE_FIELD_NUMBER = 1;
    @java.lang.Override
    public boolean hasImportedClause() {
      return stepCase_ == 1;
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratImportedClause getImportedClause() {
      if (stepCase_ == 1) {
         return (operations_research.sat.Lrat.LratImportedClause) step_;
      }
      return operations_research.sat.Lrat.LratImportedClause.getDefaultInstance();
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratImportedClauseOrBuilder getImportedClauseOrBuilder() {
      if (stepCase_ == 1) {
         return (operations_research.sat.Lrat.LratImportedClause) step_;
      }
      return operations_research.sat.Lrat.LratImportedClause.getDefaultInstance();
    }
 
    public static final int INFERRED_CLAUSE_FIELD_NUMBER = 2;
    @java.lang.Override
    public boolean hasInferredClause() {
      return stepCase_ == 2;
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratInferredClause getInferredClause() {
      if (stepCase_ == 2) {
         return (operations_research.sat.Lrat.LratInferredClause) step_;
      }
      return operations_research.sat.Lrat.LratInferredClause.getDefaultInstance();
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratInferredClauseOrBuilder getInferredClauseOrBuilder() {
      if (stepCase_ == 2) {
         return (operations_research.sat.Lrat.LratInferredClause) step_;
      }
      return operations_research.sat.Lrat.LratInferredClause.getDefaultInstance();
    }
 
    public static final int EXPORTED_CLAUSE_FIELD_NUMBER = 3;
    @java.lang.Override
    public boolean hasExportedClause() {
      return stepCase_ == 3;
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratExportedClause getExportedClause() {
      if (stepCase_ == 3) {
         return (operations_research.sat.Lrat.LratExportedClause) step_;
      }
      return operations_research.sat.Lrat.LratExportedClause.getDefaultInstance();
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratExportedClauseOrBuilder getExportedClauseOrBuilder() {
      if (stepCase_ == 3) {
         return (operations_research.sat.Lrat.LratExportedClause) step_;
      }
      return operations_research.sat.Lrat.LratExportedClause.getDefaultInstance();
    }
 
    public static final int DELETED_CLAUSES_FIELD_NUMBER = 4;
    @java.lang.Override
    public boolean hasDeletedClauses() {
      return stepCase_ == 4;
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratDeletedClauses getDeletedClauses() {
      if (stepCase_ == 4) {
         return (operations_research.sat.Lrat.LratDeletedClauses) step_;
      }
      return operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance();
    }

    @java.lang.Override
    public operations_research.sat.Lrat.LratDeletedClausesOrBuilder getDeletedClausesOrBuilder() {
      if (stepCase_ == 4) {
         return (operations_research.sat.Lrat.LratDeletedClauses) step_;
      }
      return operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance();
    }
 
    private byte memoizedIsInitialized = -1;
    @java.lang.Override
    public final boolean isInitialized() {
      byte isInitialized = memoizedIsInitialized;
      if (isInitialized == 1) return true;
      if (isInitialized == 0) return false;
 
      memoizedIsInitialized = 1;
      return true;
    }
 
    @java.lang.Override
    public void writeTo(com.google.protobuf.CodedOutputStream output)
                        throws java.io.IOException {
      if (stepCase_ == 1) {
        output.writeMessage(1, (operations_research.sat.Lrat.LratImportedClause) step_);
      }
      if (stepCase_ == 2) {
        output.writeMessage(2, (operations_research.sat.Lrat.LratInferredClause) step_);
      }
      if (stepCase_ == 3) {
        output.writeMessage(3, (operations_research.sat.Lrat.LratExportedClause) step_);
      }
      if (stepCase_ == 4) {
        output.writeMessage(4, (operations_research.sat.Lrat.LratDeletedClauses) step_);
      }
      getUnknownFields().writeTo(output);
    }
 
    @java.lang.Override
    public int getSerializedSize() {
      int size = memoizedSize;
      if (size != -1) return size;
 
      size = 0;
      if (stepCase_ == 1) {
        size += com.google.protobuf.CodedOutputStream
          .computeMessageSize(1, (operations_research.sat.Lrat.LratImportedClause) step_);
      }
      if (stepCase_ == 2) {
        size += com.google.protobuf.CodedOutputStream
          .computeMessageSize(2, (operations_research.sat.Lrat.LratInferredClause) step_);
      }
      if (stepCase_ == 3) {
        size += com.google.protobuf.CodedOutputStream
          .computeMessageSize(3, (operations_research.sat.Lrat.LratExportedClause) step_);
      }
      if (stepCase_ == 4) {
        size += com.google.protobuf.CodedOutputStream
          .computeMessageSize(4, (operations_research.sat.Lrat.LratDeletedClauses) step_);
      }
      size += getUnknownFields().getSerializedSize();
      memoizedSize = size;
      return size;
    }
 
    @java.lang.Override
    public boolean equals(final java.lang.Object obj) {
      if (obj == this) {
       return true;
      }
      if (!(obj instanceof operations_research.sat.Lrat.LratProofStep)) {
        return super.equals(obj);
      }
      operations_research.sat.Lrat.LratProofStep other = (operations_research.sat.Lrat.LratProofStep) obj;
 
      if (!getStepCase().equals(other.getStepCase())) return false;
      switch (stepCase_) {
        case 1:
          if (!getImportedClause()
              .equals(other.getImportedClause())) return false;
          break;
        case 2:
          if (!getInferredClause()
              .equals(other.getInferredClause())) return false;
          break;
        case 3:
          if (!getExportedClause()
              .equals(other.getExportedClause())) return false;
          break;
        case 4:
          if (!getDeletedClauses()
              .equals(other.getDeletedClauses())) return false;
          break;
        case 0:
        default:
      }
      if (!getUnknownFields().equals(other.getUnknownFields())) return false;
      return true;
    }
 
    @java.lang.Override
    public int hashCode() {
      if (memoizedHashCode != 0) {
        return memoizedHashCode;
      }
      int hash = 41;
      hash = (19 * hash) + getDescriptor().hashCode();
      switch (stepCase_) {
        case 1:
          hash = (37 * hash) + IMPORTED_CLAUSE_FIELD_NUMBER;
          hash = (53 * hash) + getImportedClause().hashCode();
          break;
        case 2:
          hash = (37 * hash) + INFERRED_CLAUSE_FIELD_NUMBER;
          hash = (53 * hash) + getInferredClause().hashCode();
          break;
        case 3:
          hash = (37 * hash) + EXPORTED_CLAUSE_FIELD_NUMBER;
          hash = (53 * hash) + getExportedClause().hashCode();
          break;
        case 4:
          hash = (37 * hash) + DELETED_CLAUSES_FIELD_NUMBER;
          hash = (53 * hash) + getDeletedClauses().hashCode();
          break;
        case 0:
        default:
      }
      hash = (29 * hash) + getUnknownFields().hashCode();
      memoizedHashCode = hash;
      return hash;
    }
 
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        java.nio.ByteBuffer data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        java.nio.ByteBuffer data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        com.google.protobuf.ByteString data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        com.google.protobuf.ByteString data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(byte[] data)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        byte[] data,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws com.google.protobuf.InvalidProtocolBufferException {
      return PARSER.parseFrom(data, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    public static operations_research.sat.Lrat.LratProofStep parseDelimitedFrom(java.io.InputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input);
    }
 
    public static operations_research.sat.Lrat.LratProofStep parseDelimitedFrom(
        java.io.InputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseDelimitedWithIOException(PARSER, input, extensionRegistry);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        com.google.protobuf.CodedInputStream input)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input);
    }
    public static operations_research.sat.Lrat.LratProofStep parseFrom(
        com.google.protobuf.CodedInputStream input,
        com.google.protobuf.ExtensionRegistryLite extensionRegistry)
        throws java.io.IOException {
      return com.google.protobuf.GeneratedMessage
          .parseWithIOException(PARSER, input, extensionRegistry);
    }
 
    @java.lang.Override
    public Builder newBuilderForType() { return newBuilder(); }
    public static Builder newBuilder() {
      return DEFAULT_INSTANCE.toBuilder();
    }
    public static Builder newBuilder(operations_research.sat.Lrat.LratProofStep prototype) {
      return DEFAULT_INSTANCE.toBuilder().mergeFrom(prototype);
    }
    @java.lang.Override
    public Builder toBuilder() {
      return this == DEFAULT_INSTANCE
          ? new Builder() : new Builder().mergeFrom(this);
    }
 
    @java.lang.Override
    protected Builder newBuilderForType(
        com.google.protobuf.GeneratedMessage.BuilderParent parent) {
      Builder builder = new Builder(parent);
      return builder;
    }

    public static final class Builder extends
        com.google.protobuf.GeneratedMessage.Builder<Builder> implements
        // @@protoc_insertion_point(builder_implements:operations_research.sat.LratProofStep)
        operations_research.sat.Lrat.LratProofStepOrBuilder {
      public static final com.google.protobuf.Descriptors.Descriptor
          getDescriptor() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratProofStep_descriptor;
      }
 
      @java.lang.Override
      protected com.google.protobuf.GeneratedMessage.FieldAccessorTable
          internalGetFieldAccessorTable() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratProofStep_fieldAccessorTable
            .ensureFieldAccessorsInitialized(
                operations_research.sat.Lrat.LratProofStep.class, operations_research.sat.Lrat.LratProofStep.Builder.class);
      }
 
      // Construct using operations_research.sat.Lrat.LratProofStep.newBuilder()
      private Builder() {
 
      }
 
      private Builder(
          com.google.protobuf.GeneratedMessage.BuilderParent parent) {
        super(parent);
 
      }
      @java.lang.Override
      public Builder clear() {
        super.clear();
        bitField0_ = 0;
        if (importedClauseBuilder_ != null) {
          importedClauseBuilder_.clear();
        }
        if (inferredClauseBuilder_ != null) {
          inferredClauseBuilder_.clear();
        }
        if (exportedClauseBuilder_ != null) {
          exportedClauseBuilder_.clear();
        }
        if (deletedClausesBuilder_ != null) {
          deletedClausesBuilder_.clear();
        }
        stepCase_ = 0;
        step_ = null;
        return this;
      }
 
      @java.lang.Override
      public com.google.protobuf.Descriptors.Descriptor
          getDescriptorForType() {
        return operations_research.sat.Lrat.internal_static_operations_research_sat_LratProofStep_descriptor;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratProofStep getDefaultInstanceForType() {
        return operations_research.sat.Lrat.LratProofStep.getDefaultInstance();
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratProofStep build() {
        operations_research.sat.Lrat.LratProofStep result = buildPartial();
        if (!result.isInitialized()) {
          throw newUninitializedMessageException(result);
        }
        return result;
      }
 
      @java.lang.Override
      public operations_research.sat.Lrat.LratProofStep buildPartial() {
        operations_research.sat.Lrat.LratProofStep result = new operations_research.sat.Lrat.LratProofStep(this);
        if (bitField0_ != 0) { buildPartial0(result); }
        buildPartialOneofs(result);
        onBuilt();
        return result;
      }
 
      private void buildPartial0(operations_research.sat.Lrat.LratProofStep result) {
        int from_bitField0_ = bitField0_;
      }
 
      private void buildPartialOneofs(operations_research.sat.Lrat.LratProofStep result) {
        result.stepCase_ = stepCase_;
        result.step_ = this.step_;
        if (stepCase_ == 1 &&
            importedClauseBuilder_ != null) {
          result.step_ = importedClauseBuilder_.build();
        }
        if (stepCase_ == 2 &&
            inferredClauseBuilder_ != null) {
          result.step_ = inferredClauseBuilder_.build();
        }
        if (stepCase_ == 3 &&
            exportedClauseBuilder_ != null) {
          result.step_ = exportedClauseBuilder_.build();
        }
        if (stepCase_ == 4 &&
            deletedClausesBuilder_ != null) {
          result.step_ = deletedClausesBuilder_.build();
        }
      }
 
      @java.lang.Override
      public Builder mergeFrom(com.google.protobuf.Message other) {
        if (other instanceof operations_research.sat.Lrat.LratProofStep) {
          return mergeFrom((operations_research.sat.Lrat.LratProofStep)other);
        } else {
          super.mergeFrom(other);
          return this;
        }
      }
 
      public Builder mergeFrom(operations_research.sat.Lrat.LratProofStep other) {
        if (other == operations_research.sat.Lrat.LratProofStep.getDefaultInstance()) return this;
        switch (other.getStepCase()) {
          case IMPORTED_CLAUSE: {
            mergeImportedClause(other.getImportedClause());
            break;
          }
          case INFERRED_CLAUSE: {
            mergeInferredClause(other.getInferredClause());
            break;
          }
          case EXPORTED_CLAUSE: {
            mergeExportedClause(other.getExportedClause());
            break;
          }
          case DELETED_CLAUSES: {
            mergeDeletedClauses(other.getDeletedClauses());
            break;
          }
          case STEP_NOT_SET: {
            break;
          }
        }
        this.mergeUnknownFields(other.getUnknownFields());
        onChanged();
        return this;
      }
 
      @java.lang.Override
      public final boolean isInitialized() {
        return true;
      }
 
      @java.lang.Override
      public Builder mergeFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws java.io.IOException {
        if (extensionRegistry == null) {
          throw new java.lang.NullPointerException();
        }
        try {
          boolean done = false;
          while (!done) {
            int tag = input.readTag();
            switch (tag) {
              case 0:
                done = true;
                break;
              case 10: {
                input.readMessage(
                    internalGetImportedClauseFieldBuilder().getBuilder(),
                    extensionRegistry);
                stepCase_ = 1;
                break;
              } // case 10
              case 18: {
                input.readMessage(
                    internalGetInferredClauseFieldBuilder().getBuilder(),
                    extensionRegistry);
                stepCase_ = 2;
                break;
              } // case 18
              case 26: {
                input.readMessage(
                    internalGetExportedClauseFieldBuilder().getBuilder(),
                    extensionRegistry);
                stepCase_ = 3;
                break;
              } // case 26
              case 34: {
                input.readMessage(
                    internalGetDeletedClausesFieldBuilder().getBuilder(),
                    extensionRegistry);
                stepCase_ = 4;
                break;
              } // case 34
              default: {
                if (!super.parseUnknownField(input, extensionRegistry, tag)) {
                  done = true; // was an endgroup tag
                }
                break;
              } // default:
            } // switch (tag)
          } // while (!done)
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.unwrapIOException();
        } finally {
          onChanged();
        } // finally
        return this;
      }
      private int stepCase_ = 0;
      private java.lang.Object step_;
      public StepCase
          getStepCase() {
        return StepCase.forNumber(
            stepCase_);
      }
 
      public Builder clearStep() {
        stepCase_ = 0;
        step_ = null;
        onChanged();
        return this;
      }
 
      private int bitField0_;
 
      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratImportedClause, operations_research.sat.Lrat.LratImportedClause.Builder, operations_research.sat.Lrat.LratImportedClauseOrBuilder> importedClauseBuilder_;
      @java.lang.Override
      public boolean hasImportedClause() {
        return stepCase_ == 1;
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratImportedClause getImportedClause() {
        if (importedClauseBuilder_ == null) {
          if (stepCase_ == 1) {
            return (operations_research.sat.Lrat.LratImportedClause) step_;
          }
          return operations_research.sat.Lrat.LratImportedClause.getDefaultInstance();
        } else {
          if (stepCase_ == 1) {
            return importedClauseBuilder_.getMessage();
          }
          return operations_research.sat.Lrat.LratImportedClause.getDefaultInstance();
        }
      }

      public Builder setImportedClause(operations_research.sat.Lrat.LratImportedClause value) {
        if (importedClauseBuilder_ == null) {
          if (value == null) {
            throw new NullPointerException();
          }
          step_ = value;
          onChanged();
        } else {
          importedClauseBuilder_.setMessage(value);
        }
        stepCase_ = 1;
        return this;
      }

      public Builder setImportedClause(
          operations_research.sat.Lrat.LratImportedClause.Builder builderForValue) {
        if (importedClauseBuilder_ == null) {
          step_ = builderForValue.build();
          onChanged();
        } else {
          importedClauseBuilder_.setMessage(builderForValue.build());
        }
        stepCase_ = 1;
        return this;
      }

      public Builder mergeImportedClause(operations_research.sat.Lrat.LratImportedClause value) {
        if (importedClauseBuilder_ == null) {
          if (stepCase_ == 1 &&
              step_ != operations_research.sat.Lrat.LratImportedClause.getDefaultInstance()) {
            step_ = operations_research.sat.Lrat.LratImportedClause.newBuilder((operations_research.sat.Lrat.LratImportedClause) step_)
                .mergeFrom(value).buildPartial();
          } else {
            step_ = value;
          }
          onChanged();
        } else {
          if (stepCase_ == 1) {
            importedClauseBuilder_.mergeFrom(value);
          } else {
            importedClauseBuilder_.setMessage(value);
          }
        }
        stepCase_ = 1;
        return this;
      }

      public Builder clearImportedClause() {
        if (importedClauseBuilder_ == null) {
          if (stepCase_ == 1) {
            stepCase_ = 0;
            step_ = null;
            onChanged();
          }
        } else {
          if (stepCase_ == 1) {
            stepCase_ = 0;
            step_ = null;
          }
          importedClauseBuilder_.clear();
        }
        return this;
      }

      public operations_research.sat.Lrat.LratImportedClause.Builder getImportedClauseBuilder() {
        return internalGetImportedClauseFieldBuilder().getBuilder();
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratImportedClauseOrBuilder getImportedClauseOrBuilder() {
        if ((stepCase_ == 1) && (importedClauseBuilder_ != null)) {
          return importedClauseBuilder_.getMessageOrBuilder();
        } else {
          if (stepCase_ == 1) {
            return (operations_research.sat.Lrat.LratImportedClause) step_;
          }
          return operations_research.sat.Lrat.LratImportedClause.getDefaultInstance();
        }
      }

      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratImportedClause, operations_research.sat.Lrat.LratImportedClause.Builder, operations_research.sat.Lrat.LratImportedClauseOrBuilder> 
          internalGetImportedClauseFieldBuilder() {
        if (importedClauseBuilder_ == null) {
          if (!(stepCase_ == 1)) {
            step_ = operations_research.sat.Lrat.LratImportedClause.getDefaultInstance();
          }
          importedClauseBuilder_ = new com.google.protobuf.SingleFieldBuilder<
              operations_research.sat.Lrat.LratImportedClause, operations_research.sat.Lrat.LratImportedClause.Builder, operations_research.sat.Lrat.LratImportedClauseOrBuilder>(
                  (operations_research.sat.Lrat.LratImportedClause) step_,
                  getParentForChildren(),
                  isClean());
          step_ = null;
        }
        stepCase_ = 1;
        onChanged();
        return importedClauseBuilder_;
      }
 
      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratInferredClause, operations_research.sat.Lrat.LratInferredClause.Builder, operations_research.sat.Lrat.LratInferredClauseOrBuilder> inferredClauseBuilder_;
      @java.lang.Override
      public boolean hasInferredClause() {
        return stepCase_ == 2;
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratInferredClause getInferredClause() {
        if (inferredClauseBuilder_ == null) {
          if (stepCase_ == 2) {
            return (operations_research.sat.Lrat.LratInferredClause) step_;
          }
          return operations_research.sat.Lrat.LratInferredClause.getDefaultInstance();
        } else {
          if (stepCase_ == 2) {
            return inferredClauseBuilder_.getMessage();
          }
          return operations_research.sat.Lrat.LratInferredClause.getDefaultInstance();
        }
      }

      public Builder setInferredClause(operations_research.sat.Lrat.LratInferredClause value) {
        if (inferredClauseBuilder_ == null) {
          if (value == null) {
            throw new NullPointerException();
          }
          step_ = value;
          onChanged();
        } else {
          inferredClauseBuilder_.setMessage(value);
        }
        stepCase_ = 2;
        return this;
      }

      public Builder setInferredClause(
          operations_research.sat.Lrat.LratInferredClause.Builder builderForValue) {
        if (inferredClauseBuilder_ == null) {
          step_ = builderForValue.build();
          onChanged();
        } else {
          inferredClauseBuilder_.setMessage(builderForValue.build());
        }
        stepCase_ = 2;
        return this;
      }

      public Builder mergeInferredClause(operations_research.sat.Lrat.LratInferredClause value) {
        if (inferredClauseBuilder_ == null) {
          if (stepCase_ == 2 &&
              step_ != operations_research.sat.Lrat.LratInferredClause.getDefaultInstance()) {
            step_ = operations_research.sat.Lrat.LratInferredClause.newBuilder((operations_research.sat.Lrat.LratInferredClause) step_)
                .mergeFrom(value).buildPartial();
          } else {
            step_ = value;
          }
          onChanged();
        } else {
          if (stepCase_ == 2) {
            inferredClauseBuilder_.mergeFrom(value);
          } else {
            inferredClauseBuilder_.setMessage(value);
          }
        }
        stepCase_ = 2;
        return this;
      }

      public Builder clearInferredClause() {
        if (inferredClauseBuilder_ == null) {
          if (stepCase_ == 2) {
            stepCase_ = 0;
            step_ = null;
            onChanged();
          }
        } else {
          if (stepCase_ == 2) {
            stepCase_ = 0;
            step_ = null;
          }
          inferredClauseBuilder_.clear();
        }
        return this;
      }

      public operations_research.sat.Lrat.LratInferredClause.Builder getInferredClauseBuilder() {
        return internalGetInferredClauseFieldBuilder().getBuilder();
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratInferredClauseOrBuilder getInferredClauseOrBuilder() {
        if ((stepCase_ == 2) && (inferredClauseBuilder_ != null)) {
          return inferredClauseBuilder_.getMessageOrBuilder();
        } else {
          if (stepCase_ == 2) {
            return (operations_research.sat.Lrat.LratInferredClause) step_;
          }
          return operations_research.sat.Lrat.LratInferredClause.getDefaultInstance();
        }
      }

      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratInferredClause, operations_research.sat.Lrat.LratInferredClause.Builder, operations_research.sat.Lrat.LratInferredClauseOrBuilder> 
          internalGetInferredClauseFieldBuilder() {
        if (inferredClauseBuilder_ == null) {
          if (!(stepCase_ == 2)) {
            step_ = operations_research.sat.Lrat.LratInferredClause.getDefaultInstance();
          }
          inferredClauseBuilder_ = new com.google.protobuf.SingleFieldBuilder<
              operations_research.sat.Lrat.LratInferredClause, operations_research.sat.Lrat.LratInferredClause.Builder, operations_research.sat.Lrat.LratInferredClauseOrBuilder>(
                  (operations_research.sat.Lrat.LratInferredClause) step_,
                  getParentForChildren(),
                  isClean());
          step_ = null;
        }
        stepCase_ = 2;
        onChanged();
        return inferredClauseBuilder_;
      }
 
      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratExportedClause, operations_research.sat.Lrat.LratExportedClause.Builder, operations_research.sat.Lrat.LratExportedClauseOrBuilder> exportedClauseBuilder_;
      @java.lang.Override
      public boolean hasExportedClause() {
        return stepCase_ == 3;
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratExportedClause getExportedClause() {
        if (exportedClauseBuilder_ == null) {
          if (stepCase_ == 3) {
            return (operations_research.sat.Lrat.LratExportedClause) step_;
          }
          return operations_research.sat.Lrat.LratExportedClause.getDefaultInstance();
        } else {
          if (stepCase_ == 3) {
            return exportedClauseBuilder_.getMessage();
          }
          return operations_research.sat.Lrat.LratExportedClause.getDefaultInstance();
        }
      }

      public Builder setExportedClause(operations_research.sat.Lrat.LratExportedClause value) {
        if (exportedClauseBuilder_ == null) {
          if (value == null) {
            throw new NullPointerException();
          }
          step_ = value;
          onChanged();
        } else {
          exportedClauseBuilder_.setMessage(value);
        }
        stepCase_ = 3;
        return this;
      }

      public Builder setExportedClause(
          operations_research.sat.Lrat.LratExportedClause.Builder builderForValue) {
        if (exportedClauseBuilder_ == null) {
          step_ = builderForValue.build();
          onChanged();
        } else {
          exportedClauseBuilder_.setMessage(builderForValue.build());
        }
        stepCase_ = 3;
        return this;
      }

      public Builder mergeExportedClause(operations_research.sat.Lrat.LratExportedClause value) {
        if (exportedClauseBuilder_ == null) {
          if (stepCase_ == 3 &&
              step_ != operations_research.sat.Lrat.LratExportedClause.getDefaultInstance()) {
            step_ = operations_research.sat.Lrat.LratExportedClause.newBuilder((operations_research.sat.Lrat.LratExportedClause) step_)
                .mergeFrom(value).buildPartial();
          } else {
            step_ = value;
          }
          onChanged();
        } else {
          if (stepCase_ == 3) {
            exportedClauseBuilder_.mergeFrom(value);
          } else {
            exportedClauseBuilder_.setMessage(value);
          }
        }
        stepCase_ = 3;
        return this;
      }

      public Builder clearExportedClause() {
        if (exportedClauseBuilder_ == null) {
          if (stepCase_ == 3) {
            stepCase_ = 0;
            step_ = null;
            onChanged();
          }
        } else {
          if (stepCase_ == 3) {
            stepCase_ = 0;
            step_ = null;
          }
          exportedClauseBuilder_.clear();
        }
        return this;
      }

      public operations_research.sat.Lrat.LratExportedClause.Builder getExportedClauseBuilder() {
        return internalGetExportedClauseFieldBuilder().getBuilder();
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratExportedClauseOrBuilder getExportedClauseOrBuilder() {
        if ((stepCase_ == 3) && (exportedClauseBuilder_ != null)) {
          return exportedClauseBuilder_.getMessageOrBuilder();
        } else {
          if (stepCase_ == 3) {
            return (operations_research.sat.Lrat.LratExportedClause) step_;
          }
          return operations_research.sat.Lrat.LratExportedClause.getDefaultInstance();
        }
      }

      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratExportedClause, operations_research.sat.Lrat.LratExportedClause.Builder, operations_research.sat.Lrat.LratExportedClauseOrBuilder> 
          internalGetExportedClauseFieldBuilder() {
        if (exportedClauseBuilder_ == null) {
          if (!(stepCase_ == 3)) {
            step_ = operations_research.sat.Lrat.LratExportedClause.getDefaultInstance();
          }
          exportedClauseBuilder_ = new com.google.protobuf.SingleFieldBuilder<
              operations_research.sat.Lrat.LratExportedClause, operations_research.sat.Lrat.LratExportedClause.Builder, operations_research.sat.Lrat.LratExportedClauseOrBuilder>(
                  (operations_research.sat.Lrat.LratExportedClause) step_,
                  getParentForChildren(),
                  isClean());
          step_ = null;
        }
        stepCase_ = 3;
        onChanged();
        return exportedClauseBuilder_;
      }
 
      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratDeletedClauses, operations_research.sat.Lrat.LratDeletedClauses.Builder, operations_research.sat.Lrat.LratDeletedClausesOrBuilder> deletedClausesBuilder_;
      @java.lang.Override
      public boolean hasDeletedClauses() {
        return stepCase_ == 4;
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratDeletedClauses getDeletedClauses() {
        if (deletedClausesBuilder_ == null) {
          if (stepCase_ == 4) {
            return (operations_research.sat.Lrat.LratDeletedClauses) step_;
          }
          return operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance();
        } else {
          if (stepCase_ == 4) {
            return deletedClausesBuilder_.getMessage();
          }
          return operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance();
        }
      }

      public Builder setDeletedClauses(operations_research.sat.Lrat.LratDeletedClauses value) {
        if (deletedClausesBuilder_ == null) {
          if (value == null) {
            throw new NullPointerException();
          }
          step_ = value;
          onChanged();
        } else {
          deletedClausesBuilder_.setMessage(value);
        }
        stepCase_ = 4;
        return this;
      }

      public Builder setDeletedClauses(
          operations_research.sat.Lrat.LratDeletedClauses.Builder builderForValue) {
        if (deletedClausesBuilder_ == null) {
          step_ = builderForValue.build();
          onChanged();
        } else {
          deletedClausesBuilder_.setMessage(builderForValue.build());
        }
        stepCase_ = 4;
        return this;
      }

      public Builder mergeDeletedClauses(operations_research.sat.Lrat.LratDeletedClauses value) {
        if (deletedClausesBuilder_ == null) {
          if (stepCase_ == 4 &&
              step_ != operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance()) {
            step_ = operations_research.sat.Lrat.LratDeletedClauses.newBuilder((operations_research.sat.Lrat.LratDeletedClauses) step_)
                .mergeFrom(value).buildPartial();
          } else {
            step_ = value;
          }
          onChanged();
        } else {
          if (stepCase_ == 4) {
            deletedClausesBuilder_.mergeFrom(value);
          } else {
            deletedClausesBuilder_.setMessage(value);
          }
        }
        stepCase_ = 4;
        return this;
      }

      public Builder clearDeletedClauses() {
        if (deletedClausesBuilder_ == null) {
          if (stepCase_ == 4) {
            stepCase_ = 0;
            step_ = null;
            onChanged();
          }
        } else {
          if (stepCase_ == 4) {
            stepCase_ = 0;
            step_ = null;
          }
          deletedClausesBuilder_.clear();
        }
        return this;
      }

      public operations_research.sat.Lrat.LratDeletedClauses.Builder getDeletedClausesBuilder() {
        return internalGetDeletedClausesFieldBuilder().getBuilder();
      }

      @java.lang.Override
      public operations_research.sat.Lrat.LratDeletedClausesOrBuilder getDeletedClausesOrBuilder() {
        if ((stepCase_ == 4) && (deletedClausesBuilder_ != null)) {
          return deletedClausesBuilder_.getMessageOrBuilder();
        } else {
          if (stepCase_ == 4) {
            return (operations_research.sat.Lrat.LratDeletedClauses) step_;
          }
          return operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance();
        }
      }

      private com.google.protobuf.SingleFieldBuilder<
          operations_research.sat.Lrat.LratDeletedClauses, operations_research.sat.Lrat.LratDeletedClauses.Builder, operations_research.sat.Lrat.LratDeletedClausesOrBuilder> 
          internalGetDeletedClausesFieldBuilder() {
        if (deletedClausesBuilder_ == null) {
          if (!(stepCase_ == 4)) {
            step_ = operations_research.sat.Lrat.LratDeletedClauses.getDefaultInstance();
          }
          deletedClausesBuilder_ = new com.google.protobuf.SingleFieldBuilder<
              operations_research.sat.Lrat.LratDeletedClauses, operations_research.sat.Lrat.LratDeletedClauses.Builder, operations_research.sat.Lrat.LratDeletedClausesOrBuilder>(
                  (operations_research.sat.Lrat.LratDeletedClauses) step_,
                  getParentForChildren(),
                  isClean());
          step_ = null;
        }
        stepCase_ = 4;
        onChanged();
        return deletedClausesBuilder_;
      }
 
      // @@protoc_insertion_point(builder_scope:operations_research.sat.LratProofStep)
    }
 
    // @@protoc_insertion_point(class_scope:operations_research.sat.LratProofStep)
    private static final operations_research.sat.Lrat.LratProofStep DEFAULT_INSTANCE;
    static {
      DEFAULT_INSTANCE = new operations_research.sat.Lrat.LratProofStep();
    }
 
    public static operations_research.sat.Lrat.LratProofStep getDefaultInstance() {
      return DEFAULT_INSTANCE;
    }
 
    private static final com.google.protobuf.Parser<LratProofStep>
        PARSER = new com.google.protobuf.AbstractParser<LratProofStep>() {
      @java.lang.Override
      public LratProofStep parsePartialFrom(
          com.google.protobuf.CodedInputStream input,
          com.google.protobuf.ExtensionRegistryLite extensionRegistry)
          throws com.google.protobuf.InvalidProtocolBufferException {
        Builder builder = newBuilder();
        try {
          builder.mergeFrom(input, extensionRegistry);
        } catch (com.google.protobuf.InvalidProtocolBufferException e) {
          throw e.setUnfinishedMessage(builder.buildPartial());
        } catch (com.google.protobuf.UninitializedMessageException e) {
          throw e.asInvalidProtocolBufferException().setUnfinishedMessage(builder.buildPartial());
        } catch (java.io.IOException e) {
          throw new com.google.protobuf.InvalidProtocolBufferException(e)
              .setUnfinishedMessage(builder.buildPartial());
        }
        return builder.buildPartial();
      }
    };
 
    public static com.google.protobuf.Parser<LratProofStep> parser() {
      return PARSER;
    }
 
    @java.lang.Override
    public com.google.protobuf.Parser<LratProofStep> getParserForType() {
      return PARSER;
    }
 
    @java.lang.Override
    public operations_research.sat.Lrat.LratProofStep getDefaultInstanceForType() {
      return DEFAULT_INSTANCE;
    }
 
  }
 
  private static final com.google.protobuf.Descriptors.Descriptor
    internal_static_operations_research_sat_LratImportedClause_descriptor;
  private static final 
    com.google.protobuf.GeneratedMessage.FieldAccessorTable
      internal_static_operations_research_sat_LratImportedClause_fieldAccessorTable;
  private static final com.google.protobuf.Descriptors.Descriptor
    internal_static_operations_research_sat_LratInferredClause_descriptor;
  private static final 
    com.google.protobuf.GeneratedMessage.FieldAccessorTable
      internal_static_operations_research_sat_LratInferredClause_fieldAccessorTable;
  private static final com.google.protobuf.Descriptors.Descriptor
    internal_static_operations_research_sat_LratInferredClause_RatInfo_descriptor;
  private static final 
    com.google.protobuf.GeneratedMessage.FieldAccessorTable
      internal_static_operations_research_sat_LratInferredClause_RatInfo_fieldAccessorTable;
  private static final com.google.protobuf.Descriptors.Descriptor
    internal_static_operations_research_sat_LratExportedClause_descriptor;
  private static final 
    com.google.protobuf.GeneratedMessage.FieldAccessorTable
      internal_static_operations_research_sat_LratExportedClause_fieldAccessorTable;
  private static final com.google.protobuf.Descriptors.Descriptor
    internal_static_operations_research_sat_LratDeletedClauses_descriptor;
  private static final 
    com.google.protobuf.GeneratedMessage.FieldAccessorTable
      internal_static_operations_research_sat_LratDeletedClauses_fieldAccessorTable;
  private static final com.google.protobuf.Descriptors.Descriptor
    internal_static_operations_research_sat_LratProofStep_descriptor;
  private static final 
    com.google.protobuf.GeneratedMessage.FieldAccessorTable
      internal_static_operations_research_sat_LratProofStep_fieldAccessorTable;
 
  public static com.google.protobuf.Descriptors.FileDescriptor
      getDescriptor() {
    return descriptor;
  }
  private static  com.google.protobuf.Descriptors.FileDescriptor
      descriptor;
  static {
    java.lang.String[] descriptorData = {
      "\n\026ortools/sat/lrat.proto\022\027operations_res" +
      "earch.sat\"=\n\022LratImportedClause\022\021\n\tclaus" +
      "e_id\030\001 \001(\003\022\024\n\010literals\030\002 \003(\005B\002\020\001\"\344\001\n\022Lra" +
      "tInferredClause\022\021\n\tclause_id\030\001 \001(\003\022\024\n\010li" +
      "terals\030\002 \003(\005B\002\020\001\022\024\n\010unit_ids\030\003 \003(\003B\002\020\001\022F" +
      "\n\trat_infos\030\004 \003(\01323.operations_research." +
      "sat.LratInferredClause.RatInfo\022\020\n\010export" +
      "ed\030\005 \001(\010\0325\n\007RatInfo\022\024\n\014resolvant_id\030\001 \001(" +
      "\003\022\024\n\010unit_ids\030\002 \003(\003B\002\020\001\"=\n\022LratExportedC" +
      "lause\022\021\n\tclause_id\030\001 \001(\003\022\024\n\010literals\030\002 \003" +
      "(\005B\002\020\001\",\n\022LratDeletedClauses\022\026\n\nclause_i" +
      "ds\030\001 \003(\003B\002\020\001\"\267\002\n\rLratProofStep\022F\n\017import" +
      "ed_clause\030\001 \001(\0132+.operations_research.sa" +
      "t.LratImportedClauseH\000\022F\n\017inferred_claus" +
      "e\030\002 \001(\0132+.operations_research.sat.LratIn" +
      "ferredClauseH\000\022F\n\017exported_clause\030\003 \001(\0132" +
      "+.operations_research.sat.LratExportedCl" +
      "auseH\000\022F\n\017deleted_clauses\030\004 \001(\0132+.operat" +
      "ions_research.sat.LratDeletedClausesH\000B\006" +
      "\n\004step"
    };
    descriptor = com.google.protobuf.Descriptors.FileDescriptor
      .internalBuildGeneratedFileFrom(descriptorData,
        new com.google.protobuf.Descriptors.FileDescriptor[] {
        });
    internal_static_operations_research_sat_LratImportedClause_descriptor =
      getDescriptor().getMessageType(0);
    internal_static_operations_research_sat_LratImportedClause_fieldAccessorTable = new
      com.google.protobuf.GeneratedMessage.FieldAccessorTable(
        internal_static_operations_research_sat_LratImportedClause_descriptor,
        new java.lang.String[] { "ClauseId", "Literals", });
    internal_static_operations_research_sat_LratInferredClause_descriptor =
      getDescriptor().getMessageType(1);
    internal_static_operations_research_sat_LratInferredClause_fieldAccessorTable = new
      com.google.protobuf.GeneratedMessage.FieldAccessorTable(
        internal_static_operations_research_sat_LratInferredClause_descriptor,
        new java.lang.String[] { "ClauseId", "Literals", "UnitIds", "RatInfos", "Exported", });
    internal_static_operations_research_sat_LratInferredClause_RatInfo_descriptor =
      internal_static_operations_research_sat_LratInferredClause_descriptor.getNestedType(0);
    internal_static_operations_research_sat_LratInferredClause_RatInfo_fieldAccessorTable = new
      com.google.protobuf.GeneratedMessage.FieldAccessorTable(
        internal_static_operations_research_sat_LratInferredClause_RatInfo_descriptor,
        new java.lang.String[] { "ResolvantId", "UnitIds", });
    internal_static_operations_research_sat_LratExportedClause_descriptor =
      getDescriptor().getMessageType(2);
    internal_static_operations_research_sat_LratExportedClause_fieldAccessorTable = new
      com.google.protobuf.GeneratedMessage.FieldAccessorTable(
        internal_static_operations_research_sat_LratExportedClause_descriptor,
        new java.lang.String[] { "ClauseId", "Literals", });
    internal_static_operations_research_sat_LratDeletedClauses_descriptor =
      getDescriptor().getMessageType(3);
    internal_static_operations_research_sat_LratDeletedClauses_fieldAccessorTable = new
      com.google.protobuf.GeneratedMessage.FieldAccessorTable(
        internal_static_operations_research_sat_LratDeletedClauses_descriptor,
        new java.lang.String[] { "ClauseIds", });
    internal_static_operations_research_sat_LratProofStep_descriptor =
      getDescriptor().getMessageType(4);
    internal_static_operations_research_sat_LratProofStep_fieldAccessorTable = new
      com.google.protobuf.GeneratedMessage.FieldAccessorTable(
        internal_static_operations_research_sat_LratProofStep_descriptor,
        new java.lang.String[] { "ImportedClause", "InferredClause", "ExportedClause", "DeletedClauses", "Step", });
    descriptor.resolveAllFeaturesImmutable();
  }
 
  // @@protoc_insertion_point(outer_class_scope)
}