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. More...

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.

Definition at line 1384 of file Lrat.pb.cs.

Inheritance diagram for OperationsResearch.Sat.LratProofStep:

Public Types
enum	StepOneofCase { None = 0 , ImportedClause = 1 , InferredClause = 2 , ExportedClause = 3 , DeletedClauses = 4 }
	Enum of possible cases for the "step" oneof. More...

Public Member Functions
	LratProofStep ()
	LratProofStep (LratProofStep other)
LratProofStep	Clone ()
void	ClearStep ()
override bool	Equals (object other)
bool	Equals (LratProofStep other)
override int	GetHashCode ()
override string	ToString ()
void	WriteTo (pb::CodedOutputStream output)
int	CalculateSize ()
void	MergeFrom (LratProofStep other)
void	MergeFrom (pb::CodedInputStream input)

Static Public Attributes
const int	ImportedClauseFieldNumber = 1
	Field number for the "imported_clause" field.
const int	InferredClauseFieldNumber = 2
	Field number for the "inferred_clause" field.
const int	ExportedClauseFieldNumber = 3
	Field number for the "exported_clause" field.
const int	DeletedClausesFieldNumber = 4
	Field number for the "deleted_clauses" field.

Properties
static pb::MessageParser< LratProofStep >	Parser `[get]`
static pbr::MessageDescriptor	Descriptor `[get]`
global::OperationsResearch.Sat.LratImportedClause	ImportedClause `[get, set]`
global::OperationsResearch.Sat.LratInferredClause	InferredClause `[get, set]`
global::OperationsResearch.Sat.LratExportedClause	ExportedClause `[get, set]`
global::OperationsResearch.Sat.LratDeletedClauses	DeletedClauses `[get, set]`
StepOneofCase	StepCase `[get]`

Member Enumeration Documentation

◆ StepOneofCase

enum OperationsResearch.Sat.LratProofStep.StepOneofCase

Enum of possible cases for the "step" oneof.

Enumerator
None
ImportedClause
InferredClause
ExportedClause
DeletedClauses

Definition at line 1492 of file Lrat.pb.cs.

Constructor & Destructor Documentation

◆ LratProofStep() [1/2]

OperationsResearch.Sat.LratProofStep.LratProofStep ( )

inline

Definition at line 1409 of file Lrat.pb.cs.

◆ LratProofStep() [2/2]

OperationsResearch.Sat.LratProofStep.LratProofStep ( LratProofStep other )

inline

Definition at line 1417 of file Lrat.pb.cs.

Member Function Documentation

◆ CalculateSize()

int OperationsResearch.Sat.LratProofStep.CalculateSize ( )

inline

Definition at line 1613 of file Lrat.pb.cs.

◆ ClearStep()

void OperationsResearch.Sat.LratProofStep.ClearStep ( )

inline

Definition at line 1508 of file Lrat.pb.cs.

◆ Clone()

LratProofStep OperationsResearch.Sat.LratProofStep.Clone ( )

inline

Definition at line 1438 of file Lrat.pb.cs.

◆ Equals() [1/2]

bool OperationsResearch.Sat.LratProofStep.Equals ( LratProofStep other )

inline

Definition at line 1521 of file Lrat.pb.cs.

◆ Equals() [2/2]

override bool OperationsResearch.Sat.LratProofStep.Equals ( object other )

inline

Definition at line 1515 of file Lrat.pb.cs.

◆ GetHashCode()

override int OperationsResearch.Sat.LratProofStep.GetHashCode ( )

inline

Definition at line 1538 of file Lrat.pb.cs.

◆ MergeFrom() [1/2]

void OperationsResearch.Sat.LratProofStep.MergeFrom ( LratProofStep other )

inline

Definition at line 1635 of file Lrat.pb.cs.

◆ MergeFrom() [2/2]

void OperationsResearch.Sat.LratProofStep.MergeFrom ( pb.CodedInputStream input )

inline

Definition at line 1671 of file Lrat.pb.cs.

◆ ToString()

override string OperationsResearch.Sat.LratProofStep.ToString ( )

inline

Definition at line 1553 of file Lrat.pb.cs.

◆ WriteTo()

void OperationsResearch.Sat.LratProofStep.WriteTo ( pb.CodedOutputStream output )

inline

Definition at line 1559 of file Lrat.pb.cs.

Member Data Documentation

◆ DeletedClausesFieldNumber

const int OperationsResearch.Sat.LratProofStep.DeletedClausesFieldNumber = 4

static

Field number for the "deleted_clauses" field.

Definition at line 1479 of file Lrat.pb.cs.

◆ ExportedClauseFieldNumber

const int OperationsResearch.Sat.LratProofStep.ExportedClauseFieldNumber = 3

static

Field number for the "exported_clause" field.

Definition at line 1467 of file Lrat.pb.cs.

◆ ImportedClauseFieldNumber

const int OperationsResearch.Sat.LratProofStep.ImportedClauseFieldNumber = 1

static

Field number for the "imported_clause" field.

Definition at line 1443 of file Lrat.pb.cs.

◆ InferredClauseFieldNumber

const int OperationsResearch.Sat.LratProofStep.InferredClauseFieldNumber = 2

static

Field number for the "inferred_clause" field.

Definition at line 1455 of file Lrat.pb.cs.

Property Documentation

◆ DeletedClauses

global.OperationsResearch.Sat.LratDeletedClauses OperationsResearch.Sat.LratProofStep.DeletedClauses

getset

Definition at line 1482 of file Lrat.pb.cs.

◆ Descriptor

pbr.MessageDescriptor OperationsResearch.Sat.LratProofStep.Descriptor

staticget

Definition at line 1397 of file Lrat.pb.cs.

◆ ExportedClause

global.OperationsResearch.Sat.LratExportedClause OperationsResearch.Sat.LratProofStep.ExportedClause

getset

Definition at line 1470 of file Lrat.pb.cs.

◆ ImportedClause

global.OperationsResearch.Sat.LratImportedClause OperationsResearch.Sat.LratProofStep.ImportedClause

getset

Definition at line 1446 of file Lrat.pb.cs.

◆ InferredClause

global.OperationsResearch.Sat.LratInferredClause OperationsResearch.Sat.LratProofStep.InferredClause

getset

Definition at line 1458 of file Lrat.pb.cs.

◆ Parser

pb.MessageParser<LratProofStep> OperationsResearch.Sat.LratProofStep.Parser

staticget

Definition at line 1393 of file Lrat.pb.cs.

◆ StepCase

StepOneofCase OperationsResearch.Sat.LratProofStep.StepCase

get

Definition at line 1502 of file Lrat.pb.cs.

The documentation for this class was generated from the following file:

build/dotnet/Google.OrTools/ortools/sat/Lrat.pb.cs

Detailed Description

Public Types

Public Member Functions

Static Public Attributes

Properties

Member Enumeration Documentation

◆ StepOneofCase

Constructor & Destructor Documentation

◆ LratProofStep() [1/2]

◆ LratProofStep() [2/2]

Member Function Documentation

◆ CalculateSize()

◆ ClearStep()

◆ Clone()

◆ Equals() [1/2]

◆ Equals() [2/2]

◆ GetHashCode()

◆ MergeFrom() [1/2]

◆ MergeFrom() [2/2]

◆ ToString()

◆ WriteTo()

Member Data Documentation

◆ DeletedClausesFieldNumber

◆ ExportedClauseFieldNumber

◆ ImportedClauseFieldNumber

◆ InferredClauseFieldNumber

Property Documentation

◆ DeletedClauses

◆ Descriptor

◆ ExportedClause

◆ ImportedClause

◆ InferredClause

◆ Parser

◆ StepCase