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)

Detailed Description

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

Definition at line 258 of file SolverTypes.h.

Constructor & Destructor Documentation

OccLists()

template<class Idx, class Vec, class Deleted>

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

inline

Definition at line 266 of file SolverTypes.h.

: deleted(d) {}

Member Function Documentation

clean()

template<class Idx, class Vec, class Deleted>

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

(

const Idx &

idx

)

Definition at line 302 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

cleanAll()

template<class Idx, class Vec, class Deleted>

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

(

)

Definition at line 291 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();
}

Here is the call graph for this function:

clear()

template<class Idx, class Vec, class Deleted>

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

inline

Definition at line 282 of file SolverTypes.h.

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

Here is the call graph for this function:

init()

template<class Idx, class Vec, class Deleted>

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

inline

Definition at line 268 of file SolverTypes.h.

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

Here is the call graph for this function:

lookup()

template<class Idx, class Vec, class Deleted>

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

inline

Definition at line 271 of file SolverTypes.h.

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

Here is the call graph for this function:

operator[]()

template<class Idx, class Vec, class Deleted>

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

inline

Definition at line 270 of file SolverTypes.h.

{ return occs[toInt(idx)]; }

Here is the call graph for this function:

smudge()

template<class Idx, class Vec, class Deleted>

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

inline

Definition at line 275 of file SolverTypes.h.

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

Here is the call graph for this function:

---

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

• src/sat/bsat2/SolverTypes.h