CaDiCaL::sort_assumptions_positive_rank Struct Reference

Collaboration diagram for CaDiCaL::sort_assumptions_positive_rank:

Public Types
typedef uint64_t	Type

Public Member Functions
	sort_assumptions_positive_rank (Internal *s)
Type	operator() (const int &a) const

Public Attributes
Internal *	internal
const unsigned	max_level

Detailed Description

Definition at line 515 of file cadical_assume.cpp.

Member Typedef Documentation

Type

typedef uint64_t CaDiCaL::sort_assumptions_positive_rank::Type

Definition at line 526 of file cadical_assume.cpp.

Constructor & Destructor Documentation

sort_assumptions_positive_rank()

CaDiCaL::sort_assumptions_positive_rank::sort_assumptions_positive_rank ( Internal * s )

inline

Definition at line 523 of file cadical_assume.cpp.

      : internal (s), max_level (s->level + 1u) {}

Member Function Documentation

operator()()

Type CaDiCaL::sort_assumptions_positive_rank::operator() ( const int & a ) const

inline

Definition at line 531 of file cadical_assume.cpp.

                                       {
    const int val = internal->val (a);
    const bool assigned = (val != 0);
    const Var &v = internal->var (a);
    uint64_t res = (assigned ? (unsigned) v.level : max_level);
    res <<= 32;
    res |= (assigned ? v.trail : abs (a));
    return res;
  }

Member Data Documentation

internal

Internal* CaDiCaL::sort_assumptions_positive_rank::internal

Definition at line 516 of file cadical_assume.cpp.

max_level

const unsigned CaDiCaL::sort_assumptions_positive_rank::max_level

Definition at line 521 of file cadical_assume.cpp.

---

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

• src/sat/cadical/cadical_assume.cpp