Skip to content

Commit

Permalink
Added btor_node_is_bv_const and btor_node_is_neg
Browse files Browse the repository at this point in the history
  • Loading branch information
@aniemetz
aniemetz committed Jun 13, 2018
1 parent 209d495 commit 36980f3
Show file tree
Hide file tree
Showing 4 changed files with 100 additions and 59 deletions.
52 changes: 52 additions & 0 deletions src/btornode.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,58 @@ set_kind (Btor *btor, BtorNode *exp, BtorNodeKind kind)

/*------------------------------------------------------------------------*/

bool
btor_node_is_bv_const_one (Btor *btor, BtorNode *exp)
{
assert (btor);
assert (exp);

bool result;
BtorNode *real_exp;
BtorBitVector *bits;

exp = btor_simplify_exp (btor, exp);

if (!btor_node_is_bv_const (exp)) return false;

real_exp = btor_node_real_addr (exp);
bits = btor_node_const_get_bits (real_exp);
if (btor_node_is_inverted (exp)) bits = btor_bv_not (btor->mm, bits);
result = btor_bv_is_special_const (bits) == BTOR_SPECIAL_CONST_BV_ONE;
if (btor_node_is_inverted (exp)) btor_bv_free (btor->mm, bits);

return result;
}

bool
btor_node_is_neg (Btor *btor, BtorNode *exp, BtorNode **res)
{
assert (btor);
assert (exp);

BtorNode *real_exp;

real_exp = btor_node_real_addr (exp);

if (!btor_node_is_add (real_exp)) return false;

if (btor_node_is_bv_const_one (btor, real_exp->e[0]))
{
if (res) *res = btor_node_invert (real_exp->e[1]);
return true;
}

if (btor_node_is_bv_const_one (btor, real_exp->e[1]))
{
if (res) *res = btor_node_invert (real_exp->e[0]);
return true;
}

return false;
}

/*------------------------------------------------------------------------*/

static void
inc_exp_ref_counter (Btor *btor, BtorNode *exp)
{
Expand Down
8 changes: 7 additions & 1 deletion src/btornode.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
*
* Copyright (C) 2007-2009 Robert Daniel Brummayer.
* Copyright (C) 2007-2015 Armin Biere.
* Copyright (C) 2012-2017 Aina Niemetz.
* Copyright (C) 2012-2018 Aina Niemetz.
* Copyright (C) 2012-2017 Mathias Preiner.
*
* This file is part of Boolector.
Expand Down Expand Up @@ -514,6 +514,12 @@ btor_node_is_array_or_bv_eq (const BtorNode *exp)

/*------------------------------------------------------------------------*/

bool btor_node_is_bv_const_one (Btor *btor, BtorNode *exp);

bool btor_node_is_neg (Btor *btor, BtorNode *exp, BtorNode **res);

/*------------------------------------------------------------------------*/

/* Get the id of an expression (negative if exp is inverted). */
static inline int32_t
btor_node_get_id (const BtorNode *exp)
Expand Down
64 changes: 9 additions & 55 deletions src/btorrewrite.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
* Copyright (C) 2007-2009 Robert Daniel Brummayer.
* Copyright (C) 2007-2017 Armin Biere.
* Copyright (C) 2013-2017 Mathias Preiner.
* Copyright (C) 2014-2017 Aina Niemetz.
* Copyright (C) 2014-2018 Aina Niemetz.
*
* This file is part of Boolector.
* See COPYING for more information on using this software.
Expand Down Expand Up @@ -122,28 +122,6 @@
/* -------------------------------------------------------------------------- */
/* util functions */

static bool
is_const_one_exp (Btor *btor, BtorNode *exp)
{
bool result;
BtorNode *real_exp;
BtorBitVector *bits;

assert (btor);
assert (exp);
exp = btor_simplify_exp (btor, exp);

if (!btor_node_is_bv_const (exp)) return false;

real_exp = btor_node_real_addr (exp);
bits = btor_node_const_get_bits (real_exp);
if (btor_node_is_inverted (exp)) bits = btor_bv_not (btor->mm, bits);
result = btor_bv_is_special_const (bits) == BTOR_SPECIAL_CONST_BV_ONE;
if (btor_node_is_inverted (exp)) btor_bv_free (btor->mm, bits);

return result;
}

static bool
is_const_zero_exp (Btor *btor, BtorNode *exp)
{
Expand Down Expand Up @@ -510,30 +488,6 @@ is_bit_mask (BtorNode * exp, uint32_t * upper, uint32_t * lower)
}
#endif

static bool
is_neg_exp (Btor *btor, BtorNode *exp, BtorNode **res)
{
BtorNode *real_exp;

real_exp = btor_node_real_addr (exp);

if (!btor_node_is_add (real_exp)) return false;

if (is_const_one_exp (btor, real_exp->e[0]))
{
if (res) *res = btor_node_invert (real_exp->e[1]);
return true;
}

if (is_const_one_exp (btor, real_exp->e[1]))
{
if (res) *res = btor_node_invert (real_exp->e[0]);
return true;
}

return false;
}

static bool
is_urem_exp (Btor *btor,
BtorNode *e0,
Expand All @@ -543,9 +497,9 @@ is_urem_exp (Btor *btor,
{
BtorNode *mul, *udiv, *x, *y;

if (is_neg_exp (btor, e0, &mul))
if (btor_node_is_neg (btor, e0, &mul))
x = e1;
else if (is_neg_exp (btor, e1, &mul))
else if (btor_node_is_neg (btor, e1, &mul))
x = e0;
else
return false;
Expand Down Expand Up @@ -3305,9 +3259,9 @@ applies_neg_add (Btor *btor, BtorNode *e0, BtorNode *e1)
(void) btor;
return !btor_node_is_inverted (e1) && btor_node_is_add (e1)
&& ((e0 == btor_node_invert (e1->e[0])
&& is_const_one_exp (btor, e1->e[1]))
&& btor_node_is_bv_const_one (btor, e1->e[1]))
|| (e0 == btor_node_invert (e1->e[1])
&& is_const_one_exp (btor, e1->e[0])));
&& btor_node_is_bv_const_one (btor, e1->e[0])));
}

static inline BtorNode *
Expand Down Expand Up @@ -5178,8 +5132,8 @@ applies_add_if_cond (Btor *btor, BtorNode *e0, BtorNode *e1, BtorNode *e2)
(void) e0;
return btor->rec_rw_calls < BTOR_REC_RW_BOUND && !btor_node_is_inverted (e1)
&& btor_node_is_add (e1)
&& ((e1->e[0] == e2 && is_const_one_exp (btor, e1->e[1]))
|| (e1->e[1] == e2 && is_const_one_exp (btor, e1->e[0])));
&& ((e1->e[0] == e2 && btor_node_is_bv_const_one (btor, e1->e[1]))
|| (e1->e[1] == e2 && btor_node_is_bv_const_one (btor, e1->e[0])));
}

static inline BtorNode *
Expand Down Expand Up @@ -5207,8 +5161,8 @@ applies_add_else_cond (Btor *btor, BtorNode *e0, BtorNode *e1, BtorNode *e2)
(void) e0;
return btor->rec_rw_calls < BTOR_REC_RW_BOUND && !btor_node_is_inverted (e2)
&& btor_node_is_add (e2)
&& ((e2->e[0] == e1 && is_const_one_exp (btor, e2->e[1]))
|| (e2->e[1] == e1 && is_const_one_exp (btor, e2->e[0])));
&& ((e2->e[0] == e1 && btor_node_is_bv_const_one (btor, e2->e[1]))
|| (e2->e[1] == e1 && btor_node_is_bv_const_one (btor, e2->e[0])));
}

static inline BtorNode *
Expand Down
35 changes: 32 additions & 3 deletions src/tests/testexp.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
*
* Copyright (C) 2007-2010 Robert Daniel Brummayer.
* Copyright (C) 2007-2012 Armin Biere.
* Copyright (C) 2012-2017 Aina Niemetz.
* Copyright (C) 2012-2018 Aina Niemetz.
*
* This file is part of Boolector.
* See COPYING for more information on using this software.
Expand All @@ -11,6 +11,7 @@
#include "testexp.h"
#include "btorcore.h"
#include "btorexp.h"
#include "btornode.h"
#include "dumper/btordumpbtor.h"
#include "testrunner.h"

Expand Down Expand Up @@ -94,6 +95,10 @@ test_zero_exp (void)
assert (exp1 == exp2);
assert (btor_node_get_width (g_btor, exp1) == 8);
assert (btor_node_get_width (g_btor, exp2) == 8);
assert (!btor_node_is_bv_const_one (g_btor, exp1));
assert (!btor_node_is_bv_const_one (g_btor, exp2));
assert (!btor_node_is_bv_const_one (g_btor, btor_node_invert (exp1)));
assert (!btor_node_is_bv_const_one (g_btor, btor_node_invert (exp2)));
btor_dumpbtor_dump_node (g_btor, g_logfile, exp1);
btor_node_release (g_btor, exp1);
btor_node_release (g_btor, exp2);
Expand All @@ -118,6 +123,10 @@ test_ones_exp (void)
assert (exp1 == exp2);
assert (btor_node_get_width (g_btor, exp1) == 8);
assert (btor_node_get_width (g_btor, exp2) == 8);
assert (!btor_node_is_bv_const_one (g_btor, exp1));
assert (!btor_node_is_bv_const_one (g_btor, exp2));
assert (!btor_node_is_bv_const_one (g_btor, btor_node_invert (exp1)));
assert (!btor_node_is_bv_const_one (g_btor, btor_node_invert (exp2)));
btor_dumpbtor_dump_node (g_btor, g_logfile, exp1);
btor_node_release (g_btor, exp1);
btor_node_release (g_btor, exp2);
Expand All @@ -128,8 +137,8 @@ test_ones_exp (void)
static void
test_one_exp (void)
{
BtorNode *exp1, *exp2;
BtorBitVector *bv2;
BtorNode *exp1, *exp2, *exp3;
BtorBitVector *bv2, *bv3;
BtorSortId sort;

init_exp_test ();
Expand All @@ -142,10 +151,20 @@ test_one_exp (void)
assert (exp1 == exp2);
assert (btor_node_get_width (g_btor, exp1) == 8);
assert (btor_node_get_width (g_btor, exp2) == 8);
assert (btor_node_is_bv_const_one (g_btor, exp1));
assert (btor_node_is_bv_const_one (g_btor, exp2));
assert (!btor_node_is_bv_const_one (g_btor, btor_node_invert (exp1)));
assert (!btor_node_is_bv_const_one (g_btor, btor_node_invert (exp2)));
bv3 = btor_bv_char_to_bv (g_btor->mm, "11111110");
exp3 = btor_exp_const (g_btor, bv3);
assert (!btor_node_is_bv_const_one (g_btor, exp3));
assert (btor_node_is_bv_const_one (g_btor, btor_node_invert (exp3)));
btor_dumpbtor_dump_node (g_btor, g_logfile, exp1);
btor_node_release (g_btor, exp1);
btor_node_release (g_btor, exp2);
btor_node_release (g_btor, exp3);
btor_bv_free (g_btor->mm, bv2);
btor_bv_free (g_btor->mm, bv3);
finish_exp_test ();
}

Expand Down Expand Up @@ -277,6 +296,16 @@ unary_exp_test (BtorNode *(*func) (Btor *, BtorNode *) )
{
assert (btor_node_get_width (g_btor, exp2) == len);
assert (btor_node_get_width (g_btor, exp3) == len);
if (func == btor_exp_neg)
{
assert (btor_node_is_neg (g_btor, exp2, 0));
assert (btor_node_is_neg (g_btor, exp3, 0));
}
else
{
assert (!btor_node_is_neg (g_btor, exp2, 0));
assert (!btor_node_is_neg (g_btor, exp3, 0));
}
}
else
{
Expand Down

0 comments on commit 36980f3

Please sign in to comment.