ci,tests: format scripts

Apply formatting.

Signed-off-by: Norbert Manthey <[email protected]>

tools/checker/check-drat.sh

@@ -18,34 +18,31 @@ p=p.proof
 o=drat-minimize-output.txt
 t=$(readlink -e ../../build/release/bin/mergesat)
 # allow to override the solver location via environment variable
-if [ -n "${FUZZ_SOLVER:-}" ]
-then
-	t=$(readlink -e "${FUZZ_SOLVER:-}")
+if [ -n "${FUZZ_SOLVER:-}" ]; then
+    t=$(readlink -e "${FUZZ_SOLVER:-}")
 fi
 d=$(readlink -e "$SCRIPT_DIR"/drat-trim)
 
 # run solver
 STATUS=0
 $t "$f" -drup-file="$p" $@ || STATUS=$?
 
-if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
-then
-	echo "unexpected status code $STATUS"
-	exit $STATUS
+if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then
+    echo "unexpected status code $STATUS"
+    exit $STATUS
 fi
 
 # exclude trivial unsat
 grep "^0$" $f && exit 0
 
 # run the check
-if [ "$STATUS" -ne 20 ]
-then
+if [ "$STATUS" -ne 20 ]; then
     exit $STATUS
 fi
 
 # verify binary proof format
 VERIFY_STATUS=0
-$d $f $p -v -v -n &> $o || exit $VERIFY_STATUS
+$d $f $p -v -v -n &>$o || exit $VERIFY_STATUS
 echo "verify status: $VERIFY_STATUS"
 # for now, don't be too strict
 # grep " does not occur: " $o && exit 3
@@ -54,24 +51,22 @@ exit 20
 # re-run with plain proof format
 "$t" "$f" -drup-file=$p -no-binary-proof $@ || STATUS=$?
 
-if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
-then
-	echo "unexpected status code $STATUS"
-	exit $STATUS
+if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then
+    echo "unexpected status code $STATUS"
+    exit $STATUS
 fi
 
 # exclude trivial unsat
 grep "^0$" $f && exit 0
 
 # run the check
-if [ "$STATUS" -ne 20 ]
-then
+if [ "$STATUS" -ne 20 ]; then
     exit $STATUS
 fi
 
 # verify binary proof format
 VERIFY_STATUS=0
-$d $f $p -v -v -n &> $o || exit $VERIFY_STATUS
+$d $f $p -v -v -n &>$o || exit $VERIFY_STATUS
 echo "verify status: $VERIFY_STATUS"
 # for now, don't be too strict
 # grep " does not occur: " $o && exit 3

tools/checker/fuzz-drat.sh

@@ -18,33 +18,31 @@ declare -i found_sat=0
 declare -i found_unsat=0
 
 FAILED=0
-while true
-do
-	I=$((I+1))
-	[ "$LIMIT" -ge "$I" ] || break
-	# echo "[$SECONDS] run $I ..."
-	seed="$(echo $(($(date +%s%N)/1000000)))"
-	cls=""
-	while [ -z "$cls" ]; do
-		cls="$(bash -c 'echo $((9000 + $(date +%4N) ))' 2> /dev/null)"
-	done
-	modgen_cli_args="-s $seed -n 3500 -m $cls"
-	$c $modgen_cli_args > $f
-	STATUS=0
-	timeout "$TIMEOUT" "$SCRIPT_DIR"/check-drat.sh $f &> output.log || STATUS=$?
-	# ignore time outs
-	[ "$STATUS" -ne 124 ] || continue
+while true; do
+    I=$((I + 1))
+    [ "$LIMIT" -ge "$I" ] || break
+    # echo "[$SECONDS] run $I ..."
+    seed="$(echo $(($(date +%s%N) / 1000000)))"
+    cls=""
+    while [ -z "$cls" ]; do
+        cls="$(bash -c 'echo $((9000 + $(date +%4N) ))' 2>/dev/null)"
+    done
+    modgen_cli_args="-s $seed -n 3500 -m $cls"
+    $c $modgen_cli_args >$f
+    STATUS=0
+    timeout "$TIMEOUT" "$SCRIPT_DIR"/check-drat.sh $f &>output.log || STATUS=$?
+    # ignore time outs
+    [ "$STATUS" -ne 124 ] || continue
 
-	# make failures permanent
-	if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
-	then
-		echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" $f) and generator: $c $modgen_cli_args"
-		mv $f fuzz_input.$I.cnf
-		mv output.log output.$I.log
-                FAILED=$((FAILED+1))
-	fi
-	[ "$STATUS" -eq 10 ] && found_sat=$((found_sat+1))
-	[ "$STATUS" -eq 20 ] && found_unsat=$((found_unsat+1))
+    # make failures permanent
+    if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then
+        echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" $f) and generator: $c $modgen_cli_args"
+        mv $f fuzz_input.$I.cnf
+        mv output.log output.$I.log
+        FAILED=$((FAILED + 1))
+    fi
+    [ "$STATUS" -eq 10 ] && found_sat=$((found_sat + 1))
+    [ "$STATUS" -eq 20 ] && found_unsat=$((found_unsat + 1))
 done
 echo "failed $FAILED out of $LIMIT"
 echo "($SECONDS s) sat: $found_sat unsat: $found_unsat"

tools/checker/fuzzcheck.sh

@@ -17,113 +17,106 @@ log=fuzz-$$.log
 rm -f $log $cnf $sol
 echo "[fuzz] running $prg"
 echo "[fuzz] logging $log"
-echo "run $1 $2" > $log
+echo "run $1 $2" >$log
 echo "[fuzz] run with pid $$"
 echo "[fuzz] started at $(date)"
 i=0
 
 # set limit for number of instances to be solved
 limit=1
-if [ "x$2" != "x" ]
-then
-  limit=$2
+if [ "x$2" != "x" ]; then
+    limit=$2
 fi
 test=0
 
 declare -i status=0
 declare -i found_sat=0
 declare -i found_unsat=0
 
-while [ "$test" -lt "$limit" ]
-do
-  rm -f $cnf; 
-  seed="$(echo $(($(date +%s%N)/1000000)))"
-  cls=""
-  while [ -z "$cls" ]; do
-    cls="$(bash -c 'echo $((6000 + $(date +%4N) ))' 2> /dev/null)"
-  done
-  modgen_cli_args="-s $seed -n 2800 -m $cls"
-  ./modgen $modgen_cli_args > $cnf
-  # control whether algorithm should sleep
-  seed=`grep 'c seed' $cnf|head -1|awk '{print $NF}'`
-  head="`awk '/p cnf /{print $3, $4}' $cnf`"
-  [ -n "${VERBOSE_FUZZING:-}" ] && printf "%d %16d          %6d    %6d               \r" "$i" "$seed" $head
-  i=`expr $i + 1`
-  rm -f $sol
-
-  # set limit for number of instances to be solved
-  if [ "x$2" != "x" ]
-  then
-    test=$(($test+1))
-  fi
-
-  thiscls=`awk '/p cnf /{print $4}' $cnf`
-  if [ $bestcls -ne "-1" ]
-  then
-    if [ $bestcls -le $thiscls ]
-    then
-      continue
+while [ "$test" -lt "$limit" ]; do
+    rm -f $cnf
+    seed="$(echo $(($(date +%s%N) / 1000000)))"
+    cls=""
+    while [ -z "$cls" ]; do
+        cls="$(bash -c 'echo $((6000 + $(date +%4N) ))' 2>/dev/null)"
+    done
+    modgen_cli_args="-s $seed -n 2800 -m $cls"
+    ./modgen $modgen_cli_args >$cnf
+    # control whether algorithm should sleep
+    seed=$(grep 'c seed' $cnf | head -1 | awk '{print $NF}')
+    head="$(awk '/p cnf /{print $3, $4}' $cnf)"
+    [ -n "${VERBOSE_FUZZING:-}" ] && printf "%d %16d          %6d    %6d               \r" "$i" "$seed" $head
+    i=$(expr $i + 1)
+    rm -f $sol
+
+    # set limit for number of instances to be solved
+    if [ "x$2" != "x" ]; then
+        test=$(($test + 1))
+    fi
+
+    thiscls=$(awk '/p cnf /{print $4}' $cnf)
+    if [ "$bestcls" -ne "-1" ]; then
+        if [ "$bestcls" -le "$thiscls" ]; then
+            continue
+        fi
     fi
-  fi
 
-  ./toolCheck.sh $prg $cnf > $out 2> $err
-  res=$?
-#  echo "result $res"
-  case $res in
+    ./toolCheck.sh $prg $cnf >$out 2>$err
+    res=$?
+    #  echo "result $res"
+    case $res in
     124)
-      echo "($SECONDS s) timeout with $seed" > $log
-      mv $cnf timeout-$seed.cnf
-      continue
-      ;;
+        echo "($SECONDS s) timeout with $seed" >$log
+        mv $cnf timeout-$seed.cnf
+        continue
+        ;;
     10)
-      found_sat=$((found_sat+1))
-      continue
-      ;;
+        found_sat=$((found_sat + 1))
+        continue
+        ;;
     20)
-      found_unsat=$((found_unsat+1))
-      continue
-      ;;
-    15)
-    ;;
-    25)
-    ;;
-  esac
-
-  status=1
-
-  head="`awk '/p cnf /{print $3, $4}' $cnf`"
-  echo "($SECONDS s) [fuzz] bug-$seed $head             with exit code $res"
-  echo "($SECONDS s) To reproduce, run modgen: './modgen $modgen_cli_args > reproduce.cnf' and '$prg reproduce.cnf'"
-  echo $seed >> $log
-  echo "($SECONDS s) out"
-  cat $out
-  echo "($SECONDS s) err"
-  cat $err
-
-  #
-  # consider only bugs that are smaller then the ones we found already
-  #
-  if [ $bestcls -eq "-1" ]
-  then
-    bestcls=$thiscls
-    echo "($SECONDS s) init bestcls with $bestcls"
-  elif [ $bestcls -le $thiscls ]
-  then
-    echo "($SECONDS s) reject new bug with $thiscls clauses"
-    continue
-  fi
-
-  bestcls=$thiscls # store better clause count!
-  echo "($SECONDS s) set bestcls to $bestcls"
-  red=red-$seed.cnf
-  bug=bug-$seed.cnf
-  mv $cnf $bug
-
-  if [ -f "$red" ]; then
-    head="`awk '/p cnf /{print $3, $4}' $red`"
-    echo "($SECONDS s) [fuzz] $red $head"
-  fi
-  # rm -f $bug
+        found_unsat=$((found_unsat + 1))
+        continue
+        ;;
+    15) ;;
+
+    25) ;;
+
+    esac
+
+    status=1
+
+    head="$(awk '/p cnf /{print $3, $4}' $cnf)"
+    echo "($SECONDS s) [fuzz] bug-$seed $head             with exit code $res"
+    echo "($SECONDS s) To reproduce, run modgen: './modgen $modgen_cli_args > reproduce.cnf' and '$prg reproduce.cnf'"
+    echo $seed >>$log
+    echo "($SECONDS s) out"
+    cat $out
+    echo "($SECONDS s) err"
+    cat $err
+
+    #
+    # consider only bugs that are smaller then the ones we found already
+    #
+    if [ "$bestcls" -eq "-1" ]; then
+        bestcls=$thiscls
+        echo "($SECONDS s) init bestcls with $bestcls"
+    elif [ "$bestcls" -le $thiscls ]; then
+        echo "($SECONDS s) reject new bug with $thiscls clauses"
+        continue
+    fi
+
+    bestcls="$thiscls" # store better clause count!
+    echo "($SECONDS s) set bestcls to $bestcls"
+    red=red-$seed.cnf
+    bug=bug-$seed.cnf
+    mv $cnf $bug
+
+    if [ -f "$red" ]; then
+        head="$(awk '/p cnf /{print $3, $4}' $red)"
+        echo "($SECONDS s) [fuzz] $red $head"
+    fi
+    # rm -f $bug
 done
 
 echo "($SECONDS s) sat: $found_sat unsat: $found_unsat"

tools/checker/prepare.sh

@@ -6,21 +6,20 @@
 set -e
 
 # directory of this script (in repo/scripts)
-script_dir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
+script_dir=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
 
 # get drat-trim
-if [ -d drat-trim-src ]
-then
-	pushd drat-trim-src
-	git fetch origin
-	git checkout origin/master
-	popd
+if [ -d drat-trim-src ]; then
+    pushd drat-trim-src
+    git fetch origin
+    git checkout origin/master
+    popd
 else
-	git clone https://github.com/marijnheule/drat-trim.git drat-trim-src
+    git clone https://github.com/marijnheule/drat-trim.git drat-trim-src
 fi
 
 # get and build modgen
-git clone --depth=1 git@github.com:conp-solutions/modularityGen.git modgen-src
+git clone --depth=1 https://github.com/conp-solutions/modularityGen.git modgen-src
 make -C modgen-src
 cp modgen-src/modgen .