Interface Lrat.LratInferredClauseOrBuilder

All Superinterfaces:
com.google.protobuf.MessageLiteOrBuilder, com.google.protobuf.MessageOrBuilder
All Known Implementing Classes:
Lrat.LratInferredClause, Lrat.LratInferredClause.Builder
Enclosing class:
Lrat
public static interface Lrat.LratInferredClauseOrBuilder extends com.google.protobuf.MessageOrBuilder

  • Method Summary

    Modifier and Type
    Method
    Description
    long
    getClauseId()
    optional int64 clause_id = 1;
    boolean
    getExported()
    Whether the clause must be exported, so that other workers can import it (a clause cannot be imported if it is not previously exported).
    int
    getLiterals(int index)
    Literals are represented with LiteralIndex values.
    int
    getLiteralsCount()
    Literals are represented with LiteralIndex values.
    List<Integer>
    getLiteralsList()
    Literals are represented with LiteralIndex values.
    Lrat.LratInferredClause.RatInfo
    getRatInfos(int index)
    repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
    int
    getRatInfosCount()
    repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
    List<Lrat.LratInferredClause.RatInfo>
    getRatInfosList()
    repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
    Lrat.LratInferredClause.RatInfoOrBuilder
    getRatInfosOrBuilder(int index)
    repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
    List<? extends Lrat.LratInferredClause.RatInfoOrBuilder>
    getRatInfosOrBuilderList()
    repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;
    long
    getUnitIds(int index)
    Clauses which become unit and possibly empty if all the `literals` are assumed to be false (verification stops at the first empty clause).
    int
    getUnitIdsCount()
    Clauses which become unit and possibly empty if all the `literals` are assumed to be false (verification stops at the first empty clause).
    List<Long>
    getUnitIdsList()
    Clauses which become unit and possibly empty if all the `literals` are assumed to be false (verification stops at the first empty clause).
    boolean
    hasClauseId()
    optional int64 clause_id = 1;
    boolean
    hasExported()
    Whether the clause must be exported, so that other workers can import it (a clause cannot be imported if it is not previously exported).

    Methods inherited from interface com.google.protobuf.MessageLiteOrBuilder

    isInitialized

    Methods inherited from interface com.google.protobuf.MessageOrBuilder

    findInitializationErrors, getAllFields, getDefaultInstanceForType, getDescriptorForType, getField, getInitializationErrorString, getOneofFieldDescriptor, getRepeatedField, getRepeatedFieldCount, getUnknownFields, hasField, hasOneof

  • Method Details

    • hasClauseId

      boolean hasClauseId()
      optional int64 clause_id = 1;
      Returns:
      Whether the clauseId field is set.

    • getClauseId

      long getClauseId()
      optional int64 clause_id = 1;
      Returns:
      The clauseId.

    • getLiteralsList

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

    • getLiteralsCount

      int getLiteralsCount()
      Literals are represented with LiteralIndex values.
      repeated int32 literals = 2 [packed = true];
      Returns:
      The count of literals.

    • getLiterals

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

    • getUnitIdsList

      List<Long> getUnitIdsList()
      Clauses which become unit and possibly empty if all the `literals` are
assumed to be false (verification stops at the first empty clause). This
list must be in unit propagation order. See LratChecker for more details.
      repeated int64 unit_ids = 3 [packed = true];
      Returns:
      A list containing the unitIds.

    • getUnitIdsCount

      int getUnitIdsCount()
      Clauses which become unit and possibly empty if all the `literals` are
assumed to be false (verification stops at the first empty clause). This
list must be in unit propagation order. See LratChecker for more details.
      repeated int64 unit_ids = 3 [packed = true];
      Returns:
      The count of unitIds.

    • getUnitIds

      long getUnitIds(int index)
      Clauses which become unit and possibly empty if all the `literals` are
assumed to be false (verification stops at the first empty clause). This
list must be in unit propagation order. See LratChecker for more details.
      repeated int64 unit_ids = 3 [packed = true];
      Parameters:
      index - The index of the element to return.
      Returns:
      The unitIds at the given index.

    • getRatInfosList

      List<Lrat.LratInferredClause.RatInfo> getRatInfosList()
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;

    • getRatInfos

      Lrat.LratInferredClause.RatInfo getRatInfos(int index)
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;

    • getRatInfosCount

      int getRatInfosCount()
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;

    • getRatInfosOrBuilderList

      List<? extends Lrat.LratInferredClause.RatInfoOrBuilder> getRatInfosOrBuilderList()
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;

    • getRatInfosOrBuilder

      Lrat.LratInferredClause.RatInfoOrBuilder getRatInfosOrBuilder(int index)
      repeated .operations_research.sat.LratInferredClause.RatInfo rat_infos = 4;

    • hasExported

      boolean hasExported()
      Whether the clause must be exported, so that other workers can import it (a
clause cannot be imported if it is not previously exported). This is not
needed for unary and binary clauses, which are always exported.
      optional bool exported = 5;
      Returns:
      Whether the exported field is set.

    • getExported

      boolean getExported()
      Whether the clause must be exported, so that other workers can import it (a
clause cannot be imported if it is not previously exported). This is not
needed for unary and binary clauses, which are always exported.
      optional bool exported = 5;
      Returns:
      The exported.