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)

Private Member Functions
	Clause (const vec< Lit > &ps, bool use_extra, bool learnt)
	Clause (const Clause &from, bool use_extra)

Private Attributes
struct {
unsigned   mark: 2
unsigned   learnt: 1
unsigned   has_extra: 1
unsigned   reloced: 1
unsigned   size: 27
}	header
union {
Lit   lit
float   act
uint32_t   abs
CRef   rel
}	data [0]

Friends
class	ClauseAllocator

Detailed Description

Definition at line 140 of file SolverTypes.h.

Constructor & Destructor Documentation

Minisat::Clause::Clause ( const vec< Lit > &  ps, bool  use_extra, bool  learnt  )

inlineprivate

Definition at line 152 of file SolverTypes.h.

                                                            {
        header.mark      = 0;
        header.learnt    = learnt;
        header.has_extra = use_extra;
        header.reloced   = 0;
        header.size      = ps.size();

        for (int i = 0; i < ps.size(); i++) 
            data[i].lit = ps[i];

        if (header.has_extra){
            if (header.learnt)
                data[header.size].act = 0;
            else
                calcAbstraction();
    }
    }

Here is the call graph for this function:

Minisat::Clause::Clause ( const Clause &  from, bool  use_extra  )

inlineprivate

Definition at line 171 of file SolverTypes.h.

                                              {
        header           = from.header;
        header.has_extra = use_extra;   // NOTE: the copied clause may lose the extra field.

        for (int i = 0; i < from.size(); i++)
            data[i].lit = from[i];

        if (header.has_extra){
            if (header.learnt)
                data[header.size].act = from.data[header.size].act;
            else 
                data[header.size].abs = from.data[header.size].abs;
    }
    }

Member Function Documentation

uint32_t Minisat::Clause::abstraction ( ) const

inline

Definition at line 215 of file SolverTypes.h.

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

Here is the caller graph for this function:

float& Minisat::Clause::activity ( )

inline

Definition at line 214 of file SolverTypes.h.

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

Here is the caller graph for this function:

void Minisat::Clause::calcAbstraction ( )

inline

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

bool Minisat::Clause::has_extra ( ) const

inline

Definition at line 199 of file SolverTypes.h.

{ return header.has_extra; }

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

inline

Definition at line 202 of file SolverTypes.h.

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

bool Minisat::Clause::learnt ( ) const

inline

Definition at line 198 of file SolverTypes.h.

{ return header.learnt; }

Here is the caller graph for this function:

uint32_t Minisat::Clause::mark ( ) const

inline

Definition at line 200 of file SolverTypes.h.

{ return header.mark; }

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

inline

Definition at line 201 of file SolverTypes.h.

{ header.mark = m; }

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

inline

Definition at line 212 of file SolverTypes.h.

{ return (Lit*)data; }

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

inline

Definition at line 210 of file SolverTypes.h.

{ return data[i].lit; }

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

inline

Definition at line 211 of file SolverTypes.h.

{ return data[i].lit; }

void Minisat::Clause::pop ( )

inline

Definition at line 197 of file SolverTypes.h.

{ shrink(1); }

Here is the call graph for this function:

Here is the caller graph for this function:

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

inline

Definition at line 206 of file SolverTypes.h.

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

Here is the caller graph for this function:

CRef Minisat::Clause::relocation ( ) const

inline

Definition at line 205 of file SolverTypes.h.

{ return data[0].rel; }

Here is the caller graph for this function:

bool Minisat::Clause::reloced ( ) const

inline

Definition at line 204 of file SolverTypes.h.

{ return header.reloced; }

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

inline

Definition at line 196 of file SolverTypes.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Minisat::Clause::size ( void  ) const

inline

Definition at line 195 of file SolverTypes.h.

{ return header.size; }

Here is the caller graph for this function:

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

inline

Definition at line 469 of file SolverTypes.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

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

inline

Definition at line 438 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 Function Documentation

friend class ClauseAllocator

friend

Definition at line 149 of file SolverTypes.h.

Field Documentation

uint32_t Minisat::Clause::abs

Definition at line 147 of file SolverTypes.h.

float Minisat::Clause::act

Definition at line 147 of file SolverTypes.h.

union { ... } Minisat::Clause::data[0]

unsigned Minisat::Clause::has_extra

Definition at line 144 of file SolverTypes.h.

struct { ... } Minisat::Clause::header

unsigned Minisat::Clause::learnt

Definition at line 143 of file SolverTypes.h.

Lit Minisat::Clause::lit

Definition at line 147 of file SolverTypes.h.

unsigned Minisat::Clause::mark

Definition at line 142 of file SolverTypes.h.

CRef Minisat::Clause::rel

Definition at line 147 of file SolverTypes.h.

unsigned Minisat::Clause::reloced

Definition at line 145 of file SolverTypes.h.

unsigned Minisat::Clause::size

Definition at line 146 of file SolverTypes.h.

---

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

• SolverTypes.h