Detailed Description

Definition at line 1016 of file clause.cc.

Public Types
using	Implication = absl::StrongVector< LiteralIndex, absl::InlinedVector< Literal, 6 > >

using	AtMostOne = absl::StrongVector< LiteralIndex, absl::InlinedVector< int32, 6 > >

using	SccFinder = StronglyConnectedComponentsFinder< int32, SccGraph, std::vector< std::vector< int32 > > >

Public Member Functions
	SccGraph (SccFinder finder, Implication graph, AtMostOne at_most_ones, std::vector< Literal > at_most_one_buffer)

const std::vector< int32 > &	operator[] (int32 node) const

Public Attributes
std::vector< Literal >	to_fix_

int64	work_done_ = 0

Member Typedef Documentation

◆ AtMostOne

using AtMostOne = absl::StrongVector<LiteralIndex, absl::InlinedVector<int32, 6> >

Definition at line 1020 of file clause.cc.

◆ Implication

using Implication = absl::StrongVector<LiteralIndex, absl::InlinedVector<Literal, 6> >

Definition at line 1018 of file clause.cc.

◆ SccFinder

using SccFinder = StronglyConnectedComponentsFinder<int32, SccGraph, std::vector<std::vector<int32> >>

Definition at line 1022 of file clause.cc.

Constructor & Destructor Documentation

◆ SccGraph()

SccGraph	(	SccFinder *	finder,
		Implication *	graph,
		AtMostOne *	at_most_ones,
		std::vector< Literal > *	at_most_one_buffer
	)

inlineexplicit

Definition at line 1026 of file clause.cc.

Member Function Documentation

◆ operator[]()

const std::vector< int32 > & operator[] ( int32 node ) const

inline

Definition at line 1034 of file clause.cc.

Member Data Documentation

◆ to_fix_

std::vector<Literal> to_fix_

mutable

Definition at line 1106 of file clause.cc.

◆ work_done_

int64 work_done_ = 0