Skip to content

Commit

Permalink
Refactoring to support recurrent clauses
Browse files Browse the repository at this point in the history
  • Loading branch information
@olegranmo
olegranmo committed May 8, 2024
1 parent 17560b1 commit 4a78179
Showing 1 changed file with 103 additions and 68 deletions.
171 changes: 103 additions & 68 deletions tmu/lib/src/ClauseBank.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,27 +105,65 @@ static inline void cb_dec(
}
}

/* Calculate the output of each clause using the actions of each Tsetline Automaton. */
static inline void cb_calculate_clause_output_feedback(unsigned int *ta_state, unsigned int *output_one_patches, unsigned int *clause_output, unsigned int *clause_patch, int number_of_ta_chunks, int number_of_state_bits, unsigned int filter, int number_of_patches, unsigned int *literal_active, unsigned int *Xi)
static inline unsigned int cb_calculate_clause_output_without_literal_active(
unsigned int *ta_state,
int number_of_ta_chunks,
int number_of_state_bits,
unsigned int filter,
unsigned int *Xi
)
{
int output_one_patches_count = 0;
for (int patch = 0; patch < number_of_patches; ++patch) {
unsigned int output = 1;
for (int k = 0; k < number_of_ta_chunks-1; k++) {
unsigned int pos = k*number_of_state_bits + number_of_state_bits-1;
output = output && (ta_state[pos] & (Xi[patch*number_of_ta_chunks + k] | (~literal_active[k]))) == ta_state[pos];
unsigned int output = 1;
for (int k = 0; k < number_of_ta_chunks-1; k++) {
unsigned int pos = k*number_of_state_bits + number_of_state_bits-1;
output = output && (ta_state[pos] & Xi[k]) == ta_state[pos];

if (!output) {
break;
}
if (!output) {
break;
}
}

unsigned int pos = (number_of_ta_chunks-1)*number_of_state_bits + number_of_state_bits-1;
output = output &&
(ta_state[pos] & (Xi[number_of_ta_chunks - 1]) & filter) ==
(ta_state[pos] & filter);

return output;
}

static inline unsigned int cb_calculate_clause_output(
unsigned int *ta_state,
int number_of_ta_chunks,
int number_of_state_bits,
unsigned int filter,
unsigned int *literal_active,
unsigned int *Xi
)
{
unsigned int output = 1;
for (int k = 0; k < number_of_ta_chunks-1; k++) {
unsigned int pos = k*number_of_state_bits + number_of_state_bits-1;
output = output && (ta_state[pos] & (Xi[k] | (~literal_active[k]))) == ta_state[pos];

if (!output) {
break;
}
}

unsigned int pos = (number_of_ta_chunks-1)*number_of_state_bits + number_of_state_bits-1;
output = output &&
(ta_state[pos] & (Xi[patch*number_of_ta_chunks + number_of_ta_chunks - 1] | (~literal_active[number_of_ta_chunks - 1])) & filter) ==
(ta_state[pos] & filter);
unsigned int pos = (number_of_ta_chunks-1)*number_of_state_bits + number_of_state_bits-1;
output = output &&
(ta_state[pos] & (Xi[number_of_ta_chunks - 1] | (~literal_active[number_of_ta_chunks - 1])) & filter) ==
(ta_state[pos] & filter);

if (output) {
return output;
}

/* Calculate the output of each clause using the actions of each Tsetline Automaton. */
static inline void cb_calculate_clause_output_feedback(unsigned int *ta_state, unsigned int *output_one_patches, unsigned int *clause_output, unsigned int *clause_patch, int number_of_ta_chunks, int number_of_state_bits, unsigned int filter, int number_of_patches, unsigned int *literal_active, unsigned int *Xi)
{
int output_one_patches_count = 0;
for (int patch = 0; patch < number_of_patches; ++patch) {
if (cb_calculate_clause_output(ta_state, number_of_ta_chunks, number_of_state_bits, filter, literal_active, &Xi[patch*number_of_ta_chunks])) {
output_one_patches[output_one_patches_count] = patch;
output_one_patches_count++;
}
Expand Down Expand Up @@ -199,68 +237,18 @@ static inline int cb_calculate_clause_output_single_false_literal(unsigned int *
static inline unsigned int cb_calculate_clause_output_update(unsigned int *ta_state, int number_of_ta_chunks, int number_of_state_bits, unsigned int filter, int number_of_patches, unsigned int *literal_active, unsigned int *Xi)
{
for (int patch = 0; patch < number_of_patches; ++patch) {
unsigned int output = 1;
for (int k = 0; k < number_of_ta_chunks-1; k++) {
unsigned int pos = k*number_of_state_bits + number_of_state_bits-1;
output = output && (ta_state[pos] & (Xi[patch*number_of_ta_chunks + k] | (~literal_active[k]))) == ta_state[pos];

if (!output) {
break;
}
}

unsigned int pos = (number_of_ta_chunks-1)*number_of_state_bits + number_of_state_bits-1;
output = output &&
(ta_state[pos] & (Xi[patch*number_of_ta_chunks + number_of_ta_chunks - 1] | (~literal_active[number_of_ta_chunks - 1])) & filter) ==
(ta_state[pos] & filter);

if (output) {
if (cb_calculate_clause_output(ta_state, number_of_ta_chunks, number_of_state_bits, filter, literal_active, &Xi[patch*number_of_ta_chunks])) {
return(1);
}
}

return(0);
}

static inline void cb_calculate_clause_output_recurrent(unsigned int *ta_state, int number_of_ta_chunks, int number_of_state_bits, unsigned int filter, int number_of_patches, unsigned int *output, unsigned int *Xi)
{
for (int patch = 0; patch < number_of_patches; ++patch) {
output[patch] = 1;
for (int k = 0; k < number_of_ta_chunks-1; k++) {
unsigned int pos = k*number_of_state_bits + number_of_state_bits-1;
output[patch] = output[patch] && (ta_state[pos] & Xi[patch*number_of_ta_chunks + k]) == ta_state[pos];

if (!output[patch]) {
break;
}
}

unsigned int pos = (number_of_ta_chunks-1)*number_of_state_bits + number_of_state_bits-1;
output[patch] = output[patch] &&
(ta_state[pos] & Xi[patch*number_of_ta_chunks + number_of_ta_chunks - 1] & filter) ==
(ta_state[pos] & filter);
}

return;
}

static inline void cb_calculate_clause_output_patchwise(unsigned int *ta_state, int number_of_ta_chunks, int number_of_state_bits, unsigned int filter, int number_of_patches, unsigned int *output, unsigned int *Xi)
{
for (int patch = 0; patch < number_of_patches; ++patch) {
output[patch] = 1;
for (int k = 0; k < number_of_ta_chunks-1; k++) {
unsigned int pos = k*number_of_state_bits + number_of_state_bits-1;
output[patch] = output[patch] && (ta_state[pos] & Xi[patch*number_of_ta_chunks + k]) == ta_state[pos];

if (!output[patch]) {
break;
}
}

unsigned int pos = (number_of_ta_chunks-1)*number_of_state_bits + number_of_state_bits-1;
output[patch] = output[patch] &&
(ta_state[pos] & Xi[patch*number_of_ta_chunks + number_of_ta_chunks - 1] & filter) ==
(ta_state[pos] & filter);
output[patch] = cb_calculate_clause_output_without_literal_active(ta_state, number_of_ta_chunks, number_of_state_bits, filter, &Xi[patch*number_of_ta_chunks]);
}

return;
Expand Down Expand Up @@ -770,6 +758,53 @@ void cb_calculate_clause_outputs_update(
}
}

void cb_calculate_clause_features(
unsigned int *ta_state,
int number_of_clauses,
int number_of_literals,
int number_of_state_bits,
int number_of_patches,
unsigned int *literal_active,
unsigned int *Xi
)
{
unsigned int filter;
if (((number_of_literals) % 32) != 0) {
filter = (~(0xffffffff << ((number_of_literals) % 32)));
} else {
filter = 0xffffffff;
}

unsigned int number_of_ta_chunks = (number_of_literals-1)/32 + 1;

for (int patch = 0; patch < number_of_patches; ++patch) {
for (int j = 0; j < number_of_clauses; j++) {
unsigned int clause_pos = j*number_of_ta_chunks*number_of_state_bits;
if (cb_calculate_clause_output(&ta_state[clause_pos], number_of_ta_chunks, number_of_state_bits, filter, literal_active, &Xi[patch*number_of_ta_chunks])) {
unsigned int chunk_nr = j / 32;
unsigned int chunk_pos = j % 32;

Xi[patch*number_of_ta_chunks + chunk_nr] |= (1U << chunk_pos);

chunk_nr = (j + number_of_literals / 2) / 32;
chunk_pos = (j + number_of_literals / 2) % 32;

Xi[patch*number_of_ta_chunks + chunk_nr] &= ~(1U << chunk_pos);
} else {
unsigned int chunk_nr = j / 32;
unsigned int chunk_pos = j % 32;

Xi[patch*number_of_ta_chunks + chunk_nr] &= ~(1U << chunk_pos);

chunk_nr = (j + number_of_literals / 2) / 32;
chunk_pos = (j + number_of_literals / 2) % 32;

Xi[patch*number_of_ta_chunks + chunk_nr] |= (1U << chunk_pos);
}
}
}
}

void cb_calculate_clause_outputs_patchwise(
unsigned int *ta_state,
int number_of_clauses,
Expand Down

0 comments on commit 4a78179

Please sign in to comment.