Skip to content

Commit 4225df4

Browse files
aman-goelaman-goel
committed
Exp changes
1 parent bd241b6 commit 4225df4

File tree

3 files changed

+138
-15
lines changed

3 files changed

+138
-15
lines changed

‎src/reach/avr_word_netlist.cpp

Lines changed: 79 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1822,6 +1822,17 @@ int OpInst::get_simple_version() {
18221822

18231823
void OpInst::propagate_uf() {
18241824
switch (m_op) {
1825+
case Minus: {
1826+
const InstL* ch = get_children();
1827+
if (ch->size() == 1) {
1828+
InstL::const_iterator cit = ch->begin();
1829+
Inst* lhs = (*cit)->get_simple();
1830+
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
1831+
// -0 = 0
1832+
t_simple = lhs;
1833+
}
1834+
}
1835+
} break;
18251836
case Add: {
18261837
const InstL* ch = get_children();
18271838
if (ch->size() == 2) {
@@ -1944,6 +1955,13 @@ void OpInst::propagate_uf() {
19441955
} else if (lhs == rhs) {
19451956
// x > x = false
19461957
t_simple = NumInst::create(0, 1, SORT());
1958+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
1959+
// both are numbers
1960+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) > 0) {
1961+
t_simple = NumInst::create(1, 1, SORT());
1962+
} else {
1963+
t_simple = NumInst::create(0, 1, SORT());
1964+
}
19471965
}
19481966
} break;
19491967
case SGr: {
@@ -1956,6 +1974,15 @@ void OpInst::propagate_uf() {
19561974
if (lhs == rhs) {
19571975
// x >s x = false
19581976
t_simple = NumInst::create(0, 1, SORT());
1977+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
1978+
// both are numbers
1979+
if (get_size() > 1) {
1980+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) > 0) {
1981+
t_simple = NumInst::create(1, 1, SORT());
1982+
} else {
1983+
t_simple = NumInst::create(0, 1, SORT());
1984+
}
1985+
}
19591986
}
19601987
} break;
19611988
case Le: {
@@ -1971,6 +1998,13 @@ void OpInst::propagate_uf() {
19711998
} else if (lhs == rhs) {
19721999
// x < x = false
19732000
t_simple = NumInst::create(0, 1, SORT());
2001+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
2002+
// both are numbers
2003+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) < 0) {
2004+
t_simple = NumInst::create(1, 1, SORT());
2005+
} else {
2006+
t_simple = NumInst::create(0, 1, SORT());
2007+
}
19742008
}
19752009
} break;
19762010
case SLe: {
@@ -1983,6 +2017,15 @@ void OpInst::propagate_uf() {
19832017
if (lhs == rhs) {
19842018
// x <s x = false
19852019
t_simple = NumInst::create(0, 1, SORT());
2020+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
2021+
// both are numbers
2022+
if (get_size() > 1) {
2023+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) < 0) {
2024+
t_simple = NumInst::create(1, 1, SORT());
2025+
} else {
2026+
t_simple = NumInst::create(0, 1, SORT());
2027+
}
2028+
}
19862029
}
19872030
} break;
19882031
case GrEq: {
@@ -1998,6 +2041,13 @@ void OpInst::propagate_uf() {
19982041
} else if (lhs == rhs) {
19992042
// x >= x = true
20002043
t_simple = NumInst::create(1, 1, SORT());
2044+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
2045+
// both are numbers
2046+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) >= 0) {
2047+
t_simple = NumInst::create(1, 1, SORT());
2048+
} else {
2049+
t_simple = NumInst::create(0, 1, SORT());
2050+
}
20012051
}
20022052
} break;
20032053
case SGrEq: {
@@ -2010,6 +2060,15 @@ void OpInst::propagate_uf() {
20102060
if (lhs == rhs) {
20112061
// x >=s x = true
20122062
t_simple = NumInst::create(1, 1, SORT());
2063+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
2064+
// both are numbers
2065+
if (get_size() > 1) {
2066+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) >= 0) {
2067+
t_simple = NumInst::create(1, 1, SORT());
2068+
} else {
2069+
t_simple = NumInst::create(0, 1, SORT());
2070+
}
2071+
}
20132072
}
20142073
} break;
20152074
case LeEq: {
@@ -2025,6 +2084,13 @@ void OpInst::propagate_uf() {
20252084
} else if (lhs == rhs) {
20262085
// x <= x = true
20272086
t_simple = NumInst::create(1, 1, SORT());
2087+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
2088+
// both are numbers
2089+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) <= 0) {
2090+
t_simple = NumInst::create(1, 1, SORT());
2091+
} else {
2092+
t_simple = NumInst::create(0, 1, SORT());
2093+
}
20282094
}
20292095
} break;
20302096
case SLeEq: {
@@ -2037,7 +2103,16 @@ void OpInst::propagate_uf() {
20372103
if (lhs == rhs) {
20382104
// x <=s x = true
20392105
t_simple = NumInst::create(1, 1, SORT());
2040-
}
2106+
} else if (NumInst::as(lhs) && NumInst::as(rhs)) {
2107+
// both are numbers
2108+
if (get_size() > 1) {
2109+
if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) <= 0) {
2110+
t_simple = NumInst::create(1, 1, SORT());
2111+
} else {
2112+
t_simple = NumInst::create(0, 1, SORT());
2113+
}
2114+
}
2115+
}
20412116
} break;
20422117
case BitWiseAnd: {
20432118
const InstL* ch = get_children();
@@ -2142,9 +2217,9 @@ void OpInst::propagate_uf() {
21422217
;
21432218
}
21442219

2145-
// if (this != this->get_simple()) {
2146-
// cout << "uf_prop: " << *this << " -> " << *(this->t_simple) << endl;
2147-
// }
2220+
if (this != this->get_simple()) {
2221+
cout << "uf_prop: " << *this << " -> " << *(this->t_simple) << endl;
2222+
}
21482223
}
21492224

21502225
bool OpInst::is_heavy_uf() {

‎src/reach/avr_word_netlist.h

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2131,6 +2131,26 @@ class NumInst: public Inst {
21312131
return m_mpz.get_si();
21322132
}
21332133

2134+
int num_cmp(NumInst* rhs, bool sign) {
2135+
assert (get_sort_type() == bvtype);
2136+
if (!sign) {
2137+
return mpz_cmp(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t());
2138+
} else {
2139+
assert(get_size() > 1);
2140+
string str_lhs = get_mpz()->get_str(2);
2141+
string str_rhs = rhs->get_mpz()->get_str(2);
2142+
if (str_lhs[0] == '0' && str_rhs[0] == '0') {
2143+
return mpz_cmp(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t());
2144+
} else if (str_lhs[0] == '0' && str_rhs[0] == '1') {
2145+
return 1;
2146+
} else if (str_lhs[0] == '1' && str_rhs[0] == '0') {
2147+
return -1;
2148+
} else {
2149+
return (-1)*mpz_cmpabs(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t());
2150+
}
2151+
}
2152+
}
2153+
21342154
static Inst *read_bin();
21352155
virtual void write_bin();
21362156

‎src/vwn/btor2_frontend.cpp

Lines changed: 39 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -511,21 +511,49 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
511511
} break;
512512
case BTOR2_TAG_constd: {
513513
string snum(t.constant);
514+
515+
mpz_t mpz_mask;
516+
mpz_init(mpz_mask);
517+
mpz_set_si(mpz_mask, strtol(snum.c_str(), NULL, 10));
518+
mpz_class t_mpzc(mpz_mask);
519+
string str_num = t_mpzc.get_str(2);
520+
521+
char bv_val[sz];
522+
string str_bv = "";
514523
if (snum[0] == '-') {
515-
if (sz == 1) {
516-
//boolean negative means 1 (since sign bit has to be 1)
517-
node = NumInst::create(1, sz);
518-
} else {
519-
mpz_t mpz_mask;
520-
mpz_init(mpz_mask);
521-
mpz_set_si(mpz_mask, strtol(snum.c_str(), NULL, 10));
522-
mpz_class t_mpzc(mpz_mask);
523-
node = NumInst::create(t_mpzc, sz);
524+
assert (str_num[0] == '-');
525+
526+
int i = 0;
527+
int j = str_num.length() - 1;
528+
for(; i < int(str_num.length() - 1); ++i, --j){
529+
bv_val[i] = (str_num[j] == '0') ? '1' : '0';
530+
}
531+
for(; i < sz; ++i){
532+
bv_val[i] = '1';
533+
}
534+
// plus one
535+
for(i=0; i < sz; ++i){
536+
if(bv_val[i] == '1'){
537+
bv_val[i] = '0';
538+
}else{
539+
bv_val[i] = '1';
540+
break;
541+
}
524542
}
525543
} else {
526-
node = NumInst::create(snum, sz, 10, sort);
544+
int i = 0;
545+
int j = str_num.length() - 1;
546+
for(; i < int(str_num.length()); ++i, --j){
547+
bv_val[i] = str_num[j];
548+
}
549+
for(; i < sz; ++i){
550+
bv_val[i] = '0';
551+
}
552+
}
553+
for(int i=0; i < sz; ++i){
554+
str_bv = bv_val[i] + str_bv;
527555
}
528-
// if (sz != 1)
556+
node = NumInst::create(str_bv, sz, 2, sort);
529557
// {
530558
// string numstr = NumInst::as(node)->get_mpz()->get_str(10);
531559
// if (numstr != snum) {

0 commit comments

Comments
 (0)