Gluco2::Clause Class Reference

#include <SolverTypes.h>

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

Member Function Documentation

abstraction()

uint32_t Gluco2::Clause::abstraction ( ) const

inline

Definition at line 203 of file SolverTypes.h.

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

Here is the caller graph for this function:

activity()

float & Gluco2::Clause::activity ( )

inline

Definition at line 202 of file SolverTypes.h.

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

Here is the caller graph for this function:

calcAbstraction()

void Gluco2::Clause::calcAbstraction ( )

inline

Definition at line 175 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 Gluco2::Clause::canBeDel ( )

inline

Definition at line 211 of file SolverTypes.h.

{return header.canbedel;}

Here is the caller graph for this function:

has_extra()

bool Gluco2::Clause::has_extra ( ) const

inline

Definition at line 187 of file SolverTypes.h.

{ return header.has_extra; }

last()

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

inline

Definition at line 190 of file SolverTypes.h.

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

lbd()

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

inline

Definition at line 209 of file SolverTypes.h.

{ return header.lbd; }

learnt()

bool Gluco2::Clause::learnt ( ) const

inline

Definition at line 186 of file SolverTypes.h.

{ return header.learnt; }

mark() [1/2]

uint32_t Gluco2::Clause::mark ( ) const

inline

Definition at line 188 of file SolverTypes.h.

{ return header.mark; }

mark() [2/2]

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

inline

Definition at line 189 of file SolverTypes.h.

{ header.mark = m; }

operator const Lit *()

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

inline

Definition at line 200 of file SolverTypes.h.

{ return (Lit*)data; }

operator[]() [1/2]

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

inline

Definition at line 198 of file SolverTypes.h.

{ return data[i].lit; }

operator[]() [2/2]

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

inline

Definition at line 199 of file SolverTypes.h.

{ return data[i].lit; }

pop()

void Gluco2::Clause::pop ( )

inline

Definition at line 185 of file SolverTypes.h.

{ shrink(1); }

Here is the call graph for this function:

relocate()

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

inline

Definition at line 194 of file SolverTypes.h.

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

Here is the caller graph for this function:

relocation()

CRef Gluco2::Clause::relocation ( ) const

inline

Definition at line 193 of file SolverTypes.h.

{ return data[0].rel; }

Here is the caller graph for this function:

reloced()

bool Gluco2::Clause::reloced ( ) const

inline

Definition at line 192 of file SolverTypes.h.

{ return header.reloced; }

setCanBeDel()

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

inline

Definition at line 210 of file SolverTypes.h.

{header.canbedel = b;}

Here is the caller graph for this function:

setLBD()

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

inline

Definition at line 207 of file SolverTypes.h.

{header.lbd = i;} 

Here is the caller graph for this function:

setSizeWithoutSelectors()

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

inline

Definition at line 212 of file SolverTypes.h.

{header.szWithoutSelectors = n; }

shrink()

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

inline

Definition at line 184 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 Gluco2::Clause::size ( ) const

inline

Definition at line 183 of file SolverTypes.h.

{ return header.size; }

sizeWithoutSelectors()

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

inline

Definition at line 213 of file SolverTypes.h.

{ return header.szWithoutSelectors; }

Here is the caller graph for this function:

strengthen()

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

inline

Definition at line 439 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 Gluco2::Clause::subsumes ( const Clause & other ) const

inline

Definition at line 408 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 148 of file SolverTypes.h.

Member Data Documentation

abs

uint32_t Gluco2::Clause::abs

Definition at line 146 of file SolverTypes.h.

act

float Gluco2::Clause::act

Definition at line 146 of file SolverTypes.h.

canbedel

unsigned Gluco2::Clause::canbedel

Definition at line 141 of file SolverTypes.h.

has_extra

unsigned Gluco2::Clause::has_extra

Definition at line 138 of file SolverTypes.h.

lbd

unsigned Gluco2::Clause::lbd

Definition at line 140 of file SolverTypes.h.

learnt

unsigned Gluco2::Clause::learnt

Definition at line 137 of file SolverTypes.h.

lit

Lit Gluco2::Clause::lit

Definition at line 146 of file SolverTypes.h.

mark

unsigned Gluco2::Clause::mark

Definition at line 136 of file SolverTypes.h.

rel

CRef Gluco2::Clause::rel

Definition at line 146 of file SolverTypes.h.

reloced

unsigned Gluco2::Clause::reloced

Definition at line 139 of file SolverTypes.h.

size

unsigned Gluco2::Clause::size

Definition at line 142 of file SolverTypes.h.

szWithoutSelectors

unsigned Gluco2::Clause::szWithoutSelectors

Definition at line 143 of file SolverTypes.h.

---

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

• src/sat/glucose2/SolverTypes.h