Minisat::Clause Class Reference

#include <SolverTypes.h>

Collaboration diagram for Minisat::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)

Friends
class	ClauseAllocator

Detailed Description

Definition at line 125 of file SolverTypes.h.

Member Function Documentation

abstraction()

uint32_t Minisat::Clause::abstraction ( ) const

inline

Definition at line 184 of file SolverTypes.h.

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

Here is the caller graph for this function:

activity()

float & Minisat::Clause::activity ( )

inline

Definition at line 183 of file SolverTypes.h.

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

Here is the caller graph for this function:

calcAbstraction()

void Minisat::Clause::calcAbstraction ( )

inline

Definition at line 156 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:

has_extra()

bool Minisat::Clause::has_extra ( ) const

inline

Definition at line 168 of file SolverTypes.h.

{ return header.has_extra; }

last()

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

inline

Definition at line 171 of file SolverTypes.h.

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

learnt()

bool Minisat::Clause::learnt ( ) const

inline

Definition at line 167 of file SolverTypes.h.

{ return header.learnt; }

mark() [1/2]

uint32_t Minisat::Clause::mark ( ) const

inline

Definition at line 169 of file SolverTypes.h.

{ return header.mark; }

mark() [2/2]

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

inline

Definition at line 170 of file SolverTypes.h.

{ header.mark = m; }

operator const Lit *()

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

inline

Definition at line 181 of file SolverTypes.h.

{ return (Lit*)data; }

operator[]() [1/2]

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

inline

Definition at line 179 of file SolverTypes.h.

{ return data[i].lit; }

operator[]() [2/2]

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

inline

Definition at line 180 of file SolverTypes.h.

{ return data[i].lit; }

pop()

void Minisat::Clause::pop ( )

inline

Definition at line 166 of file SolverTypes.h.

{ shrink(1); }

Here is the call graph for this function:

relocate()

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

inline

Definition at line 175 of file SolverTypes.h.

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

Here is the caller graph for this function:

relocation()

CRef Minisat::Clause::relocation ( ) const

inline

Definition at line 174 of file SolverTypes.h.

{ return data[0].rel; }

Here is the caller graph for this function:

reloced()

bool Minisat::Clause::reloced ( ) const

inline

Definition at line 173 of file SolverTypes.h.

{ return header.reloced; }

shrink()

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

inline

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

inline

Definition at line 164 of file SolverTypes.h.

{ return header.size; }

strengthen()

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

inline

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

inline

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

Member Data Documentation

abs

uint32_t Minisat::Clause::abs

Definition at line 132 of file SolverTypes.h.

act

float Minisat::Clause::act

Definition at line 132 of file SolverTypes.h.

has_extra

unsigned Minisat::Clause::has_extra

Definition at line 129 of file SolverTypes.h.

learnt

unsigned Minisat::Clause::learnt

Definition at line 128 of file SolverTypes.h.

lit

Lit Minisat::Clause::lit

Definition at line 132 of file SolverTypes.h.

mark

unsigned Minisat::Clause::mark

Definition at line 127 of file SolverTypes.h.

rel

CRef Minisat::Clause::rel

Definition at line 132 of file SolverTypes.h.

reloced

unsigned Minisat::Clause::reloced

Definition at line 130 of file SolverTypes.h.

size

unsigned Minisat::Clause::size

Definition at line 131 of file SolverTypes.h.

---

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

• src/sat/bsat2/SolverTypes.h