Lrat.pb.cs

Go to the documentation of this file.

// <auto-generated>
//     Generated by the protocol buffer compiler.  DO NOT EDIT!
//     source: ortools/sat/lrat.proto
// </auto-generated>
#pragma warning disable 1591, 0612, 3021, 8981
#region Designer generated code
 
using pb = global::Google.Protobuf;
using pbc = global::Google.Protobuf.Collections;
using pbr = global::Google.Protobuf.Reflection;
using scg = global::System.Collections.Generic;
namespace OperationsResearch.Sat {

  public static partial class LratReflection {
 
    #region Descriptor
    public static pbr::FileDescriptor Descriptor {
      get { return descriptor; }
    }
    private static pbr::FileDescriptor descriptor;
 
    static LratReflection() {
      byte[] descriptorData = global::System.Convert.FromBase64String(
          string.Concat(
            "ChZvcnRvb2xzL3NhdC9scmF0LnByb3RvEhdvcGVyYXRpb25zX3Jlc2VhcmNo",
            "LnNhdCI9ChJMcmF0SW1wb3J0ZWRDbGF1c2USEQoJY2xhdXNlX2lkGAEgASgD",
            "EhQKCGxpdGVyYWxzGAIgAygFQgIQASLkAQoSTHJhdEluZmVycmVkQ2xhdXNl",
            "EhEKCWNsYXVzZV9pZBgBIAEoAxIUCghsaXRlcmFscxgCIAMoBUICEAESFAoI",
            "dW5pdF9pZHMYAyADKANCAhABEkYKCXJhdF9pbmZvcxgEIAMoCzIzLm9wZXJh",
            "dGlvbnNfcmVzZWFyY2guc2F0LkxyYXRJbmZlcnJlZENsYXVzZS5SYXRJbmZv",
            "EhAKCGV4cG9ydGVkGAUgASgIGjUKB1JhdEluZm8SFAoMcmVzb2x2YW50X2lk",
            "GAEgASgDEhQKCHVuaXRfaWRzGAIgAygDQgIQASI9ChJMcmF0RXhwb3J0ZWRD",
            "bGF1c2USEQoJY2xhdXNlX2lkGAEgASgDEhQKCGxpdGVyYWxzGAIgAygFQgIQ",
            "ASIsChJMcmF0RGVsZXRlZENsYXVzZXMSFgoKY2xhdXNlX2lkcxgBIAMoA0IC",
            "EAEitwIKDUxyYXRQcm9vZlN0ZXASRgoPaW1wb3J0ZWRfY2xhdXNlGAEgASgL",
            "Misub3BlcmF0aW9uc19yZXNlYXJjaC5zYXQuTHJhdEltcG9ydGVkQ2xhdXNl",
            "SAASRgoPaW5mZXJyZWRfY2xhdXNlGAIgASgLMisub3BlcmF0aW9uc19yZXNl",
            "YXJjaC5zYXQuTHJhdEluZmVycmVkQ2xhdXNlSAASRgoPZXhwb3J0ZWRfY2xh",
            "dXNlGAMgASgLMisub3BlcmF0aW9uc19yZXNlYXJjaC5zYXQuTHJhdEV4cG9y",
            "dGVkQ2xhdXNlSAASRgoPZGVsZXRlZF9jbGF1c2VzGAQgASgLMisub3BlcmF0",
            "aW9uc19yZXNlYXJjaC5zYXQuTHJhdERlbGV0ZWRDbGF1c2VzSABCBgoEc3Rl",
            "cA=="));
      descriptor = pbr::FileDescriptor.FromGeneratedCode(descriptorData,
          new pbr::FileDescriptor[] { },
          new pbr::GeneratedClrTypeInfo(null, null, new pbr::GeneratedClrTypeInfo[] {
            new pbr::GeneratedClrTypeInfo(typeof(global::OperationsResearch.Sat.LratImportedClause), global::OperationsResearch.Sat.LratImportedClause.Parser, new[]{ "ClauseId", "Literals" }, null, null, null, null),
            new pbr::GeneratedClrTypeInfo(typeof(global::OperationsResearch.Sat.LratInferredClause), global::OperationsResearch.Sat.LratInferredClause.Parser, new[]{ "ClauseId", "Literals", "UnitIds", "RatInfos", "Exported" }, null, null, null, new pbr::GeneratedClrTypeInfo[] { new pbr::GeneratedClrTypeInfo(typeof(global::OperationsResearch.Sat.LratInferredClause.Types.RatInfo), global::OperationsResearch.Sat.LratInferredClause.Types.RatInfo.Parser, new[]{ "ResolvantId", "UnitIds" }, null, null, null, null)}),
            new pbr::GeneratedClrTypeInfo(typeof(global::OperationsResearch.Sat.LratExportedClause), global::OperationsResearch.Sat.LratExportedClause.Parser, new[]{ "ClauseId", "Literals" }, null, null, null, null),
            new pbr::GeneratedClrTypeInfo(typeof(global::OperationsResearch.Sat.LratDeletedClauses), global::OperationsResearch.Sat.LratDeletedClauses.Parser, new[]{ "ClauseIds" }, null, null, null, null),
            new pbr::GeneratedClrTypeInfo(typeof(global::OperationsResearch.Sat.LratProofStep), global::OperationsResearch.Sat.LratProofStep.Parser, new[]{ "ImportedClause", "InferredClause", "ExportedClause", "DeletedClauses" }, new[]{ "Step" }, null, null, null)
          }));
    }
    #endregion
 
  }
  #region Messages
  [global::System.Diagnostics.DebuggerDisplayAttribute("{ToString(),nq}")]
  public sealed partial class LratImportedClause : pb::IMessage<LratImportedClause>
  #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      , pb::IBufferMessage
  #endif
  {
    private static readonly pb::MessageParser<LratImportedClause> _parser = new pb::MessageParser<LratImportedClause>(() => new LratImportedClause());
    private pb::UnknownFieldSet _unknownFields;
    private int _hasBits0;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pb::MessageParser<LratImportedClause> Parser { get { return _parser; } }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pbr::MessageDescriptor Descriptor {
      get { return global::OperationsResearch.Sat.LratReflection.Descriptor.MessageTypes[0]; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    pbr::MessageDescriptor pb::IMessage.Descriptor {
      get { return Descriptor; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratImportedClause() {
      OnConstruction();
    }
 
    partial void OnConstruction();
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratImportedClause(LratImportedClause other) : this() {
      _hasBits0 = other._hasBits0;
      clauseId_ = other.clauseId_;
      literals_ = other.literals_.Clone();
      _unknownFields = pb::UnknownFieldSet.Clone(other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratImportedClause Clone() {
      return new LratImportedClause(this);
    }

    public const int ClauseIdFieldNumber = 1;
    private readonly static long ClauseIdDefaultValue = 0L;
 
    private long clauseId_;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public long ClauseId {
      get { if ((_hasBits0 & 1) != 0) { return clauseId_; } else { return ClauseIdDefaultValue; } }
      set {
        _hasBits0 |= 1;
        clauseId_ = value;
      }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool HasClauseId {
      get { return (_hasBits0 & 1) != 0; }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void ClearClauseId() {
      _hasBits0 &= ~1;
    }

    public const int LiteralsFieldNumber = 2;
    private static readonly pb::FieldCodec<int> _repeated_literals_codec
        = pb::FieldCodec.ForInt32(18);
    private readonly pbc::RepeatedField<int> literals_ = new pbc::RepeatedField<int>();
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public pbc::RepeatedField<int> Literals {
      get { return literals_; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override bool Equals(object other) {
      return Equals(other as LratImportedClause);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool Equals(LratImportedClause other) {
      if (ReferenceEquals(other, null)) {
        return false;
      }
      if (ReferenceEquals(other, this)) {
        return true;
      }
      if (ClauseId != other.ClauseId) return false;
      if(!literals_.Equals(other.literals_)) return false;
      return Equals(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override int GetHashCode() {
      int hash = 1;
      if (HasClauseId) hash ^= ClauseId.GetHashCode();
      hash ^= literals_.GetHashCode();
      if (_unknownFields != null) {
        hash ^= _unknownFields.GetHashCode();
      }
      return hash;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override string ToString() {
      return pb::JsonFormatter.ToDiagnosticString(this);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void WriteTo(pb::CodedOutputStream output) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      output.WriteRawMessage(this);
    #else
      if (HasClauseId) {
        output.WriteRawTag(8);
        output.WriteInt64(ClauseId);
      }
      literals_.WriteTo(output, _repeated_literals_codec);
      if (_unknownFields != null) {
        _unknownFields.WriteTo(output);
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalWriteTo(ref pb::WriteContext output) {
      if (HasClauseId) {
        output.WriteRawTag(8);
        output.WriteInt64(ClauseId);
      }
      literals_.WriteTo(ref output, _repeated_literals_codec);
      if (_unknownFields != null) {
        _unknownFields.WriteTo(ref output);
      }
    }
    #endif
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public int CalculateSize() {
      int size = 0;
      if (HasClauseId) {
        size += 1 + pb::CodedOutputStream.ComputeInt64Size(ClauseId);
      }
      size += literals_.CalculateSize(_repeated_literals_codec);
      if (_unknownFields != null) {
        size += _unknownFields.CalculateSize();
      }
      return size;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(LratImportedClause other) {
      if (other == null) {
        return;
      }
      if (other.HasClauseId) {
        ClauseId = other.ClauseId;
      }
      literals_.Add(other.literals_);
      _unknownFields = pb::UnknownFieldSet.MergeFrom(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(pb::CodedInputStream input) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      input.ReadRawMessage(this);
    #else
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, input);
            break;
          case 8: {
            ClauseId = input.ReadInt64();
            break;
          }
          case 18:
          case 16: {
            literals_.AddEntriesFrom(input, _repeated_literals_codec);
            break;
          }
        }
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalMergeFrom(ref pb::ParseContext input) {
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, ref input);
            break;
          case 8: {
            ClauseId = input.ReadInt64();
            break;
          }
          case 18:
          case 16: {
            literals_.AddEntriesFrom(ref input, _repeated_literals_codec);
            break;
          }
        }
      }
    }
    #endif
 
  }

  [global::System.Diagnostics.DebuggerDisplayAttribute("{ToString(),nq}")]
  public sealed partial class LratInferredClause : pb::IMessage<LratInferredClause>
  #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      , pb::IBufferMessage
  #endif
  {
    private static readonly pb::MessageParser<LratInferredClause> _parser = new pb::MessageParser<LratInferredClause>(() => new LratInferredClause());
    private pb::UnknownFieldSet _unknownFields;
    private int _hasBits0;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pb::MessageParser<LratInferredClause> Parser { get { return _parser; } }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pbr::MessageDescriptor Descriptor {
      get { return global::OperationsResearch.Sat.LratReflection.Descriptor.MessageTypes[1]; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    pbr::MessageDescriptor pb::IMessage.Descriptor {
      get { return Descriptor; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratInferredClause() {
      OnConstruction();
    }
 
    partial void OnConstruction();
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratInferredClause(LratInferredClause other) : this() {
      _hasBits0 = other._hasBits0;
      clauseId_ = other.clauseId_;
      literals_ = other.literals_.Clone();
      unitIds_ = other.unitIds_.Clone();
      ratInfos_ = other.ratInfos_.Clone();
      exported_ = other.exported_;
      _unknownFields = pb::UnknownFieldSet.Clone(other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratInferredClause Clone() {
      return new LratInferredClause(this);
    }

    public const int ClauseIdFieldNumber = 1;
    private readonly static long ClauseIdDefaultValue = 0L;
 
    private long clauseId_;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public long ClauseId {
      get { if ((_hasBits0 & 1) != 0) { return clauseId_; } else { return ClauseIdDefaultValue; } }
      set {
        _hasBits0 |= 1;
        clauseId_ = value;
      }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool HasClauseId {
      get { return (_hasBits0 & 1) != 0; }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void ClearClauseId() {
      _hasBits0 &= ~1;
    }

    public const int LiteralsFieldNumber = 2;
    private static readonly pb::FieldCodec<int> _repeated_literals_codec
        = pb::FieldCodec.ForInt32(18);
    private readonly pbc::RepeatedField<int> literals_ = new pbc::RepeatedField<int>();
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public pbc::RepeatedField<int> Literals {
      get { return literals_; }
    }

    public const int UnitIdsFieldNumber = 3;
    private static readonly pb::FieldCodec<long> _repeated_unitIds_codec
        = pb::FieldCodec.ForInt64(26);
    private readonly pbc::RepeatedField<long> unitIds_ = new pbc::RepeatedField<long>();
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public pbc::RepeatedField<long> UnitIds {
      get { return unitIds_; }
    }

    public const int RatInfosFieldNumber = 4;
    private static readonly pb::FieldCodec<global::OperationsResearch.Sat.LratInferredClause.Types.RatInfo> _repeated_ratInfos_codec
        = pb::FieldCodec.ForMessage(34, global::OperationsResearch.Sat.LratInferredClause.Types.RatInfo.Parser);
    private readonly pbc::RepeatedField<global::OperationsResearch.Sat.LratInferredClause.Types.RatInfo> ratInfos_ = new pbc::RepeatedField<global::OperationsResearch.Sat.LratInferredClause.Types.RatInfo>();
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public pbc::RepeatedField<global::OperationsResearch.Sat.LratInferredClause.Types.RatInfo> RatInfos {
      get { return ratInfos_; }
    }

    public const int ExportedFieldNumber = 5;
    private readonly static bool ExportedDefaultValue = false;
 
    private bool exported_;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool Exported {
      get { if ((_hasBits0 & 2) != 0) { return exported_; } else { return ExportedDefaultValue; } }
      set {
        _hasBits0 |= 2;
        exported_ = value;
      }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool HasExported {
      get { return (_hasBits0 & 2) != 0; }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void ClearExported() {
      _hasBits0 &= ~2;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override bool Equals(object other) {
      return Equals(other as LratInferredClause);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool Equals(LratInferredClause other) {
      if (ReferenceEquals(other, null)) {
        return false;
      }
      if (ReferenceEquals(other, this)) {
        return true;
      }
      if (ClauseId != other.ClauseId) return false;
      if(!literals_.Equals(other.literals_)) return false;
      if(!unitIds_.Equals(other.unitIds_)) return false;
      if(!ratInfos_.Equals(other.ratInfos_)) return false;
      if (Exported != other.Exported) return false;
      return Equals(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override int GetHashCode() {
      int hash = 1;
      if (HasClauseId) hash ^= ClauseId.GetHashCode();
      hash ^= literals_.GetHashCode();
      hash ^= unitIds_.GetHashCode();
      hash ^= ratInfos_.GetHashCode();
      if (HasExported) hash ^= Exported.GetHashCode();
      if (_unknownFields != null) {
        hash ^= _unknownFields.GetHashCode();
      }
      return hash;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override string ToString() {
      return pb::JsonFormatter.ToDiagnosticString(this);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void WriteTo(pb::CodedOutputStream output) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      output.WriteRawMessage(this);
    #else
      if (HasClauseId) {
        output.WriteRawTag(8);
        output.WriteInt64(ClauseId);
      }
      literals_.WriteTo(output, _repeated_literals_codec);
      unitIds_.WriteTo(output, _repeated_unitIds_codec);
      ratInfos_.WriteTo(output, _repeated_ratInfos_codec);
      if (HasExported) {
        output.WriteRawTag(40);
        output.WriteBool(Exported);
      }
      if (_unknownFields != null) {
        _unknownFields.WriteTo(output);
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalWriteTo(ref pb::WriteContext output) {
      if (HasClauseId) {
        output.WriteRawTag(8);
        output.WriteInt64(ClauseId);
      }
      literals_.WriteTo(ref output, _repeated_literals_codec);
      unitIds_.WriteTo(ref output, _repeated_unitIds_codec);
      ratInfos_.WriteTo(ref output, _repeated_ratInfos_codec);
      if (HasExported) {
        output.WriteRawTag(40);
        output.WriteBool(Exported);
      }
      if (_unknownFields != null) {
        _unknownFields.WriteTo(ref output);
      }
    }
    #endif
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public int CalculateSize() {
      int size = 0;
      if (HasClauseId) {
        size += 1 + pb::CodedOutputStream.ComputeInt64Size(ClauseId);
      }
      size += literals_.CalculateSize(_repeated_literals_codec);
      size += unitIds_.CalculateSize(_repeated_unitIds_codec);
      size += ratInfos_.CalculateSize(_repeated_ratInfos_codec);
      if (HasExported) {
        size += 1 + 1;
      }
      if (_unknownFields != null) {
        size += _unknownFields.CalculateSize();
      }
      return size;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(LratInferredClause other) {
      if (other == null) {
        return;
      }
      if (other.HasClauseId) {
        ClauseId = other.ClauseId;
      }
      literals_.Add(other.literals_);
      unitIds_.Add(other.unitIds_);
      ratInfos_.Add(other.ratInfos_);
      if (other.HasExported) {
        Exported = other.Exported;
      }
      _unknownFields = pb::UnknownFieldSet.MergeFrom(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(pb::CodedInputStream input) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      input.ReadRawMessage(this);
    #else
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, input);
            break;
          case 8: {
            ClauseId = input.ReadInt64();
            break;
          }
          case 18:
          case 16: {
            literals_.AddEntriesFrom(input, _repeated_literals_codec);
            break;
          }
          case 26:
          case 24: {
            unitIds_.AddEntriesFrom(input, _repeated_unitIds_codec);
            break;
          }
          case 34: {
            ratInfos_.AddEntriesFrom(input, _repeated_ratInfos_codec);
            break;
          }
          case 40: {
            Exported = input.ReadBool();
            break;
          }
        }
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalMergeFrom(ref pb::ParseContext input) {
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, ref input);
            break;
          case 8: {
            ClauseId = input.ReadInt64();
            break;
          }
          case 18:
          case 16: {
            literals_.AddEntriesFrom(ref input, _repeated_literals_codec);
            break;
          }
          case 26:
          case 24: {
            unitIds_.AddEntriesFrom(ref input, _repeated_unitIds_codec);
            break;
          }
          case 34: {
            ratInfos_.AddEntriesFrom(ref input, _repeated_ratInfos_codec);
            break;
          }
          case 40: {
            Exported = input.ReadBool();
            break;
          }
        }
      }
    }
    #endif
 
    #region Nested types
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static partial class Types {
      [global::System.Diagnostics.DebuggerDisplayAttribute("{ToString(),nq}")]
      public sealed partial class RatInfo : pb::IMessage<RatInfo>
      #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
          , pb::IBufferMessage
      #endif
      {
        private static readonly pb::MessageParser<RatInfo> _parser = new pb::MessageParser<RatInfo>(() => new RatInfo());
        private pb::UnknownFieldSet _unknownFields;
        private int _hasBits0;
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public static pb::MessageParser<RatInfo> Parser { get { return _parser; } }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public static pbr::MessageDescriptor Descriptor {
          get { return global::OperationsResearch.Sat.LratInferredClause.Descriptor.NestedTypes[0]; }
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        pbr::MessageDescriptor pb::IMessage.Descriptor {
          get { return Descriptor; }
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public RatInfo() {
          OnConstruction();
        }
 
        partial void OnConstruction();
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public RatInfo(RatInfo other) : this() {
          _hasBits0 = other._hasBits0;
          resolvantId_ = other.resolvantId_;
          unitIds_ = other.unitIds_.Clone();
          _unknownFields = pb::UnknownFieldSet.Clone(other._unknownFields);
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public RatInfo Clone() {
          return new RatInfo(this);
        }

        public const int ResolvantIdFieldNumber = 1;
        private readonly static long ResolvantIdDefaultValue = 0L;
 
        private long resolvantId_;
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public long ResolvantId {
          get { if ((_hasBits0 & 1) != 0) { return resolvantId_; } else { return ResolvantIdDefaultValue; } }
          set {
            _hasBits0 |= 1;
            resolvantId_ = value;
          }
        }

        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public bool HasResolvantId {
          get { return (_hasBits0 & 1) != 0; }
        }

        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public void ClearResolvantId() {
          _hasBits0 &= ~1;
        }

        public const int UnitIdsFieldNumber = 2;
        private static readonly pb::FieldCodec<long> _repeated_unitIds_codec
            = pb::FieldCodec.ForInt64(18);
        private readonly pbc::RepeatedField<long> unitIds_ = new pbc::RepeatedField<long>();
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public pbc::RepeatedField<long> UnitIds {
          get { return unitIds_; }
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public override bool Equals(object other) {
          return Equals(other as RatInfo);
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public bool Equals(RatInfo other) {
          if (ReferenceEquals(other, null)) {
            return false;
          }
          if (ReferenceEquals(other, this)) {
            return true;
          }
          if (ResolvantId != other.ResolvantId) return false;
          if(!unitIds_.Equals(other.unitIds_)) return false;
          return Equals(_unknownFields, other._unknownFields);
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public override int GetHashCode() {
          int hash = 1;
          if (HasResolvantId) hash ^= ResolvantId.GetHashCode();
          hash ^= unitIds_.GetHashCode();
          if (_unknownFields != null) {
            hash ^= _unknownFields.GetHashCode();
          }
          return hash;
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public override string ToString() {
          return pb::JsonFormatter.ToDiagnosticString(this);
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public void WriteTo(pb::CodedOutputStream output) {
        #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
          output.WriteRawMessage(this);
        #else
          if (HasResolvantId) {
            output.WriteRawTag(8);
            output.WriteInt64(ResolvantId);
          }
          unitIds_.WriteTo(output, _repeated_unitIds_codec);
          if (_unknownFields != null) {
            _unknownFields.WriteTo(output);
          }
        #endif
        }
 
        #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        void pb::IBufferMessage.InternalWriteTo(ref pb::WriteContext output) {
          if (HasResolvantId) {
            output.WriteRawTag(8);
            output.WriteInt64(ResolvantId);
          }
          unitIds_.WriteTo(ref output, _repeated_unitIds_codec);
          if (_unknownFields != null) {
            _unknownFields.WriteTo(ref output);
          }
        }
        #endif
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public int CalculateSize() {
          int size = 0;
          if (HasResolvantId) {
            size += 1 + pb::CodedOutputStream.ComputeInt64Size(ResolvantId);
          }
          size += unitIds_.CalculateSize(_repeated_unitIds_codec);
          if (_unknownFields != null) {
            size += _unknownFields.CalculateSize();
          }
          return size;
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public void MergeFrom(RatInfo other) {
          if (other == null) {
            return;
          }
          if (other.HasResolvantId) {
            ResolvantId = other.ResolvantId;
          }
          unitIds_.Add(other.unitIds_);
          _unknownFields = pb::UnknownFieldSet.MergeFrom(_unknownFields, other._unknownFields);
        }
 
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        public void MergeFrom(pb::CodedInputStream input) {
        #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
          input.ReadRawMessage(this);
        #else
          uint tag;
          while ((tag = input.ReadTag()) != 0) {
          if ((tag & 7) == 4) {
            // Abort on any end group tag.
            return;
          }
          switch(tag) {
              default:
                _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, input);
                break;
              case 8: {
                ResolvantId = input.ReadInt64();
                break;
              }
              case 18:
              case 16: {
                unitIds_.AddEntriesFrom(input, _repeated_unitIds_codec);
                break;
              }
            }
          }
        #endif
        }
 
        #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
        [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
        [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
        void pb::IBufferMessage.InternalMergeFrom(ref pb::ParseContext input) {
          uint tag;
          while ((tag = input.ReadTag()) != 0) {
          if ((tag & 7) == 4) {
            // Abort on any end group tag.
            return;
          }
          switch(tag) {
              default:
                _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, ref input);
                break;
              case 8: {
                ResolvantId = input.ReadInt64();
                break;
              }
              case 18:
              case 16: {
                unitIds_.AddEntriesFrom(ref input, _repeated_unitIds_codec);
                break;
              }
            }
          }
        }
        #endif
 
      }
 
    }
    #endregion
 
  }

  [global::System.Diagnostics.DebuggerDisplayAttribute("{ToString(),nq}")]
  public sealed partial class LratExportedClause : pb::IMessage<LratExportedClause>
  #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      , pb::IBufferMessage
  #endif
  {
    private static readonly pb::MessageParser<LratExportedClause> _parser = new pb::MessageParser<LratExportedClause>(() => new LratExportedClause());
    private pb::UnknownFieldSet _unknownFields;
    private int _hasBits0;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pb::MessageParser<LratExportedClause> Parser { get { return _parser; } }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pbr::MessageDescriptor Descriptor {
      get { return global::OperationsResearch.Sat.LratReflection.Descriptor.MessageTypes[2]; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    pbr::MessageDescriptor pb::IMessage.Descriptor {
      get { return Descriptor; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratExportedClause() {
      OnConstruction();
    }
 
    partial void OnConstruction();
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratExportedClause(LratExportedClause other) : this() {
      _hasBits0 = other._hasBits0;
      clauseId_ = other.clauseId_;
      literals_ = other.literals_.Clone();
      _unknownFields = pb::UnknownFieldSet.Clone(other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratExportedClause Clone() {
      return new LratExportedClause(this);
    }

    public const int ClauseIdFieldNumber = 1;
    private readonly static long ClauseIdDefaultValue = 0L;
 
    private long clauseId_;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public long ClauseId {
      get { if ((_hasBits0 & 1) != 0) { return clauseId_; } else { return ClauseIdDefaultValue; } }
      set {
        _hasBits0 |= 1;
        clauseId_ = value;
      }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool HasClauseId {
      get { return (_hasBits0 & 1) != 0; }
    }

    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void ClearClauseId() {
      _hasBits0 &= ~1;
    }

    public const int LiteralsFieldNumber = 2;
    private static readonly pb::FieldCodec<int> _repeated_literals_codec
        = pb::FieldCodec.ForInt32(18);
    private readonly pbc::RepeatedField<int> literals_ = new pbc::RepeatedField<int>();
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public pbc::RepeatedField<int> Literals {
      get { return literals_; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override bool Equals(object other) {
      return Equals(other as LratExportedClause);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool Equals(LratExportedClause other) {
      if (ReferenceEquals(other, null)) {
        return false;
      }
      if (ReferenceEquals(other, this)) {
        return true;
      }
      if (ClauseId != other.ClauseId) return false;
      if(!literals_.Equals(other.literals_)) return false;
      return Equals(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override int GetHashCode() {
      int hash = 1;
      if (HasClauseId) hash ^= ClauseId.GetHashCode();
      hash ^= literals_.GetHashCode();
      if (_unknownFields != null) {
        hash ^= _unknownFields.GetHashCode();
      }
      return hash;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override string ToString() {
      return pb::JsonFormatter.ToDiagnosticString(this);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void WriteTo(pb::CodedOutputStream output) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      output.WriteRawMessage(this);
    #else
      if (HasClauseId) {
        output.WriteRawTag(8);
        output.WriteInt64(ClauseId);
      }
      literals_.WriteTo(output, _repeated_literals_codec);
      if (_unknownFields != null) {
        _unknownFields.WriteTo(output);
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalWriteTo(ref pb::WriteContext output) {
      if (HasClauseId) {
        output.WriteRawTag(8);
        output.WriteInt64(ClauseId);
      }
      literals_.WriteTo(ref output, _repeated_literals_codec);
      if (_unknownFields != null) {
        _unknownFields.WriteTo(ref output);
      }
    }
    #endif
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public int CalculateSize() {
      int size = 0;
      if (HasClauseId) {
        size += 1 + pb::CodedOutputStream.ComputeInt64Size(ClauseId);
      }
      size += literals_.CalculateSize(_repeated_literals_codec);
      if (_unknownFields != null) {
        size += _unknownFields.CalculateSize();
      }
      return size;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(LratExportedClause other) {
      if (other == null) {
        return;
      }
      if (other.HasClauseId) {
        ClauseId = other.ClauseId;
      }
      literals_.Add(other.literals_);
      _unknownFields = pb::UnknownFieldSet.MergeFrom(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(pb::CodedInputStream input) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      input.ReadRawMessage(this);
    #else
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, input);
            break;
          case 8: {
            ClauseId = input.ReadInt64();
            break;
          }
          case 18:
          case 16: {
            literals_.AddEntriesFrom(input, _repeated_literals_codec);
            break;
          }
        }
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalMergeFrom(ref pb::ParseContext input) {
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, ref input);
            break;
          case 8: {
            ClauseId = input.ReadInt64();
            break;
          }
          case 18:
          case 16: {
            literals_.AddEntriesFrom(ref input, _repeated_literals_codec);
            break;
          }
        }
      }
    }
    #endif
 
  }

  [global::System.Diagnostics.DebuggerDisplayAttribute("{ToString(),nq}")]
  public sealed partial class LratDeletedClauses : pb::IMessage<LratDeletedClauses>
  #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      , pb::IBufferMessage
  #endif
  {
    private static readonly pb::MessageParser<LratDeletedClauses> _parser = new pb::MessageParser<LratDeletedClauses>(() => new LratDeletedClauses());
    private pb::UnknownFieldSet _unknownFields;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pb::MessageParser<LratDeletedClauses> Parser { get { return _parser; } }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pbr::MessageDescriptor Descriptor {
      get { return global::OperationsResearch.Sat.LratReflection.Descriptor.MessageTypes[3]; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    pbr::MessageDescriptor pb::IMessage.Descriptor {
      get { return Descriptor; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratDeletedClauses() {
      OnConstruction();
    }
 
    partial void OnConstruction();
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratDeletedClauses(LratDeletedClauses other) : this() {
      clauseIds_ = other.clauseIds_.Clone();
      _unknownFields = pb::UnknownFieldSet.Clone(other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratDeletedClauses Clone() {
      return new LratDeletedClauses(this);
    }

    public const int ClauseIdsFieldNumber = 1;
    private static readonly pb::FieldCodec<long> _repeated_clauseIds_codec
        = pb::FieldCodec.ForInt64(10);
    private readonly pbc::RepeatedField<long> clauseIds_ = new pbc::RepeatedField<long>();
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public pbc::RepeatedField<long> ClauseIds {
      get { return clauseIds_; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override bool Equals(object other) {
      return Equals(other as LratDeletedClauses);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool Equals(LratDeletedClauses other) {
      if (ReferenceEquals(other, null)) {
        return false;
      }
      if (ReferenceEquals(other, this)) {
        return true;
      }
      if(!clauseIds_.Equals(other.clauseIds_)) return false;
      return Equals(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override int GetHashCode() {
      int hash = 1;
      hash ^= clauseIds_.GetHashCode();
      if (_unknownFields != null) {
        hash ^= _unknownFields.GetHashCode();
      }
      return hash;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override string ToString() {
      return pb::JsonFormatter.ToDiagnosticString(this);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void WriteTo(pb::CodedOutputStream output) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      output.WriteRawMessage(this);
    #else
      clauseIds_.WriteTo(output, _repeated_clauseIds_codec);
      if (_unknownFields != null) {
        _unknownFields.WriteTo(output);
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalWriteTo(ref pb::WriteContext output) {
      clauseIds_.WriteTo(ref output, _repeated_clauseIds_codec);
      if (_unknownFields != null) {
        _unknownFields.WriteTo(ref output);
      }
    }
    #endif
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public int CalculateSize() {
      int size = 0;
      size += clauseIds_.CalculateSize(_repeated_clauseIds_codec);
      if (_unknownFields != null) {
        size += _unknownFields.CalculateSize();
      }
      return size;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(LratDeletedClauses other) {
      if (other == null) {
        return;
      }
      clauseIds_.Add(other.clauseIds_);
      _unknownFields = pb::UnknownFieldSet.MergeFrom(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(pb::CodedInputStream input) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      input.ReadRawMessage(this);
    #else
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, input);
            break;
          case 10:
          case 8: {
            clauseIds_.AddEntriesFrom(input, _repeated_clauseIds_codec);
            break;
          }
        }
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalMergeFrom(ref pb::ParseContext input) {
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, ref input);
            break;
          case 10:
          case 8: {
            clauseIds_.AddEntriesFrom(ref input, _repeated_clauseIds_codec);
            break;
          }
        }
      }
    }
    #endif
 
  }

  [global::System.Diagnostics.DebuggerDisplayAttribute("{ToString(),nq}")]
  public sealed partial class LratProofStep : pb::IMessage<LratProofStep>
  #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      , pb::IBufferMessage
  #endif
  {
    private static readonly pb::MessageParser<LratProofStep> _parser = new pb::MessageParser<LratProofStep>(() => new LratProofStep());
    private pb::UnknownFieldSet _unknownFields;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pb::MessageParser<LratProofStep> Parser { get { return _parser; } }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public static pbr::MessageDescriptor Descriptor {
      get { return global::OperationsResearch.Sat.LratReflection.Descriptor.MessageTypes[4]; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    pbr::MessageDescriptor pb::IMessage.Descriptor {
      get { return Descriptor; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratProofStep() {
      OnConstruction();
    }
 
    partial void OnConstruction();
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratProofStep(LratProofStep other) : this() {
      switch (other.StepCase) {
        case StepOneofCase.ImportedClause:
          ImportedClause = other.ImportedClause.Clone();
          break;
        case StepOneofCase.InferredClause:
          InferredClause = other.InferredClause.Clone();
          break;
        case StepOneofCase.ExportedClause:
          ExportedClause = other.ExportedClause.Clone();
          break;
        case StepOneofCase.DeletedClauses:
          DeletedClauses = other.DeletedClauses.Clone();
          break;
      }
 
      _unknownFields = pb::UnknownFieldSet.Clone(other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public LratProofStep Clone() {
      return new LratProofStep(this);
    }

    public const int ImportedClauseFieldNumber = 1;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public global::OperationsResearch.Sat.LratImportedClause ImportedClause {
      get { return stepCase_ == StepOneofCase.ImportedClause ? (global::OperationsResearch.Sat.LratImportedClause) step_ : null; }
      set {
        step_ = value;
        stepCase_ = value == null ? StepOneofCase.None : StepOneofCase.ImportedClause;
      }
    }

    public const int InferredClauseFieldNumber = 2;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public global::OperationsResearch.Sat.LratInferredClause InferredClause {
      get { return stepCase_ == StepOneofCase.InferredClause ? (global::OperationsResearch.Sat.LratInferredClause) step_ : null; }
      set {
        step_ = value;
        stepCase_ = value == null ? StepOneofCase.None : StepOneofCase.InferredClause;
      }
    }

    public const int ExportedClauseFieldNumber = 3;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public global::OperationsResearch.Sat.LratExportedClause ExportedClause {
      get { return stepCase_ == StepOneofCase.ExportedClause ? (global::OperationsResearch.Sat.LratExportedClause) step_ : null; }
      set {
        step_ = value;
        stepCase_ = value == null ? StepOneofCase.None : StepOneofCase.ExportedClause;
      }
    }

    public const int DeletedClausesFieldNumber = 4;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public global::OperationsResearch.Sat.LratDeletedClauses DeletedClauses {
      get { return stepCase_ == StepOneofCase.DeletedClauses ? (global::OperationsResearch.Sat.LratDeletedClauses) step_ : null; }
      set {
        step_ = value;
        stepCase_ = value == null ? StepOneofCase.None : StepOneofCase.DeletedClauses;
      }
    }
 
    private object step_;
    public enum StepOneofCase {
      None = 0,
      ImportedClause = 1,
      InferredClause = 2,
      ExportedClause = 3,
      DeletedClauses = 4,
    }
    private StepOneofCase stepCase_ = StepOneofCase.None;
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public StepOneofCase StepCase {
      get { return stepCase_; }
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void ClearStep() {
      stepCase_ = StepOneofCase.None;
      step_ = null;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override bool Equals(object other) {
      return Equals(other as LratProofStep);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public bool Equals(LratProofStep other) {
      if (ReferenceEquals(other, null)) {
        return false;
      }
      if (ReferenceEquals(other, this)) {
        return true;
      }
      if (!object.Equals(ImportedClause, other.ImportedClause)) return false;
      if (!object.Equals(InferredClause, other.InferredClause)) return false;
      if (!object.Equals(ExportedClause, other.ExportedClause)) return false;
      if (!object.Equals(DeletedClauses, other.DeletedClauses)) return false;
      if (StepCase != other.StepCase) return false;
      return Equals(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override int GetHashCode() {
      int hash = 1;
      if (stepCase_ == StepOneofCase.ImportedClause) hash ^= ImportedClause.GetHashCode();
      if (stepCase_ == StepOneofCase.InferredClause) hash ^= InferredClause.GetHashCode();
      if (stepCase_ == StepOneofCase.ExportedClause) hash ^= ExportedClause.GetHashCode();
      if (stepCase_ == StepOneofCase.DeletedClauses) hash ^= DeletedClauses.GetHashCode();
      hash ^= (int) stepCase_;
      if (_unknownFields != null) {
        hash ^= _unknownFields.GetHashCode();
      }
      return hash;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public override string ToString() {
      return pb::JsonFormatter.ToDiagnosticString(this);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void WriteTo(pb::CodedOutputStream output) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      output.WriteRawMessage(this);
    #else
      if (stepCase_ == StepOneofCase.ImportedClause) {
        output.WriteRawTag(10);
        output.WriteMessage(ImportedClause);
      }
      if (stepCase_ == StepOneofCase.InferredClause) {
        output.WriteRawTag(18);
        output.WriteMessage(InferredClause);
      }
      if (stepCase_ == StepOneofCase.ExportedClause) {
        output.WriteRawTag(26);
        output.WriteMessage(ExportedClause);
      }
      if (stepCase_ == StepOneofCase.DeletedClauses) {
        output.WriteRawTag(34);
        output.WriteMessage(DeletedClauses);
      }
      if (_unknownFields != null) {
        _unknownFields.WriteTo(output);
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalWriteTo(ref pb::WriteContext output) {
      if (stepCase_ == StepOneofCase.ImportedClause) {
        output.WriteRawTag(10);
        output.WriteMessage(ImportedClause);
      }
      if (stepCase_ == StepOneofCase.InferredClause) {
        output.WriteRawTag(18);
        output.WriteMessage(InferredClause);
      }
      if (stepCase_ == StepOneofCase.ExportedClause) {
        output.WriteRawTag(26);
        output.WriteMessage(ExportedClause);
      }
      if (stepCase_ == StepOneofCase.DeletedClauses) {
        output.WriteRawTag(34);
        output.WriteMessage(DeletedClauses);
      }
      if (_unknownFields != null) {
        _unknownFields.WriteTo(ref output);
      }
    }
    #endif
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public int CalculateSize() {
      int size = 0;
      if (stepCase_ == StepOneofCase.ImportedClause) {
        size += 1 + pb::CodedOutputStream.ComputeMessageSize(ImportedClause);
      }
      if (stepCase_ == StepOneofCase.InferredClause) {
        size += 1 + pb::CodedOutputStream.ComputeMessageSize(InferredClause);
      }
      if (stepCase_ == StepOneofCase.ExportedClause) {
        size += 1 + pb::CodedOutputStream.ComputeMessageSize(ExportedClause);
      }
      if (stepCase_ == StepOneofCase.DeletedClauses) {
        size += 1 + pb::CodedOutputStream.ComputeMessageSize(DeletedClauses);
      }
      if (_unknownFields != null) {
        size += _unknownFields.CalculateSize();
      }
      return size;
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(LratProofStep other) {
      if (other == null) {
        return;
      }
      switch (other.StepCase) {
        case StepOneofCase.ImportedClause:
          if (ImportedClause == null) {
            ImportedClause = new global::OperationsResearch.Sat.LratImportedClause();
          }
          ImportedClause.MergeFrom(other.ImportedClause);
          break;
        case StepOneofCase.InferredClause:
          if (InferredClause == null) {
            InferredClause = new global::OperationsResearch.Sat.LratInferredClause();
          }
          InferredClause.MergeFrom(other.InferredClause);
          break;
        case StepOneofCase.ExportedClause:
          if (ExportedClause == null) {
            ExportedClause = new global::OperationsResearch.Sat.LratExportedClause();
          }
          ExportedClause.MergeFrom(other.ExportedClause);
          break;
        case StepOneofCase.DeletedClauses:
          if (DeletedClauses == null) {
            DeletedClauses = new global::OperationsResearch.Sat.LratDeletedClauses();
          }
          DeletedClauses.MergeFrom(other.DeletedClauses);
          break;
      }
 
      _unknownFields = pb::UnknownFieldSet.MergeFrom(_unknownFields, other._unknownFields);
    }
 
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    public void MergeFrom(pb::CodedInputStream input) {
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
      input.ReadRawMessage(this);
    #else
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, input);
            break;
          case 10: {
            global::OperationsResearch.Sat.LratImportedClause subBuilder = new global::OperationsResearch.Sat.LratImportedClause();
            if (stepCase_ == StepOneofCase.ImportedClause) {
              subBuilder.MergeFrom(ImportedClause);
            }
            input.ReadMessage(subBuilder);
            ImportedClause = subBuilder;
            break;
          }
          case 18: {
            global::OperationsResearch.Sat.LratInferredClause subBuilder = new global::OperationsResearch.Sat.LratInferredClause();
            if (stepCase_ == StepOneofCase.InferredClause) {
              subBuilder.MergeFrom(InferredClause);
            }
            input.ReadMessage(subBuilder);
            InferredClause = subBuilder;
            break;
          }
          case 26: {
            global::OperationsResearch.Sat.LratExportedClause subBuilder = new global::OperationsResearch.Sat.LratExportedClause();
            if (stepCase_ == StepOneofCase.ExportedClause) {
              subBuilder.MergeFrom(ExportedClause);
            }
            input.ReadMessage(subBuilder);
            ExportedClause = subBuilder;
            break;
          }
          case 34: {
            global::OperationsResearch.Sat.LratDeletedClauses subBuilder = new global::OperationsResearch.Sat.LratDeletedClauses();
            if (stepCase_ == StepOneofCase.DeletedClauses) {
              subBuilder.MergeFrom(DeletedClauses);
            }
            input.ReadMessage(subBuilder);
            DeletedClauses = subBuilder;
            break;
          }
        }
      }
    #endif
    }
 
    #if !GOOGLE_PROTOBUF_REFSTRUCT_COMPATIBILITY_MODE
    [global::System.Diagnostics.DebuggerNonUserCodeAttribute]
    [global::System.CodeDom.Compiler.GeneratedCode("protoc", null)]
    void pb::IBufferMessage.InternalMergeFrom(ref pb::ParseContext input) {
      uint tag;
      while ((tag = input.ReadTag()) != 0) {
      if ((tag & 7) == 4) {
        // Abort on any end group tag.
        return;
      }
      switch(tag) {
          default:
            _unknownFields = pb::UnknownFieldSet.MergeFieldFrom(_unknownFields, ref input);
            break;
          case 10: {
            global::OperationsResearch.Sat.LratImportedClause subBuilder = new global::OperationsResearch.Sat.LratImportedClause();
            if (stepCase_ == StepOneofCase.ImportedClause) {
              subBuilder.MergeFrom(ImportedClause);
            }
            input.ReadMessage(subBuilder);
            ImportedClause = subBuilder;
            break;
          }
          case 18: {
            global::OperationsResearch.Sat.LratInferredClause subBuilder = new global::OperationsResearch.Sat.LratInferredClause();
            if (stepCase_ == StepOneofCase.InferredClause) {
              subBuilder.MergeFrom(InferredClause);
            }
            input.ReadMessage(subBuilder);
            InferredClause = subBuilder;
            break;
          }
          case 26: {
            global::OperationsResearch.Sat.LratExportedClause subBuilder = new global::OperationsResearch.Sat.LratExportedClause();
            if (stepCase_ == StepOneofCase.ExportedClause) {
              subBuilder.MergeFrom(ExportedClause);
            }
            input.ReadMessage(subBuilder);
            ExportedClause = subBuilder;
            break;
          }
          case 34: {
            global::OperationsResearch.Sat.LratDeletedClauses subBuilder = new global::OperationsResearch.Sat.LratDeletedClauses();
            if (stepCase_ == StepOneofCase.DeletedClauses) {
              subBuilder.MergeFrom(DeletedClauses);
            }
            input.ReadMessage(subBuilder);
            DeletedClauses = subBuilder;
            break;
          }
        }
      }
    }
    #endif
 
  }
 
  #endregion
 
}
 
#endregion Designer generated code