#include <SimpSolver.h>

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

Constructor & Destructor Documentation

◆ ElimLt()

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

inlineexplicit

Definition at line 125 of file SimpSolver.h.

125: n_occ(no) {}

Gluco2::SimpSolver::ElimLt::n_occ

const vec< int > & n_occ

Definition SimpSolver.h:124

Member Function Documentation

◆ cost()

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

inline

Definition at line 129 of file SimpSolver.h.

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

Gluco2::mkLit

Lit mkLit(Var var, bool sign=false)

Definition SolverTypes.h:69

Gluco2::toInt

int toInt(Var v)

Definition SolverTypes.h:76

Here is the call graph for this function:

Here is the caller graph for this function:

◆ operator()()

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

inline

Definition at line 130 of file SimpSolver.h.

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

Gluco2::SimpSolver::ElimLt::cost

uint64_t cost(Var x) const

Definition SimpSolver.h:129

Here is the call graph for this function:

Member Data Documentation

◆ n_occ

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

Definition at line 124 of file SimpSolver.h.

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

src/sat/glucose2/SimpSolver.h

Public Member Functions

Public Attributes