structure.proto

package pomagma.atlas.protobuf;

//----------------------------------------------------------------------------
// raw data

message ObMap {
  // Either key,val are both set, or key_diff_minus_one,val_diff are both set.
  repeated uint32 key = 1 [packed=true];
  repeated uint32 val = 2 [packed=true];
  repeated uint32 key_diff_minus_one = 3 [packed=true];
  repeated int32 val_diff = 4 [packed=true];
}

message ObSet {
  required bytes dense = 1;
}

//----------------------------------------------------------------------------
// algebraic structure

message Carrier {
  optional string name = 1;
  optional bytes hash = 2;
  optional uint32 item_count = 3;
}

message NullaryFunction {
  optional string name = 1;
  optional bytes hash = 2;
  optional uint32 val = 3;

  repeated bytes blobs = 15;
}

message UnaryFunction {
  optional string name = 1;
  optional bytes hash = 2;
  optional ObMap map = 3;

  repeated bytes blobs = 15;
}

message BinaryFunction {
  message Row {
    required uint32 lhs = 1;
    required ObMap rhs_val = 2;
  }

  optional string name = 1;
  optional bytes hash = 2;
  repeated Row rows = 3;

  repeated bytes blobs = 15;
}

message UnaryRelation {
  optional string name = 1;
  optional bytes hash = 2;
  optional ObSet set = 3;

  repeated bytes blobs = 15;
}

message BinaryRelation {
  message Row {
    required uint32 lhs = 1;
    required ObSet rhs = 2;
  }

  optional string name = 1;
  optional bytes hash = 2;
  repeated Row rows = 3;

  repeated bytes blobs = 15;
}

message Structure {
  optional string name = 1;
  optional bytes hash = 2;

  optional Carrier carrier = 3;

  repeated NullaryFunction nullary_functions = 4;
  // reserved 5;  // For unary_functions.
  repeated UnaryFunction injective_functions = 6;
  repeated BinaryFunction binary_functions = 7;
  repeated BinaryFunction symmetric_functions = 8;
  repeated UnaryRelation unary_relations = 9;
  repeated BinaryRelation binary_relations = 10;
}

//----------------------------------------------------------------------------
// chart

// Charts are small so that many can fit in an Atlas.
message Chart {
  // Presentation blobs refer to pomagma.compiler.protobuf.Presentation protos.
  // The min_presentation contains only those terms which are present in the
  // structure, and a theory wrt which the structure has been saturated.
  // The max_presentation.signature contains at least all terms that are
  // present, and max_presentation.theory contains at least all facts that have
  // ever been applied, or a theory entailing such.
  // Lemma: min_presentation.signature is a subset of
  //   max_presentation.signature.
  // Lemma: min_presentation.theory is entailed by max_presentation.theory.
  required bytes min_presentation_blob = 1;
  required bytes max_presentation_blob = 2;
  required bytes structure_blob = 3;
  repeated bytes subsumed_structure_blobs = 4;
}

//----------------------------------------------------------------------------
// atlas

message Atlas {
  // This represents a map from the .max_presentation_blob field to Charts;
  // elements should be sorted.
  repeated Chart charts = 1;
}