Minisat::OccLists< K, Vec, Deleted, MkIndex > Class Template Reference

#include <SolverTypes.h>

Collaboration diagram for Minisat::OccLists< K, Vec, Deleted, MkIndex >:

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

Private Attributes
IntMap< K, Vec, MkIndex >	occs
IntMap< K, char, MkIndex >	dirty
vec< K >	dirties
Deleted	deleted

Detailed Description

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>
class Minisat::OccLists< K, Vec, Deleted, MkIndex >

Definition at line 325 of file SolverTypes.h.

Constructor & Destructor Documentation

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

Minisat::OccLists< K, Vec, Deleted, MkIndex >::OccLists ( const Deleted &  d, MkIndex  _index = MkIndex()  )

inline

Definition at line 333 of file SolverTypes.h.

                                                           :
        occs(_index), 
        dirty(_index), 
        deleted(d){}

Member Function Documentation

template<class K, class Vec , class Deleted , class MkIndex >

void Minisat::OccLists< K, Vec, Deleted, MkIndex >::clean

(

const K &

idx

)

Definition at line 371 of file SolverTypes.h.

{
    Vec& vec = occs[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[idx] = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

template<class K , class Vec , class Deleted , class MkIndex >

void Minisat::OccLists< K, Vec, Deleted, MkIndex >::cleanAll

(

)

Definition at line 360 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[dirties[i]])
            clean(dirties[i]);
    dirties.clear();
}

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

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

inline

Definition at line 351 of file SolverTypes.h.

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

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

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

inline

Definition at line 338 of file SolverTypes.h.

{ occs.reserve(idx); occs[idx].clear(); dirty.reserve(idx, 0); }

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

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

inline

Definition at line 340 of file SolverTypes.h.

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

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

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

inline

Definition at line 339 of file SolverTypes.h.

{ return occs[idx]; }

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

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

inline

Definition at line 344 of file SolverTypes.h.

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

Field Documentation

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

Deleted Minisat::OccLists< K, Vec, Deleted, MkIndex >::deleted

private

Definition at line 330 of file SolverTypes.h.

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

vec<K> Minisat::OccLists< K, Vec, Deleted, MkIndex >::dirties

private

Definition at line 329 of file SolverTypes.h.

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

IntMap<K, char, MkIndex> Minisat::OccLists< K, Vec, Deleted, MkIndex >::dirty

private

Definition at line 328 of file SolverTypes.h.

template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K>>

IntMap<K, Vec, MkIndex> Minisat::OccLists< K, Vec, Deleted, MkIndex >::occs

private

Definition at line 327 of file SolverTypes.h.

---

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

• SolverTypes.h