Class BasePackedComponent

Inheritance Relationships

Derived Type

Class Documentation

class BasePackedComponent

Stores the specifications for package cache components including the number of bits in a variable, clause, and other information.

Subclassed by DifferencePackedComponent

Public Functions

BasePackedComponent()
BasePackedComponent(unsigned creation_time)

Creates a packed component and records with it the creation time.

Parameters
  • creation_time:

~BasePackedComponent()
unsigned creation_time()
const mpz_class &model_count() const
unsigned alloc_of_model_count() const
void set_creation_time(unsigned time)
void set_model_count(const mpz_class &rn, unsigned time)
unsigned hashkey() const
bool modelCountFound()
bool isDeletable() const

Determines if a cache entry is deletable. This entails that the entry is not connected to an active component in the component stack.

Return
true if the cache entry is disconnected from an active component and can be deleted.

void set_deletable()

Mark the packed cache entry as deletable.

void clear()

Free the memory associated with the packed cache entry’s data.

Public Static Functions

static unsigned bits_per_variable()

Accessor to get n := {lg |var(F)|}, i.e., the number of bits that represent a VARIABLE.

Return
Number of bits to store a VARIABLE

static unsigned variable_mask()
static unsigned bits_per_clause()

Accessor to get m := {lg |cl(F)|}, i.e., the number of bits that represent a CLAUSE.

Return
Number of bits to store a CLAUSE.

static unsigned bits_per_block()
static unsigned bits_of_data_size()
void adjustPackSize(unsigned int maxVarId, unsigned int maxClId)

Configures that variables that define the packing size variables.

Parameters
  • maxVarId: Maximum ID number for a variable
  • maxClId: Maximum ID number for a clause

static void outbit(unsigned v)

Prints a bit string to the console. The MSB is printed first and the LSB last.

Parameters
  • v: Value to be printed by bit to the console.

static unsigned log2(unsigned v)

Public Static Attributes

unsigned _debug_static_val = 0

Protected Attributes

unsigned *data_ = nullptr

Packed data array to be stored in memory,

data_ contains in packed form the variable indices and clause indices of the component ordered structure is

var var … clause clause …

clauses begin at clauses_ofs_

unsigned hashkey_ = 0
mpz_class model_count_
unsigned creation_time_ = 1
unsigned length_solution_period_and_flags_ = 0

Protected Static Attributes

unsigned _bits_per_clause = 0

In the sharpSAT paper, bits per clause (m) is defined as:

m := {lg |cl(F)|}

It is the minimum number of bits per clause when packing is enabled.

The implementation is slightly different in the code. It is defined as:

m := {lg |cl(F)| + 1}

base_packed_component.cpp

Purpose: Defines the static variables and methods for the BasePackedComponent() class.

Copyright (C) 2018 Zayd Hammoudeh. All rights reserved.

Author
Zayd Hammoudeh zayd@ucsc.edu
Version
0.00.00

This software may be modified and distributed under the terms of the MIT license. See the LICENSE file for details.

Original Author: Marc Thurley.

unsigned _bits_per_variable = 0

In the sharpSAT paper, bits per variable (n) is defined as:

n := {lg |var(F)|}

It is the minimum number of bits per clause when packing is enabled.

The implementation is slightly different in the code. It is defined as:

n := {lg |var(F)| + 1}

unsigned _bits_of_data_size = 0
unsigned _data_size_mask = 0
unsigned _variable_mask = 0

Bit mask in the form of bits of 0b1 of length “n”

See
BasePackedComponent::_bits_per_variable.

unsigned _clause_mask = 0

Bit mask in the form of bits of 0b1 of length “m”

See
BasePackedComponent::_bits_per_variable.

const unsigned _bits_per_block = (sizeof(unsigned) << 3)

Equals 32 (= 4 * 8 bits)

sizeof(unsigned) = 4 Three left bit shifts equals 8