Minisat::OccLists< Idx, Vec, Deleted > Class Template Reference

#include <SolverTypes.h>

Public Member Functions
	OccLists (const Deleted &d)
void	init (const Idx &idx)
Vec &	operator[] (const Idx &idx)
Vec &	lookup (const Idx &idx)
void	cleanAll ()
void	clean (const Idx &idx)
void	smudge (const Idx &idx)
void	clear (bool free=true)

Private Attributes
vec< Vec >	occs
vec< char >	dirty
vec< Idx >	dirties
Deleted	deleted

Detailed Description

template<class Idx, class Vec, class Deleted>
class Minisat::OccLists< Idx, Vec, Deleted >

Definition at line 256 of file SolverTypes.h.

Constructor & Destructor Documentation

template<class Idx, class Vec, class Deleted>

Minisat::OccLists< Idx, Vec, Deleted >::OccLists ( const Deleted &  d )

inline

Definition at line 264 of file SolverTypes.h.

: deleted(d) {}

Member Function Documentation

template<class Idx, class Vec , class Deleted >

void Minisat::OccLists< Idx, Vec, Deleted >::clean

(

const Idx &

idx

)

Definition at line 300 of file SolverTypes.h.

{
    Vec& vec = occs[toInt(idx)];
    int  i, j;
    for (i = j = 0; i < vec.size(); i++)
        if (!deleted(vec[i]))
            vec[j++] = vec[i];
    vec.shrink(i - j);
    dirty[toInt(idx)] = 0;
}

template<class Idx , class Vec , class Deleted >

void Minisat::OccLists< Idx, Vec, Deleted >::cleanAll

(

)

Definition at line 289 of file SolverTypes.h.

{
    for (int i = 0; i < dirties.size(); i++)
        // Dirties may contain duplicates so check here if a variable is already cleaned:
        if (dirty[toInt(dirties[i])])
            clean(dirties[i]);
    dirties.clear();
}

template<class Idx, class Vec, class Deleted>

void Minisat::OccLists< Idx, Vec, Deleted >::clear ( bool  free = true )

inline

Definition at line 280 of file SolverTypes.h.

                                 {
        occs   .clear(free);
        dirty  .clear(free);
        dirties.clear(free);
    }

template<class Idx, class Vec, class Deleted>

void Minisat::OccLists< Idx, Vec, Deleted >::init ( const Idx &  idx )

inline

Definition at line 266 of file SolverTypes.h.

{ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }

template<class Idx, class Vec, class Deleted>

Vec& Minisat::OccLists< Idx, Vec, Deleted >::lookup ( const Idx &  idx )

inline

Definition at line 269 of file SolverTypes.h.

{ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }

template<class Idx, class Vec, class Deleted>

Vec& Minisat::OccLists< Idx, Vec, Deleted >::operator[] ( const Idx &  idx )

inline

Definition at line 268 of file SolverTypes.h.

{ return occs[toInt(idx)]; }

template<class Idx, class Vec, class Deleted>

void Minisat::OccLists< Idx, Vec, Deleted >::smudge ( const Idx &  idx )

inline

Definition at line 273 of file SolverTypes.h.

                                    {
        if (dirty[toInt(idx)] == 0){
            dirty[toInt(idx)] = 1;
            dirties.push(idx);
        }
    }

Field Documentation

template<class Idx, class Vec, class Deleted>

Deleted Minisat::OccLists< Idx, Vec, Deleted >::deleted

private

Definition at line 261 of file SolverTypes.h.

template<class Idx, class Vec, class Deleted>

vec<Idx> Minisat::OccLists< Idx, Vec, Deleted >::dirties

private

Definition at line 260 of file SolverTypes.h.

template<class Idx, class Vec, class Deleted>

vec<char> Minisat::OccLists< Idx, Vec, Deleted >::dirty

private

Definition at line 259 of file SolverTypes.h.

template<class Idx, class Vec, class Deleted>

vec<Vec> Minisat::OccLists< Idx, Vec, Deleted >::occs

private

Definition at line 258 of file SolverTypes.h.

---

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

• SolverTypes.h