Detailed Description

Definition at line 1068 of file clause.cc.

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

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

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

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

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

Public Attributes
std::vector< Literal >	to_fix_

int64_t	work_done_ = 0

Member Typedef Documentation

◆ AtMostOne

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

Definition at line 1072 of file clause.cc.

◆ Implication

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

Definition at line 1070 of file clause.cc.

◆ SccFinder

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

Definition at line 1074 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 1078 of file clause.cc.

Member Function Documentation

◆ operator[]()

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

inline

Definition at line 1086 of file clause.cc.

Member Data Documentation

◆ to_fix_

std::vector<Literal> to_fix_

mutable

Definition at line 1158 of file clause.cc.

◆ work_done_

int64_t work_done_ = 0