operations_research::sat::SatPostsolver Class Reference

Detailed Description

Definition at line 45 of file simplification.h.

#include <simplification.h>

Public Member Functions
	SatPostsolver (int num_variables)
	SatPostsolver (const SatPostsolver &)=delete
SatPostsolver &	operator= (const SatPostsolver &)=delete
void	Add (Literal x, absl::Span< const Literal > clause)
void	FixVariable (Literal x)
void	ApplyMapping (const util_intops::StrongVector< BooleanVariable, BooleanVariable > &mapping)
std::vector< bool >	ExtractAndPostsolveSolution (const SatSolver &solver)
std::vector< bool >	PostsolveSolution (const std::vector< bool > &solution)
int	NumClauses () const
std::vector< Literal >	Clause (int i) const
const VariablesAssignment &	assignment ()

Constructor & Destructor Documentation

SatPostsolver() [1/2]

operations_research::sat::SatPostsolver::SatPostsolver ( int num_variables )

explicit

Definition at line 47 of file simplification.cc.

SatPostsolver() [2/2]

operations_research::sat::SatPostsolver::SatPostsolver ( const SatPostsolver & )

delete

Member Function Documentation

Add()

void operations_research::sat::SatPostsolver::Add	(	Literal	x,
		absl::Span< const Literal >	clause )

Definition at line 56 of file simplification.cc.

ApplyMapping()

void operations_research::sat::SatPostsolver::ApplyMapping

(

const util_intops::StrongVector< BooleanVariable, BooleanVariable > &

mapping

)

Definition at line 71 of file simplification.cc.

assignment()

const VariablesAssignment & operations_research::sat::SatPostsolver::assignment ( )

inline

Definition at line 107 of file simplification.h.

Clause()

std::vector< Literal > operations_research::sat::SatPostsolver::Clause ( int i ) const

inline

Definition at line 86 of file simplification.h.

ExtractAndPostsolveSolution()

std::vector< bool > operations_research::sat::SatPostsolver::ExtractAndPostsolveSolution

(

const SatSolver &

solver

)

Definition at line 139 of file simplification.cc.

FixVariable()

void operations_research::sat::SatPostsolver::FixVariable

(

Literal

x

)

Definition at line 66 of file simplification.cc.

NumClauses()

int operations_research::sat::SatPostsolver::NumClauses ( ) const

inline

Definition at line 85 of file simplification.h.

operator=()

SatPostsolver & operations_research::sat::SatPostsolver::operator= ( const SatPostsolver & )

delete

PostsolveSolution()

std::vector< bool > operations_research::sat::SatPostsolver::PostsolveSolution

(

const std::vector< bool > &

solution

)

Definition at line 150 of file simplification.cc.

---

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

• ortools/sat/simplification.h
• ortools/sat/simplification.cc