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

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

Classes

enum  StepCase
class  Builder

Public Member Functions

StepCase getStepCase ()
boolean hasImportedClause ()
operations_research.sat.Lrat.LratImportedClause getImportedClause ()
operations_research.sat.Lrat.LratImportedClauseOrBuilder getImportedClauseOrBuilder ()
boolean hasInferredClause ()
operations_research.sat.Lrat.LratInferredClause getInferredClause ()
operations_research.sat.Lrat.LratInferredClauseOrBuilder getInferredClauseOrBuilder ()
boolean hasExportedClause ()
operations_research.sat.Lrat.LratExportedClause getExportedClause ()
operations_research.sat.Lrat.LratExportedClauseOrBuilder getExportedClauseOrBuilder ()
boolean hasDeletedClauses ()
operations_research.sat.Lrat.LratDeletedClauses getDeletedClauses ()
operations_research.sat.Lrat.LratDeletedClausesOrBuilder getDeletedClausesOrBuilder ()
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< LratProofStep > getParserForType ()
operations_research.sat.Lrat.LratProofStep getDefaultInstanceForType ()

Static Public Member Functions

static final com.google.protobuf.Descriptors.Descriptor getDescriptor ()
static operations_research.sat.Lrat.LratProofStep parseFrom (java.nio.ByteBuffer data) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratProofStep parseFrom (java.nio.ByteBuffer data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratProofStep parseFrom (com.google.protobuf.ByteString data) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratProofStep parseFrom (com.google.protobuf.ByteString data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratProofStep parseFrom (byte[] data) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratProofStep parseFrom (byte[] data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
static operations_research.sat.Lrat.LratProofStep parseFrom (java.io.InputStream input) throws java.io.IOException
static operations_research.sat.Lrat.LratProofStep parseFrom (java.io.InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
static operations_research.sat.Lrat.LratProofStep parseDelimitedFrom (java.io.InputStream input) throws java.io.IOException
static operations_research.sat.Lrat.LratProofStep parseDelimitedFrom (java.io.InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
static operations_research.sat.Lrat.LratProofStep parseFrom (com.google.protobuf.CodedInputStream input) throws java.io.IOException
static operations_research.sat.Lrat.LratProofStep 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.LratProofStep prototype)
static operations_research.sat.Lrat.LratProofStep getDefaultInstance ()
static com.google.protobuf.Parser< LratProofStep > parser ()

Static Public Attributes

static final int IMPORTED_CLAUSE_FIELD_NUMBER = 1
static final int INFERRED_CLAUSE_FIELD_NUMBER = 2
static final int EXPORTED_CLAUSE_FIELD_NUMBER = 3
static final int DELETED_CLAUSES_FIELD_NUMBER = 4

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.LratProofStep.equals ( final java.lang.Object obj)

Definition at line 4520 of file Lrat.java.

◆ getDefaultInstance()

operations_research.sat.Lrat.LratProofStep operations_research.sat.Lrat.LratProofStep.getDefaultInstance ( )
static

Definition at line 5488 of file Lrat.java.

◆ getDefaultInstanceForType()

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

Definition at line 5524 of file Lrat.java.

◆ getDeletedClauses()

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

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Returns
The deletedClauses.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4446 of file Lrat.java.

◆ getDeletedClausesOrBuilder()

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

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4456 of file Lrat.java.

◆ getDescriptor()

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

Definition at line 4281 of file Lrat.java.

◆ getExportedClause()

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

.operations_research.sat.LratExportedClause exported_clause = 3;

Returns
The exportedClause.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4415 of file Lrat.java.

◆ getExportedClauseOrBuilder()

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

.operations_research.sat.LratExportedClause exported_clause = 3;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4425 of file Lrat.java.

◆ getImportedClause()

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

.operations_research.sat.LratImportedClause imported_clause = 1;

Returns
The importedClause.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4353 of file Lrat.java.

◆ getImportedClauseOrBuilder()

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

.operations_research.sat.LratImportedClause imported_clause = 1;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4363 of file Lrat.java.

◆ getInferredClause()

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

.operations_research.sat.LratInferredClause inferred_clause = 2;

Returns
The inferredClause.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4384 of file Lrat.java.

◆ getInferredClauseOrBuilder()

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

.operations_research.sat.LratInferredClause inferred_clause = 2;

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4394 of file Lrat.java.

◆ getParserForType()

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

Definition at line 5519 of file Lrat.java.

◆ getSerializedSize()

int operations_research.sat.Lrat.LratProofStep.getSerializedSize ( )

Definition at line 4493 of file Lrat.java.

◆ getStepCase()

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

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4334 of file Lrat.java.

◆ hasDeletedClauses()

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

.operations_research.sat.LratDeletedClauses deleted_clauses = 4;

Returns
Whether the deletedClauses field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4438 of file Lrat.java.

◆ hasExportedClause()

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

.operations_research.sat.LratExportedClause exported_clause = 3;

Returns
Whether the exportedClause field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4407 of file Lrat.java.

◆ hashCode()

int operations_research.sat.Lrat.LratProofStep.hashCode ( )

Definition at line 4555 of file Lrat.java.

◆ hasImportedClause()

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

.operations_research.sat.LratImportedClause imported_clause = 1;

Returns
Whether the importedClause field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4345 of file Lrat.java.

◆ hasInferredClause()

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

.operations_research.sat.LratInferredClause inferred_clause = 2;

Returns
Whether the inferredClause field is set.

Implements operations_research.sat.Lrat.LratProofStepOrBuilder.

Definition at line 4376 of file Lrat.java.

◆ internalGetFieldAccessorTable()

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

Definition at line 4287 of file Lrat.java.

◆ isInitialized()

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

Definition at line 4465 of file Lrat.java.

◆ newBuilder() [1/2]

Builder operations_research.sat.Lrat.LratProofStep.newBuilder ( )
static

Definition at line 4660 of file Lrat.java.

◆ newBuilder() [2/2]

Builder operations_research.sat.Lrat.LratProofStep.newBuilder ( operations_research.sat.Lrat.LratProofStep prototype)
static

Definition at line 4663 of file Lrat.java.

◆ newBuilderForType() [1/2]

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

Definition at line 4659 of file Lrat.java.

◆ newBuilderForType() [2/2]

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

Definition at line 4673 of file Lrat.java.

◆ parseDelimitedFrom() [1/2]

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

Definition at line 4631 of file Lrat.java.

◆ parseDelimitedFrom() [2/2]

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

Definition at line 4637 of file Lrat.java.

◆ parseFrom() [1/10]

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

Definition at line 4608 of file Lrat.java.

◆ parseFrom() [2/10]

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

Definition at line 4612 of file Lrat.java.

◆ parseFrom() [3/10]

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

Definition at line 4597 of file Lrat.java.

◆ parseFrom() [4/10]

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

Definition at line 4602 of file Lrat.java.

◆ parseFrom() [5/10]

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

Definition at line 4644 of file Lrat.java.

◆ parseFrom() [6/10]

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

Definition at line 4650 of file Lrat.java.

◆ parseFrom() [7/10]

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

Definition at line 4618 of file Lrat.java.

◆ parseFrom() [8/10]

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

Definition at line 4623 of file Lrat.java.

◆ parseFrom() [9/10]

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

Definition at line 4586 of file Lrat.java.

◆ parseFrom() [10/10]

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

Definition at line 4591 of file Lrat.java.

◆ parser()

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

Definition at line 5514 of file Lrat.java.

◆ toBuilder()

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

Definition at line 4667 of file Lrat.java.

◆ writeTo()

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

Definition at line 4475 of file Lrat.java.

Member Data Documentation

◆ DELETED_CLAUSES_FIELD_NUMBER

final int operations_research.sat.Lrat.LratProofStep.DELETED_CLAUSES_FIELD_NUMBER = 4
static

Definition at line 4432 of file Lrat.java.

◆ EXPORTED_CLAUSE_FIELD_NUMBER

final int operations_research.sat.Lrat.LratProofStep.EXPORTED_CLAUSE_FIELD_NUMBER = 3
static

Definition at line 4401 of file Lrat.java.

◆ IMPORTED_CLAUSE_FIELD_NUMBER

final int operations_research.sat.Lrat.LratProofStep.IMPORTED_CLAUSE_FIELD_NUMBER = 1
static

Definition at line 4339 of file Lrat.java.

◆ INFERRED_CLAUSE_FIELD_NUMBER

final int operations_research.sat.Lrat.LratProofStep.INFERRED_CLAUSE_FIELD_NUMBER = 2
static

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