#include <SimpSolver.h>

Collaboration diagram for Minisat::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 104 of file SimpSolver.h.

Constructor & Destructor Documentation

◆ ElimLt()

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

inlineexplicit

Definition at line 106 of file SimpSolver.h.

106: n_occ(no) {}

Minisat::SimpSolver::ElimLt::n_occ

const vec< int > & n_occ

Definition SimpSolver.h:105

Member Function Documentation

◆ cost()

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

inline

Definition at line 110 of file SimpSolver.h.

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

Minisat::toInt

int toInt(Var v)

Definition SolverTypes.h:67

Minisat::mkLit

Lit mkLit(Var var, bool sign=false)

Definition SolverTypes.h:60

Here is the call graph for this function:

Here is the caller graph for this function:

◆ operator()()

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

inline

Definition at line 111 of file SimpSolver.h.

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

Minisat::SimpSolver::ElimLt::cost

uint64_t cost(Var x) const

Definition SimpSolver.h:110

Here is the call graph for this function:

Member Data Documentation

◆ n_occ

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

Definition at line 105 of file SimpSolver.h.

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

src/sat/bsat2/SimpSolver.h

Public Member Functions

Public Attributes