From 04802e93e857a227b48479abd7970cb4152f496b Mon Sep 17 00:00:00 2001 From: Tim 'mithro' Ansell Date: Fri, 24 Nov 2017 15:26:56 +1100 Subject: [PATCH 1/6] subcircuit: Class with virtual methods should have virtual destructor. Fixes a compile warning. * https://stackoverflow.com/questions/1123044/when-should-your-destructor-be-virtual --- libs/subcircuit/subcircuit.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/subcircuit/subcircuit.h b/libs/subcircuit/subcircuit.h index 5291c6421..8368efab1 100644 --- a/libs/subcircuit/subcircuit.h +++ b/libs/subcircuit/subcircuit.h @@ -131,7 +131,7 @@ namespace SubCircuit public: Solver(); - ~Solver(); + virtual ~Solver(); void setVerbose(); void addGraph(std::string graphId, const Graph &graph); From 8d48b47450f5e62a7db1766da57d5736872077a9 Mon Sep 17 00:00:00 2001 From: Tim 'mithro' Ansell Date: Fri, 24 Nov 2017 15:30:55 +1100 Subject: [PATCH 2/6] minisat: Remove template with gzFile specialization. All the other gzFile functions have been removed but this template was still left around. --- libs/minisat/00_PATCH_remove_zlib.patch | 17 +++++++++++++++++ libs/minisat/Dimacs.h | 8 ++++---- 2 files changed, 21 insertions(+), 4 deletions(-) diff --git a/libs/minisat/00_PATCH_remove_zlib.patch b/libs/minisat/00_PATCH_remove_zlib.patch index 61a36f7e5..068356b73 100644 --- a/libs/minisat/00_PATCH_remove_zlib.patch +++ b/libs/minisat/00_PATCH_remove_zlib.patch @@ -36,3 +36,20 @@ int operator * () const { return (pos >= size) ? EOF : buf[pos]; } void operator ++ () { pos++; assureLookahead(); } +--- Dimacs.h ++++ Dimacs.h +@@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) { + + // Inserts problem into solver. + // +-template +-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { +- StreamBuffer in(input_stream); +- parse_DIMACS_main(in, S, strictp); } ++//template ++//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { ++// StreamBuffer in(input_stream); ++// parse_DIMACS_main(in, S, strictp); } + + //================================================================================================= + } diff --git a/libs/minisat/Dimacs.h b/libs/minisat/Dimacs.h index ccfa1c013..61b9d3ca0 100644 --- a/libs/minisat/Dimacs.h +++ b/libs/minisat/Dimacs.h @@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) { // Inserts problem into solver. // -template -static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { - StreamBuffer in(input_stream); - parse_DIMACS_main(in, S, strictp); } +//template +//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { +// StreamBuffer in(input_stream); +// parse_DIMACS_main(in, S, strictp); } //================================================================================================= } From 34c9fbab5367133fe6e0365068f78762ded70623 Mon Sep 17 00:00:00 2001 From: Tim 'mithro' Ansell Date: Fri, 24 Nov 2017 15:34:46 +1100 Subject: [PATCH 3/6] minisat: Only define __STDC_XXX_MACROS if not already defined. Replace; #define __STDC_LIMIT_MACROS #define __STDC_FORMAT_MACROS With #ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS #endif #ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS #endif This fixes a compile warning if you are defining these macros in your CXXFLAGS (as some distros do). --- libs/ezsat/ezminisat.cc | 6 +++++- libs/minisat/00_UPDATE.sh | 4 ++-- libs/minisat/Options.cc | 4 ++++ libs/minisat/SimpSolver.cc | 4 ++++ libs/minisat/Solver.cc | 4 ++++ libs/minisat/System.cc | 4 ++++ 6 files changed, 23 insertions(+), 3 deletions(-) diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index e0ee6292d..4be5fd493 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -18,8 +18,12 @@ */ // needed for MiniSAT headers (see Minisat Makefile) -#define __STDC_LIMIT_MACROS +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS +#define __STDC_LIMIT_MACROS +#endif #include "ezminisat.h" diff --git a/libs/minisat/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh index 2ffc11553..ea26215ab 100644 --- a/libs/minisat/00_UPDATE.sh +++ b/libs/minisat/00_UPDATE.sh @@ -9,8 +9,8 @@ rm -rf minisat_upstream sed -i -e 's,^#include *"minisat/[^/]\+/\?,#include ",' *.cc *.h sed -i -e 's/Minisat::memUsedPeak()/Minisat::memUsedPeak(bool)/' System.cc sed -i -e 's/PRI[iu]64/ & /' Options.h Solver.cc -sed -i -e '1 i #define __STDC_LIMIT_MACROS' *.cc -sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc +sed -i -e '1 i #ifndef __STDC_LIMIT_MACROS\n#define __STDC_LIMIT_MACROS\n#endif' *.cc +sed -i -e '1 i #ifndef __STDC_FORMAT_MACROS\n#define __STDC_FORMAT_MACROS\n#endif' *.cc patch -p0 < 00_PATCH_mkLit_default_arg.patch patch -p0 < 00_PATCH_remove_zlib.patch diff --git a/libs/minisat/Options.cc b/libs/minisat/Options.cc index 1aff3fab2..5c45dd6ac 100644 --- a/libs/minisat/Options.cc +++ b/libs/minisat/Options.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /**************************************************************************************[Options.cc] Copyright (c) 2008-2010, Niklas Sorensson diff --git a/libs/minisat/SimpSolver.cc b/libs/minisat/SimpSolver.cc index fd5774e0e..7348a905d 100644 --- a/libs/minisat/SimpSolver.cc +++ b/libs/minisat/SimpSolver.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /***********************************************************************************[SimpSolver.cc] Copyright (c) 2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson diff --git a/libs/minisat/Solver.cc b/libs/minisat/Solver.cc index ab476853a..f6d4fb5ae 100644 --- a/libs/minisat/Solver.cc +++ b/libs/minisat/Solver.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /***************************************************************************************[Solver.cc] Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc index ceef4292b..1921a1d71 100644 --- a/libs/minisat/System.cc +++ b/libs/minisat/System.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /***************************************************************************************[System.cc] Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson From 1b231b442c576bacc5d25a35a5846f896394e2f1 Mon Sep 17 00:00:00 2001 From: Tim 'mithro' Ansell Date: Fri, 24 Nov 2017 15:37:35 +1100 Subject: [PATCH 4/6] minisat: Make update script executable. --- libs/minisat/00_UPDATE.sh | 0 1 file changed, 0 insertions(+), 0 deletions(-) mode change 100644 => 100755 libs/minisat/00_UPDATE.sh diff --git a/libs/minisat/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh old mode 100644 new mode 100755 From b24b600287dd64cd170eff53837b34cd17a0cfa5 Mon Sep 17 00:00:00 2001 From: Tim 'mithro' Ansell Date: Sat, 25 Nov 2017 19:44:41 -0800 Subject: [PATCH 5/6] travis: Print branches before fetching, try both locations. --- .travis/setup.sh | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.travis/setup.sh b/.travis/setup.sh index 23bdf563f..81ff37742 100755 --- a/.travis/setup.sh +++ b/.travis/setup.sh @@ -29,8 +29,16 @@ fi if [ z"$TRAVIS_BRANCH" != z ]; then TRAVIS_COMMIT_ACTUAL=$(git log --pretty=format:'%H' -n 1) echo "- Fixing detached head (current $TRAVIS_COMMIT_ACTUAL -> $TRAVIS_COMMIT)" - git fetch origin $TRAVIS_COMMIT + git remote -v git branch -v + if [ x"$(git show-ref -s HEAD)" = x"$TRAVIS_COMMIT" ]; then + echo "Checked out at $TRAVIS_COMMIT" + else + if [ z"$TRAVIS_PULL_REQUEST_SLUG" != z ]; then + git fetch source $TRAVIS_COMMIT || echo "Unable to fetch $TRAVIS_COMMIT from source" + fi + git fetch origin $TRAVIS_COMMIT || echo "Unable to fetch $TRAVIS_COMMIT from origin" + fi git branch -D $TRAVIS_BRANCH || true git checkout $TRAVIS_COMMIT -b $TRAVIS_BRANCH git branch -v From da91b31bb242bb947533702ac7484773fa3f3d57 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 27 Nov 2017 17:42:32 +0100 Subject: [PATCH 6/6] Fixed "yosys-smtbmc -g" handling of no solution --- backends/smt2/smtbmc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index d9b79e26e..560e39d86 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1279,7 +1279,7 @@ else: # not tempind, covermode step += step_size - if gentrace: + if gentrace and retstatus: print_anyconsts(0) write_trace(0, num_steps, '%')