CaDiCaL::Mapper Struct Reference

Collaboration diagram for CaDiCaL::Mapper:

Public Member Functions
	Mapper (Internal *i)
	~Mapper ()
int	map_idx (int src)
int	map_lit (int src)
template<class T>
void	map_vector (vector< T > &v)
template<class T>
void	map2_vector (vector< T > &v)
void	map_flush_and_shrink_lits (vector< int > &v)

Public Attributes
Internal *	internal
int	new_max_var
int *	table
int	first_fixed
int	map_first_fixed
signed char	first_fixed_val
size_t	new_vsize

Detailed Description

Definition at line 35 of file cadical_compact.cpp.

Constructor & Destructor Documentation

Mapper()

CaDiCaL::Mapper::Mapper ( Internal * i )

inline

Definition at line 53 of file cadical_compact.cpp.

      : internal (i), new_max_var (0), first_fixed (0), map_first_fixed (0),
        first_fixed_val (0) {
    table = new int[internal->max_var + 1u];
    clear_n (table, internal->max_var + 1u);
 
    CADICAL_assert (!internal->level);
 
    for (auto src : internal->vars) {
      const Flags &f = internal->flags (src);
      if (f.active ())
        table[src] = ++new_max_var;
      else if (f.fixed () && !first_fixed)
        table[first_fixed = src] = map_first_fixed = ++new_max_var;
    }
 
    first_fixed_val = first_fixed ? internal->val (first_fixed) : 0;
    new_vsize = new_max_var + 1u;
  }

Here is the call graph for this function:

~Mapper()

CaDiCaL::Mapper::~Mapper ( )

inline

Definition at line 73 of file cadical_compact.cpp.

{ delete[] table; }

Member Function Documentation

map2_vector()

template<class T>

void CaDiCaL::Mapper::map2_vector ( vector< T > & v )

inline

Definition at line 126 of file cadical_compact.cpp.

                                                     {
    for (auto src : internal->vars) {
      const int dst = map_idx (src);
      if (!dst)
        continue;
      CADICAL_assert (0 < dst);
      CADICAL_assert (dst <= src);
      v[2 * dst] = v[2 * src];
      v[2 * dst + 1] = v[2 * src + 1];
    }
    v.resize (2 * new_vsize);
    shrink_vector (v);
  }

Here is the call graph for this function:

Here is the caller graph for this function:

map_flush_and_shrink_lits()

void CaDiCaL::Mapper::map_flush_and_shrink_lits ( vector< int > & v )

inline

Definition at line 144 of file cadical_compact.cpp.

                                                  {
    const auto end = v.end ();
    auto j = v.begin (), i = j;
    for (; i != end; i++) {
      const int src = *i;
      int dst = map_idx (abs (src));
      CADICAL_assert (abs (dst) <= abs (src));
      if (!dst)
        continue;
      if (src < 0)
        dst = -dst;
      *j++ = dst;
    }
    v.resize (j - v.begin ());
    shrink_vector (v);
  }

Here is the call graph for this function:

Here is the caller graph for this function:

map_idx()

int CaDiCaL::Mapper::map_idx ( int src )

inline

Definition at line 78 of file cadical_compact.cpp.

                        {
    CADICAL_assert (0 < src);
    CADICAL_assert (src <= internal->max_var);
    const int res = table[src];
    CADICAL_assert (res <= new_max_var);
    return res;
  }

Here is the caller graph for this function:

map_lit()

int CaDiCaL::Mapper::map_lit ( int src )

inline

Definition at line 91 of file cadical_compact.cpp.

                        {
    int res = map_idx (abs (src));
    if (!res) {
      const signed char tmp = internal->val (src);
      if (tmp) {
        CADICAL_assert (first_fixed);
        res = map_first_fixed;
        if (tmp != first_fixed_val)
          res = -res;
      }
    } else if ((src) < 0)
      res = -res;
    CADICAL_assert (abs (res) <= new_max_var);
    return res;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

map_vector()

template<class T>

void CaDiCaL::Mapper::map_vector ( vector< T > & v )

inline

Definition at line 110 of file cadical_compact.cpp.

                                                    {
    for (auto src : internal->vars) {
      const int dst = map_idx (src);
      if (!dst)
        continue;
      CADICAL_assert (0 < dst);
      CADICAL_assert (dst <= src);
      v[dst] = v[src];
    }
    v.resize (new_vsize);
    shrink_vector (v);
  }

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

first_fixed

int CaDiCaL::Mapper::first_fixed

Definition at line 40 of file cadical_compact.cpp.

first_fixed_val

signed char CaDiCaL::Mapper::first_fixed_val

Definition at line 42 of file cadical_compact.cpp.

internal

Internal* CaDiCaL::Mapper::internal

Definition at line 37 of file cadical_compact.cpp.

map_first_fixed

int CaDiCaL::Mapper::map_first_fixed

Definition at line 41 of file cadical_compact.cpp.

new_max_var

int CaDiCaL::Mapper::new_max_var

Definition at line 38 of file cadical_compact.cpp.

new_vsize

size_t CaDiCaL::Mapper::new_vsize

Definition at line 43 of file cadical_compact.cpp.

table

int* CaDiCaL::Mapper::table

Definition at line 39 of file cadical_compact.cpp.

---

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

• src/sat/cadical/cadical_compact.cpp