Merge branch 'master' into btor-ng

.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

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"
 

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<class Solver>
+-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+-    StreamBuffer in(input_stream);
+-    parse_DIMACS_main(in, S, strictp); }
++//template<class Solver>
++//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
++//    StreamBuffer in(input_stream);
++//    parse_DIMACS_main(in, S, strictp); }
+ 
+ //=================================================================================================
+ }

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

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<class Solver>
-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
-    StreamBuffer in(input_stream);
-    parse_DIMACS_main(in, S, strictp); }
+//template<class Solver>
+//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+//    StreamBuffer in(input_stream);
+//    parse_DIMACS_main(in, S, strictp); }
 
 //=================================================================================================
 }

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
 

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

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

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

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);