Renamed TRUE/FALSE to CONST_TRUE/CONST_FALSE because of name collision on Win32
authorClifford Wolf <clifford@clifford.at>
Fri, 10 Oct 2014 15:06:02 +0000 (17:06 +0200)
committerClifford Wolf <clifford@clifford.at>
Fri, 10 Oct 2014 15:07:24 +0000 (17:07 +0200)
kernel/satgen.h
libs/ezsat/ezminisat.cc
libs/ezsat/ezsat.cc
libs/ezsat/ezsat.h
passes/sat/eval.cc

index 2759b3927b231d30685c7fd187dc05016f1a90e6..779c97506fd6aca719e2caf3a863bb1e08cb7603 100644 (file)
@@ -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<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &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<int> 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<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++)
                                {
@@ -482,7 +482,7 @@ struct SatGen
                        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));
                        }
 
@@ -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<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();
@@ -703,16 +703,16 @@ struct SatGen
                        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));
 
@@ -723,7 +723,7 @@ struct SatGen
                                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();
 
@@ -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<int> undef_all_y_bits(undef_y.size(), undef_any_b);
@@ -764,10 +764,10 @@ struct SatGen
 
                        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);
@@ -791,7 +791,7 @@ struct SatGen
                        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)
                        {
@@ -799,17 +799,17 @@ struct SatGen
                                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)
@@ -828,7 +828,7 @@ struct SatGen
                        }
 
                        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);
                        }
@@ -871,14 +871,14 @@ struct SatGen
                        }
 
                        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);
@@ -905,13 +905,13 @@ struct SatGen
                                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());
@@ -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<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--)
                                {
index dc4e5d28374283324157c7ce27e240f1ddd51411..267355adab00656cd4325d5bd3ca0c6a0705ac95 100644 (file)
@@ -37,8 +37,8 @@ ezMiniSAT::ezMiniSAT() : minisatSolver(NULL)
        minisatSolver = NULL;
        foundContradiction = false;
 
-       freeze(TRUE);
-       freeze(FALSE);
+       freeze(CONST_TRUE);
+       freeze(CONST_FALSE);
 }
 
 ezMiniSAT::~ezMiniSAT()
index 13ed112ed231a506272a29e23920d683b973c887..754691f7b7b33c8ea15d3d358e3138bf84905f56 100644 (file)
@@ -25,8 +25,8 @@
 
 #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()
 {
@@ -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<int> &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<int> &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<int> &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<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;
        }
@@ -295,39 +295,39 @@ int ezSAT::eval(int id, const std::vector<int> &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<int> &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<int> ezSAT::vec_const(const std::vector<bool> &bits)
 {
        std::vector<int> 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<int> ezSAT::vec_const_signed(int64_t value, int numBits)
 {
        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;
 }
 
@@ -654,7 +654,7 @@ std::vector<int> ezSAT::vec_const_unsigned(uint64_t value, int numBits)
 {
        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;
 }
 
@@ -679,7 +679,7 @@ std::vector<int> ezSAT::vec_cast(const std::vector<int> &vec1, int toBits, bool
        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;
@@ -807,7 +807,7 @@ std::vector<int> ezSAT::vec_add(const std::vector<int> &vec1, const std::vector<
 {
        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]);
 
@@ -831,7 +831,7 @@ std::vector<int> ezSAT::vec_sub(const std::vector<int> &vec1, const std::vector<
 {
        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]);
 
@@ -853,15 +853,15 @@ std::vector<int> ezSAT::vec_sub(const std::vector<int> &vec1, const std::vector<
 
 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);
@@ -954,11 +954,11 @@ std::vector<int> ezSAT::vec_shl(const std::vector<int> &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<int> ezSAT::vec_shift_right(const std::vector<int> &vec1, const std:
        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()));
@@ -1330,7 +1330,7 @@ int ezSAT::manyhot(const std::vector<int> &vec, int min_hot, int max_hot)
 
        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++) {
@@ -1358,7 +1358,7 @@ int ezSAT::manyhot(const std::vector<int> &vec, int min_hot, int max_hot)
 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++)
@@ -1366,7 +1366,7 @@ int ezSAT::ordered(const std::vector<int> &vec1, const std::vector<int> &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;
index c5ef6b0a2c298cd2a89617bd54f671e63aa9473a..cac6ff0f70e2395f71f8c3bdafab2847ffef6e14 100644 (file)
@@ -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;
index 875896fcdb96d85c4857927d35c00a254ab5bed5..7a5a02a9bb0df4250e3be97d22b808769bdfaca8 100644 (file)
@@ -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));