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

Detailed Description

An LRAT UNSAT proof is a sequence of steps, starting from imported clauses
and ending with the empty clause. At each step new clauses can be inferred
from previous ones (with an explicit proof), or imported from another proof
built by another thread. A proof step can also delete clauses which are no
longer needed, or export a clause for other workers to import. Each clause is
identified by a unique clause ID.

Protobuf type operations_research.sat.LratProofStep

Definition at line 4690 of file Lrat.java.

Inheritance diagram for operations_research.sat.Lrat.LratProofStep.Builder:
operations_research.sat.Lrat.LratProofStepOrBuilder

Public Member Functions

Builder clear ()
com.google.protobuf.Descriptors.Descriptor getDescriptorForType ()
operations_research.sat.Lrat.LratProofStep getDefaultInstanceForType ()
operations_research.sat.Lrat.LratProofStep build ()
operations_research.sat.Lrat.LratProofStep buildPartial ()
Builder mergeFrom (com.google.protobuf.Message other)
Builder mergeFrom (operations_research.sat.Lrat.LratProofStep other)
final boolean isInitialized ()
Builder mergeFrom (com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
StepCase getStepCase ()
Builder clearStep ()
boolean hasImportedClause ()
operations_research.sat.Lrat.LratImportedClause getImportedClause ()
Builder setImportedClause (operations_research.sat.Lrat.LratImportedClause value)
Builder setImportedClause (operations_research.sat.Lrat.LratImportedClause.Builder builderForValue)
Builder mergeImportedClause (operations_research.sat.Lrat.LratImportedClause value)
Builder clearImportedClause ()
operations_research.sat.Lrat.LratImportedClause.Builder getImportedClauseBuilder ()
operations_research.sat.Lrat.LratImportedClauseOrBuilder getImportedClauseOrBuilder ()
boolean hasInferredClause ()
operations_research.sat.Lrat.LratInferredClause getInferredClause ()
Builder setInferredClause (operations_research.sat.Lrat.LratInferredClause value)
Builder setInferredClause (operations_research.sat.Lrat.LratInferredClause.Builder builderForValue)
Builder mergeInferredClause (operations_research.sat.Lrat.LratInferredClause value)
Builder clearInferredClause ()
operations_research.sat.Lrat.LratInferredClause.Builder getInferredClauseBuilder ()
operations_research.sat.Lrat.LratInferredClauseOrBuilder getInferredClauseOrBuilder ()
boolean hasExportedClause ()
operations_research.sat.Lrat.LratExportedClause getExportedClause ()
Builder setExportedClause (operations_research.sat.Lrat.LratExportedClause value)
Builder setExportedClause (operations_research.sat.Lrat.LratExportedClause.Builder builderForValue)
Builder mergeExportedClause (operations_research.sat.Lrat.LratExportedClause value)
Builder clearExportedClause ()
operations_research.sat.Lrat.LratExportedClause.Builder getExportedClauseBuilder ()
operations_research.sat.Lrat.LratExportedClauseOrBuilder getExportedClauseOrBuilder ()
boolean hasDeletedClauses ()
operations_research.sat.Lrat.LratDeletedClauses getDeletedClauses ()
Builder setDeletedClauses (operations_research.sat.Lrat.LratDeletedClauses value)
Builder setDeletedClauses (operations_research.sat.Lrat.LratDeletedClauses.Builder builderForValue)
Builder mergeDeletedClauses (operations_research.sat.Lrat.LratDeletedClauses value)
Builder clearDeletedClauses ()
operations_research.sat.Lrat.LratDeletedClauses.Builder getDeletedClausesBuilder ()
operations_research.sat.Lrat.LratDeletedClausesOrBuilder getDeletedClausesOrBuilder ()

Static Public Member Functions

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

Protected Member Functions

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

Member Function Documentation

◆ build()

operations_research.sat.Lrat.LratProofStep operations_research.sat.Lrat.LratProofStep.Builder.build ( )

Definition at line 4750 of file Lrat.java.

◆ buildPartial()

operations_research.sat.Lrat.LratProofStep operations_research.sat.Lrat.LratProofStep.Builder.buildPartial ( )

Definition at line 4759 of file Lrat.java.

◆ clear()

Builder operations_research.sat.Lrat.LratProofStep.Builder.clear ( )

Definition at line 4718 of file Lrat.java.

◆ clearDeletedClauses()

Builder operations_research.sat.Lrat.LratProofStep.Builder.clearDeletedClauses ( )

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Definition at line 5421 of file Lrat.java.

◆ clearExportedClause()

Builder operations_research.sat.Lrat.LratProofStep.Builder.clearExportedClause ( )

.operations_research.sat.LratExportedClause exported_clause = 3;

Definition at line 5279 of file Lrat.java.

◆ clearImportedClause()

Builder operations_research.sat.Lrat.LratProofStep.Builder.clearImportedClause ( )

.operations_research.sat.LratImportedClause imported_clause = 1;

Definition at line 4995 of file Lrat.java.

◆ clearInferredClause()

Builder operations_research.sat.Lrat.LratProofStep.Builder.clearInferredClause ( )

.operations_research.sat.LratInferredClause inferred_clause = 2;

Definition at line 5137 of file Lrat.java.

◆ clearStep()

Builder operations_research.sat.Lrat.LratProofStep.Builder.clearStep ( )

Definition at line 4902 of file Lrat.java.

◆ getDefaultInstanceForType()

operations_research.sat.Lrat.LratProofStep operations_research.sat.Lrat.LratProofStep.Builder.getDefaultInstanceForType ( )

Definition at line 4745 of file Lrat.java.

◆ getDeletedClauses()

operations_research.sat.Lrat.LratDeletedClauses operations_research.sat.Lrat.LratProofStep.Builder.getDeletedClauses ( )

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Returns
The deletedClauses.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5352 of file Lrat.java.

◆ getDeletedClausesBuilder()

operations_research.sat.Lrat.LratDeletedClauses.Builder operations_research.sat.Lrat.LratProofStep.Builder.getDeletedClausesBuilder ( )

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Definition at line 5440 of file Lrat.java.

◆ getDeletedClausesOrBuilder()

operations_research.sat.Lrat.LratDeletedClausesOrBuilder operations_research.sat.Lrat.LratProofStep.Builder.getDeletedClausesOrBuilder ( )

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5447 of file Lrat.java.

◆ getDescriptor()

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

Definition at line 4695 of file Lrat.java.

◆ getDescriptorForType()

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

Definition at line 4740 of file Lrat.java.

◆ getExportedClause()

operations_research.sat.Lrat.LratExportedClause operations_research.sat.Lrat.LratProofStep.Builder.getExportedClause ( )

.operations_research.sat.LratExportedClause exported_clause = 3;

Returns
The exportedClause.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5210 of file Lrat.java.

◆ getExportedClauseBuilder()

operations_research.sat.Lrat.LratExportedClause.Builder operations_research.sat.Lrat.LratProofStep.Builder.getExportedClauseBuilder ( )

.operations_research.sat.LratExportedClause exported_clause = 3;

Definition at line 5298 of file Lrat.java.

◆ getExportedClauseOrBuilder()

operations_research.sat.Lrat.LratExportedClauseOrBuilder operations_research.sat.Lrat.LratProofStep.Builder.getExportedClauseOrBuilder ( )

.operations_research.sat.LratExportedClause exported_clause = 3;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5305 of file Lrat.java.

◆ getImportedClause()

operations_research.sat.Lrat.LratImportedClause operations_research.sat.Lrat.LratProofStep.Builder.getImportedClause ( )

.operations_research.sat.LratImportedClause imported_clause = 1;

Returns
The importedClause.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4926 of file Lrat.java.

◆ getImportedClauseBuilder()

operations_research.sat.Lrat.LratImportedClause.Builder operations_research.sat.Lrat.LratProofStep.Builder.getImportedClauseBuilder ( )

.operations_research.sat.LratImportedClause imported_clause = 1;

Definition at line 5014 of file Lrat.java.

◆ getImportedClauseOrBuilder()

operations_research.sat.Lrat.LratImportedClauseOrBuilder operations_research.sat.Lrat.LratProofStep.Builder.getImportedClauseOrBuilder ( )

.operations_research.sat.LratImportedClause imported_clause = 1;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5021 of file Lrat.java.

◆ getInferredClause()

operations_research.sat.Lrat.LratInferredClause operations_research.sat.Lrat.LratProofStep.Builder.getInferredClause ( )

.operations_research.sat.LratInferredClause inferred_clause = 2;

Returns
The inferredClause.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5068 of file Lrat.java.

◆ getInferredClauseBuilder()

operations_research.sat.Lrat.LratInferredClause.Builder operations_research.sat.Lrat.LratProofStep.Builder.getInferredClauseBuilder ( )

.operations_research.sat.LratInferredClause inferred_clause = 2;

Definition at line 5156 of file Lrat.java.

◆ getInferredClauseOrBuilder()

operations_research.sat.Lrat.LratInferredClauseOrBuilder operations_research.sat.Lrat.LratProofStep.Builder.getInferredClauseOrBuilder ( )

.operations_research.sat.LratInferredClause inferred_clause = 2;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5163 of file Lrat.java.

◆ getStepCase()

StepCase operations_research.sat.Lrat.LratProofStep.Builder.getStepCase ( )

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4897 of file Lrat.java.

◆ hasDeletedClauses()

boolean operations_research.sat.Lrat.LratProofStep.Builder.hasDeletedClauses ( )

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Returns
Whether the deletedClauses field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5344 of file Lrat.java.

◆ hasExportedClause()

boolean operations_research.sat.Lrat.LratProofStep.Builder.hasExportedClause ( )

.operations_research.sat.LratExportedClause exported_clause = 3;

Returns
Whether the exportedClause field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5202 of file Lrat.java.

◆ hasImportedClause()

boolean operations_research.sat.Lrat.LratProofStep.Builder.hasImportedClause ( )

.operations_research.sat.LratImportedClause imported_clause = 1;

Returns
Whether the importedClause field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4918 of file Lrat.java.

◆ hasInferredClause()

boolean operations_research.sat.Lrat.LratProofStep.Builder.hasInferredClause ( )

.operations_research.sat.LratInferredClause inferred_clause = 2;

Returns
Whether the inferredClause field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 5060 of file Lrat.java.

◆ internalGetFieldAccessorTable()

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

Definition at line 4701 of file Lrat.java.

◆ isInitialized()

final boolean operations_research.sat.Lrat.LratProofStep.Builder.isInitialized ( )

Definition at line 4831 of file Lrat.java.

◆ mergeDeletedClauses()

Builder operations_research.sat.Lrat.LratProofStep.Builder.mergeDeletedClauses ( operations_research.sat.Lrat.LratDeletedClauses value)

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Definition at line 5398 of file Lrat.java.

◆ mergeExportedClause()

Builder operations_research.sat.Lrat.LratProofStep.Builder.mergeExportedClause ( operations_research.sat.Lrat.LratExportedClause value)

.operations_research.sat.LratExportedClause exported_clause = 3;

Definition at line 5256 of file Lrat.java.

◆ mergeFrom() [1/3]

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

Definition at line 4836 of file Lrat.java.

◆ mergeFrom() [2/3]

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

Definition at line 4793 of file Lrat.java.

◆ mergeFrom() [3/3]

Builder operations_research.sat.Lrat.LratProofStep.Builder.mergeFrom ( operations_research.sat.Lrat.LratProofStep other)

Definition at line 4802 of file Lrat.java.

◆ mergeImportedClause()

Builder operations_research.sat.Lrat.LratProofStep.Builder.mergeImportedClause ( operations_research.sat.Lrat.LratImportedClause value)

.operations_research.sat.LratImportedClause imported_clause = 1;

Definition at line 4972 of file Lrat.java.

◆ mergeInferredClause()

Builder operations_research.sat.Lrat.LratProofStep.Builder.mergeInferredClause ( operations_research.sat.Lrat.LratInferredClause value)

.operations_research.sat.LratInferredClause inferred_clause = 2;

Definition at line 5114 of file Lrat.java.

◆ setDeletedClauses() [1/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setDeletedClauses ( operations_research.sat.Lrat.LratDeletedClauses value)

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Definition at line 5368 of file Lrat.java.

◆ setDeletedClauses() [2/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setDeletedClauses ( operations_research.sat.Lrat.LratDeletedClauses.Builder builderForValue)

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Definition at line 5384 of file Lrat.java.

◆ setExportedClause() [1/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setExportedClause ( operations_research.sat.Lrat.LratExportedClause value)

.operations_research.sat.LratExportedClause exported_clause = 3;

Definition at line 5226 of file Lrat.java.

◆ setExportedClause() [2/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setExportedClause ( operations_research.sat.Lrat.LratExportedClause.Builder builderForValue)

.operations_research.sat.LratExportedClause exported_clause = 3;

Definition at line 5242 of file Lrat.java.

◆ setImportedClause() [1/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setImportedClause ( operations_research.sat.Lrat.LratImportedClause value)

.operations_research.sat.LratImportedClause imported_clause = 1;

Definition at line 4942 of file Lrat.java.

◆ setImportedClause() [2/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setImportedClause ( operations_research.sat.Lrat.LratImportedClause.Builder builderForValue)

.operations_research.sat.LratImportedClause imported_clause = 1;

Definition at line 4958 of file Lrat.java.

◆ setInferredClause() [1/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setInferredClause ( operations_research.sat.Lrat.LratInferredClause value)

.operations_research.sat.LratInferredClause inferred_clause = 2;

Definition at line 5084 of file Lrat.java.

◆ setInferredClause() [2/2]

Builder operations_research.sat.Lrat.LratProofStep.Builder.setInferredClause ( operations_research.sat.Lrat.LratInferredClause.Builder builderForValue)

.operations_research.sat.LratInferredClause inferred_clause = 2;

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