From 7cb0d3aa1acf37025e82846f809d066356a98843 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 10 Oct 2014 17:06:02 +0200 Subject: [PATCH] Renamed TRUE/FALSE to CONST_TRUE/CONST_FALSE because of name collision on Win32 --- kernel/satgen.h | 104 +++++++++++++++++----------------- libs/ezsat/ezminisat.cc | 4 +- libs/ezsat/ezsat.cc | 120 ++++++++++++++++++++-------------------- libs/ezsat/ezsat.h | 6 +- passes/sat/eval.cc | 2 +- 5 files changed, 118 insertions(+), 118 deletions(-) diff --git a/kernel/satgen.h b/kernel/satgen.h index 2759b3927..779c97506 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -66,7 +66,7 @@ struct SatGen 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)); @@ -160,9 +160,9 @@ struct SatGen 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 &vec_a, std::vector &vec_b, std::vector &vec_y, RTLIL::Cell *cell, bool forced_signed = false) @@ -176,7 +176,7 @@ struct SatGen { 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()); } @@ -226,7 +226,7 @@ struct SatGen 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 undef_y_bits(undef_y.size(), undef_y_bit); @@ -307,7 +307,7 @@ struct SatGen 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; @@ -321,7 +321,7 @@ struct SatGen 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) @@ -433,14 +433,14 @@ struct SatGen std::vector undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep); std::vector 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 bits_set = std::vector(undef_y.size(), ez->FALSE); - std::vector bits_clr = std::vector(undef_y.size(), ez->FALSE); + std::vector bits_set = std::vector(undef_y.size(), ez->CONST_FALSE); + std::vector bits_clr = std::vector(undef_y.size(), ez->CONST_FALSE); for (size_t i = 0; i < s.size(); i++) { @@ -482,7 +482,7 @@ struct SatGen if (cell->type == "$pos") { ez->assume(ez->vec_eq(a, yy)); } else { - std::vector zero(a.size(), ez->FALSE); + std::vector zero(a.size(), ez->CONST_FALSE); ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy)); } @@ -524,7 +524,7 @@ struct SatGen 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) { @@ -546,7 +546,7 @@ struct SatGen 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); } @@ -569,7 +569,7 @@ struct SatGen 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) { @@ -592,7 +592,7 @@ struct SatGen 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); } @@ -630,7 +630,7 @@ struct SatGen 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")) { @@ -645,7 +645,7 @@ struct SatGen 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)); } @@ -667,7 +667,7 @@ struct SatGen 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); @@ -689,7 +689,7 @@ struct SatGen std::vector b = importDefSigSpec(cell->getPort("\\B"), timestep); std::vector 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(); @@ -703,16 +703,16 @@ struct SatGen std::vector 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)); @@ -723,7 +723,7 @@ struct SatGen std::vector undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep); std::vector 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(); @@ -733,19 +733,19 @@ struct SatGen 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 undef_all_y_bits(undef_y.size(), undef_any_b); @@ -764,10 +764,10 @@ struct SatGen std::vector yy = model_undef ? ez->vec_var(y.size()) : y; - std::vector tmp(a.size(), ez->FALSE); + std::vector tmp(a.size(), ez->CONST_FALSE); for (int i = 0; i < int(a.size()); i++) { - std::vector shifted_a(a.size(), ez->FALSE); + std::vector 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); @@ -791,7 +791,7 @@ struct SatGen Macc macc; macc.from_cell(cell); - std::vector tmp(GetSize(y), ez->FALSE); + std::vector tmp(GetSize(y), ez->CONST_FALSE); for (auto &port : macc.ports) { @@ -799,17 +799,17 @@ struct SatGen std::vector 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 shifted_a(in_a.size(), ez->FALSE); + std::vector 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) @@ -828,7 +828,7 @@ struct SatGen } for (int i = 0; i < GetSize(b); i++) { - std::vector val(GetSize(y), ez->FALSE); + std::vector val(GetSize(y), ez->CONST_FALSE); val.at(0) = b.at(i); tmp = ez->vec_add(tmp, val); } @@ -871,14 +871,14 @@ struct SatGen } std::vector chain_buf = a_u; - std::vector y_u(a_u.size(), ez->FALSE); + std::vector 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 b_shl(i, ez->FALSE); + std::vector 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); @@ -905,13 +905,13 @@ struct SatGen std::vector div_zero_result; if (cell->type == "$div") { if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) { - std::vector all_ones(y.size(), ez->TRUE); - std::vector only_first_one(y.size(), ez->FALSE); - only_first_one.at(0) = ez->TRUE; + std::vector all_ones(y.size(), ez->CONST_TRUE); + std::vector 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()); @@ -919,7 +919,7 @@ struct SatGen 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))); } @@ -939,15 +939,15 @@ struct SatGen std::vector 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 undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep); - std::vector t(lut), u(GetSize(t), ez->FALSE); + std::vector t(lut), u(GetSize(t), ez->CONST_FALSE); for (int i = GetSize(a)-1; i >= 0; i--) { diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index dc4e5d283..267355ada 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -37,8 +37,8 @@ ezMiniSAT::ezMiniSAT() : minisatSolver(NULL) minisatSolver = NULL; foundContradiction = false; - freeze(TRUE); - freeze(FALSE); + freeze(CONST_TRUE); + freeze(CONST_FALSE); } ezMiniSAT::~ezMiniSAT() diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 13ed112ed..754691f7b 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -25,8 +25,8 @@ #include -const int ezSAT::TRUE = 1; -const int ezSAT::FALSE = 2; +const int ezSAT::CONST_TRUE = 1; +const int ezSAT::CONST_FALSE = 2; ezSAT::ezSAT() { @@ -42,11 +42,11 @@ 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() @@ -55,7 +55,7 @@ ezSAT::~ezSAT() int ezSAT::value(bool val) { - return val ? TRUE : FALSE; + return val ? CONST_TRUE : CONST_FALSE; } int ezSAT::literal() @@ -105,11 +105,11 @@ int ezSAT::expression(OpId op, const std::vector &args) { 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; } @@ -131,29 +131,29 @@ int ezSAT::expression(OpId op, const std::vector &args) { 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; @@ -161,15 +161,15 @@ int ezSAT::expression(OpId op, const std::vector &args) 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; @@ -281,7 +281,7 @@ std::string ezSAT::to_string(int id) const int ezSAT::eval(int id, const std::vector &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; } @@ -295,39 +295,39 @@ int ezSAT::eval(int id, const std::vector &values) const 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: @@ -335,18 +335,18 @@ int ezSAT::eval(int id, const std::vector &values) const 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: @@ -516,9 +516,9 @@ int ezSAT::bind(int id, bool auto_freeze) } 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]; @@ -638,7 +638,7 @@ std::vector ezSAT::vec_const(const std::vector &bits) { std::vector vec; for (auto bit : bits) - vec.push_back(bit ? TRUE : FALSE); + vec.push_back(bit ? CONST_TRUE : CONST_FALSE); return vec; } @@ -646,7 +646,7 @@ std::vector ezSAT::vec_const_signed(int64_t value, int numBits) { std::vector 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; } @@ -654,7 +654,7 @@ std::vector ezSAT::vec_const_unsigned(uint64_t value, int numBits) { std::vector 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; } @@ -679,7 +679,7 @@ std::vector ezSAT::vec_cast(const std::vector &vec1, int toBits, bool std::vector 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; @@ -807,7 +807,7 @@ std::vector ezSAT::vec_add(const std::vector &vec1, const std::vector< { assert(vec1.size() == vec2.size()); std::vector 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]); @@ -831,7 +831,7 @@ std::vector ezSAT::vec_sub(const std::vector &vec1, const std::vector< { assert(vec1.size() == vec2.size()); std::vector 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]); @@ -853,15 +853,15 @@ std::vector ezSAT::vec_sub(const std::vector &vec1, const std::vector< std::vector ezSAT::vec_neg(const std::vector &vec) { - std::vector zero(vec.size(), FALSE); + std::vector zero(vec.size(), CONST_FALSE); return vec_sub(zero, vec); } void ezSAT::vec_cmp(const std::vector &vec1, const std::vector &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); @@ -954,11 +954,11 @@ std::vector ezSAT::vec_shl(const std::vector &vec1, int shift, bool si 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; } @@ -1005,10 +1005,10 @@ std::vector ezSAT::vec_shift_right(const std::vector &vec1, const std: int vec2_bits = std::min(my_clog2(vec1.size()) + (vec2_signed ? 1 : 0), int(vec2.size())); std::vector 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())); @@ -1330,7 +1330,7 @@ int ezSAT::manyhot(const std::vector &vec, int min_hot, int max_hot) for (int i = -1; i < N; i++) for (int j = -1; j < M; j++) - x[std::pair(i,j)] = j < 0 ? TRUE : i < 0 ? FALSE : literal(); + x[std::pair(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++) { @@ -1358,7 +1358,7 @@ int ezSAT::manyhot(const std::vector &vec, int min_hot, int max_hot) int ezSAT::ordered(const std::vector &vec1, const std::vector &vec2, bool allow_equal) { std::vector formula; - int last_x = FALSE; + int last_x = CONST_FALSE; assert(vec1.size() == vec2.size()); for (size_t i = 0; i < vec1.size(); i++) @@ -1366,7 +1366,7 @@ int ezSAT::ordered(const std::vector &vec1, const std::vector &vec2, b 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; diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index c5ef6b0a2..cac6ff0f7 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -34,7 +34,7 @@ class ezSAT // the number zero is not used as valid token number and is used to encode // unused parameters for the functions. // - // positive numbers are literals, with 1 = TRUE and 2 = FALSE; + // positive numbers are literals, with 1 = CONST_TRUE and 2 = CONST_FALSE; // // negative numbers are non-literal expressions. each expression is represented // by an operator id and a list of expressions (literals or non-literals). @@ -44,8 +44,8 @@ public: OpNot, OpAnd, OpOr, OpXor, OpIFF, OpITE }; - static const int TRUE; - static const int FALSE; + static const int CONST_TRUE; + static const int CONST_FALSE; private: bool flag_keep_cnf; diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index 875896fcd..7a5a02a9b 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -204,7 +204,7 @@ struct VlogHammerReporter if (y_undef.at(i)) { log(" Toggling undef bit %d to test undef gating.\n", i); - if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.FALSE : ez.TRUE))) + if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.CONST_FALSE : ez.CONST_TRUE))) log_error("Failed to find solution with toggled bit!\n"); cmp_vars.push_back(y_vec.at(expected_y.size() + i)); -- 2.30.2