Google OR-Tools v9.15
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder 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 1202 of file Lrat.java.

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

Public Member Functions

Builder clear ()
com.google.protobuf.Descriptors.Descriptor getDescriptorForType ()
operations_research.sat.Lrat.LratInferredClause.RatInfo getDefaultInstanceForType ()
operations_research.sat.Lrat.LratInferredClause.RatInfo build ()
operations_research.sat.Lrat.LratInferredClause.RatInfo buildPartial ()
Builder mergeFrom (com.google.protobuf.Message other)
Builder mergeFrom (operations_research.sat.Lrat.LratInferredClause.RatInfo other)
final boolean isInitialized ()
Builder mergeFrom (com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
boolean hasResolvantId ()
long getResolvantId ()
Builder setResolvantId (long value)
Builder clearResolvantId ()
java.util.List< java.lang.Long > getUnitIdsList ()
int getUnitIdsCount ()
long getUnitIds (int index)
Builder setUnitIds (int index, long value)
Builder addUnitIds (long value)
Builder addAllUnitIds (java.lang.Iterable<? extends java.lang.Long > values)
Builder clearUnitIds ()

Static Public Member Functions

static final com.google.protobuf.Descriptors.Descriptor getDescriptor ()

Protected Member Functions

com.google.protobuf.GeneratedMessage.FieldAccessorTable internalGetFieldAccessorTable ()

Member Function Documentation

◆ addAllUnitIds()

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.addAllUnitIds ( java.lang.Iterable<? extends java.lang.Long > values)

repeated int64 unit_ids = 2 [packed = true];

Parameters
valuesThe unitIds to add.
Returns
This builder for chaining.

Definition at line 1474 of file Lrat.java.

◆ addUnitIds()

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.addUnitIds ( long value)

repeated int64 unit_ids = 2 [packed = true];

Parameters
valueThe unitIds to add.
Returns
This builder for chaining.

Definition at line 1461 of file Lrat.java.

◆ build()

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

Definition at line 1250 of file Lrat.java.

◆ buildPartial()

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

Definition at line 1259 of file Lrat.java.

◆ clear()

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

Definition at line 1230 of file Lrat.java.

◆ clearResolvantId()

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

optional int64 resolvant_id = 1;

Returns
This builder for chaining.

Definition at line 1403 of file Lrat.java.

◆ clearUnitIds()

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

repeated int64 unit_ids = 2 [packed = true];

Returns
This builder for chaining.

Definition at line 1487 of file Lrat.java.

◆ getDefaultInstanceForType()

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

Definition at line 1245 of file Lrat.java.

◆ getDescriptor()

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

Definition at line 1207 of file Lrat.java.

◆ getDescriptorForType()

com.google.protobuf.Descriptors.Descriptor operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.getDescriptorForType ( )

Definition at line 1240 of file Lrat.java.

◆ getResolvantId()

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

optional int64 resolvant_id = 1;

Returns
The resolvantId.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 1384 of file Lrat.java.

◆ getUnitIds()

long operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.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 1438 of file Lrat.java.

◆ getUnitIdsCount()

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

repeated int64 unit_ids = 2 [packed = true];

Returns
The count of unitIds.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 1430 of file Lrat.java.

◆ getUnitIdsList()

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

repeated int64 unit_ids = 2 [packed = true];

Returns
A list containing the unitIds.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 1422 of file Lrat.java.

◆ hasResolvantId()

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

optional int64 resolvant_id = 1;

Returns
Whether the resolvantId field is set.

Implements operations_research.sat.Lrat.LratInferredClause.RatInfoOrBuilder.

Definition at line 1376 of file Lrat.java.

◆ internalGetFieldAccessorTable()

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

Definition at line 1213 of file Lrat.java.

◆ isInitialized()

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

Definition at line 1312 of file Lrat.java.

◆ mergeFrom() [1/3]

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

Definition at line 1317 of file Lrat.java.

◆ mergeFrom() [2/3]

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.mergeFrom ( com.google.protobuf.Message other)

Definition at line 1281 of file Lrat.java.

◆ mergeFrom() [3/3]

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.mergeFrom ( operations_research.sat.Lrat.LratInferredClause.RatInfo other)

Definition at line 1290 of file Lrat.java.

◆ setResolvantId()

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.setResolvantId ( long value)

optional int64 resolvant_id = 1;

Parameters
valueThe resolvantId to set.
Returns
This builder for chaining.

Definition at line 1392 of file Lrat.java.

◆ setUnitIds()

Builder operations_research.sat.Lrat.LratInferredClause.RatInfo.Builder.setUnitIds ( int index,
long value )

repeated int64 unit_ids = 2 [packed = true];

Parameters
indexThe index to set the value at.
valueThe unitIds to set.
Returns
This builder for chaining.

Definition at line 1447 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