Merge remote-tracking branch 'upstream/master'

LICENSE

@@ -1,6 +1,7 @@
 MIT License
 
-Copyright (c) 2016-2019 Armin Biere, Johannes Kepler University Linz, Austria
+Copyright (c) 2016-2020 Armin Biere, Johannes Kepler University Linz, Austria
+Copyright (c) 2020 Mathias Fleury, Johannes Kepler University Linz, Austria
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

VERSION

@@ -1 +1 @@
-1.2.1
+1.3.0

configure

@@ -18,8 +18,11 @@ all=no
 debug=no
 logging=no
 check=no
+competition=no
 coverage=no
 profile=no
+contracts=yes
+tracing=yes
 unlocked=yes
 pedantic=no
 options=""
@@ -48,12 +51,12 @@ die () {
   else
     checklog=""
   fi
-  echo "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}"
+  cecho "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}"
   exit 1
 }
 
 msg () {
-  echo "${BOLD}configure:${NORMAL} $*"
+  cecho "${BOLD}configure:${NORMAL} $*"
 }
 
 # if we can find the 'color.sh' script source it and overwrite color codes
@@ -79,14 +82,20 @@ where '<option>' is one of the following
 -g|--debug         compile with debugging information
 -c|--check         compile with assertion checking (default for '-g')
 -l|--log[ging]     include logging code (but disabled by default)
--a|--all           short cut for all above, e.g., '-g -l -s' (thus also '-c')
+-a|--all           short cut for all above, e.g., '-g -l' (thus also '-c')
 -q|--quiet         exclude message and profiling code (logging too)
 -p|--pedantic      add '--pedantic' and '-Werror' compilation flag
 -s|--symbols       add '-ggdb3' (even for optimized compilation)
 
 --coverage         compile with '-ftest-coverage -fprofile-arcs' for 'gcov'
 --profile          compile with '-pg' to profile with 'gprof'
 
+--no-contracts     compile without API contract checking code
+--no-tracing       compile without API call tracing code
+
+--competition      configure for the competition
+                   ('--quiet', '--no-contracts', '--no-tracing')
+
 -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')
@@ -135,9 +144,14 @@ do
     -p|--pedantic) pedantic=yes;;
     -q|--quiet) quiet=yes;;
 
+    --no-contracts | --no-contract) contracts=no;;
+    --no-tracing | --no-trace) tracing=no;;
+
     --coverage) coverage=yes;;
     --profile) profile=yes;;
 
+    --competition) competition=yes;;
+
     --no-unlocked) unlocked=no;;
 
     -j*) MAKEFLAGS="$1";;
@@ -255,12 +269,21 @@ then
   esac
 fi
 
+if [ $competition = yes ]
+then
+  quiet=yes
+  contracts=no
+  tracing=no
+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"
+[ $contracts = no ] && CXXFLAGS="$CXXFLAGS -DNCONTRACTS"
+[ $tracing = no ] && CXXFLAGS="$CXXFLAGS -DNTRACING"
 
 CXXFLAGS="$CXXFLAGS$options"
 
@@ -416,7 +439,6 @@ clean:
 	  if [ -f "\$(CADICALBUILD)"/makefile ]; \\
 	  then \\
 	     touch "\$(CADICALBUILD)"/build.hpp; \\
-	     touch "\$(CADICALBUILD)"/dependencies; \\
 	     \$(MAKE) -C "\$(CADICALBUILD)" clean; \\
 	  fi; \\
 	  rm -rf "\$(CADICALBUILD)"; \\

makefile.in

@@ -19,9 +19,9 @@ MAKEFLAGS=@MAKEFLAGS@
 ############################################################################
 
 APP=cadical.cpp mobical.cpp
-ALL=$(sort $(wildcard ../src/*.[ch]pp))
-SRC=$(filter %.cpp,$(subst ../src/,,$(ALL)))
-LIB=$(filter-out $(APP),$(SRC))
+SRC=$(sort $(wildcard ../src/*.cpp))
+SUB=$(subst ../src/,,$(SRC))
+LIB=$(filter-out $(APP),$(SUB))
 OBJ=$(LIB:.cpp=.o)
 DIR=../$(shell pwd|sed -e 's,.*/,,')
 COMPILE=$(CXX) $(CXXFLAGS) -I$(DIR)

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

@@ -60,8 +60,15 @@ run () {
 
 ############################################################################
 
-run		# default configuration
-run -p		# check pedantic first
+# start with these two for fast fail
+
+run -j		# default configuration with fast parallel compilation
+run -j -p	# check pedantic in parallel
+
+run		# default configuration (depends on 'MAKEFLAGS'!)
+run -p		# then check default pedantic first
+
+run -j1		# forced slow sequential compilation (checks '-j1' option)
 
 run -q		# library users might want to disable messages
 run -q -p	# also check '--quiet' pedantically
@@ -85,12 +92,16 @@ run -l -p
 # ('-g' can not be combined '-c')
 
 run -c -l
+run -c -q
 run -g -l
+run -g -q
 
 # the same pairs but now with pedantic compilation
 
 run -c -l -p
+run -c -q -p
 run -g -l -p
+run -g -q -p
 
 # finally check that these also work to some extend
 
@@ -100,4 +111,10 @@ run -m32 -a -p
 run --no-unlocked -q
 run --no-unlocked -a -p
 
+run --no-contracts -q
+run --no-contracts -a -p
+
+run --no-tracing -q
+run --no-tracing -a -p
+
 echo "successfully compiled and tested ${GOOD}${ok}${NORMAL} configurations"

scripts/colors.sh

@@ -1,13 +1,20 @@
 # Use colors if '<stdin>' is connected to a terminal.
 
+color_echo_options=""
+
 if [ -t 1 ]
 then
-  BAD="\033[1;31m"	# bright red
-  HILITE="\033[32m"	# normal green
-  GOOD="\033[1;32m"	# bright green
-  HIDE="\033[34m"	# cyan
-  BOLD="\033[1m"        # bold color
-  NORMAL="\033[0m"	# normal color
+  BAD="\033[1;31m"  # bright red
+  HILITE="\033[32m" # normal green
+  GOOD="\033[1;32m" # bright green
+  HIDE="\033[34m"   # cyan
+  BOLD="\033[1m"    # bold color
+  NORMAL="\033[0m"  # normal color
+
+  if [ x"`echo -e 2>/dev/null`" = x ]
+  then
+    color_echo_options=" -e"
+  fi
 else
   BAD=""
   HILITE=""
@@ -16,3 +23,7 @@ else
   BOLD=""
   NORMAL=""
 fi
+
+cecho () {
+  echo$color_echo_options $*
+}

scripts/generate-cubes.sh

@@ -0,0 +1,37 @@
+#!/bin/sh
+usage () {
+cat <<EOF 2>&1
+usage: generate-cubes.sh [-h] <input> [ <output> [ <march_cu option> ... ] ]
+EOF
+exit 0
+}
+[ "$1" = -h ] && usage
+die () {
+  echo "generate-cubes.sh: error: $*" 1>&2
+  exit 1
+}
+[ $# -lt 1 ] && die "expected DIMACS file argument"
+output=""
+options=""
+[ -f "$1" ] || die "first argument is not a DIMACS file"
+input="$1"
+shift
+while [ $# -gt 0 ]
+do
+  case "$1" in
+    -*) options="$options $1";;
+    *) exec 1>"$1";;
+  esac
+  shift
+done
+prefix=/tmp/generate-cubes-$$
+cleanup () {
+  rm -f $prefix*
+}
+trap "cleanup" 2 11
+cubes=$prefix.cubes
+march_cu $input -o $cubes $options 1>&2 || exit 1
+sed -e 's,^p cnf.*,p inccnf,' $input
+cat $cubes
+cleanup
+exit 0

scripts/make-build-header.sh

@@ -76,7 +76,7 @@ else
 fi
 
 #--------------------------------------------------------------------------#
-# Use time of executing this script as build time.
+# Use time of executing this script at build time.
 #
 LC_TIME="en_US" # Avoid umlaut in 'DATE'.
 export LC_TIME

scripts/prepare-sr2019-submission.sh → scripts/prepare-sc2020-submission.sh

@@ -1,7 +1,7 @@
 #!/bin/sh
 cd `dirname $0`/..
 root=`pwd`
-tmp=/tmp/prepare-cadical-sr2018-submission.log
+tmp=/tmp/prepare-cadical-sc2020-submission.log
 VERSION=`cat VERSION`
 rm -f $tmp
 ##########################################################################
@@ -25,7 +25,7 @@ cat <<EOF >$dir/build/build.sh
 tar xf ../archives/cadical*
 mv cadical* cadical
 cd cadical
-./configure
+./configure --competition
 make test
 install -s build/cadical ../../bin/
 EOF
@@ -41,6 +41,9 @@ cat <<EOF >$dir/bin/starexec_run_default
 exec ./cadical --$option \$1 \$2/proof.out
 EOF
 chmod 755 $dir/bin/starexec_run_default
+description=$dir/starexec_description.txt
+grep '^CaDiCaL' README.md|head -1 >$description
+cat $description
 archive=/tmp/$base.zip
 rm -f $archive
 cd $dir

src/README.md

@@ -2,7 +2,7 @@ This is the source code of the library `libcadical.a` with header
 `cadical.hpp`, the stand-alone solver `cadical` (in `cadical.cpp`) and the
 model based tester `mobical` (in `mobical.app`).
 
-The links to the `configure` script and the `makefile` in the root directory
+The `configure` script and link to the `makefile` in the root directory
 can be used from within the `src` sub-directory too and then will just work
 as if used from the root directory.  For instance