CaDiCaL::Clause Struct Reference

#include <clause.hpp>

Collaboration diagram for CaDiCaL::Clause:

Public Member Functions
literal_iterator	begin ()
literal_iterator	end ()
const_literal_iterator	begin () const
const_literal_iterator	end () const
size_t	bytes () const
bool	collect () const

Static Public Member Functions
static size_t	bytes (int size)

Public Attributes
union {
int64_t   id
Clause *   copy
};
bool	conditioned: 1
bool	covered: 1
bool	enqueued: 1
bool	frozen: 1
bool	garbage: 1
bool	gate: 1
bool	hyper: 1
bool	instantiated: 1
bool	moved: 1
bool	reason: 1
bool	redundant: 1
bool	transred: 1
bool	subsume: 1
bool	swept: 1
bool	flushed: 1
unsigned	used: 8
bool	vivified: 1
bool	vivify: 1
int	glue
int	size
int	pos
int	literals []

Detailed Description

Definition at line 34 of file clause.hpp.

Member Function Documentation

begin() [1/2]

literal_iterator CaDiCaL::Clause::begin ( )

inline

Definition at line 131 of file clause.hpp.

{ return literals; }

Here is the caller graph for this function:

begin() [2/2]

const_literal_iterator CaDiCaL::Clause::begin ( ) const

inline

Definition at line 134 of file clause.hpp.

{ return literals; }

bytes() [1/2]

size_t CaDiCaL::Clause::bytes ( ) const

inline

Definition at line 157 of file clause.hpp.

{ return bytes (size); }

Here is the call graph for this function:

Here is the caller graph for this function:

bytes() [2/2]

static size_t CaDiCaL::Clause::bytes ( int size )

inlinestatic

Definition at line 137 of file clause.hpp.

                                 {
 
    // Memory sanitizer insists that clauses put into consecutive memory in
    // the arena are still 8 byte aligned.  We could also allocate 8 byte
    // aligned memory there.  However, assuming the real memory foot print
    // of a clause is 8 bytes anyhow, we just allocate 8 byte aligned memory
    // all the time (even if allocated outside of the arena).
    //
    CADICAL_assert (size > 1);
    const size_t header_bytes = sizeof (Clause);
    const size_t actual_literal_bytes = size * sizeof (int);
    size_t combined_bytes = header_bytes + actual_literal_bytes;
#ifdef NFLEXIBLE
    const size_t faked_literals_bytes = sizeof ((Clause *) 0)->literals;
    combined_bytes -= faked_literals_bytes;
#endif
    size_t aligned_bytes = align (combined_bytes, 8);
    return aligned_bytes;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

collect()

bool CaDiCaL::Clause::collect ( ) const

inline

Definition at line 166 of file clause.hpp.

{ return !reason && garbage; }

Here is the caller graph for this function:

end() [1/2]

literal_iterator CaDiCaL::Clause::end ( )

inline

Definition at line 132 of file clause.hpp.

{ return literals + size; }

Here is the caller graph for this function:

end() [2/2]

const_literal_iterator CaDiCaL::Clause::end ( ) const

inline

Definition at line 135 of file clause.hpp.

{ return literals + size; }

Member Data Documentation

[union]

union { ... } CaDiCaL::Clause

conditioned

bool CaDiCaL::Clause::conditioned

Definition at line 44 of file clause.hpp.

copy

Clause* CaDiCaL::Clause::copy

Definition at line 37 of file clause.hpp.

covered

bool CaDiCaL::Clause::covered

Definition at line 45 of file clause.hpp.

enqueued

bool CaDiCaL::Clause::enqueued

Definition at line 46 of file clause.hpp.

flushed

bool CaDiCaL::Clause::flushed

Definition at line 58 of file clause.hpp.

frozen

bool CaDiCaL::Clause::frozen

Definition at line 47 of file clause.hpp.

garbage

bool CaDiCaL::Clause::garbage

Definition at line 48 of file clause.hpp.

gate

bool CaDiCaL::Clause::gate

Definition at line 49 of file clause.hpp.

glue

int CaDiCaL::Clause::glue

Definition at line 97 of file clause.hpp.

hyper

bool CaDiCaL::Clause::hyper

Definition at line 50 of file clause.hpp.

id

int64_t CaDiCaL::Clause::id

Definition at line 36 of file clause.hpp.

instantiated

bool CaDiCaL::Clause::instantiated

Definition at line 51 of file clause.hpp.

literals

int CaDiCaL::Clause::literals[]

Definition at line 124 of file clause.hpp.

moved

bool CaDiCaL::Clause::moved

Definition at line 52 of file clause.hpp.

pos

int CaDiCaL::Clause::pos

Definition at line 100 of file clause.hpp.

reason

bool CaDiCaL::Clause::reason

Definition at line 53 of file clause.hpp.

redundant

bool CaDiCaL::Clause::redundant

Definition at line 54 of file clause.hpp.

size

int CaDiCaL::Clause::size

Definition at line 99 of file clause.hpp.

subsume

bool CaDiCaL::Clause::subsume

Definition at line 56 of file clause.hpp.

swept

bool CaDiCaL::Clause::swept

Definition at line 57 of file clause.hpp.

transred

bool CaDiCaL::Clause::transred

Definition at line 55 of file clause.hpp.

used

unsigned CaDiCaL::Clause::used

Definition at line 59 of file clause.hpp.

vivified

bool CaDiCaL::Clause::vivified

Definition at line 60 of file clause.hpp.

vivify

bool CaDiCaL::Clause::vivify

Definition at line 61 of file clause.hpp.

---

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

• src/sat/cadical/clause.hpp