operations_research::sat::PostsolveClauses Struct Reference

#include <sat_inprocessing.h>

Public Member Functions
void	AddClauseWithSpecialLiteral (Literal literal, absl::Span< const Literal > clause)

Public Attributes
std::deque< std::vector< Literal > >	clauses

Detailed Description

The order is important and each clauses has a "special" literal that is put first.

Todo

(user): Use a flat memory structure instead.

Definition at line 51 of file sat_inprocessing.h.

Member Function Documentation

AddClauseWithSpecialLiteral()

void operations_research::sat::PostsolveClauses::AddClauseWithSpecialLiteral	(	Literal	literal,
		absl::Span< const Literal >	clause )

Utility function that push back clause but also make sure the given literal from clause appear first.

Definition at line 50 of file sat_inprocessing.cc.

Member Data Documentation

clauses

std::deque<std::vector<Literal> > operations_research::sat::PostsolveClauses::clauses

Definition at line 57 of file sat_inprocessing.h.

---

The documentation for this struct was generated from the following files:

• ortools/sat/sat_inprocessing.h
• ortools/sat/sat_inprocessing.cc