operations_research::sat::SatPresolver Class Reference

Detailed Description

Definition at line 148 of file simplification.h.

#include <simplification.h>

Public Types
typedef int32_t	ClauseIndex

Public Member Functions
	SatPresolver (SatPostsolver *postsolver, SolverLogger *logger)
	SatPresolver (const SatPresolver &)=delete
SatPresolver &	operator= (const SatPresolver &)=delete
void	SetParameters (const SatParameters &params)
void	SetTimeLimit (TimeLimit *time_limit)
void	SetEquivalentLiteralMapping (const util_intops::StrongVector< LiteralIndex, LiteralIndex > &mapping)
void	SetNumVariables (int num_variables)
void	AddBinaryClause (Literal a, Literal b)
void	AddClause (absl::Span< const Literal > clause)
bool	Presolve ()
bool	Presolve (const std::vector< bool > &var_that_can_be_removed)
int	NumClauses () const
const std::vector< Literal > &	Clause (ClauseIndex ci) const
int	NumVariables () const
util_intops::StrongVector< BooleanVariable, BooleanVariable >	VariableMapping () const
void	LoadProblemIntoSatSolver (SatSolver *solver)
bool	ProcessClauseToSimplifyOthers (ClauseIndex clause_index)
bool	CrossProduct (Literal x)
void	PresolveWithBva ()

Member Typedef Documentation

ClauseIndex

typedef int32_t operations_research::sat::SatPresolver::ClauseIndex

Definition at line 151 of file simplification.h.

Constructor & Destructor Documentation

SatPresolver() [1/2]

operations_research::sat::SatPresolver::SatPresolver ( SatPostsolver * postsolver, SolverLogger * logger )

inlineexplicit

Definition at line 153 of file simplification.h.

SatPresolver() [2/2]

operations_research::sat::SatPresolver::SatPresolver ( const SatPresolver & )

delete

Member Function Documentation

AddBinaryClause()

void operations_research::sat::SatPresolver::AddBinaryClause	(	Literal	a,
		Literal	b )

Definition at line 169 of file simplification.cc.

AddClause()

void operations_research::sat::SatPresolver::AddClause

(

absl::Span< const Literal >

clause

)

Definition at line 171 of file simplification.cc.

Clause()

const std::vector< Literal > & operations_research::sat::SatPresolver::Clause ( ClauseIndex ci ) const

inline

Definition at line 189 of file simplification.h.

CrossProduct()

bool operations_research::sat::SatPresolver::CrossProduct

(

Literal

x

)

Definition at line 722 of file simplification.cc.

LoadProblemIntoSatSolver()

void operations_research::sat::SatPresolver::LoadProblemIntoSatSolver

(

SatSolver *

solver

)

Definition at line 276 of file simplification.cc.

NumClauses()

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

inline

Definition at line 188 of file simplification.h.

NumVariables()

int operations_research::sat::SatPresolver::NumVariables ( ) const

inline

Definition at line 195 of file simplification.h.

operator=()

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

delete

Presolve() [1/2]

bool operations_research::sat::SatPresolver::Presolve

(

)

Definition at line 334 of file simplification.cc.

Presolve() [2/2]

bool operations_research::sat::SatPresolver::Presolve

(

const std::vector< bool > &

var_that_can_be_removed

)

Definition at line 341 of file simplification.cc.

PresolveWithBva()

void operations_research::sat::SatPresolver::PresolveWithBva

(

)

Definition at line 393 of file simplification.cc.

ProcessClauseToSimplifyOthers()

bool operations_research::sat::SatPresolver::ProcessClauseToSimplifyOthers

(

ClauseIndex

clause_index

)

Definition at line 641 of file simplification.cc.

SetEquivalentLiteralMapping()

void operations_research::sat::SatPresolver::SetEquivalentLiteralMapping ( const util_intops::StrongVector< LiteralIndex, LiteralIndex > & mapping )

inline

Definition at line 165 of file simplification.h.

SetNumVariables()

void operations_research::sat::SatPresolver::SetNumVariables

(

int

num_variables

)

Definition at line 221 of file simplification.cc.

SetParameters()

void operations_research::sat::SatPresolver::SetParameters ( const SatParameters & params )

inline

Definition at line 160 of file simplification.h.

SetTimeLimit()

void operations_research::sat::SatPresolver::SetTimeLimit ( TimeLimit * time_limit )

inline

Definition at line 161 of file simplification.h.

VariableMapping()

util_intops::StrongVector< BooleanVariable, BooleanVariable > operations_research::sat::SatPresolver::VariableMapping

(

)

const

Definition at line 261 of file simplification.cc.

---

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

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