Google OR-Tools v9.15
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research.sat.Lrat.LratInferredClause.RatInfo Class Reference

Detailed Description

If `rat_infos` is empty, the last `unit_ids` clause must become empty after
unit propagation. If the last `unit_ids` clause does not become empty by
unit propagation, then `rat_infos` must contain all the clauses which
contain the negation of the first `literals` (called the pivot 'p') -- and
no other clauses. Moreover, for each r in `rat_infos`, all the `r.unit_ids`
clauses must become unit and eventually empty if all the literals of the
`r.resolvant_id` clause (minus ~p), plus those in `literals`, are assumed
to be false (this list must be in unit propagation order; verification
stops at the first empty clause). See LratChecker for more details.

Protobuf type operations_research.sat.LratInferredClause.RatInfo

Definition at line 911 of file Lrat.java.

Inheritance diagram for operations_research.sat.Lrat.LratInferredClause.RatInfo:
operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder

Classes

class  Builder

Public Member Functions

boolean hasResolvantId ()
long getResolvantId ()
java.util.List< java.lang.Long > getUnitIdsList ()
int getUnitIdsCount ()
long getUnitIds (int index)
final boolean isInitialized ()
void writeTo (com.google.protobuf.CodedOutputStream output) throws java.io.IOException
int getSerializedSize ()
boolean equals (final java.lang.Object obj)
int hashCode ()
Builder newBuilderForType ()
Builder toBuilder ()
com.google.protobuf.Parser< RatInfo > getParserForType ()
operations_research.sat.Lrat.LratInferredClause.RatInfo getDefaultInstanceForType ()

Static Public Member Functions

static final com.google.protobuf.Descriptors.Descriptor getDescriptor ()
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (java.nio.ByteBuffer data) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (java.nio.ByteBuffer data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (com.google.protobuf.ByteString data) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (com.google.protobuf.ByteString data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (byte[] data) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (byte[] data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (java.io.InputStream input) throws java.io.IOException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (java.io.InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseDelimitedFrom (java.io.InputStream input) throws java.io.IOException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseDelimitedFrom (java.io.InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (com.google.protobuf.CodedInputStream input) throws java.io.IOException
static operations_research.sat.Lrat.LratInferredClause.RatInfo parseFrom (com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
static Builder newBuilder ()
static Builder newBuilder (operations_research.sat.Lrat.LratInferredClause.RatInfo prototype)
static operations_research.sat.Lrat.LratInferredClause.RatInfo getDefaultInstance ()
static com.google.protobuf.Parser< RatInfo > parser ()

Static Public Attributes

static final int RESOLVANT_ID_FIELD_NUMBER = 1
static final int UNIT_IDS_FIELD_NUMBER = 2

Protected Member Functions

com.google.protobuf.GeneratedMessage.FieldAccessorTable internalGetFieldAccessorTable ()
Builder newBuilderForType (com.google.protobuf.GeneratedMessage.BuilderParent parent)

Member Function Documentation

◆ equals()

boolean operations_research.sat.Lrat.LratInferredClause.RatInfo.equals ( final java.lang.Object obj)

Definition at line 1054 of file Lrat.java.

◆ getDefaultInstance()

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.getDefaultInstance ( )
static

Definition at line 1503 of file Lrat.java.

◆ getDefaultInstanceForType()

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.getDefaultInstanceForType ( )

Definition at line 1539 of file Lrat.java.

◆ getDescriptor()

final com.google.protobuf.Descriptors.Descriptor operations_research.sat.Lrat.LratInferredClause.RatInfo.getDescriptor ( )
static

Definition at line 934 of file Lrat.java.

◆ getParserForType()

com.google.protobuf.Parser< RatInfo > operations_research.sat.Lrat.LratInferredClause.RatInfo.getParserForType ( )

Definition at line 1534 of file Lrat.java.

◆ getResolvantId()

long operations_research.sat.Lrat.LratInferredClause.RatInfo.getResolvantId ( )

optional int64 resolvant_id = 1;

Returns
The resolvantId.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 962 of file Lrat.java.

◆ getSerializedSize()

int operations_research.sat.Lrat.LratInferredClause.RatInfo.getSerializedSize ( )

Definition at line 1025 of file Lrat.java.

◆ getUnitIds()

long operations_research.sat.Lrat.LratInferredClause.RatInfo.getUnitIds ( int index)

repeated int64 unit_ids = 2 [packed = true];

Parameters
indexThe index of the element to return.
Returns
The unitIds at the given index.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 991 of file Lrat.java.

◆ getUnitIdsCount()

int operations_research.sat.Lrat.LratInferredClause.RatInfo.getUnitIdsCount ( )

repeated int64 unit_ids = 2 [packed = true];

Returns
The count of unitIds.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 983 of file Lrat.java.

◆ getUnitIdsList()

java.util.List< java.lang.Long > operations_research.sat.Lrat.LratInferredClause.RatInfo.getUnitIdsList ( )

repeated int64 unit_ids = 2 [packed = true];

Returns
A list containing the unitIds.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 976 of file Lrat.java.

◆ hashCode()

int operations_research.sat.Lrat.LratInferredClause.RatInfo.hashCode ( )

Definition at line 1075 of file Lrat.java.

◆ hasResolvantId()

boolean operations_research.sat.Lrat.LratInferredClause.RatInfo.hasResolvantId ( )

optional int64 resolvant_id = 1;

Returns
Whether the resolvantId field is set.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 954 of file Lrat.java.

◆ internalGetFieldAccessorTable()

com.google.protobuf.GeneratedMessage.FieldAccessorTable operations_research.sat.Lrat.LratInferredClause.RatInfo.internalGetFieldAccessorTable ( )
protected

Definition at line 940 of file Lrat.java.

◆ isInitialized()

final boolean operations_research.sat.Lrat.LratInferredClause.RatInfo.isInitialized ( )

Definition at line 998 of file Lrat.java.

◆ newBuilder() [1/2]

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.newBuilder ( )
static

Definition at line 1169 of file Lrat.java.

◆ newBuilder() [2/2]

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.newBuilder ( operations_research.sat.Lrat.LratInferredClause.RatInfo prototype)
static

Definition at line 1172 of file Lrat.java.

◆ newBuilderForType() [1/2]

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.newBuilderForType ( )

Definition at line 1168 of file Lrat.java.

◆ newBuilderForType() [2/2]

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.newBuilderForType ( com.google.protobuf.GeneratedMessage.BuilderParent parent)
protected

Definition at line 1182 of file Lrat.java.

◆ parseDelimitedFrom() [1/2]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseDelimitedFrom ( java.io.InputStream input) throws java.io.IOException
static

Definition at line 1140 of file Lrat.java.

◆ parseDelimitedFrom() [2/2]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseDelimitedFrom ( java.io.InputStream input,
com.google.protobuf.ExtensionRegistryLite extensionRegistry ) throws java.io.IOException
static

Definition at line 1146 of file Lrat.java.

◆ parseFrom() [1/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( byte[] data) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 1117 of file Lrat.java.

◆ parseFrom() [2/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( byte[] data,
com.google.protobuf.ExtensionRegistryLite extensionRegistry ) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 1121 of file Lrat.java.

◆ parseFrom() [3/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( com.google.protobuf.ByteString data) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 1106 of file Lrat.java.

◆ parseFrom() [4/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( com.google.protobuf.ByteString data,
com.google.protobuf.ExtensionRegistryLite extensionRegistry ) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 1111 of file Lrat.java.

◆ parseFrom() [5/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( com.google.protobuf.CodedInputStream input) throws java.io.IOException
static

Definition at line 1153 of file Lrat.java.

◆ parseFrom() [6/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( com.google.protobuf.CodedInputStream input,
com.google.protobuf.ExtensionRegistryLite extensionRegistry ) throws java.io.IOException
static

Definition at line 1159 of file Lrat.java.

◆ parseFrom() [7/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( java.io.InputStream input) throws java.io.IOException
static

Definition at line 1127 of file Lrat.java.

◆ parseFrom() [8/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( java.io.InputStream input,
com.google.protobuf.ExtensionRegistryLite extensionRegistry ) throws java.io.IOException
static

Definition at line 1132 of file Lrat.java.

◆ parseFrom() [9/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( java.nio.ByteBuffer data) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 1095 of file Lrat.java.

◆ parseFrom() [10/10]

operations_research.sat.Lrat.LratInferredClause.RatInfo operations_research.sat.Lrat.LratInferredClause.RatInfo.parseFrom ( java.nio.ByteBuffer data,
com.google.protobuf.ExtensionRegistryLite extensionRegistry ) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 1100 of file Lrat.java.

◆ parser()

com.google.protobuf.Parser< RatInfo > operations_research.sat.Lrat.LratInferredClause.RatInfo.parser ( )
static

Definition at line 1529 of file Lrat.java.

◆ toBuilder()

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.toBuilder ( )

Definition at line 1176 of file Lrat.java.

◆ writeTo()

void operations_research.sat.Lrat.LratInferredClause.RatInfo.writeTo ( com.google.protobuf.CodedOutputStream output) throws java.io.IOException

Definition at line 1008 of file Lrat.java.

Member Data Documentation

◆ RESOLVANT_ID_FIELD_NUMBER

final int operations_research.sat.Lrat.LratInferredClause.RatInfo.RESOLVANT_ID_FIELD_NUMBER = 1
static

Definition at line 947 of file Lrat.java.

◆ UNIT_IDS_FIELD_NUMBER

final int operations_research.sat.Lrat.LratInferredClause.RatInfo.UNIT_IDS_FIELD_NUMBER = 2
static

Definition at line 966 of file Lrat.java.

The documentation for this class was generated from the following file:
  • build/java/ortools-java/src/main/java/operations_research/sat/Lrat.java