diff --git a/src/btor2parser/btor2parser.c b/src/btor2parser/btor2parser.c index 462d00b..b9c0398 100644 --- a/src/btor2parser/btor2parser.c +++ b/src/btor2parser/btor2parser.c @@ -374,11 +374,8 @@ parse_opt_symbol_bfr (Btor2Parser *bfr, Btor2Line *l) } static Btor2Line * -new_line_bfr (Btor2Parser *bfr, - long id, - long lineno, - const char *name, - Btor2Tag tag) +new_line_bfr ( + Btor2Parser *bfr, long id, long lineno, const char *name, Btor2Tag tag) { Btor2Line *res; assert (0 < id); @@ -397,9 +394,7 @@ new_line_bfr (Btor2Parser *bfr, } static int -check_sort_bitvec (Btor2Parser *bfr, - Btor2Line *l, - Btor2Line *args[]) +check_sort_bitvec (Btor2Parser *bfr, Btor2Line *l, Btor2Line *args[]) { unsigned i; /* check if bit-vector operators have bit-vector operands */ @@ -614,8 +609,7 @@ check_sorts_bfr (Btor2Parser *bfr, Btor2Line *l) case BTOR2_TAG_implies: assert (l->nargs == 2); if (!check_sort_bitvec (bfr, l, args)) return 0; - if (l->sort.tag != BTOR2_TAG_SORT_bitvec - || l->sort.bitvec.width != 1) + if (l->sort.tag != BTOR2_TAG_SORT_bitvec || l->sort.bitvec.width != 1) return perr_bfr (bfr, "expected bitvec of size 1"); if (cmp_sorts (bfr, args[0], l)) return perr_bfr (bfr, @@ -1174,8 +1168,7 @@ parse_constant_bfr (Btor2Parser *bfr, Btor2Line *l) ungetc_bfr (bfr, '\n'); pushc_bfr (bfr, 0); - if (l->tag == BTOR2_TAG_const - && strlen (bfr->buf) != l->sort.bitvec.width) + if (l->tag == BTOR2_TAG_const && strlen (bfr->buf) != l->sort.bitvec.width) { return perr_bfr (bfr, "constant '%s' does not match bit-vector sort size %u", @@ -1323,8 +1316,8 @@ parse_justice_bfr (Btor2Parser *bfr, Btor2Line *l) { \ if (!strcmp (tag, #NAME)) \ { \ - Btor2Line *LINE = \ - new_line_bfr (bfr, id, lineno, #NAME, BTOR2_TAG_##NAME); \ + Btor2Line *LINE = \ + new_line_bfr (bfr, id, lineno, #NAME, BTOR2_TAG_##NAME); \ if (parse_##GENERIC##_bfr (bfr, LINE)) \ { \ pusht_bfr (bfr, LINE); \ diff --git a/src/btor2parser/btor2parser.h b/src/btor2parser/btor2parser.h index 05f058a..d66c8e1 100644 --- a/src/btor2parser/btor2parser.h +++ b/src/btor2parser/btor2parser.h @@ -147,16 +147,16 @@ struct Btor2Sort struct Btor2Line { - long id; /* positive id (non zero) */ - long lineno; /* line number in original file */ - const char *name; /* name in ASCII: "and", "add", ... */ - Btor2Tag tag; /* same as name but encoded as integer */ + long id; /* positive id (non zero) */ + long lineno; /* line number in original file */ + const char *name; /* name in ASCII: "and", "add", ... */ + Btor2Tag tag; /* same as name but encoded as integer */ Btor2Sort sort; - long init, next; /* non zero if initialized or has next */ - char *constant; /* non zero for const, constd, consth */ - char *symbol; /* optional for: var array state input */ - unsigned nargs; /* number of arguments */ - long *args; /* non zero ids up to nargs */ + long init, next; /* non zero if initialized or has next */ + char *constant; /* non zero for const, constd, consth */ + char *symbol; /* optional for: var array state input */ + unsigned nargs; /* number of arguments */ + long *args; /* non zero ids up to nargs */ }; struct Btor2LineIterator diff --git a/src/btorsim/btorsimbv.c b/src/btorsim/btorsimbv.c index 128e8db..0c0a774 100644 --- a/src/btorsim/btorsimbv.c +++ b/src/btorsim/btorsimbv.c @@ -18,7 +18,7 @@ #include #include -#define BTOR2_MASK_REM_BITS(bv) \ +#define BTOR2_MASK_REM_BITS(bv) \ ((((BTORSIM_BV_TYPE) 1 << (BTORSIM_BV_TYPE_BW - 1)) - 1) \ >> (BTORSIM_BV_TYPE_BW - 1 - (bv->width % BTORSIM_BV_TYPE_BW))) diff --git a/src/btorsim/btorsimmain.c b/src/btorsim/btorsimmain.c index d9b187b..8230769 100644 --- a/src/btorsim/btorsimmain.c +++ b/src/btorsim/btorsimmain.c @@ -19,9 +19,9 @@ #include #include +#include "btor2parser/btor2parser.h" #include "btorsimbv.h" #include "btorsimrng.h" -#include "btor2parser/btor2parser.h" #include "util/btor2mem.h" #include "util/btor2stack.h" @@ -405,12 +405,8 @@ simulate (long id) assert (l->nargs == 1); res = btorsim_bv_not (args[0]); break; - case BTOR2_TAG_one: - res = btorsim_bv_one (l->sort.bitvec.width); - break; - case BTOR2_TAG_ones: - res = btorsim_bv_ones (l->sort.bitvec.width); - break; + case BTOR2_TAG_one: res = btorsim_bv_one (l->sort.bitvec.width); break; + case BTOR2_TAG_ones: res = btorsim_bv_ones (l->sort.bitvec.width); break; case BTOR2_TAG_or: assert (l->nargs == 2); res = btorsim_bv_or (args[0], args[1]); @@ -468,9 +464,7 @@ simulate (long id) assert (l->nargs == 2); res = btorsim_bv_xor (args[0], args[1]); break; - case BTOR2_TAG_zero: - res = btorsim_bv_zero (l->sort.bitvec.width); - break; + case BTOR2_TAG_zero: res = btorsim_bv_zero (l->sort.bitvec.width); break; default: die ("can not randomly simulate operator '%s' at line %ld", l->name, @@ -501,7 +495,7 @@ initialize_inputs (long k, int randomize) for (long i = 0; i < BTOR2_COUNT_STACK (inputs); i++) { Btor2Line *input = BTOR2_PEEK_STACK (inputs, i); - uint32_t width = input->sort.bitvec.width; + uint32_t width = input->sort.bitvec.width; if (current_state[input->id]) continue; BtorSimBitVector *update; if (randomize) @@ -567,8 +561,8 @@ simulate_step (long k, int randomize_states_that_are_inputs) if (!l) continue; if (l->tag == BTOR2_TAG_sort || l->tag == BTOR2_TAG_init || l->tag == BTOR2_TAG_next || l->tag == BTOR2_TAG_bad - || l->tag == BTOR2_TAG_constraint - || l->tag == BTOR2_TAG_fair || l->tag == BTOR2_TAG_justice) + || l->tag == BTOR2_TAG_constraint || l->tag == BTOR2_TAG_fair + || l->tag == BTOR2_TAG_justice) continue; BtorSimBitVector *bv = simulate (i); @@ -609,7 +603,7 @@ simulate_step (long k, int randomize_states_that_are_inputs) for (long i = 0; i < BTOR2_COUNT_STACK (constraints); i++) { Btor2Line *constraint = BTOR2_PEEK_STACK (constraints, i); - BtorSimBitVector *bv = current_state[constraint->args[0]]; + BtorSimBitVector *bv = current_state[constraint->args[0]]; if (!btorsim_bv_is_zero (bv)) continue; msg (1, "constraint(%ld) '%ld constraint %ld' violated at time %ld", @@ -627,7 +621,7 @@ simulate_step (long k, int randomize_states_that_are_inputs) { long r = BTOR2_PEEK_STACK (reached_bads, i); if (r >= 0) continue; - Btor2Line *bad = BTOR2_PEEK_STACK (bads, i); + Btor2Line *bad = BTOR2_PEEK_STACK (bads, i); BtorSimBitVector *bv = current_state[bad->args[0]]; if (btorsim_bv_is_zero (bv)) continue; long bound = BTOR2_PEEK_STACK (reached_bads, i); @@ -928,7 +922,7 @@ parse_state_part (long k) state->id, k); BtorSimBitVector *val = btorsim_bv_char_to_bv (constant.start); - Btor2Line *init = inits[state->id]; + Btor2Line *init = inits[state->id]; if (init) { assert (init->nargs == 2); @@ -1061,8 +1055,8 @@ parse_sat_witness () for (long i = 0; i < BTOR2_COUNT_STACK (claimed_bad_witnesses); i++) { - long bad_pos = BTOR2_PEEK_STACK (claimed_bad_witnesses, i); - long bound = BTOR2_PEEK_STACK (reached_bads, bad_pos); + long bad_pos = BTOR2_PEEK_STACK (claimed_bad_witnesses, i); + long bound = BTOR2_PEEK_STACK (reached_bads, bad_pos); Btor2Line *l = BTOR2_PEEK_STACK (bads, bad_pos); if (bound < 0) die ("claimed bad state property 'b%ld' id %ld not reached", diff --git a/src/catbtor.c b/src/catbtor.c index 80eca9f..ef03381 100644 --- a/src/catbtor.c +++ b/src/catbtor.c @@ -108,9 +108,7 @@ main (int argc, char** argv) printf (" %s", l->sort.name); switch (l->sort.tag) { - case BTOR2_TAG_SORT_bitvec: - printf (" %u", l->sort.bitvec.width); - break; + case BTOR2_TAG_SORT_bitvec: printf (" %u", l->sort.bitvec.width); break; case BTOR2_TAG_SORT_array: printf (" %ld %ld", l->sort.array.index, l->sort.array.element); break; @@ -123,8 +121,7 @@ main (int argc, char** argv) else if (l->sort.id) printf (" %ld", l->sort.id); for (i = 0; i < l->nargs; i++) printf (" %ld", l->args[i]); - if (l->tag == BTOR2_TAG_slice) - printf (" %ld %ld", l->args[1], l->args[2]); + if (l->tag == BTOR2_TAG_slice) printf (" %ld %ld", l->args[1], l->args[2]); if (l->tag == BTOR2_TAG_sext || l->tag == BTOR2_TAG_uext) printf (" %ld", l->args[1]); if (l->constant) printf (" %s", l->constant); diff --git a/src/util/btor2stack.h b/src/util/btor2stack.h index 416ae41..b228dd2 100644 --- a/src/util/btor2stack.h +++ b/src/util/btor2stack.h @@ -17,7 +17,7 @@ #include "btor2mem.h" -#define BTOR2_DECLARE_STACK(name, type) \ +#define BTOR2_DECLARE_STACK(name, type) \ typedef struct name##Stack name##Stack; \ struct name##Stack \ { \ @@ -31,11 +31,11 @@ BTOR2_DECLARE_STACK (BtorCharPtr, char *); BTOR2_DECLARE_STACK (BtorVoidPtr, void *); #define BTOR2_INIT_STACK(stack) \ - do \ - { \ - (stack).start = 0; \ - (stack).top = 0; \ - (stack).end = 0; \ + do \ + { \ + (stack).start = 0; \ + (stack).top = 0; \ + (stack).end = 0; \ } while (0) #define BTOR2_COUNT_STACK(stack) ((stack).top - (stack).start) @@ -45,35 +45,35 @@ BTOR2_DECLARE_STACK (BtorVoidPtr, void *); #define BTOR2_RESET_STACK(stack) ((stack).top = (stack).start) #define BTOR2_RELEASE_STACK(stack) \ - do \ - { \ + do \ + { \ BTOR2_DELETE ((stack).start); \ BTOR2_INIT_STACK ((stack)); \ } while (0) -#define BTOR2_ENLARGE(p, o, n) \ +#define BTOR2_ENLARGE(p, o, n) \ do \ { \ size_t internaln = (o) ? 2 * (o) : 1; \ - BTOR2_REALLOC ((p), internaln); \ + BTOR2_REALLOC ((p), internaln); \ (n) = internaln; \ } while (0) #define BTOR2_ENLARGE_STACK(stack) \ - do \ - { \ + do \ + { \ size_t old_size = BTOR2_SIZE_STACK (stack), new_size; \ size_t old_count = BTOR2_COUNT_STACK (stack); \ BTOR2_ENLARGE ((stack).start, old_size, new_size); \ - (stack).top = (stack).start + old_count; \ - (stack).end = (stack).start + new_size; \ + (stack).top = (stack).start + old_count; \ + (stack).end = (stack).start + new_size; \ } while (0) -#define BTOR2_PUSH_STACK(stack, elem) \ - do \ - { \ +#define BTOR2_PUSH_STACK(stack, elem) \ + do \ + { \ if (BTOR2_FULL_STACK ((stack))) BTOR2_ENLARGE_STACK ((stack)); \ - *((stack).top++) = (elem); \ + *((stack).top++) = (elem); \ } while (0) #define BTOR2_POP_STACK(stack) \ @@ -83,10 +83,10 @@ BTOR2_DECLARE_STACK (BtorVoidPtr, void *); (assert ((idx) < BTOR2_COUNT_STACK (stack)), (stack).start[idx]) #define BTOR2_POKE_STACK(stack, idx, elem) \ - do \ - { \ + do \ + { \ assert ((idx) < BTOR2_COUNT_STACK (stack)); \ - (stack).start[idx] = (elem); \ + (stack).start[idx] = (elem); \ } while (0) #endif