From 7cb0d3aa1acf37025e82846f809d066356a98843 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 10 Oct 2014 17:06:02 +0200 Subject: Renamed TRUE/FALSE to CONST_TRUE/CONST_FALSE because of name collision on Win32 --- libs/ezsat/ezminisat.cc | 4 +- libs/ezsat/ezsat.cc | 120 ++++++++++++++++++++++++------------------------ libs/ezsat/ezsat.h | 6 +-- 3 files changed, 65 insertions(+), 65 deletions(-) (limited to 'libs') 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; -- cgit v1.2.3 From 54bf3a95dd859ac1811a5265ad45f9eb596de3db Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 10 Oct 2014 18:34:19 +0200 Subject: More Win32 build fixes --- libs/subcircuit/subcircuit.cc | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'libs') diff --git a/libs/subcircuit/subcircuit.cc b/libs/subcircuit/subcircuit.cc index 84f23d636..cf14df0ac 100644 --- a/libs/subcircuit/subcircuit.cc +++ b/libs/subcircuit/subcircuit.cc @@ -34,6 +34,7 @@ using namespace SubCircuit; +#ifndef _YOSYS_ static std::string my_stringf(const char *fmt, ...) { std::string string; @@ -52,6 +53,9 @@ static std::string my_stringf(const char *fmt, ...) return string; } +#else +# define my_stringf YOSYS_NAMESPACE_PREFIX stringf +#endif SubCircuit::Graph::Graph(const Graph &other, const std::vector &otherNodes) { -- cgit v1.2.3 From 93e6ebe771c675280742adf6905298301575d0a7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 11 Oct 2014 10:24:46 +0200 Subject: Disabled ezminisat timeout feature for Win32 --- libs/ezsat/ezminisat.cc | 6 ++++++ libs/ezsat/ezminisat.h | 2 ++ 2 files changed, 8 insertions(+) (limited to 'libs') diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index 267355ada..b996d4a3d 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -77,6 +77,7 @@ bool ezMiniSAT::eliminated(int idx) } #endif +#ifndef _WIN32 ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL; clock_t ezMiniSAT::alarmHandlerTimeout = 0; @@ -88,6 +89,7 @@ void ezMiniSAT::alarmHandler(int) } else alarm(1); } +#endif bool ezMiniSAT::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { @@ -174,6 +176,7 @@ contradiction: #endif } +#ifndef _WIN32 struct sigaction sig_action; struct sigaction old_sig_action; int old_alarm_timeout = 0; @@ -188,9 +191,11 @@ contradiction: sigaction(SIGALRM, &sig_action, &old_sig_action); alarm(1); } +#endif bool foundSolution = minisatSolver->solve(assumps); +#ifndef _WIN32 if (solverTimeout > 0) { if (alarmHandlerTimeout == 0) solverTimoutStatus = true; @@ -198,6 +203,7 @@ contradiction: sigaction(SIGALRM, &old_sig_action, NULL); alarm(old_alarm_timeout); } +#endif if (!foundSolution) { #if !EZMINISAT_INCREMENTAL diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h index ac9c071c3..5b5252d88 100644 --- a/libs/ezsat/ezminisat.h +++ b/libs/ezsat/ezminisat.h @@ -51,9 +51,11 @@ private: std::set cnfFrozenVars; #endif +#ifndef _WIN32 static ezMiniSAT *alarmHandlerThis; static clock_t alarmHandlerTimeout; static void alarmHandler(int); +#endif public: ezMiniSAT(); -- cgit v1.2.3 From 7df8cbe2a9d48dbccb4a2c665e4087ed4f1514a8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 11 Oct 2014 10:46:50 +0200 Subject: Not using std::to_string in ezsat (problems with mingw) --- libs/ezsat/ezsat.cc | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'libs') diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 754691f7b..54a6e9c71 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -669,8 +669,11 @@ std::vector ezSAT::vec_var(int numBits) std::vector ezSAT::vec_var(std::string name, int numBits) { std::vector vec; - for (int i = 0; i < numBits; i++) - vec.push_back(VAR(name + "[" + std::to_string(i) + "]")); + for (int i = 0; i < numBits; i++) { + char buf[64]; + snprintf(buf, 64, " [%d]", i); + vec.push_back(VAR(name + buf)); + } return vec; } @@ -1195,7 +1198,7 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const fprintf(f, "c mapping of variables to expressions:\n"); for (int i = 0; i < int(cnfExpressionVariables.size()); i++) if (cnfExpressionVariables[i] != 0) - fprintf(f, "c %*d: %s\n", digits, cnfExpressionVariables[i], to_string(-i-1).c_str()); + fprintf(f, "c %*d: %d\n", digits, cnfExpressionVariables[i], -i-1); if (mode_keep_cnf()) { fprintf(f, "c\n"); @@ -1242,8 +1245,11 @@ static std::string expression2str(const std::pair> #undef X } text += ":"; - for (auto it : data.second) - text += " " + std::to_string(it); + for (auto it : data.second) { + char buf[64]; + snprintf(buf, 64, " %d", it); + text += buf; + } return text; } -- cgit v1.2.3 From 9ee3a4b94fa78ad2ccf4178d7a49bc659df29cb1 Mon Sep 17 00:00:00 2001 From: William Speirs Date: Tue, 14 Oct 2014 17:15:08 -0400 Subject: Changed to explicit heap allocated memory --- libs/sha1/sha1.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'libs') diff --git a/libs/sha1/sha1.cpp b/libs/sha1/sha1.cpp index dc86b2ce2..825274b9b 100644 --- a/libs/sha1/sha1.cpp +++ b/libs/sha1/sha1.cpp @@ -256,9 +256,12 @@ void SHA1::buffer_to_block(const std::string &buffer, uint32 block[BLOCK_BYTES]) void SHA1::read(std::istream &is, std::string &s, int max) { - char sbuf[max]; + char* sbuf = new char[max]; + is.read(sbuf, max); s.assign(sbuf, is.gcount()); + + delete[] sbuf; } -- cgit v1.2.3 From cf85aab62f961c905e4691fde59af774053d3d58 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 15 Oct 2014 01:05:08 +0200 Subject: A few indent fixes --- libs/sha1/sha1.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'libs') diff --git a/libs/sha1/sha1.cpp b/libs/sha1/sha1.cpp index 825274b9b..883d42837 100644 --- a/libs/sha1/sha1.cpp +++ b/libs/sha1/sha1.cpp @@ -261,7 +261,7 @@ void SHA1::read(std::istream &is, std::string &s, int max) is.read(sbuf, max); s.assign(sbuf, is.gcount()); - delete[] sbuf; + delete[] sbuf; } -- cgit v1.2.3 From 31267a1ae8d670c4b8749fc55b07c01d9285a488 Mon Sep 17 00:00:00 2001 From: William Speirs Date: Thu, 16 Oct 2014 12:06:54 -0400 Subject: Header changes so it will compile on VS --- libs/ezsat/ezminisat.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'libs') diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index b996d4a3d..dee82a8df 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -27,7 +27,10 @@ #include #include #include -#include + +#ifndef _WIN32 +# include +#endif #include "../minisat/Solver.h" #include "../minisat/SimpSolver.h" -- cgit v1.2.3 From 468ae923748a01b2763bafa3cf5fba883fe06479 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 17 Oct 2014 14:01:47 +0200 Subject: Various win32 / vs build fixes --- libs/ezsat/ezsat.h | 1 + 1 file changed, 1 insertion(+) (limited to 'libs') diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index cac6ff0f7..5c8c1ed0c 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -25,6 +25,7 @@ #include #include #include +#include class ezSAT { -- cgit v1.2.3 From b3a6f8f53019d1984d4e319db459b11da0663aa3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 17 Oct 2014 15:51:33 +0200 Subject: More win32 (mxe and vs) build fixes --- libs/ezsat/ezsat.cc | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) (limited to 'libs') diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 54a6e9c71..657bed9d2 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -22,12 +22,24 @@ #include #include #include +#include #include const int ezSAT::CONST_TRUE = 1; const int ezSAT::CONST_FALSE = 2; +static std::string my_int_to_string(int i) +{ +#ifdef __MINGW32__ + char buffer[64]; + snprintf(buffer, 64, "%d", i); + return buffer; +#else + return std::to_string(i); +#endif +} + ezSAT::ezSAT() { flag_keep_cnf = false; @@ -183,7 +195,7 @@ int ezSAT::expression(OpId op, const std::vector &args) if (expressionsCache.count(myExpr) > 0) { id = expressionsCache.at(myExpr); } else { - id = -(expressions.size() + 1); + id = -(int(expressions.size()) + 1); expressionsCache[myExpr] = id; expressions.push_back(myExpr); } @@ -490,13 +502,13 @@ int ezSAT::bound(int id) const std::string ezSAT::cnfLiteralInfo(int idx) const { - for (size_t i = 0; i < cnfLiteralVariables.size(); i++) { + for (int i = 0; i < int(cnfLiteralVariables.size()); i++) { if (cnfLiteralVariables[i] == idx) return to_string(i+1); if (cnfLiteralVariables[i] == -idx) return "NOT " + to_string(i+1); } - for (size_t i = 0; i < cnfExpressionVariables.size(); i++) { + for (int i = 0; i < int(cnfExpressionVariables.size()); i++) { if (cnfExpressionVariables[i] == idx) return to_string(-i-1); if (cnfExpressionVariables[i] == -idx) @@ -670,9 +682,7 @@ std::vector ezSAT::vec_var(std::string name, int numBits) { std::vector vec; for (int i = 0; i < numBits; i++) { - char buf[64]; - snprintf(buf, 64, " [%d]", i); - vec.push_back(VAR(name + buf)); + vec.push_back(VAR(name + my_int_to_string(i))); } return vec; } @@ -1245,11 +1255,8 @@ static std::string expression2str(const std::pair> #undef X } text += ":"; - for (auto it : data.second) { - char buf[64]; - snprintf(buf, 64, " %d", it); - text += buf; - } + for (auto it : data.second) + text += " " + my_int_to_string(it); return text; } -- cgit v1.2.3 From 84ffe04075bbddfd1b288295c07d036416923c3a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 18 Oct 2014 15:20:38 +0200 Subject: Fixed various VS warnings --- libs/ezsat/ezsat.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'libs') diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 657bed9d2..b713c4c91 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -1118,7 +1118,7 @@ int64_t ezSAT::vec_model_get_signed(const std::vector &modelExpressions, co for (int i = 0; i < 64; i++) { int j = i < int(vec1.size()) ? i : vec1.size()-1; if (modelMap.at(vec1[j])) - value |= 1 << i; + value |= int64_t(1) << i; } return value; } @@ -1132,7 +1132,7 @@ uint64_t ezSAT::vec_model_get_unsigned(const std::vector &modelExpressions, modelMap[modelExpressions[i]] = modelValues[i]; for (int i = 0; i < int(vec1.size()); i++) if (modelMap.at(vec1[i])) - value |= 1 << i; + value |= uint64_t(1) << i; return value; } -- cgit v1.2.3 From 76cc2bf7b43140698618e9dbb87a219c3bd7d32f Mon Sep 17 00:00:00 2001 From: SlowRiot Date: Thu, 20 Nov 2014 01:58:57 +0000 Subject: fixing incorrect buffer size allocation, and unsafe integer size type --- libs/sha1/sha1.cpp | 86 ++++++++++++++++++++++++++++-------------------------- libs/sha1/sha1.h | 38 ++++++++++++------------ 2 files changed, 64 insertions(+), 60 deletions(-) (limited to 'libs') diff --git a/libs/sha1/sha1.cpp b/libs/sha1/sha1.cpp index 883d42837..3d46da7be 100644 --- a/libs/sha1/sha1.cpp +++ b/libs/sha1/sha1.cpp @@ -1,55 +1,57 @@ /* sha1.cpp - source code of - + ============ SHA-1 in C++ ============ - + 100% Public Domain. - + Original C Code -- Steve Reid Small changes to fit into bglibs -- Bruce Guenter Translation to simpler C++ Code -- Volker Grabsch + Fixing bugs and improving style + -- Eugene Hopkinson */ - + #include "sha1.h" #include #include #include - + /* Help macros */ #define SHA1_ROL(value, bits) (((value) << (bits)) | (((value) & 0xffffffff) >> (32 - (bits)))) #define SHA1_BLK(i) (block[i&15] = SHA1_ROL(block[(i+13)&15] ^ block[(i+8)&15] ^ block[(i+2)&15] ^ block[i&15],1)) - + /* (R0+R1), R2, R3, R4 are the different operations used in SHA1 */ #define SHA1_R0(v,w,x,y,z,i) z += ((w&(x^y))^y) + block[i] + 0x5a827999 + SHA1_ROL(v,5); w=SHA1_ROL(w,30); #define SHA1_R1(v,w,x,y,z,i) z += ((w&(x^y))^y) + SHA1_BLK(i) + 0x5a827999 + SHA1_ROL(v,5); w=SHA1_ROL(w,30); #define SHA1_R2(v,w,x,y,z,i) z += (w^x^y) + SHA1_BLK(i) + 0x6ed9eba1 + SHA1_ROL(v,5); w=SHA1_ROL(w,30); #define SHA1_R3(v,w,x,y,z,i) z += (((w|x)&y)|(w&x)) + SHA1_BLK(i) + 0x8f1bbcdc + SHA1_ROL(v,5); w=SHA1_ROL(w,30); #define SHA1_R4(v,w,x,y,z,i) z += (w^x^y) + SHA1_BLK(i) + 0xca62c1d6 + SHA1_ROL(v,5); w=SHA1_ROL(w,30); - + SHA1::SHA1() { reset(); } - - + + void SHA1::update(const std::string &s) { std::istringstream is(s); update(is); } - - + + void SHA1::update(std::istream &is) { std::string rest_of_buffer; read(is, rest_of_buffer, BLOCK_BYTES - buffer.size()); buffer += rest_of_buffer; - + while (is) { uint32 block[BLOCK_INTS]; @@ -58,17 +60,17 @@ void SHA1::update(std::istream &is) read(is, buffer, BLOCK_BYTES); } } - - + + /* * Add padding and return the message digest. */ - + std::string SHA1::final() { /* Total number of hashed bits */ uint64 total_bits = (transforms*BLOCK_BYTES + buffer.size()) * 8; - + /* Padding */ buffer += 0x80; unsigned int orig_size = buffer.size(); @@ -76,10 +78,10 @@ std::string SHA1::final() { buffer += (char)0x00; } - + uint32 block[BLOCK_INTS]; buffer_to_block(buffer, block); - + if (orig_size > BLOCK_BYTES - 8) { transform(block); @@ -88,12 +90,12 @@ std::string SHA1::final() block[i] = 0; } } - + /* Append total_bits, split this uint64 into two uint32 */ block[BLOCK_INTS - 1] = total_bits; block[BLOCK_INTS - 2] = (total_bits >> 32); transform(block); - + /* Hex std::string */ std::ostringstream result; for (unsigned int i = 0; i < DIGEST_INTS; i++) @@ -101,14 +103,14 @@ std::string SHA1::final() result << std::hex << std::setfill('0') << std::setw(8); result << (digest[i] & 0xffffffff); } - + /* Reset for next run */ reset(); - + return result.str(); } - - + + std::string SHA1::from_file(const std::string &filename) { std::ifstream stream(filename.c_str(), std::ios::binary); @@ -116,8 +118,8 @@ std::string SHA1::from_file(const std::string &filename) checksum.update(stream); return checksum.final(); } - - + + void SHA1::reset() { /* SHA1 initialization constants */ @@ -126,17 +128,17 @@ void SHA1::reset() digest[2] = 0x98badcfe; digest[3] = 0x10325476; digest[4] = 0xc3d2e1f0; - + /* Reset counters */ transforms = 0; buffer = ""; } - - + + /* * Hash a single 512-bit block. This is the core of the algorithm. */ - + void SHA1::transform(uint32 block[BLOCK_BYTES]) { /* Copy digest[] to working vars */ @@ -145,8 +147,8 @@ void SHA1::transform(uint32 block[BLOCK_BYTES]) uint32 c = digest[2]; uint32 d = digest[3]; uint32 e = digest[4]; - - + + /* 4 rounds of 20 operations each. Loop unrolled. */ SHA1_R0(a,b,c,d,e, 0); SHA1_R0(e,a,b,c,d, 1); @@ -228,20 +230,20 @@ void SHA1::transform(uint32 block[BLOCK_BYTES]) SHA1_R4(d,e,a,b,c,77); SHA1_R4(c,d,e,a,b,78); SHA1_R4(b,c,d,e,a,79); - + /* Add the working vars back into digest[] */ digest[0] += a; digest[1] += b; digest[2] += c; digest[3] += d; digest[4] += e; - + /* Count the number of transformations */ transforms++; } - - -void SHA1::buffer_to_block(const std::string &buffer, uint32 block[BLOCK_BYTES]) + + +void SHA1::buffer_to_block(const std::string &buffer, uint32 block[BLOCK_INTS]) { /* Convert the std::string (byte buffer) to a uint32 array (MSB) */ for (unsigned int i = 0; i < BLOCK_INTS; i++) @@ -252,9 +254,9 @@ void SHA1::buffer_to_block(const std::string &buffer, uint32 block[BLOCK_BYTES]) | (buffer[4*i+0] & 0xff)<<24; } } - - -void SHA1::read(std::istream &is, std::string &s, int max) + + +void SHA1::read(std::istream &is, std::string &s, size_t max) { char* sbuf = new char[max]; @@ -263,8 +265,8 @@ void SHA1::read(std::istream &is, std::string &s, int max) delete[] sbuf; } - - + + std::string sha1(const std::string &string) { SHA1 checksum; diff --git a/libs/sha1/sha1.h b/libs/sha1/sha1.h index 15edee12e..898575d6c 100644 --- a/libs/sha1/sha1.h +++ b/libs/sha1/sha1.h @@ -1,27 +1,29 @@ /* sha1.h - header of - + ============ SHA-1 in C++ ============ - + 100% Public Domain. - + Original C Code -- Steve Reid Small changes to fit into bglibs -- Bruce Guenter Translation to simpler C++ Code -- Volker Grabsch + Fixing bugs and improving style + -- Eugene Hopkinson */ - + #ifndef SHA1_HPP #define SHA1_HPP - - + + #include #include - + class SHA1 { public: @@ -30,28 +32,28 @@ public: void update(std::istream &is); std::string final(); static std::string from_file(const std::string &filename); - + private: typedef unsigned long int uint32; /* just needs to be at least 32bit */ typedef unsigned long long uint64; /* just needs to be at least 64bit */ - + static const unsigned int DIGEST_INTS = 5; /* number of 32bit integers per SHA1 digest */ static const unsigned int BLOCK_INTS = 16; /* number of 32bit integers per SHA1 block */ static const unsigned int BLOCK_BYTES = BLOCK_INTS * 4; - + uint32 digest[DIGEST_INTS]; std::string buffer; uint64 transforms; - + void reset(); void transform(uint32 block[BLOCK_BYTES]); - - static void buffer_to_block(const std::string &buffer, uint32 block[BLOCK_BYTES]); - static void read(std::istream &is, std::string &s, int max); + + static void read(std::istream &is, std::string &s, size_t max); + static void buffer_to_block(const std::string &buffer, uint32 block[BLOCK_INTS]); }; - + std::string sha1(const std::string &string); - - - + + + #endif /* SHA1_HPP */ -- cgit v1.2.3 From 4aae465867cd1221e47eaaa7550f1eb9aa2f5863 Mon Sep 17 00:00:00 2001 From: SlowRiot Date: Thu, 20 Nov 2014 02:03:08 +0000 Subject: switching from unreliable typedefs to precisely sized uint32_t and uint64_t --- libs/sha1/sha1.cpp | 24 ++++++++++++------------ libs/sha1/sha1.h | 11 ++++------- 2 files changed, 16 insertions(+), 19 deletions(-) (limited to 'libs') diff --git a/libs/sha1/sha1.cpp b/libs/sha1/sha1.cpp index 3d46da7be..51bbd85c8 100644 --- a/libs/sha1/sha1.cpp +++ b/libs/sha1/sha1.cpp @@ -54,7 +54,7 @@ void SHA1::update(std::istream &is) while (is) { - uint32 block[BLOCK_INTS]; + uint32_t block[BLOCK_INTS]; buffer_to_block(buffer, block); transform(block); read(is, buffer, BLOCK_BYTES); @@ -69,7 +69,7 @@ void SHA1::update(std::istream &is) std::string SHA1::final() { /* Total number of hashed bits */ - uint64 total_bits = (transforms*BLOCK_BYTES + buffer.size()) * 8; + uint64_t total_bits = (transforms*BLOCK_BYTES + buffer.size()) * 8; /* Padding */ buffer += 0x80; @@ -79,7 +79,7 @@ std::string SHA1::final() buffer += (char)0x00; } - uint32 block[BLOCK_INTS]; + uint32_t block[BLOCK_INTS]; buffer_to_block(buffer, block); if (orig_size > BLOCK_BYTES - 8) @@ -91,7 +91,7 @@ std::string SHA1::final() } } - /* Append total_bits, split this uint64 into two uint32 */ + /* Append total_bits, split this uint64_t into two uint32_t */ block[BLOCK_INTS - 1] = total_bits; block[BLOCK_INTS - 2] = (total_bits >> 32); transform(block); @@ -139,14 +139,14 @@ void SHA1::reset() * Hash a single 512-bit block. This is the core of the algorithm. */ -void SHA1::transform(uint32 block[BLOCK_BYTES]) +void SHA1::transform(uint32_t block[BLOCK_BYTES]) { /* Copy digest[] to working vars */ - uint32 a = digest[0]; - uint32 b = digest[1]; - uint32 c = digest[2]; - uint32 d = digest[3]; - uint32 e = digest[4]; + uint32_t a = digest[0]; + uint32_t b = digest[1]; + uint32_t c = digest[2]; + uint32_t d = digest[3]; + uint32_t e = digest[4]; /* 4 rounds of 20 operations each. Loop unrolled. */ @@ -243,9 +243,9 @@ void SHA1::transform(uint32 block[BLOCK_BYTES]) } -void SHA1::buffer_to_block(const std::string &buffer, uint32 block[BLOCK_INTS]) +void SHA1::buffer_to_block(const std::string &buffer, uint32_t block[BLOCK_INTS]) { - /* Convert the std::string (byte buffer) to a uint32 array (MSB) */ + /* Convert the std::string (byte buffer) to a uint32_t array (MSB) */ for (unsigned int i = 0; i < BLOCK_INTS; i++) { block[i] = (buffer[4*i+3] & 0xff) diff --git a/libs/sha1/sha1.h b/libs/sha1/sha1.h index 898575d6c..f6a03e735 100644 --- a/libs/sha1/sha1.h +++ b/libs/sha1/sha1.h @@ -34,22 +34,19 @@ public: static std::string from_file(const std::string &filename); private: - typedef unsigned long int uint32; /* just needs to be at least 32bit */ - typedef unsigned long long uint64; /* just needs to be at least 64bit */ - static const unsigned int DIGEST_INTS = 5; /* number of 32bit integers per SHA1 digest */ static const unsigned int BLOCK_INTS = 16; /* number of 32bit integers per SHA1 block */ static const unsigned int BLOCK_BYTES = BLOCK_INTS * 4; - uint32 digest[DIGEST_INTS]; + uint32_t digest[DIGEST_INTS]; std::string buffer; - uint64 transforms; + uint64_t transforms; void reset(); - void transform(uint32 block[BLOCK_BYTES]); + void transform(uint32_t block[BLOCK_BYTES]); static void read(std::istream &is, std::string &s, size_t max); - static void buffer_to_block(const std::string &buffer, uint32 block[BLOCK_INTS]); + static void buffer_to_block(const std::string &buffer, uint32_t block[BLOCK_INTS]); }; std::string sha1(const std::string &string); -- cgit v1.2.3 From df52eedb3025c5250931c29c2417fbd0129500e1 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 11 Dec 2014 15:27:38 +0100 Subject: Compile fix for visual studio --- libs/sha1/sha1.h | 1 + 1 file changed, 1 insertion(+) (limited to 'libs') diff --git a/libs/sha1/sha1.h b/libs/sha1/sha1.h index f6a03e735..9f526376e 100644 --- a/libs/sha1/sha1.h +++ b/libs/sha1/sha1.h @@ -23,6 +23,7 @@ #include #include +#include class SHA1 { -- cgit v1.2.3 From 29a555ec7eaa0e561f76c65258a50c54b6468546 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 29 Dec 2014 17:10:37 +0100 Subject: Added statehash to ezSAT --- libs/ezsat/ezsat.cc | 49 +++++++++++++++++++++++++++++++++++++++++++------ libs/ezsat/ezsat.h | 3 +++ 2 files changed, 46 insertions(+), 6 deletions(-) (limited to 'libs') diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index b713c4c91..1224fd3a9 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -42,6 +42,8 @@ static std::string my_int_to_string(int i) ezSAT::ezSAT() { + statehash = 5381; + flag_keep_cnf = false; flag_non_incremental = false; @@ -65,6 +67,11 @@ ezSAT::~ezSAT() { } +void ezSAT::addhash(unsigned int h) +{ + statehash = ((statehash << 5) + statehash) ^ h; +} + int ezSAT::value(bool val) { return val ? CONST_TRUE : CONST_FALSE; @@ -113,8 +120,14 @@ int ezSAT::expression(OpId op, const std::vector &args) myArgs.reserve(args.size()); bool xorRemovedOddTrues = false; + addhash(__LINE__); + addhash(op); + for (auto arg : args) { + addhash(__LINE__); + addhash(arg); + if (arg == 0) continue; if (op == OpAnd && arg == CONST_TRUE) @@ -200,7 +213,13 @@ int ezSAT::expression(OpId op, const std::vector &args) expressions.push_back(myExpr); } - return xorRemovedOddTrues ? NOT(id) : id; + if (xorRemovedOddTrues) + id = NOT(id); + + addhash(__LINE__); + addhash(id); + + return id; } void ezSAT::lookup_literal(int id, std::string &name) const @@ -387,6 +406,9 @@ bool ezSAT::eliminated(int) void ezSAT::assume(int id) { + addhash(__LINE__); + addhash(id); + if (id < 0) { assert(0 < -id && -id <= int(expressions.size())); @@ -429,6 +451,10 @@ void ezSAT::assume(int id) void ezSAT::add_clause(const std::vector &args) { + addhash(__LINE__); + for (auto arg : args) + addhash(arg); + cnfClauses.push_back(args); cnfClausesCount++; } @@ -519,6 +545,10 @@ std::string ezSAT::cnfLiteralInfo(int idx) const int ezSAT::bind(int id, bool auto_freeze) { + addhash(__LINE__); + addhash(id); + addhash(auto_freeze); + if (id >= 0) { assert(0 < id && id <= int(literals.size())); cnfLiteralVariables.resize(literals.size()); @@ -561,10 +591,13 @@ int ezSAT::bind(int id, bool auto_freeze) while (args.size() > 1) { std::vector newArgs; for (int i = 0; i < int(args.size()); i += 2) - if (i+1 == int(args.size())) + if (i+1 == int(args.size())) { newArgs.push_back(args[i]); - else - newArgs.push_back(OR(AND(args[i], NOT(args[i+1])), AND(NOT(args[i]), args[i+1]))); + } else { + int sub1 = AND(args[i], NOT(args[i+1])); + int sub2 = AND(NOT(args[i]), args[i+1]); + newArgs.push_back(OR(sub1, sub2)); + } args.swap(newArgs); } idx = bind(args.at(0), false); @@ -575,12 +608,16 @@ int ezSAT::bind(int id, bool auto_freeze) std::vector invArgs; for (auto arg : args) invArgs.push_back(NOT(arg)); - idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs)), false); + int sub1 = expression(OpAnd, args); + int sub2 = expression(OpAnd, invArgs); + idx = bind(OR(sub1, sub2), false); goto assign_idx; } if (op == OpITE) { - idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2])), false); + int sub1 = AND(args[0], args[1]); + int sub2 = AND(NOT(args[0]), args[2]); + idx = bind(OR(sub1, sub2), false); goto assign_idx; } diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 5c8c1ed0c..a20713bc1 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -83,6 +83,9 @@ public: ezSAT(); virtual ~ezSAT(); + unsigned int statehash; + void addhash(unsigned int); + void keep_cnf() { flag_keep_cnf = true; } void non_incremental() { flag_non_incremental = true; } -- cgit v1.2.3 From 2a9ad48eb63a5f019c528fe46ceca0065364a44d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 24 Jan 2015 12:16:46 +0100 Subject: Added ENABLE_NDEBUG makefile options --- libs/ezsat/ezsat.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'libs') diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 1224fd3a9..8d232f335 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -1096,7 +1096,7 @@ std::vector ezSAT::vec_shift_right(const std::vector &vec1, const std: std::vector ezSAT::vec_shift_left(const std::vector &vec1, const std::vector &vec2, bool vec2_signed, int extend_left, int extend_right) { // vec2_signed is not implemented in vec_shift_left() yet - assert(vec2_signed == false); + if (vec2_signed) assert(vec2_signed == false); int vec2_bits = std::min(my_clog2(vec1.size()), int(vec2.size())); -- cgit v1.2.3 From 893fe87a33dc6646cabc7538d4dbe411041afb94 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 1 Feb 2015 22:41:03 +0100 Subject: Improved performance in equiv_simple --- libs/ezsat/ezsat.h | 1 + 1 file changed, 1 insertion(+) (limited to 'libs') diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index a20713bc1..0faaa6b8d 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -163,6 +163,7 @@ public: virtual void freeze(int id); virtual bool eliminated(int idx); void assume(int id); + void assume(int id, int context_id) { assume(OR(id, NOT(context_id))); } int bind(int id, bool auto_freeze = true); int bound(int id) const; -- cgit v1.2.3