Browse files

A bit of compiler code cleanup

  • Loading branch information...
1 parent 7ee4a6a commit 1bd19a2f609bc33b8e16d7a454a96c43cad3862a @mwolf76 committed Jan 18, 2013
View
194 src/model/compilers/algebra.cc
@@ -122,15 +122,8 @@ void Compiler::algebraic_plus(const Expr_ptr expr)
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_arithmetical();
- ADD rhs[width];
- for (unsigned i = 0; i < width ; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width ; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
/* perform arithmetic sum using positional algorithm */
ADD carry = f_enc.zero();
@@ -141,37 +134,31 @@ void Compiler::algebraic_plus(const Expr_ptr expr)
ADD tmp = lhs[ndx].Plus(rhs[ndx]).Plus(carry);
carry = f_enc.base().LEQ(tmp); /* c >= 0x10 */
- /* x[i] = (x[i] + y[i] + c) % base */ // TODO: detect overflow on MSB
- f_add_stack.push_back(tmp.Modulus(f_enc.base()));
+ /* x[i] = (x[i] + y[i] + c) % base */
+ PUSH(tmp.Modulus(f_enc.base()));
}
}
void Compiler::algebraic_sub(const Expr_ptr expr)
{
+ ExprMgr& em = f_owner.em();
assert( is_binary_algebraic(expr) );
/* rewrite requires discarding operands */
algebraic_discard_op();
algebraic_discard_op();
- ExprMgr& em = f_owner.em();
- (*this)(em.make_add(expr->lhs(), em.make_neg(expr->rhs())));
+ (*this)( em.make_add( expr->lhs(),
+ em.make_neg(expr->rhs())));
}
void Compiler::algebraic_mul(const Expr_ptr expr)
{
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_arithmetical();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
ADD res[width];
ADD tmp[width];
@@ -209,7 +196,7 @@ void Compiler::algebraic_mul(const Expr_ptr expr)
}
// return i-th digit of result
- f_add_stack.push_back(res[ndx_i]);
+ PUSH(res[ndx_i]);
}
}
@@ -230,22 +217,15 @@ void Compiler::algebraic_and(const Expr_ptr expr)
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_arithmetical();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
/* perform bw arithmetic, nothing fancy here :-) */
for (unsigned i = 0; i < width; ++ i) {
/* x[i] & y[i] */
unsigned ndx = width - i - 1;
- f_add_stack.push_back(lhs[ndx].BWTimes(rhs[ndx]));
+ PUSH(lhs[ndx].BWTimes(rhs[ndx]));
}
}
@@ -254,22 +234,15 @@ void Compiler::algebraic_or(const Expr_ptr expr)
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_arithmetical();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
/* perform bw arithmetic, nothing fancy here :-) */
for (unsigned i = 0; i < width; ++ i) {
/* x[i] | y[i] */
unsigned ndx = width - i - 1;
- f_add_stack.push_back(lhs[ndx].BWOr(rhs[ndx]));
+ PUSH(lhs[ndx].BWOr(rhs[ndx]));
}
}
@@ -278,65 +251,52 @@ void Compiler::algebraic_xor(const Expr_ptr expr)
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_arithmetical();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
/* perform bw arithmetic, nothing fancy here :-) */
for (unsigned i = 0; i < width; ++ i) {
/* x[i] ^ y[i] */
unsigned ndx = width - i - 1;
- f_add_stack.push_back(lhs[ndx].BWXor(rhs[ndx]));
+ PUSH(lhs[ndx].BWXor(rhs[ndx]));
}
}
void Compiler::algebraic_xnor(const Expr_ptr expr)
{
+ ExprMgr& em = f_owner.em();
assert( is_binary_algebraic(expr) );
/* rewrite requires discarding operands */
algebraic_discard_op();
algebraic_discard_op();
- ExprMgr& em = f_owner.em();
- (*this)(em.make_not( em.make_xor( expr->lhs(), expr->rhs())));
+ (*this)(em.make_not( em.make_xor( expr->lhs(),
+ expr->rhs())));
}
void Compiler::algebraic_implies(const Expr_ptr expr)
{
+ ExprMgr& em = f_owner.em();
assert( is_binary_algebraic(expr) );
/* rewrite requires discarding operands */
algebraic_discard_op();
algebraic_discard_op();
- ExprMgr& em = f_owner.em();
- (*this)(em.make_or( em.make_not( expr->lhs()), expr->rhs()));
+ (*this)(em.make_or( em.make_not( expr->lhs()),
+ expr->rhs()));
}
void Compiler::algebraic_lshift(const Expr_ptr expr)
{
+ ExprMgr& em = f_owner.em();
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_arithmetical();
- ExprMgr& em = f_owner.em();
-
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
ADD tmp[width];
for (unsigned i = 0; i < width; ++ i) {
@@ -379,26 +339,19 @@ void Compiler::algebraic_lshift(const Expr_ptr expr)
/* push result (reversed) */
for (unsigned i = 0; i < width; ++ i) {
unsigned ndx = width - i - 1;
- f_add_stack.push_back( res[ndx]);
+ PUSH( res[ndx]);
}
}
void Compiler::algebraic_rshift(const Expr_ptr expr)
{
- assert( is_binary_algebraic(expr) );
- unsigned width = algebrize_binary_arithmetical();
-
ExprMgr& em = f_owner.em();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ assert( is_binary_algebraic(expr) );
+ unsigned width = algebrize_binary_arithmetical();
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
ADD tmp[width];
for (unsigned i = 0; i < width; ++ i) {
@@ -443,25 +396,17 @@ void Compiler::algebraic_rshift(const Expr_ptr expr)
/* push result (reversed) */
for (unsigned i = 0; i < width; ++ i) {
unsigned ndx = width - i - 1;
- f_add_stack.push_back(res[ndx]);
+ PUSH(res[ndx]);
}
}
void Compiler::algebraic_equals(const Expr_ptr expr)
{
assert( is_binary_algebraic(expr) );
-
unsigned width = algebrize_binary_relational();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
ADD tmp[width];
for (unsigned i = 0; i < width; ++ i) {
@@ -470,19 +415,20 @@ void Compiler::algebraic_equals(const Expr_ptr expr)
}
/* just one result */
- f_add_stack.push_back(optimize_and_chain(tmp, width));
+ PUSH(optimize_and_chain(tmp, width));
}
void Compiler::algebraic_not_equals(const Expr_ptr expr)
{
+ ExprMgr& em = f_owner.em();
assert( is_binary_algebraic(expr) );
/* rewrite requires discarding operands */
algebraic_discard_op();
algebraic_discard_op();
- ExprMgr& em = f_owner.em();
- (*this)(em.make_not(em.make_eq(expr->lhs(), expr->rhs())));
+ (*this)(em.make_not(em.make_eq(expr->lhs(),
+ expr->rhs())));
}
void Compiler::algebraic_gt(const Expr_ptr expr)
@@ -499,34 +445,28 @@ void Compiler::algebraic_gt(const Expr_ptr expr)
void Compiler::algebraic_ge(const Expr_ptr expr)
{
+ ExprMgr& em = f_owner.em();
assert( is_binary_algebraic(expr) );
/* rewrite requires discarding operands */
algebraic_discard_op();
algebraic_discard_op();
- ExprMgr& em = f_owner.em();
- (*this)(em.make_not( em.make_lt( expr->lhs(), expr->rhs())));
+ (*this)(em.make_not( em.make_lt( expr->lhs(),
+ expr->rhs())));
}
void Compiler::algebraic_lt(const Expr_ptr expr)
{
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_relational();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
/* MSB predicate first, if false and prefix matches, inspect next
digit. */
- ADD tmp = f_enc.zero();
+ ADD pred = f_enc.zero();
for (unsigned i = 0; i < width; ++ i) {
ADD phi[1 + i];
@@ -539,31 +479,24 @@ void Compiler::algebraic_lt(const Expr_ptr expr)
phi[i] = lhs[i].LT(rhs[i]);
/* add optimized chain to disjunction */
- tmp = tmp.Or( optimize_and_chain(phi, 1 + i));
+ pred = pred.Or( optimize_and_chain(phi, 1 + i));
}
- /* just one result */
- f_add_stack.push_back(tmp);
+ /* just one predult */
+ PUSH(pred);
}
void Compiler::algebraic_le(const Expr_ptr expr)
{
assert( is_binary_algebraic(expr) );
unsigned width = algebrize_binary_relational();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
/* MSB predicate first, if false and prefix matches, inspect next
digit. */
- ADD tmp = f_enc.zero();
+ ADD pred = f_enc.zero();
for (unsigned i = 0; i < width; ++ i) {
ADD phi[1 + i];
@@ -577,34 +510,25 @@ void Compiler::algebraic_le(const Expr_ptr expr)
phi[i] = lhs[i].LEQ(rhs[i]);
/* add optimized chain to disjunction */
- tmp = tmp.Or( optimize_and_chain(phi, 1 + i));
+ pred = pred.Or( optimize_and_chain(phi, 1 + i));
}
/* just one result */
- f_add_stack.push_back(tmp);
+ PUSH(pred);
}
void Compiler::algebraic_ite(const Expr_ptr expr)
{
assert( is_ite_algebraic(expr) );
unsigned width = algebrize_ternary_ite();
- ADD rhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- rhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD lhs[width];
- for (unsigned i = 0; i < width; ++ i) {
- lhs[i] = f_add_stack.back(); f_add_stack.pop_back();
- }
-
- ADD cond = f_add_stack.back(); f_add_stack.pop_back();
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
+ POP_ADD(cnd);
+ /* (cond) ? x[i] : y[i] */
for (unsigned i = 0; i < width; ++ i) {
-
- /* (cond) ? x[i] : y[i] */
unsigned ndx = width - i - 1;
- f_add_stack.push_back(cond.Ite(lhs[ndx], rhs[ndx]));
+ PUSH(cnd.Ite(lhs[ndx], rhs[ndx]));
}
}
View
37 src/model/compilers/boolean.cc
@@ -39,52 +39,47 @@
void Compiler::boolean_not(const Expr_ptr expr)
{
- const ADD top = f_add_stack.back(); f_add_stack.pop_back();
- f_add_stack.push_back(top.Cmpl());
+ POP_ADD(lhs);
+ f_add_stack.push_back(lhs.Cmpl());
}
void Compiler::boolean_and(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Times(rhs)); /* 0, 1 logic uses arithmetic product for AND */
- f_add_stack.push_back(lhs.Times(rhs)); /* 0, 1 logic uses arithmetic product */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::boolean_or(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Or(rhs));
- f_add_stack.push_back(lhs.Or(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::boolean_xor(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Xor(rhs));
- f_add_stack.push_back(lhs.Xor(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::boolean_xnor(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Xnor(rhs));
- f_add_stack.push_back(lhs.Xnor(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::boolean_implies(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Cmpl().Or(rhs));
- f_add_stack.push_back(lhs.Cmpl().Or(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
@@ -96,11 +91,9 @@ void Compiler::boolean_not_equals(const Expr_ptr expr)
void Compiler::boolean_ite(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD cnd = f_add_stack.back(); f_add_stack.pop_back();
-
- f_add_stack.push_back(cnd.Ite(lhs, rhs));
+ POP_TWO(rhs, lhs);
+ POP_ADD(cnd);
+ PUSH(cnd.Ite(lhs, rhs));
// consume two operand types, leave the third
f_type_stack.pop_back();
View
230 src/model/compilers/compiler.cc
@@ -132,16 +132,16 @@ void Compiler::walk_neg_postorder(const Expr_ptr expr)
{
if (is_unary_integer(expr)) {
integer_neg(expr);
- memoize_result(expr);
- return;
+ }
+ else if (is_unary_fixed(expr)) {
+ fixed_neg(expr);
}
else if (is_unary_algebraic(expr)) {
algebraic_neg(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_not_preorder(const Expr_ptr expr)
@@ -150,16 +150,16 @@ void Compiler::walk_not_postorder(const Expr_ptr expr)
{
if (is_unary_boolean(expr)) {
boolean_not(expr);
- memoize_result(expr);
- return;
+ }
+ else if (is_unary_integer(expr)) {
+ integer_not(expr);
}
else if (is_unary_algebraic(expr)) {
algebraic_not(expr); // bitwise
- memoize_result(expr);
- return;
}
+ else assert(false); // unreachable
- assert(false); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_add_preorder(const Expr_ptr expr)
@@ -170,17 +170,16 @@ void Compiler::walk_add_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_plus(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_plus(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_plus(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_sub_preorder(const Expr_ptr expr)
@@ -190,17 +189,17 @@ bool Compiler::walk_sub_inorder(const Expr_ptr expr)
void Compiler::walk_sub_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
- memoize_result(expr);
- return;
+ integer_sub(expr);
+ }
+ else if (is_binary_fixed(expr)) {
+ fixed_sub(expr);
}
-
else if (is_binary_algebraic(expr)) {
algebraic_sub(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unexpected
- assert( false ); // unexpected
+ memoize_result(expr);
}
bool Compiler::walk_div_preorder(const Expr_ptr expr)
@@ -211,17 +210,16 @@ void Compiler::walk_div_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_div(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_div(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_div(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unexpected
- assert( false ); // unexpected
+ memoize_result(expr);
}
bool Compiler::walk_mul_preorder(const Expr_ptr expr)
@@ -232,17 +230,16 @@ void Compiler::walk_mul_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_mul(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_mul(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_mul(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_mod_preorder(const Expr_ptr expr)
@@ -253,17 +250,13 @@ void Compiler::walk_mod_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_mod(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_algebraic(expr)) {
algebraic_mod(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_and_preorder(const Expr_ptr expr)
@@ -274,23 +267,16 @@ void Compiler::walk_and_postorder(const Expr_ptr expr)
{
if (is_binary_boolean(expr)) {
boolean_and(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_integer(expr)) {
integer_and(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_algebraic(expr)) {
algebraic_and(expr); // bitwise
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_or_preorder(const Expr_ptr expr)
@@ -301,21 +287,16 @@ void Compiler::walk_or_postorder(const Expr_ptr expr)
{
if (is_binary_boolean(expr)) {
boolean_or(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_integer(expr)) {
integer_or(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_algebraic(expr)) {
algebraic_or(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
+
+ memoize_result(expr);
}
bool Compiler::walk_xor_preorder(const Expr_ptr expr)
@@ -326,23 +307,16 @@ void Compiler::walk_xor_postorder(const Expr_ptr expr)
{
if (is_binary_boolean(expr)) {
boolean_xor(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_integer(expr)) {
integer_xor(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_algebraic(expr)) {
algebraic_xor(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_xnor_preorder(const Expr_ptr expr)
@@ -353,23 +327,16 @@ void Compiler::walk_xnor_postorder(const Expr_ptr expr)
{
if (is_binary_boolean(expr)) {
boolean_xnor(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_integer(expr)) {
integer_xnor(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_algebraic(expr)) {
algebraic_xnor(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_implies_preorder(const Expr_ptr expr)
@@ -380,23 +347,16 @@ void Compiler::walk_implies_postorder(const Expr_ptr expr)
{
if (is_binary_boolean(expr)) {
boolean_implies(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_integer(expr)) {
integer_implies(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_algebraic(expr)) {
algebraic_implies(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_iff_preorder(const Expr_ptr expr)
@@ -414,16 +374,13 @@ void Compiler::walk_lshift_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_lshift(expr);
- memoize_result(expr);
- return;
}
else if (is_binary_algebraic(expr)) {
algebraic_lshift(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_rshift_preorder(const Expr_ptr expr)
@@ -434,16 +391,13 @@ void Compiler::walk_rshift_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_rshift(expr);
- memoize_result(expr);
- return;
}
else if (is_binary_algebraic(expr)) {
algebraic_rshift(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_eq_preorder(const Expr_ptr expr)
@@ -454,23 +408,19 @@ void Compiler::walk_eq_postorder(const Expr_ptr expr)
{
if (is_binary_boolean(expr)) {
boolean_equals(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_integer(expr)) {
integer_equals(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_equals(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_equals(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_ne_preorder(const Expr_ptr expr)
@@ -481,23 +431,19 @@ void Compiler::walk_ne_postorder(const Expr_ptr expr)
{
if (is_binary_boolean(expr)) {
boolean_not_equals(expr);
- memoize_result(expr);
- return;
}
-
else if (is_binary_integer(expr)) {
integer_not_equals(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_not_equals(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_not_equals(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_gt_preorder(const Expr_ptr expr)
@@ -508,16 +454,16 @@ void Compiler::walk_gt_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_gt(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_gt(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_gt(expr);
- memoize_result(expr);
- return;
}
else assert( false );
+
+ memoize_result(expr);
}
bool Compiler::walk_ge_preorder(const Expr_ptr expr)
@@ -528,17 +474,16 @@ void Compiler::walk_ge_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_ge(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_ge(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_ge(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_lt_preorder(const Expr_ptr expr)
@@ -549,17 +494,18 @@ void Compiler::walk_lt_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_lt(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_lt(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_lt(expr);
memoize_result(expr);
return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_le_preorder(const Expr_ptr expr)
@@ -570,17 +516,16 @@ void Compiler::walk_le_postorder(const Expr_ptr expr)
{
if (is_binary_integer(expr)) {
integer_le(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_binary_fixed(expr)) {
+ fixed_le(expr);
+ }
else if (is_binary_algebraic(expr)) {
algebraic_le(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
+ memoize_result(expr);
}
bool Compiler::walk_ite_preorder(const Expr_ptr expr)
@@ -591,30 +536,23 @@ void Compiler::walk_ite_postorder(const Expr_ptr expr)
{
if (is_ite_boolean(expr)) {
boolean_ite(expr);
- memoize_result(expr);
- return;
}
-
else if (is_ite_integer(expr)) {
integer_ite(expr);
- memoize_result(expr);
- return;
}
-
+ else if (is_ite_fixed(expr)) {
+ fixed_ite(expr);
+ }
else if (is_ite_enumerative(expr)) {
enumerative_ite(expr);
- memoize_result(expr);
- return;
}
-
else if (is_ite_algebraic(expr)) {
algebraic_ite(expr);
- memoize_result(expr);
- return;
}
+ else assert( false ); // unreachable
- assert( false ); // unreachable
- }
+ memoize_result(expr);
+}
bool Compiler::walk_cond_preorder(const Expr_ptr expr)
{ return cache_miss(expr); }
View
28 src/model/compilers/compiler.hh
@@ -50,6 +50,24 @@ typedef pair<YDDMap::iterator, bool> YDDHit;
typedef unordered_map<FQExpr, IEncoding_ptr, FQExprHash, FQExprEq> ENCMap;
typedef pair<ENCMap::iterator, bool> ENCHit;
+/* shortcuts to to simplify manipulation of the internal ADD stack */
+#define POP_ADD(op) \
+ const ADD op = f_add_stack.back(); \
+ f_add_stack.pop_back()
+
+#define POP_TWO(rhs,lhs) \
+ POP_ADD(rhs); POP_ADD(lhs)
+
+#define POP_ALGEBRAIC(vec, width) \
+ ADD vec[width]; \
+ for (unsigned i = 0; i < width ; ++ i) { \
+ vec[i] = f_add_stack.back(); \
+ f_add_stack.pop_back(); \
+ }
+
+/* shortcut for pushing */
+#define PUSH(add) f_add_stack.push_back(add)
+
class Compiler : public SimpleWalker {
public:
Compiler();
@@ -155,6 +173,7 @@ protected:
// partial results
ADDStack f_add_stack;
+ ADDStack f_tmp_stack; // used for binary algebrizations
// current ctx stack, for symbol resolution
ExprStack f_ctx_stack;
@@ -226,19 +245,11 @@ protected:
void integer_ite(const Expr_ptr expr);
void fixed_neg(const Expr_ptr expr);
- void fixed_not(const Expr_ptr expr);
void fixed_plus(const Expr_ptr expr);
void fixed_sub(const Expr_ptr expr);
void fixed_div(const Expr_ptr expr);
void fixed_mul(const Expr_ptr expr);
void fixed_mod(const Expr_ptr expr);
- void fixed_and(const Expr_ptr expr);
- void fixed_or(const Expr_ptr expr);
- void fixed_xor(const Expr_ptr expr);
- void fixed_xnor(const Expr_ptr expr);
- void fixed_implies(const Expr_ptr expr);
- void fixed_lshift(const Expr_ptr expr);
- void fixed_rshift(const Expr_ptr expr);
void fixed_equals(const Expr_ptr expr);
void fixed_not_equals(const Expr_ptr expr);
void fixed_gt(const Expr_ptr expr);
@@ -278,6 +289,7 @@ protected:
/* -- internals --------------------------------------------------------- */
bool cache_miss(const Expr_ptr expr);
void memoize_result(const Expr_ptr expr);
+ void flush_operands();
/* push dds and type information for variables (used by walk_leaf) */
void push_variable(IEncoding_ptr enc, Type_ptr type);
View
25 src/model/compilers/enumerative.cc
@@ -39,33 +39,30 @@
void Compiler::enumerative_equals(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Equals(rhs));
- f_add_stack.push_back(lhs.Equals(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::enumerative_not_equals(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Equals(rhs).Cmpl());
- f_add_stack.push_back(lhs.Equals(rhs).Cmpl());
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::enumerative_ite(const Expr_ptr expr)
{
- TypeMgr& tm = f_owner.tm();
-
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD c = f_add_stack.back(); f_add_stack.pop_back();
- f_add_stack.push_back(c.Ite(lhs, rhs));
+ POP_TWO(rhs, lhs);
+ POP_ADD(cnd);
+ PUSH(cnd.Ite(lhs, rhs));
+ // consume all, push rhs type
+ Type_ptr type = f_type_stack.back();
+ f_type_stack.pop_back();
f_type_stack.pop_back();
f_type_stack.pop_back();
- f_type_stack.pop_back(); // consume all, push integer
- f_type_stack.push_back(tm.find_int_const());
+ f_type_stack.push_back(type);
}
View
76 src/model/compilers/fixed.cc
@@ -40,103 +40,65 @@
#include <compiler.hh>
void Compiler::fixed_neg(const Expr_ptr expr)
-{
-}
+{ integer_neg(expr); }
void Compiler::fixed_plus(const Expr_ptr expr)
-{
-}
+{ integer_plus(expr); }
void Compiler::fixed_sub(const Expr_ptr expr)
-{
-}
+{ integer_sub(expr); }
void Compiler::fixed_mul(const Expr_ptr expr)
{
+ assert( false ); // TODO
}
void Compiler::fixed_div(const Expr_ptr expr)
{
+ assert( false ); // TODO
}
void Compiler::fixed_mod(const Expr_ptr expr)
{
-}
-
-void Compiler::fixed_and(const Expr_ptr expr)
-{
-}
-
-void Compiler::fixed_or(const Expr_ptr expr)
-{
-}
-
-void Compiler::fixed_xor(const Expr_ptr expr)
-{
-}
-
-void Compiler::fixed_xnor(const Expr_ptr expr)
-{
-}
-
-void Compiler::fixed_implies(const Expr_ptr expr)
-{
-}
-
-void Compiler::fixed_lshift(const Expr_ptr expr)
-{
-}
-
-void Compiler::fixed_rshift(const Expr_ptr expr)
-{
+ assert( false ); // TODO
}
void Compiler::fixed_equals(const Expr_ptr expr)
-{
-}
+{ integer_equals(expr); }
void Compiler::fixed_not_equals(const Expr_ptr expr)
-{
-}
+{ integer_not_equals(expr); }
void Compiler::fixed_gt(const Expr_ptr expr)
-{
-}
+{ integer_gt(expr); }
void Compiler::fixed_ge(const Expr_ptr expr)
-{
-}
+{ integer_ge(expr); }
void Compiler::fixed_lt(const Expr_ptr expr)
-{
-}
+{ integer_lt(expr); }
void Compiler::fixed_le(const Expr_ptr expr)
-{
-}
+{ integer_le(expr); }
void Compiler::fixed_ite(const Expr_ptr expr)
{
- #if 0 // LATER
TypeMgr& tm = f_owner.tm();
FQExpr key(expr); const Type_ptr type = f_owner.type(key);
- unsigned width = tm.as_algebraic(type)->width();
+ unsigned width = tm.calculate_width(type);
- const ADD tmp = f_add_stack.back(); f_add_stack.pop_back();
- algebraic_from_integer_const(width); // rhs
-
- f_add_stack.push_back(tmp);
- algebraic_from_integer_const(width); // lhs
+ assert( 0 == f_tmp_stack.size() );
+ algebraic_from_fxd_const(width); // rhs
+ algebraic_from_fxd_const(width); // lhs
+ flush_operands();
/* fix type stack, constants are always unsigned */
f_type_stack.pop_back();
f_type_stack.pop_back();
- f_type_stack.push_back( tm.find_unsigned( width ));
- f_type_stack.push_back( tm.find_unsigned( width ));
+ f_type_stack.push_back( type );
+ f_type_stack.push_back( type );
/* re-uses general algorithm */
algebraic_ite(expr);
-#endif
-
}
View
114 src/model/compilers/integer.cc
@@ -39,194 +39,174 @@
void Compiler::integer_neg(const Expr_ptr expr)
{
- const ADD top = f_add_stack.back(); f_add_stack.pop_back();
-
- f_add_stack.push_back(top.Negate());
+ POP_ADD(lhs);
+ PUSH(lhs.Negate());
}
void Compiler::integer_plus(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Plus(rhs));
- f_add_stack.push_back(lhs.Plus(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_sub(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Minus(rhs));
- f_add_stack.push_back(lhs.Minus(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_mul(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Times(rhs));
- f_add_stack.push_back(lhs.Times(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_div(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Divide(rhs));
- f_add_stack.push_back(lhs.Divide(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_mod(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Modulus(rhs));
- f_add_stack.push_back(lhs.Modulus(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_and(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.BWTimes(rhs)); /* bitwise integer arithmetic */
- f_add_stack.push_back(lhs.BWTimes(rhs)); /* bitwise integer arithmetic */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_or(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.BWOr(rhs)); /* bitwise integer arithmetic */
- f_add_stack.push_back(lhs.BWOr(rhs)); /* bitwise integer arithmetic */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_xor(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.BWXor(rhs)); /* bitwise integer arithmetic */
- f_add_stack.push_back(lhs.BWXor(rhs)); /* bitwise integer arithmetic */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_xnor(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.BWXnor(rhs)); /* bitwise integer arithmetic */
- f_add_stack.push_back(lhs.BWXnor(rhs)); /* bitwise integer arithmetic */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_implies(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.BWCmpl().BWXor(rhs)); /* bitwise integer arithmetic */
- f_add_stack.push_back(lhs.BWCmpl().BWXor(rhs)); /* bitwise integer arithmetic */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_lshift(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.LShift(rhs)); /* bitwise integer arithmetic */
- f_add_stack.push_back(lhs.LShift(rhs)); /* bitwise integer arithmetic */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_rshift(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.RShift(rhs)); /* bitwise integer arithmetic */
- f_add_stack.push_back(lhs.RShift(rhs)); /* bitwise integer arithmetic */
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_equals(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Equals(rhs));
- f_add_stack.push_back(lhs.Equals(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_not_equals(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.Equals(rhs).Cmpl());
- f_add_stack.push_back(lhs.Equals(rhs).Cmpl());
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_gt(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(rhs.LT(lhs)); // simulate GT op
- f_add_stack.push_back(rhs.LT(lhs)); // simulate GT op
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_ge(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(rhs.LEQ(lhs)); // simulate GEQ op
- f_add_stack.push_back(rhs.LEQ(lhs)); // simulate GEQ op
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_lt(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.LT(rhs));
- f_add_stack.push_back(lhs.LT(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
void Compiler::integer_le(const Expr_ptr expr)
{
- const ADD rhs = f_add_stack.back(); f_add_stack.pop_back();
- const ADD lhs = f_add_stack.back(); f_add_stack.pop_back();
+ POP_TWO(rhs, lhs);
+ PUSH(lhs.LEQ(rhs));
- f_add_stack.push_back(lhs.LEQ(rhs));
f_type_stack.pop_back(); // consume one, leave the other
}
+/* ITE is not a proper const manipulation as it *always* is a function
+ of the condition. The result of an ITE is an algebraic */
void Compiler::integer_ite(const Expr_ptr expr)
{
-#if 0 // LATER
TypeMgr& tm = f_owner.tm();
FQExpr key(expr); const Type_ptr type = f_owner.type(key);
- unsigned width = tm.as_algebraic(type)->width();
-
- const ADD tmp = f_add_stack.back(); f_add_stack.pop_back();
- algebraic_from_integer_const(width); // rhs
+ unsigned width = tm.calculate_width(type);
- f_add_stack.push_back(tmp);
- algebraic_from_integer_const(width); // lhs
+ assert( 0 == f_tmp_stack.size() );
+ algebraic_from_int_const(width); // rhs
+ algebraic_from_int_const(width); // lhs
+ flush_operands();
/* fix type stack, constants are always unsigned */
f_type_stack.pop_back();
f_type_stack.pop_back();
- f_type_stack.push_back( tm.find_unsigned( width ));
- f_type_stack.push_back( tm.find_unsigned( width ));
+ f_type_stack.push_back( type );
+ f_type_stack.push_back( type );
/* re-uses general algorithm */
algebraic_ite(expr);
-#endif
}
View
49 src/model/compilers/internals.cc
@@ -246,17 +246,17 @@ unsigned Compiler::algebrize_unary_subscript()
void Compiler::algebraic_from_int_const(unsigned width)
{
- const ADD top = f_add_stack.back(); f_add_stack.pop_back();
- assert (f_enc.is_constant(top));
+ POP_ADD(add);
+ assert (f_enc.is_constant(add));
- value_t value = f_enc.const_value(top);
+ value_t value = f_enc.const_value(add);
unsigned base = Cudd_V(f_enc.base().getNode());
if (value < 0) {
value += pow(base, width); // 2's complement
}
for (unsigned i = 0; i < width; ++ i) {
ADD digit = f_enc.constant(value % base);
- f_add_stack.push_back(digit);
+ f_tmp_stack.push_back(digit);
value /= base;
}
@@ -266,12 +266,10 @@ void Compiler::algebraic_from_int_const(unsigned width)
void Compiler::algebraic_from_fxd_const(unsigned width)
{
-#if 0 // LATER...
-
- const ADD top = f_add_stack.back(); f_add_stack.pop_back();
- assert (f_enc.is_constant(top));
+ POP_ADD(add);
+ assert (f_enc.is_constant(add));
- value_t value = f_enc.const_value(top);
+ value_t value = f_enc.const_value(add);
unsigned base = Cudd_V(f_enc.base().getNode());
if (value < 0) {
value += pow(base, width); // 2's complement
@@ -283,32 +281,8 @@ void Compiler::algebraic_from_fxd_const(unsigned width)
}
assert (value == 0); // not overflowing
-#endif
-
- assert (0);
}
-// void Compiler::algebraic_from_int_const(unsigned width)
-// {
-// const ADD top = f_add_stack.back(); f_add_stack.pop_back();
-// assert (f_enc.is_constant(top));
-
-// value_t value = f_enc.const_value(top);
-// unsigned base = Cudd_V(f_enc.base().getNode());
-// if (value < 0) {
-// value += pow(base, width); // 2's complement
-// }
-// for (unsigned i = 0; i < width; ++ i) {
-// ADD digit = f_enc.constant(value % base);
-// f_add_stack.push_back(digit);
-// value /= base;
-// }
-
-// assert (value == 0); // not overflowing
-// // DRIVEL << "ALGEBRAIC " << width << endl;
-// }
-
-
/* extends a DD vector on top of the stack from old_width to
new_width */
void Compiler::algebraic_padding(unsigned old_width,
@@ -815,3 +789,12 @@ Type_ptr Compiler::algebraic_make_int_of_fxd_type(Type_ptr type)
return res;
}
+
+void Compiler::flush_operands()
+{
+ for (ADDStack::reverse_iterator ri = f_tmp_stack.rbegin();
+ f_tmp_stack.rend() != ri; ++ ri) {
+ PUSH(*ri);
+ }
+ f_tmp_stack.clear();
+}

0 comments on commit 1bd19a2

Please sign in to comment.