Merge pull request #104 from conp-solutions/more-testing

More testing

.github/workflows/build-and-test-parallel.yml

@@ -12,7 +12,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

.github/workflows/build-and-test.yml

@@ -8,7 +8,7 @@ on:
 jobs:
   CrossARM:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

.github/workflows/build-werror.yml

@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

.github/workflows/check-style.yml

@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

.github/workflows/compare-upstream.yml

@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

.github/workflows/mini-competition.yml

@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

.github/workflows/unit-tests.yml

@@ -9,7 +9,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

CHANGELOG

@@ -7,6 +7,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [unreleased]
 
+ * testing: use modgen generator during fuzzing runs
  * fix FPU control to compile on ARM
 
 ## [v3.2.1] - 2021-12-20

tools/checker/check-drat.sh

@@ -11,39 +11,38 @@ shift
 # check for file
 [ -f "$f" ] || exit 2
 
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
+
 # static variables
 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 drat-trim)
+d=$(readlink -e "$SCRIPT_DIR"/drat-trim)
 
 # run solver
 STATUS=0
-"$t" "$f" -drup-file=$p $@ || STATUS=$?
+$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
@@ -52,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

@@ -8,33 +8,43 @@ TIMEOUT=$2
 
 [ -n "$TIMEOUT" ] || exit 2
 
-c=$(readlink -e cnfuzz)
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
+
+c="$SCRIPT_DIR/modgen"
 
 I=0
-f=input.cnf
+f=fuzz_input.cnf
+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 ..."
-	$c > $f
-	STATUS=0
-	timeout "$TIMEOUT" ./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" input.cnf) seed $(awk '/c seed/ {print $3}' input.cnf)"
-		mv input.cnf input.$I.cnf
-		mv output.log output.$I.log
-                FAILED=$((FAILED+1))
-	fi
+    # 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"
 [ "$FAILED" -eq 0 ] || exit 1
 exit 0