#include <SimpSolver.h>

Collaboration diagram for Gluco::SimpSolver::ElimLt:

Public Member Functions
	ElimLt (const vec< int > &no)

uint64_t	cost (Var x) const

bool	operator() (Var x, Var y) const

Public Attributes
const vec< int > &	n_occ

Detailed Description

Definition at line 108 of file SimpSolver.h.

Constructor & Destructor Documentation

◆ ElimLt()

Gluco::SimpSolver::ElimLt::ElimLt ( const vec< int > & no )

inlineexplicit

Definition at line 110 of file SimpSolver.h.

110: n_occ(no) {}

Gluco::SimpSolver::ElimLt::n_occ

const vec< int > & n_occ

Definition SimpSolver.h:109

Member Function Documentation

◆ cost()

uint64_t Gluco::SimpSolver::ElimLt::cost ( Var x ) const

inline

Definition at line 114 of file SimpSolver.h.

114{ return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }

Gluco::toInt

int toInt(Var v)

Definition SolverTypes.h:74

Gluco::mkLit

Lit mkLit(Var var, bool sign=false)

Definition SolverTypes.h:67

Here is the call graph for this function:

Here is the caller graph for this function:

◆ operator()()

bool Gluco::SimpSolver::ElimLt::operator()	(	Var	x,
		Var	y ) const

inline

Definition at line 115 of file SimpSolver.h.

115{ return cost(x) < cost(y); }

Gluco::SimpSolver::ElimLt::cost

uint64_t cost(Var x) const

Definition SimpSolver.h:114

Here is the call graph for this function:

Member Data Documentation

◆ n_occ

const vec<int>& Gluco::SimpSolver::ElimLt::n_occ

Definition at line 109 of file SimpSolver.h.

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

src/sat/glucose/SimpSolver.h

Public Member Functions

Public Attributes