Skip to content

Commit

Permalink
Format
Browse files Browse the repository at this point in the history
  • Loading branch information
@aniemetz
aniemetz committed May 4, 2018
1 parent cece23d commit 1108cc8
Show file tree
Hide file tree
Showing 6 changed files with 52 additions and 68 deletions.
21 changes: 7 additions & 14 deletions src/btor2parser/btor2parser.c
View file
Expand Up @@ -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);
Expand All @@ -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 */
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -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); \
Expand Down
18 changes: 9 additions & 9 deletions src/btor2parser/btor2parser.h
View file
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/btorsim/btorsimbv.c
View file
Expand Up @@ -18,7 +18,7 @@
#include <ctype.h>
#include <limits.h>

#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)))

Expand Down
30 changes: 12 additions & 18 deletions src/btorsim/btorsimmain.c
View file
Expand Up @@ -19,9 +19,9 @@
#include <stdlib.h>
#include <string.h>

#include "btor2parser/btor2parser.h"
#include "btorsimbv.h"
#include "btorsimrng.h"
#include "btor2parser/btor2parser.h"
#include "util/btor2mem.h"
#include "util/btor2stack.h"

Expand Down Expand Up @@ -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]);
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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",
Expand All @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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",
Expand Down
7 changes: 2 additions & 5 deletions src/catbtor.c
View file
Expand Up @@ -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;
Expand All @@ -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);
Expand Down
42 changes: 21 additions & 21 deletions src/util/btor2stack.h
View file
Expand Up @@ -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 \
{ \
Expand All @@ -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)
Expand All @@ -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) \
Expand All @@ -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

0 comments on commit 1108cc8

Please sign in to comment.