Skip to content

Commit

Permalink
Exp changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@aman-goel
aman-goel committed Aug 31, 2024
1 parent bd241b6 commit 4225df4
Show file tree
Hide file tree
Showing 3 changed files with 138 additions and 15 deletions.
83 changes: 79 additions & 4 deletions src/reach/avr_word_netlist.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1822,6 +1822,17 @@ int OpInst::get_simple_version() {

void OpInst::propagate_uf() {
switch (m_op) {
case Minus: {
const InstL* ch = get_children();
if (ch->size() == 1) {
InstL::const_iterator cit = ch->begin();
Inst* lhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
// -0 = 0
t_simple = lhs;
}
}
} break;
case Add: {
const InstL* ch = get_children();
if (ch->size() == 2) {
Expand Down Expand Up @@ -1944,6 +1955,13 @@ void OpInst::propagate_uf() {
} else if (lhs == rhs) {
// x > x = false
t_simple = NumInst::create(0, 1, SORT());
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) > 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
} break;
case SGr: {
Expand All @@ -1956,6 +1974,15 @@ void OpInst::propagate_uf() {
if (lhs == rhs) {
// x >s x = false
t_simple = NumInst::create(0, 1, SORT());
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (get_size() > 1) {
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) > 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
}
} break;
case Le: {
Expand All @@ -1971,6 +1998,13 @@ void OpInst::propagate_uf() {
} else if (lhs == rhs) {
// x < x = false
t_simple = NumInst::create(0, 1, SORT());
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) < 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
} break;
case SLe: {
Expand All @@ -1983,6 +2017,15 @@ void OpInst::propagate_uf() {
if (lhs == rhs) {
// x <s x = false
t_simple = NumInst::create(0, 1, SORT());
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (get_size() > 1) {
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) < 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
}
} break;
case GrEq: {
Expand All @@ -1998,6 +2041,13 @@ void OpInst::propagate_uf() {
} else if (lhs == rhs) {
// x >= x = true
t_simple = NumInst::create(1, 1, SORT());
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) >= 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
} break;
case SGrEq: {
Expand All @@ -2010,6 +2060,15 @@ void OpInst::propagate_uf() {
if (lhs == rhs) {
// x >=s x = true
t_simple = NumInst::create(1, 1, SORT());
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (get_size() > 1) {
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) >= 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
}
} break;
case LeEq: {
Expand All @@ -2025,6 +2084,13 @@ void OpInst::propagate_uf() {
} else if (lhs == rhs) {
// x <= x = true
t_simple = NumInst::create(1, 1, SORT());
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) <= 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
} break;
case SLeEq: {
Expand All @@ -2037,7 +2103,16 @@ void OpInst::propagate_uf() {
if (lhs == rhs) {
// x <=s x = true
t_simple = NumInst::create(1, 1, SORT());
}
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
// both are numbers
if (get_size() > 1) {
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) <= 0) {
t_simple = NumInst::create(1, 1, SORT());
} else {
t_simple = NumInst::create(0, 1, SORT());
}
}
}
} break;
case BitWiseAnd: {
const InstL* ch = get_children();
Expand Down Expand Up @@ -2142,9 +2217,9 @@ void OpInst::propagate_uf() {
;
}

// if (this != this->get_simple()) {
// cout << "uf_prop: " << *this << " -> " << *(this->t_simple) << endl;
// }
if (this != this->get_simple()) {
cout << "uf_prop: " << *this << " -> " << *(this->t_simple) << endl;
}
}

bool OpInst::is_heavy_uf() {
Expand Down
20 changes: 20 additions & 0 deletions src/reach/avr_word_netlist.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2131,6 +2131,26 @@ class NumInst: public Inst {
return m_mpz.get_si();
}

int num_cmp(NumInst* rhs, bool sign) {
assert (get_sort_type() == bvtype);
if (!sign) {
return mpz_cmp(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t());
} else {
assert(get_size() > 1);
string str_lhs = get_mpz()->get_str(2);
string str_rhs = rhs->get_mpz()->get_str(2);
if (str_lhs[0] == '0' && str_rhs[0] == '0') {
return mpz_cmp(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t());
} else if (str_lhs[0] == '0' && str_rhs[0] == '1') {
return 1;
} else if (str_lhs[0] == '1' && str_rhs[0] == '0') {
return -1;
} else {
return (-1)*mpz_cmpabs(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t());
}
}
}

static Inst *read_bin();
virtual void write_bin();

Expand Down
50 changes: 39 additions & 11 deletions src/vwn/btor2_frontend.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -511,21 +511,49 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
} break;
case BTOR2_TAG_constd: {
string snum(t.constant);

mpz_t mpz_mask;
mpz_init(mpz_mask);
mpz_set_si(mpz_mask, strtol(snum.c_str(), NULL, 10));
mpz_class t_mpzc(mpz_mask);
string str_num = t_mpzc.get_str(2);

char bv_val[sz];
string str_bv = "";
if (snum[0] == '-') {
if (sz == 1) {
//boolean negative means 1 (since sign bit has to be 1)
node = NumInst::create(1, sz);
} else {
mpz_t mpz_mask;
mpz_init(mpz_mask);
mpz_set_si(mpz_mask, strtol(snum.c_str(), NULL, 10));
mpz_class t_mpzc(mpz_mask);
node = NumInst::create(t_mpzc, sz);
assert (str_num[0] == '-');

int i = 0;
int j = str_num.length() - 1;
for(; i < int(str_num.length() - 1); ++i, --j){
bv_val[i] = (str_num[j] == '0') ? '1' : '0';
}
for(; i < sz; ++i){
bv_val[i] = '1';
}
// plus one
for(i=0; i < sz; ++i){
if(bv_val[i] == '1'){
bv_val[i] = '0';
}else{
bv_val[i] = '1';
break;
}
}
} else {
node = NumInst::create(snum, sz, 10, sort);
int i = 0;
int j = str_num.length() - 1;
for(; i < int(str_num.length()); ++i, --j){
bv_val[i] = str_num[j];
}
for(; i < sz; ++i){
bv_val[i] = '0';
}
}
for(int i=0; i < sz; ++i){
str_bv = bv_val[i] + str_bv;
}
// if (sz != 1)
node = NumInst::create(str_bv, sz, 2, sort);
// {
// string numstr = NumInst::as(node)->get_mpz()->get_str(10);
// if (numstr != snum) {
Expand Down

0 comments on commit 4225df4

Please sign in to comment.