From 4a78179d4572ab8a7798930c1830788fc43c6532 Mon Sep 17 00:00:00 2001 From: Ole-Christoffer Granmo Date: Wed, 8 May 2024 12:07:10 +0200 Subject: [PATCH] Refactoring to support recurrent clauses --- tmu/lib/src/ClauseBank.c | 171 +++++++++++++++++++++++---------------- 1 file changed, 103 insertions(+), 68 deletions(-) diff --git a/tmu/lib/src/ClauseBank.c b/tmu/lib/src/ClauseBank.c index 232bb3dc..bec6ec3d 100644 --- a/tmu/lib/src/ClauseBank.c +++ b/tmu/lib/src/ClauseBank.c @@ -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++; } @@ -199,22 +237,7 @@ 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); } } @@ -222,45 +245,10 @@ static inline unsigned int cb_calculate_clause_output_update(unsigned int *ta_st 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; @@ -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,