32 bit port, fixed MS VC++ issue in radix, fixed -j not default anymore

Author: Armin Biere

.travis.yml

@@ -9,3 +9,4 @@ os:
 - osx
 branches:
 - master
+- development

VERSION

@@ -1 +1 @@
-1.0.2
+1.0.3

configure

@@ -21,10 +21,10 @@ check=no
 coverage=no
 profile=no
 unlocked=yes
-stdint=unknown
 pedantic=no
 options=""
 quiet=no
+m32=no
 
 #--------------------------------------------------------------------------#
 
@@ -88,9 +88,12 @@ where '<option>' is one of the following
 --profile          compile with '-pg' to profile with 'gprof'
 
 -f...              pass '-f<option>[=<val>]' options to the makefile
+-m32               pass '-m32' to the compiler (compile for 32 bit)
 -ggdb3             pass '-ggdb3' to makefile (like '-s')
 -O|-O[123]         pass '-O' or '-O[123]' to the makefile
 
+-j|-j...           pass this option to the makefile (for parallel build)
+
 The environment variable CXX can be used to set a different C++
 compiler than the default 'g++'.  Similarly you can add additional
 compilation options by setting CXXFLAGS.  For example
@@ -111,8 +114,6 @@ The following configuration options might be usefull during porting the
 code to a new platform and are usually not necessary to change.
 
 --no-unlocked      force compilation without unlocked IO
---no-[c]stdint     avoid trying to '#include <cstdint>'
---[c]stdint        force '#include <cstdint>'
 EOF
 exit 0
 }
@@ -138,9 +139,10 @@ do
     --profile) profile=yes;;
 
     --no-unlocked) unlocked=no;;
-    --no-stdint) stdint=no;;
-    --stdint) stdint=yes;;
 
+    -j*) MAKEFLAGS="$1";;
+
+    -m32) options="$options $1";m32=yes;;
     -f*|-ggdb3|-O|-O1|-O2|-O3) options="$options $1";;
     -s|--symbols) options="$options -ggdb3";;
 
@@ -227,10 +229,12 @@ msg "root directory '$root'"
 
 [ x"$CXX" = x ] && CXX=g++
 [ x"$CXXFLAGS" = x ] || CXXFLAGS="$CXXFLAGS "
+
 case x"$CXX" in
   xg++*|xclang++*) CXXFLAGS="${CXXFLAGS}-Wall -Wextra";;
   *) CXXFLAGS="${CXXFLAGS}-W";;
 esac
+
 if [ $debug = yes ]
 then
   CXXFLAGS="$CXXFLAGS -g"
@@ -241,12 +245,23 @@ else
   esac
 fi
 
+if [ $m32 = yes ]
+then
+  case x"$CXX" in
+    xg++*)
+      options="$options -mpc64"
+      msg "forcing portable 64-bit FPU mode ('-mpc64') for '$CXX'"
+      ;;
+  esac
+fi
+
 [ $check = no ] && CXXFLAGS="$CXXFLAGS -DNDEBUG"
 [ $logging = yes ] && CXXFLAGS="$CXXFLAGS -DLOGGING"
 [ $quiet = yes ] && CXXFLAGS="$CXXFLAGS -DQUIET"
 [ $profile = yes ] && CXXFLAGS="$CXXFLAGS -pg"
 [ $coverage = yes ] && CXXFLAGS="$CXXFLAGS -ftest-coverage -fprofile-arcs"
 [ $pedantic = yes ] && CXXFLAGS="$CXXFLAGS --pedantic -Werror"
+
 CXXFLAGS="$CXXFLAGS$options"
 
 #--------------------------------------------------------------------------#
@@ -372,78 +387,6 @@ fi
 
 #--------------------------------------------------------------------------#
 
-# For 'Random.hpp' we really needed a clean unsigned 64 bit word type such
-# as 'uint64_t'. Since this requires 'cstdint' to be included, we feature
-# whether we can do that or otherwise try to find alternatives.
-
-if [ $stdint = unknown ]
-then
-  feature=./configure-have-stdint
-cat <<EOF > $feature.cpp
-#include <cstdint>
-EOF
-  if $CXX $CXXFLAGS -c $feature.cpp 2>>configure.log
-  then
-    msg "using '#include <cstdint>' for 'uint32_t' and 'uint64_t'"
-    stdint=yes
-  else
-    msg "can not use '#include <cstdint>'"
-    stdint=no
-    uint64_t=""
-    uint32_t=""
-    for type in "unsigned" "size_t" "unsigned long" "unsigned long long"
-    do
-      feature=./"configure-`echo $type|sed -e 's, ,-,g'`"
-cat <<EOF > $feature.cpp
-#include <cstdlib>
-#include <cstdio>
-int main () {
-  $type x = 0, y = x >> 1;
-  size_t bytes = sizeof x;
-  if (y & (1 << (bytes*8 - 1))) abort (); // signed type!
-  printf ("%ld\n", (long) bytes);
-  return 0;
-}
-EOF
-      if $CXX $CXXFLAGS -o $feature.exe $feature.cpp 2>&1 2>>configure.log
-      then
-        bytes="`$feature.exe 2>>configure.log`"
-	msg "sizeof ($type) = $bytes"
-	case x"$bytes" in
-	  x4) [ "$uint32_t" ] || uint32_t="$type";;
-	  x8) [ "$uint64_t" ] || uint64_t="$type";;
-	esac
-      fi
-      [ "$uint32_t" -a "$uint64_t" ] && break
-    done
-    if [ "$uint32_t" ]
-    then
-      msg "using '$uint32_t' for 'uint32_t'"
-      [ "$uint32_t" = "unsigned" ] || \
-      CXXFLAGS="$CXXFLAGS -Duint32_t=\"$type\""
-    else
-      die "no 4 bytes unsigned type found for 'uint32_t'"
-    fi
-    if [ "$uint64_t" ]
-    then
-      msg "using '$uint64_t' for 'uint64_t'"
-      [ "$uint64_t" = "size_t" ] || \
-      CXXFLAGS="$CXXFLAGS -Duint64_t=\"$type\""
-    else
-      die "no 8 bytes unsigned type found for 'uint64_t'"
-    fi
-  fi
-elif [ $stdint = yes ]
-then
-  msg "forced to use '#include <cstdint>' for 'uint32_t' and 'uint64_t'"
-else
-  msg "will not use '#include <cstdint>' for 'uint32_t' and 'uint64_t'"
-fi
-
-[ $stdint = no ] && CXXFLAGS="$CXXFLAGS -DNSTDINT"
-
-#--------------------------------------------------------------------------#
-
 # Instantiate '../makefile.in' template to produce 'makefile' in 'build'.
 
 msg "compiling with ${HILITE}'$CXX $CXXFLAGS'${NORMAL}"
@@ -454,6 +397,7 @@ sed \
 # This 'makefile' is generated from '../makefile.in'." \
 -e "s,@CXX@,$CXX," \
 -e "s,@CXXFLAGS@,$CXXFLAGS," \
+-e "s,@MAKEFLAGS@,$MAKEFLAGS," \
 ../makefile.in > makefile
 
 msg "generated '$build/makefile' from '../makefile.in'"

makefile.in

@@ -10,11 +10,14 @@
 CXX=@CXX@
 CXXFLAGS=@CXXFLAGS@
 
+# Mainly used for parallel build ('-j' option to 'configure')
+
+MAKEFLAGS=@MAKEFLAGS@
+
 ############################################################################
 #    It is usually not necessary to change anything below this line!       #
 ############################################################################
 
-MAKEFLAGS=-j12
 APP=cadical.cpp mobical.cpp
 ALL=$(sort $(wildcard ../src/*.[ch]pp))
 SRC=$(filter %.cpp,$(subst ../src/,,$(ALL)))

scripts/README.md

@@ -3,7 +3,7 @@
 Scripts needed for the build process
 
     ./make-build-header.sh   # generates 'build.hpp'
-    ./get-git-id.sh          # get GIT id (needed by 'make-build-headers.sh')
+    ./get-git-id.sh          # get GIT id (needed by 'make-build-header.sh')
     ./update-version.sh      # synchronizes VERSION in '../src/version.cpp'
 
 and a script which builds and tests all configurations

scripts/build-and-test-all-configurations.sh

@@ -94,12 +94,10 @@ run -g -l -p
 
 # finally check that these also work to some extend
 
-run --no-unlocked -p
-run --no-stdint -p
-run --stdint -p
+run -m32 -q
+run -m32 -a -p
 
+run --no-unlocked -q
 run --no-unlocked -a -p
-run --no-stdint -a -p
-run --stdint -a -p
 
 echo "successfully compiled and tested ${GOOD}${ok}${NORMAL} configurations"

src/analyze.cpp

@@ -39,8 +39,9 @@ void Internal::bump_queue (int lit) {
   if (!links[idx].next) return;
   queue.dequeue (links, idx);
   queue.enqueue (links, idx);
+  assert (stats.bumped != INT64_MAX);
   btab[idx] = ++stats.bumped;
-  LOG ("moved to front variable %d and bumped to %ld", idx, btab[idx]);
+  LOG ("moved to front variable %d and bumped to %" PRId64 "", idx, btab[idx]);
   if (!vals[idx]) update_queue_unassigned (idx);
 }
 
@@ -77,7 +78,7 @@ void Internal::rescore () {
     stab[idx] *= factor;
   scinc *= factor;
   PHASE ("rescore", stats.rescored,
-    "new score increment %g after %ld conflicts",
+    "new score increment %g after %" PRId64 " conflicts",
     scinc, stats.conflicts);
 }
 
@@ -130,15 +131,17 @@ void Internal::bump_scinc () {
 struct analyze_bumped_rank {
   Internal * internal;
   analyze_bumped_rank (Internal * i) : internal (i) { }
-  size_t operator () (const int & a) const { return internal->bumped (a); }
+  uint64_t operator () (const int & a) const {
+    return internal->bumped (a);
+  }
 };
 
 struct analyze_bumped_smaller {
   Internal * internal;
   analyze_bumped_smaller (Internal * i) : internal (i) { }
   bool operator () (const int & a, const int & b) const {
-    const size_t s = analyze_bumped_rank (internal) (a);
-    const size_t t = analyze_bumped_rank (internal) (b);
+    const auto s = analyze_bumped_rank (internal) (a);
+    const auto t = analyze_bumped_rank (internal) (b);
     return s < t;
   }
 };
@@ -160,7 +163,8 @@ void Internal::bump_variables () {
     // queue and seems to work best.  We also experimented with focusing on
     // variables of the last decision level, but results were mixed.
 
-    MSORT (analyzed.begin (), analyzed.end (),
+    MSORT (opts.radixsortlim,
+      analyzed.begin (), analyzed.end (),
       analyze_bumped_rank (this), analyze_bumped_smaller (this));
   }
 
@@ -294,9 +298,9 @@ void Internal::clear_analyzed_levels () {
 struct analyze_trail_negative_rank {
   Internal * internal;
   analyze_trail_negative_rank (Internal * s) : internal (s) { }
-  size_t operator () (int a) {
+  uint64_t operator () (int a) {
     Var & v = internal->var (a);
-    size_t res = v.level;
+    uint64_t res = v.level;
     res <<= 32;
     res |= v.trail;
     return ~res;
@@ -344,7 +348,8 @@ Clause * Internal::new_driving_clause (const int glue, int & jump) {
     // the opposite order) with the hope to hit the recursion limit less
     // frequently.  Thus sorting effort is doubled here.
     //
-    MSORT (clause.begin (), clause.end (),
+    MSORT (opts.radixsortlim,
+      clause.begin (), clause.end (),
       analyze_trail_negative_rank (this), analyze_trail_larger (this));
 
     jump = var (clause[1]).level;
@@ -479,7 +484,7 @@ inline int Internal::determine_actual_backtrack_level (int jump) {
         best_idx = idx;
         best_pos = i;
       }
-      LOG ("best variable bumped %ld", bumped (best_idx));
+      LOG ("best variable bumped %" PRId64 "", bumped (best_idx));
     }
     assert (best_idx);
     LOG ("best variable %d at trail position %d", best_idx, best_pos);
@@ -516,11 +521,11 @@ void Internal::eagerly_subsume_recently_learned_clauses (Clause * c) {
   assert (opts.eagersubsume);
   LOG (c, "trying eager subsumption with");
   mark (c);
-  long lim = stats.eagertried + opts.eagersubsumelim;
+  int64_t lim = stats.eagertried + opts.eagersubsumelim;
   const auto begin = clauses.begin ();
   auto it = clauses.end ();
 #ifdef LOGGING
-  long before = stats.eagersub;
+  int64_t before = stats.eagersub;
 #endif
   while (it != begin && stats.eagertried++ <= lim) {
     Clause * d =  *--it;
@@ -540,7 +545,7 @@ void Internal::eagerly_subsume_recently_learned_clauses (Clause * c) {
   }
   unmark (c);
 #ifdef LOGGING
-  long subsumed = stats.eagersub - before;
+  uint64_t subsumed = stats.eagersub - before;
   if (subsumed) LOG ("eagerly subsumed %d clauses", subsumed);
 #endif
 }
@@ -667,8 +672,8 @@ void Internal::analyze () {
   // Update glue statistics.
   //
   const int glue = (int) levels.size ();
-  LOG (clause, "1st UIP size %ld and glue %d clause",
-    (long) clause.size (), glue);
+  LOG (clause, "1st UIP size %zd and glue %d clause",
+    clause.size (), glue);
   UPDATE_AVERAGE (averages.current.glue.fast, glue);
   UPDATE_AVERAGE (averages.current.glue.slow, glue);
 

src/arena.cpp

@@ -13,16 +13,16 @@ Arena::~Arena () {
 }
 
 void Arena::prepare (size_t bytes) {
-  LOG ("preparing 'to' space of arena with %ld bytes", (long) bytes);
+  LOG ("preparing 'to' space of arena with %zd bytes", bytes);
   assert (!to.start);
   to.top = to.start = new char[bytes];
   to.end = to.start + bytes;
 }
 
 void Arena::swap () {
   delete [] from.start;
-  LOG ("delete 'from' space of arena with %ld bytes",
-    (long) (from.end - from.start));
+  LOG ("delete 'from' space of arena with %zd bytes",
+    (size_t) (from.end - from.start));
   from = to;
   to.start = to.top = to.end = 0;
 }

src/averages.hpp

@@ -7,7 +7,7 @@ namespace CaDiCaL {
 
 struct Averages {
 
-  long swapped;
+  int64_t swapped;
 
   struct {