if (model_undef && dup_undef && bit == RTLIL::State::Sx)
vec.push_back(ez->frozen_literal());
else
- vec.push_back(bit == (undef_mode ? RTLIL::State::Sx : RTLIL::State::S1) ? ez->TRUE : ez->FALSE);
+ vec.push_back(bit == (undef_mode ? RTLIL::State::Sx : RTLIL::State::S1) ? ez->CONST_TRUE : ez->CONST_FALSE);
} else {
std::string name = pf + stringf(bit.wire->width == 1 ? "%s" : "%s [%d]", RTLIL::id2cstr(bit.wire->name), bit.offset);
vec.push_back(ez->frozen_literal(name));
if (!forced_signed && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
- vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
+ vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->CONST_FALSE);
while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
- vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
+ vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->CONST_FALSE);
}
void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
{
bool is_signed = forced_signed || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
while (vec_a.size() < vec_y.size())
- vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
+ vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->CONST_FALSE);
while (vec_y.size() < vec_a.size())
vec_y.push_back(ez->literal());
}
if (is_arith_compare) {
for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->FALSE, undef_y.at(i));
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
ez->SET(undef_y_bit, undef_y.at(0));
} else {
std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
int a = importDefSigSpec(cell->getPort("\\A"), timestep).at(0);
int b = importDefSigSpec(cell->getPort("\\B"), timestep).at(0);
int c = importDefSigSpec(cell->getPort("\\C"), timestep).at(0);
- int d = three_mode ? (aoi_mode ? ez->TRUE : ez->FALSE) : importDefSigSpec(cell->getPort("\\D"), timestep).at(0);
+ int d = three_mode ? (aoi_mode ? ez->CONST_TRUE : ez->CONST_FALSE) : importDefSigSpec(cell->getPort("\\D"), timestep).at(0);
int y = importDefSigSpec(cell->getPort("\\Y"), timestep).at(0);
int yy = model_undef ? ez->literal() : y;
int undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep).at(0);
int undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep).at(0);
int undef_c = importUndefSigSpec(cell->getPort("\\C"), timestep).at(0);
- int undef_d = three_mode ? ez->FALSE : importUndefSigSpec(cell->getPort("\\D"), timestep).at(0);
+ int undef_d = three_mode ? ez->CONST_FALSE : importUndefSigSpec(cell->getPort("\\D"), timestep).at(0);
int undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep).at(0);
if (aoi_mode)
std::vector<int> undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
- int maybe_one_hot = ez->FALSE;
- int maybe_many_hot = ez->FALSE;
+ int maybe_one_hot = ez->CONST_FALSE;
+ int maybe_many_hot = ez->CONST_FALSE;
- int sure_one_hot = ez->FALSE;
- int sure_many_hot = ez->FALSE;
+ int sure_one_hot = ez->CONST_FALSE;
+ int sure_many_hot = ez->CONST_FALSE;
- std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->FALSE);
- std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->FALSE);
+ std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
+ std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
for (size_t i = 0; i < s.size(); i++)
{
if (cell->type == "$pos") {
ez->assume(ez->vec_eq(a, yy));
} else {
- std::vector<int> zero(a.size(), ez->FALSE);
+ std::vector<int> zero(a.size(), ez->CONST_FALSE);
ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
}
if (cell->type == "$logic_not")
ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->FALSE, yy.at(i));
+ ez->SET(ez->CONST_FALSE, yy.at(i));
if (model_undef)
{
log_abort();
for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->FALSE, undef_y.at(i));
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
undefGating(y, yy, undef_y);
}
else
ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->FALSE, yy.at(i));
+ ez->SET(ez->CONST_FALSE, yy.at(i));
if (model_undef)
{
log_abort();
for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->FALSE, undef_y.at(i));
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
undefGating(y, yy, undef_y);
}
if (cell->type == "$gt")
ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->FALSE, yy.at(i));
+ ez->SET(ez->CONST_FALSE, yy.at(i));
if (model_undef && (cell->type == "$eqx" || cell->type == "$nex"))
{
yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
for (size_t i = 0; i < y.size(); i++)
- ez->SET(ez->FALSE, undef_y.at(i));
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
ez->assume(ez->vec_eq(y, yy));
}
int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->FALSE, undef_y.at(i));
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
ez->SET(undef_y_bit, undef_y.at(0));
undefGating(y, yy, undef_y);
std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
- int extend_bit = ez->FALSE;
+ int extend_bit = ez->CONST_FALSE;
if (!cell->type.in("$shift", "$shiftx") && cell->parameters["\\A_SIGNED"].as_bool())
extend_bit = a.back();
std::vector<int> shifted_a;
if (cell->type == "$shl" || cell->type == "$sshl")
- shifted_a = ez->vec_shift_left(a, b, false, ez->FALSE, ez->FALSE);
+ shifted_a = ez->vec_shift_left(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
if (cell->type == "$shr")
- shifted_a = ez->vec_shift_right(a, b, false, ez->FALSE, ez->FALSE);
+ shifted_a = ez->vec_shift_right(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
if (cell->type == "$sshr")
- shifted_a = ez->vec_shift_right(a, b, false, cell->parameters["\\A_SIGNED"].as_bool() ? a.back() : ez->FALSE, ez->FALSE);
+ shifted_a = ez->vec_shift_right(a, b, false, cell->parameters["\\A_SIGNED"].as_bool() ? a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
if (cell->type == "$shift" || cell->type == "$shiftx")
- shifted_a = ez->vec_shift_right(a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->FALSE, ez->FALSE);
+ shifted_a = ez->vec_shift_right(a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
ez->assume(ez->vec_eq(shifted_a, yy));
std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
std::vector<int> undef_a_shifted;
- extend_bit = cell->type == "$shiftx" ? ez->TRUE : ez->FALSE;
+ extend_bit = cell->type == "$shiftx" ? ez->CONST_TRUE : ez->CONST_FALSE;
if (!cell->type.in("$shift", "$shiftx") && cell->parameters["\\A_SIGNED"].as_bool())
extend_bit = undef_a.back();
undef_a.push_back(extend_bit);
if (cell->type == "$shl" || cell->type == "$sshl")
- undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->FALSE, ez->FALSE);
+ undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
if (cell->type == "$shr")
- undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->FALSE, ez->FALSE);
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
if (cell->type == "$sshr")
- undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters["\\A_SIGNED"].as_bool() ? undef_a.back() : ez->FALSE, ez->FALSE);
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters["\\A_SIGNED"].as_bool() ? undef_a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
if (cell->type == "$shift")
- undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->FALSE, ez->FALSE);
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
if (cell->type == "$shiftx")
- undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->TRUE, ez->TRUE);
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->CONST_TRUE, ez->CONST_TRUE);
int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- std::vector<int> tmp(a.size(), ez->FALSE);
+ std::vector<int> tmp(a.size(), ez->CONST_FALSE);
for (int i = 0; i < int(a.size()); i++)
{
- std::vector<int> shifted_a(a.size(), ez->FALSE);
+ std::vector<int> shifted_a(a.size(), ez->CONST_FALSE);
for (int j = i; j < int(a.size()); j++)
shifted_a.at(j) = a.at(j-i);
tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
Macc macc;
macc.from_cell(cell);
- std::vector<int> tmp(GetSize(y), ez->FALSE);
+ std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
for (auto &port : macc.ports)
{
std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
while (GetSize(in_a) < GetSize(y))
- in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->FALSE);
+ in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->CONST_FALSE);
in_a.resize(GetSize(y));
if (GetSize(in_b))
{
while (GetSize(in_b) < GetSize(y))
- in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->FALSE);
+ in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->CONST_FALSE);
in_b.resize(GetSize(y));
for (int i = 0; i < GetSize(in_b); i++) {
- std::vector<int> shifted_a(in_a.size(), ez->FALSE);
+ std::vector<int> shifted_a(in_a.size(), ez->CONST_FALSE);
for (int j = i; j < int(in_a.size()); j++)
shifted_a.at(j) = in_a.at(j-i);
if (port.do_subtract)
}
for (int i = 0; i < GetSize(b); i++) {
- std::vector<int> val(GetSize(y), ez->FALSE);
+ std::vector<int> val(GetSize(y), ez->CONST_FALSE);
val.at(0) = b.at(i);
tmp = ez->vec_add(tmp, val);
}
}
std::vector<int> chain_buf = a_u;
- std::vector<int> y_u(a_u.size(), ez->FALSE);
+ std::vector<int> y_u(a_u.size(), ez->CONST_FALSE);
for (int i = int(a.size())-1; i >= 0; i--)
{
- chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->FALSE);
+ chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->CONST_FALSE);
- std::vector<int> b_shl(i, ez->FALSE);
+ std::vector<int> b_shl(i, ez->CONST_FALSE);
b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
- b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->FALSE);
+ b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->CONST_FALSE);
y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
std::vector<int> div_zero_result;
if (cell->type == "$div") {
if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
- std::vector<int> all_ones(y.size(), ez->TRUE);
- std::vector<int> only_first_one(y.size(), ez->FALSE);
- only_first_one.at(0) = ez->TRUE;
+ std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
+ std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
+ only_first_one.at(0) = ez->CONST_TRUE;
div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
} else {
- div_zero_result.insert(div_zero_result.end(), cell->getPort("\\A").size(), ez->TRUE);
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
+ div_zero_result.insert(div_zero_result.end(), cell->getPort("\\A").size(), ez->CONST_TRUE);
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
}
} else {
int copy_a_bits = std::min(cell->getPort("\\A").size(), cell->getPort("\\B").size());
if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
else
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
}
ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
}
std::vector<int> lut;
for (auto bit : cell->getParam("\\LUT").bits)
- lut.push_back(bit == RTLIL::S1 ? ez->TRUE : ez->FALSE);
+ lut.push_back(bit == RTLIL::S1 ? ez->CONST_TRUE : ez->CONST_FALSE);
while (GetSize(lut) < (1 << GetSize(a)))
- lut.push_back(ez->FALSE);
+ lut.push_back(ez->CONST_FALSE);
lut.resize(1 << GetSize(a));
if (model_undef)
{
std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
- std::vector<int> t(lut), u(GetSize(t), ez->FALSE);
+ std::vector<int> t(lut), u(GetSize(t), ez->CONST_FALSE);
for (int i = GetSize(a)-1; i >= 0; i--)
{
#include <stdlib.h>
-const int ezSAT::TRUE = 1;
-const int ezSAT::FALSE = 2;
+const int ezSAT::CONST_TRUE = 1;
+const int ezSAT::CONST_FALSE = 2;
ezSAT::ezSAT()
{
solverTimeout = 0;
solverTimoutStatus = false;
- literal("TRUE");
- literal("FALSE");
+ literal("CONST_TRUE");
+ literal("CONST_FALSE");
- assert(literal("TRUE") == TRUE);
- assert(literal("FALSE") == FALSE);
+ assert(literal("CONST_TRUE") == CONST_TRUE);
+ assert(literal("CONST_FALSE") == CONST_FALSE);
}
ezSAT::~ezSAT()
int ezSAT::value(bool val)
{
- return val ? TRUE : FALSE;
+ return val ? CONST_TRUE : CONST_FALSE;
}
int ezSAT::literal()
{
if (arg == 0)
continue;
- if (op == OpAnd && arg == TRUE)
+ if (op == OpAnd && arg == CONST_TRUE)
continue;
- if ((op == OpOr || op == OpXor) && arg == FALSE)
+ if ((op == OpOr || op == OpXor) && arg == CONST_FALSE)
continue;
- if (op == OpXor && arg == TRUE) {
+ if (op == OpXor && arg == CONST_TRUE) {
xorRemovedOddTrues = !xorRemovedOddTrues;
continue;
}
{
case OpNot:
assert(myArgs.size() == 1);
- if (myArgs[0] == TRUE)
- return FALSE;
- if (myArgs[0] == FALSE)
- return TRUE;
+ if (myArgs[0] == CONST_TRUE)
+ return CONST_FALSE;
+ if (myArgs[0] == CONST_FALSE)
+ return CONST_TRUE;
break;
case OpAnd:
if (myArgs.size() == 0)
- return TRUE;
+ return CONST_TRUE;
if (myArgs.size() == 1)
return myArgs[0];
break;
case OpOr:
if (myArgs.size() == 0)
- return FALSE;
+ return CONST_FALSE;
if (myArgs.size() == 1)
return myArgs[0];
break;
case OpXor:
if (myArgs.size() == 0)
- return xorRemovedOddTrues ? TRUE : FALSE;
+ return xorRemovedOddTrues ? CONST_TRUE : CONST_FALSE;
if (myArgs.size() == 1)
return xorRemovedOddTrues ? NOT(myArgs[0]) : myArgs[0];
break;
case OpIFF:
assert(myArgs.size() >= 1);
if (myArgs.size() == 1)
- return TRUE;
+ return CONST_TRUE;
// FIXME: Add proper const folding
break;
case OpITE:
assert(myArgs.size() == 3);
- if (myArgs[0] == TRUE)
+ if (myArgs[0] == CONST_TRUE)
return myArgs[1];
- if (myArgs[0] == FALSE)
+ if (myArgs[0] == CONST_FALSE)
return myArgs[2];
break;
int ezSAT::eval(int id, const std::vector<int> &values) const
{
if (id > 0) {
- if (id <= int(values.size()) && (values[id-1] == TRUE || values[id-1] == FALSE || values[id-1] == 0))
+ if (id <= int(values.size()) && (values[id-1] == CONST_TRUE || values[id-1] == CONST_FALSE || values[id-1] == 0))
return values[id-1];
return 0;
}
case OpNot:
assert(args.size() == 1);
a = eval(args[0], values);
- if (a == TRUE)
- return FALSE;
- if (a == FALSE)
- return TRUE;
+ if (a == CONST_TRUE)
+ return CONST_FALSE;
+ if (a == CONST_FALSE)
+ return CONST_TRUE;
return 0;
case OpAnd:
- a = TRUE;
+ a = CONST_TRUE;
for (auto arg : args) {
b = eval(arg, values);
- if (b != TRUE && b != FALSE)
+ if (b != CONST_TRUE && b != CONST_FALSE)
a = 0;
- if (b == FALSE)
- return FALSE;
+ if (b == CONST_FALSE)
+ return CONST_FALSE;
}
return a;
case OpOr:
- a = FALSE;
+ a = CONST_FALSE;
for (auto arg : args) {
b = eval(arg, values);
- if (b != TRUE && b != FALSE)
+ if (b != CONST_TRUE && b != CONST_FALSE)
a = 0;
- if (b == TRUE)
- return TRUE;
+ if (b == CONST_TRUE)
+ return CONST_TRUE;
}
return a;
case OpXor:
- a = FALSE;
+ a = CONST_FALSE;
for (auto arg : args) {
b = eval(arg, values);
- if (b != TRUE && b != FALSE)
+ if (b != CONST_TRUE && b != CONST_FALSE)
return 0;
- if (b == TRUE)
- a = a == TRUE ? FALSE : TRUE;
+ if (b == CONST_TRUE)
+ a = a == CONST_TRUE ? CONST_FALSE : CONST_TRUE;
}
return a;
case OpIFF:
a = eval(args[0], values);
for (auto arg : args) {
b = eval(arg, values);
- if (b != TRUE && b != FALSE)
+ if (b != CONST_TRUE && b != CONST_FALSE)
return 0;
if (b != a)
- return FALSE;
+ return CONST_FALSE;
}
- return TRUE;
+ return CONST_TRUE;
case OpITE:
assert(args.size() == 3);
a = eval(args[0], values);
- if (a == TRUE)
+ if (a == CONST_TRUE)
return eval(args[1], values);
- if (a == FALSE)
+ if (a == CONST_FALSE)
return eval(args[2], values);
return 0;
default:
}
if (cnfLiteralVariables[id-1] == 0) {
cnfLiteralVariables[id-1] = ++cnfVariableCount;
- if (id == TRUE)
+ if (id == CONST_TRUE)
add_clause(+cnfLiteralVariables[id-1]);
- if (id == FALSE)
+ if (id == CONST_FALSE)
add_clause(-cnfLiteralVariables[id-1]);
}
return cnfLiteralVariables[id-1];
{
std::vector<int> vec;
for (auto bit : bits)
- vec.push_back(bit ? TRUE : FALSE);
+ vec.push_back(bit ? CONST_TRUE : CONST_FALSE);
return vec;
}
{
std::vector<int> vec;
for (int i = 0; i < numBits; i++)
- vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE);
+ vec.push_back(((value >> i) & 1) != 0 ? CONST_TRUE : CONST_FALSE);
return vec;
}
{
std::vector<int> vec;
for (int i = 0; i < numBits; i++)
- vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE);
+ vec.push_back(((value >> i) & 1) != 0 ? CONST_TRUE : CONST_FALSE);
return vec;
}
std::vector<int> vec;
for (int i = 0; i < toBits; i++)
if (i >= int(vec1.size()))
- vec.push_back(signExtend ? vec1.back() : FALSE);
+ vec.push_back(signExtend ? vec1.back() : CONST_FALSE);
else
vec.push_back(vec1[i]);
return vec;
{
assert(vec1.size() == vec2.size());
std::vector<int> vec(vec1.size());
- int carry = FALSE;
+ int carry = CONST_FALSE;
for (int i = 0; i < int(vec1.size()); i++)
fulladder(this, vec1[i], vec2[i], carry, carry, vec[i]);
{
assert(vec1.size() == vec2.size());
std::vector<int> vec(vec1.size());
- int carry = TRUE;
+ int carry = CONST_TRUE;
for (int i = 0; i < int(vec1.size()); i++)
fulladder(this, vec1[i], NOT(vec2[i]), carry, carry, vec[i]);
std::vector<int> ezSAT::vec_neg(const std::vector<int> &vec)
{
- std::vector<int> zero(vec.size(), FALSE);
+ std::vector<int> zero(vec.size(), CONST_FALSE);
return vec_sub(zero, vec);
}
void ezSAT::vec_cmp(const std::vector<int> &vec1, const std::vector<int> &vec2, int &carry, int &overflow, int &sign, int &zero)
{
assert(vec1.size() == vec2.size());
- carry = TRUE;
- zero = FALSE;
+ carry = CONST_TRUE;
+ zero = CONST_FALSE;
for (int i = 0; i < int(vec1.size()); i++) {
overflow = carry;
fulladder(this, vec1[i], NOT(vec2[i]), carry, carry, sign);
for (int i = 0; i < int(vec1.size()); i++) {
int j = i-shift;
if (int(vec1.size()) <= j)
- vec.push_back(signExtend ? vec1.back() : FALSE);
+ vec.push_back(signExtend ? vec1.back() : CONST_FALSE);
else if (0 <= j)
vec.push_back(vec1[j]);
else
- vec.push_back(FALSE);
+ vec.push_back(CONST_FALSE);
}
return vec;
}
int vec2_bits = std::min(my_clog2(vec1.size()) + (vec2_signed ? 1 : 0), int(vec2.size()));
std::vector<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
- int overflow_left = FALSE, overflow_right = FALSE;
+ int overflow_left = CONST_FALSE, overflow_right = CONST_FALSE;
if (vec2_signed) {
- int overflow = FALSE;
+ int overflow = CONST_FALSE;
for (auto bit : overflow_bits)
overflow = OR(overflow, XOR(bit, vec2[vec2_bits-1]));
overflow_left = AND(overflow, NOT(vec2.back()));
for (int i = -1; i < N; i++)
for (int j = -1; j < M; j++)
- x[std::pair<int,int>(i,j)] = j < 0 ? TRUE : i < 0 ? FALSE : literal();
+ x[std::pair<int,int>(i,j)] = j < 0 ? CONST_TRUE : i < 0 ? CONST_FALSE : literal();
for (int i = 0; i < N; i++)
for (int j = 0; j < M; j++) {
int ezSAT::ordered(const std::vector<int> &vec1, const std::vector<int> &vec2, bool allow_equal)
{
std::vector<int> formula;
- int last_x = FALSE;
+ int last_x = CONST_FALSE;
assert(vec1.size() == vec2.size());
for (size_t i = 0; i < vec1.size(); i++)
int a = vec1[i], b = vec2[i];
formula.push_back(OR(NOT(a), b, last_x));
- int next_x = i+1 < vec1.size() ? literal() : allow_equal ? FALSE : TRUE;
+ int next_x = i+1 < vec1.size() ? literal() : allow_equal ? CONST_FALSE : CONST_TRUE;
formula.push_back(OR(a, b, last_x, NOT(next_x)));
formula.push_back(OR(NOT(a), NOT(b), last_x, NOT(next_x)));
last_x = next_x;