Minisat::Clause Class Reference

#include <SolverTypes.h>

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
template<class V >
	Clause (const V &ps, bool use_extra, bool learnt)

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 123 of file SolverTypes.h.

Constructor & Destructor Documentation

template<class V >

Minisat::Clause::Clause ( const V &  ps, bool  use_extra, bool  learnt  )

inlineprivate

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

Member Function Documentation

uint32_t Minisat::Clause::abstraction ( ) const

inline

Definition at line 182 of file SolverTypes.h.

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

float& Minisat::Clause::activity ( )

inline

Definition at line 181 of file SolverTypes.h.

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

void Minisat::Clause::calcAbstraction ( )

inline

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

bool Minisat::Clause::has_extra ( ) const

inline

Definition at line 166 of file SolverTypes.h.

{ return header.has_extra; }

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

inline

Definition at line 169 of file SolverTypes.h.

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

bool Minisat::Clause::learnt ( ) const

inline

Definition at line 165 of file SolverTypes.h.

{ return header.learnt; }

uint32_t Minisat::Clause::mark ( ) const

inline

Definition at line 167 of file SolverTypes.h.

{ return header.mark; }

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

inline

Definition at line 168 of file SolverTypes.h.

{ header.mark = m; }

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

inline

Definition at line 179 of file SolverTypes.h.

{ return (Lit*)data; }

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

inline

Definition at line 177 of file SolverTypes.h.

{ return data[i].lit; }

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

inline

Definition at line 178 of file SolverTypes.h.

{ return data[i].lit; }

void Minisat::Clause::pop ( )

inline

Definition at line 164 of file SolverTypes.h.

{ shrink(1); }

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

inline

Definition at line 173 of file SolverTypes.h.

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

CRef Minisat::Clause::relocation ( ) const

inline

Definition at line 172 of file SolverTypes.h.

{ return data[0].rel; }

bool Minisat::Clause::reloced ( ) const

inline

Definition at line 171 of file SolverTypes.h.

{ return header.reloced; }

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

inline

Definition at line 163 of file SolverTypes.h.

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

int Minisat::Clause::size ( ) const

inline

Definition at line 162 of file SolverTypes.h.

{ return header.size; }

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

inline

Definition at line 398 of file SolverTypes.h.

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

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

inline

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

Friends And Related Function Documentation

friend class ClauseAllocator

friend

Definition at line 132 of file SolverTypes.h.

Field Documentation

uint32_t Minisat::Clause::abs

Definition at line 130 of file SolverTypes.h.

float Minisat::Clause::act

Definition at line 130 of file SolverTypes.h.

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

unsigned Minisat::Clause::has_extra

Definition at line 127 of file SolverTypes.h.

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

unsigned Minisat::Clause::learnt

Definition at line 126 of file SolverTypes.h.

Lit Minisat::Clause::lit

Definition at line 130 of file SolverTypes.h.

unsigned Minisat::Clause::mark

Definition at line 125 of file SolverTypes.h.

CRef Minisat::Clause::rel

Definition at line 130 of file SolverTypes.h.

unsigned Minisat::Clause::reloced

Definition at line 128 of file SolverTypes.h.

unsigned Minisat::Clause::size

Definition at line 129 of file SolverTypes.h.

---

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

• SolverTypes.h