Gluco::Clause Class Reference

#include <SolverTypes.h>

Collaboration diagram for Gluco::Clause:

Public Member Functions
void	calcAbstraction ()
int	size () const
void	shrink (int i)
void	pop ()
bool	learnt () const
bool	has_extra () const
uint32_t	mark () const
void	mark (uint32_t m)
const Lit &	last () const
bool	reloced () const
CRef	relocation () const
void	relocate (CRef c)
Lit &	operator[] (int i)
Lit	operator[] (int i) const
	operator const Lit * (void) const
float &	activity ()
uint32_t	abstraction () const
Lit	subsumes (const Clause &other) const
void	strengthen (Lit p)
void	setLBD (int i)
unsigned int	lbd () const
void	setCanBeDel (bool b)
bool	canBeDel ()
void	setSizeWithoutSelectors (unsigned int n)
unsigned int	sizeWithoutSelectors () const

Friends
class	ClauseAllocator

Detailed Description

Definition at line 132 of file SolverTypes.h.

Member Function Documentation

abstraction()

uint32_t Gluco::Clause::abstraction ( ) const

inline

Definition at line 197 of file SolverTypes.h.

{ assert(header.has_extra); return data[header.size].abs; }

Here is the caller graph for this function:

activity()

float & Gluco::Clause::activity ( )

inline

Definition at line 196 of file SolverTypes.h.

{ assert(header.has_extra); return data[header.size].act; }

Here is the caller graph for this function:

calcAbstraction()

void Gluco::Clause::calcAbstraction ( )

inline

Definition at line 169 of file SolverTypes.h.

                           {
        assert(header.has_extra);
        uint32_t abstraction = 0;
        for (int i = 0; i < size(); i++)
            abstraction |= 1 << (var(data[i].lit) & 31);
        data[header.size].abs = abstraction;  }

Here is the call graph for this function:

Here is the caller graph for this function:

canBeDel()

bool Gluco::Clause::canBeDel ( )

inline

Definition at line 205 of file SolverTypes.h.

{return header.canbedel;}

Here is the caller graph for this function:

has_extra()

bool Gluco::Clause::has_extra ( ) const

inline

Definition at line 181 of file SolverTypes.h.

{ return header.has_extra; }

last()

const Lit & Gluco::Clause::last ( ) const

inline

Definition at line 184 of file SolverTypes.h.

{ return data[header.size-1].lit; }

lbd()

unsigned int Gluco::Clause::lbd ( ) const

inline

Definition at line 203 of file SolverTypes.h.

{ return header.lbd; }

learnt()

bool Gluco::Clause::learnt ( ) const

inline

Definition at line 180 of file SolverTypes.h.

{ return header.learnt; }

mark() [1/2]

uint32_t Gluco::Clause::mark ( ) const

inline

Definition at line 182 of file SolverTypes.h.

{ return header.mark; }

mark() [2/2]

void Gluco::Clause::mark ( uint32_t m )

inline

Definition at line 183 of file SolverTypes.h.

{ header.mark = m; }

operator const Lit *()

Gluco::Clause::operator const Lit * ( void ) const

inline

Definition at line 194 of file SolverTypes.h.

{ return (Lit*)data; }

operator[]() [1/2]

Lit & Gluco::Clause::operator[] ( int i )

inline

Definition at line 192 of file SolverTypes.h.

{ return data[i].lit; }

operator[]() [2/2]

Lit Gluco::Clause::operator[] ( int i ) const

inline

Definition at line 193 of file SolverTypes.h.

{ return data[i].lit; }

pop()

void Gluco::Clause::pop ( )

inline

Definition at line 179 of file SolverTypes.h.

{ shrink(1); }

Here is the call graph for this function:

relocate()

void Gluco::Clause::relocate ( CRef c )

inline

Definition at line 188 of file SolverTypes.h.

{ header.reloced = 1; data[0].rel = c; }

Here is the caller graph for this function:

relocation()

CRef Gluco::Clause::relocation ( ) const

inline

Definition at line 187 of file SolverTypes.h.

{ return data[0].rel; }

Here is the caller graph for this function:

reloced()

bool Gluco::Clause::reloced ( ) const

inline

Definition at line 186 of file SolverTypes.h.

{ return header.reloced; }

setCanBeDel()

void Gluco::Clause::setCanBeDel ( bool b )

inline

Definition at line 204 of file SolverTypes.h.

{header.canbedel = b;}

Here is the caller graph for this function:

setLBD()

void Gluco::Clause::setLBD ( int i )

inline

Definition at line 201 of file SolverTypes.h.

{header.lbd = i;} 

Here is the caller graph for this function:

setSizeWithoutSelectors()

void Gluco::Clause::setSizeWithoutSelectors ( unsigned int n )

inline

Definition at line 206 of file SolverTypes.h.

{header.szWithoutSelectors = n; }

shrink()

void Gluco::Clause::shrink ( int i )

inline

Definition at line 178 of file SolverTypes.h.

{ assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }

Here is the caller graph for this function:

size()

int Gluco::Clause::size ( ) const

inline

Definition at line 177 of file SolverTypes.h.

{ return header.size; }

sizeWithoutSelectors()

unsigned int Gluco::Clause::sizeWithoutSelectors ( ) const

inline

Definition at line 207 of file SolverTypes.h.

{ return header.szWithoutSelectors; }

Here is the caller graph for this function:

strengthen()

void Gluco::Clause::strengthen ( Lit p )

inline

Definition at line 432 of file SolverTypes.h.

{
    remove(*this, p);
    calcAbstraction();
}

Here is the call graph for this function:

Here is the caller graph for this function:

subsumes()

Lit Gluco::Clause::subsumes ( const Clause & other ) const

inline

Definition at line 401 of file SolverTypes.h.

{
    //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
    //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
    assert(!header.learnt);   assert(!other.header.learnt);
    assert(header.has_extra); assert(other.header.has_extra);
    if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
        return lit_Error;
 
    Lit        ret = lit_Undef;
    const Lit* c   = (const Lit*)(*this);
    const Lit* d   = (const Lit*)other;
 
    for (unsigned i = 0; i < header.size; i++) {
        // search for c[i] or ~c[i]
        for (unsigned j = 0; j < other.header.size; j++)
            if (c[i] == d[j])
                goto ok;
            else if (ret == lit_Undef && c[i] == ~d[j]){
                ret = c[i];
                goto ok;
            }
 
        // did not find it
        return lit_Error;
    ok:;
    }
 
    return ret;
}

Here is the caller graph for this function:

Friends And Related Symbol Documentation

ClauseAllocator

friend class ClauseAllocator

friend

Definition at line 146 of file SolverTypes.h.

Member Data Documentation

abs

uint32_t Gluco::Clause::abs

Definition at line 144 of file SolverTypes.h.

act

float Gluco::Clause::act

Definition at line 144 of file SolverTypes.h.

canbedel

unsigned Gluco::Clause::canbedel

Definition at line 139 of file SolverTypes.h.

has_extra

unsigned Gluco::Clause::has_extra

Definition at line 136 of file SolverTypes.h.

lbd

unsigned Gluco::Clause::lbd

Definition at line 138 of file SolverTypes.h.

learnt

unsigned Gluco::Clause::learnt

Definition at line 135 of file SolverTypes.h.

lit

Lit Gluco::Clause::lit

Definition at line 144 of file SolverTypes.h.

mark

unsigned Gluco::Clause::mark

Definition at line 134 of file SolverTypes.h.

rel

CRef Gluco::Clause::rel

Definition at line 144 of file SolverTypes.h.

reloced

unsigned Gluco::Clause::reloced

Definition at line 137 of file SolverTypes.h.

size

unsigned Gluco::Clause::size

Definition at line 140 of file SolverTypes.h.

szWithoutSelectors

unsigned Gluco::Clause::szWithoutSelectors

Definition at line 141 of file SolverTypes.h.

---

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

• src/sat/glucose/SolverTypes.h