Merge pull request #72 from nicdard/feat/docker-schedule

fix: Remove outdated GitHub endpoint from Dockerfile

Dockerfile

@@ -33,7 +33,6 @@ RUN git clone https://github.com/testsmt/yinyang.git
 RUN git clone https://github.com/testsmt/semantic-fusion-seeds.git
 
 # Clone z3 on changes to the master branch
-ADD https://api.github.com/repos/Z3Prover/z3/compare/master...HEAD /dev/null
 RUN git clone https://github.com/Z3Prover/z3
 RUN cd z3 && \
     CXXFLAGS="-fprofile-arcs -ftest-coverage" CFLAGS="-fprofile-arcs -ftest-coverage" LDFLAGS="-fprofile-arcs -ftest-coverage" ./configure --debug && \
@@ -42,7 +41,6 @@ RUN cd z3 && \
     make install
 
 # Clone cvc5 on changes to the master branch
-ADD https://api.github.com/repos/cvc5/cvc5/compare/master...HEAD /dev/null
 RUN git clone https://github.com/cvc5/cvc5
 RUN cd cvc5 && \
     CXXFLAGS="-fprofile-arcs -ftest-coverage" CFLAGS="-fprofile-arcs -ftest-coverage" LDFLAGS="-fprofile-arcs -ftest-coverage" ./configure.sh  debug --coverage --auto-download --poly --cryptominisat --kissat && \

scripts/reproduce_smt.sh

@@ -0,0 +1,105 @@
+#!/bin/bash
+
+source $1 
+
+TIMEOUT=15
+# BAD="./$1"
+# GOOD=$2
+FILE=$2
+
+echo $GOOD
+
+if [ -z "$1" ] || [ -z "$2" ]; then
+    echo "invalid args"
+    rm -f $$bad.out $$good.out
+    exit 10
+fi
+
+echo "A" | timeout -s 9 $TIMEOUT $GOOD $FILE >& $$good.out
+ret=$?
+if grep -q "Parse Error" $$good.out; then
+    echo 2
+    rm -f $$bad.out $$good.out
+    exit 2
+fi
+if  grep -q "(error" $$good.out; then
+    echo 3
+    rm -f $$bad.out $$good.out
+    exit 3
+fi
+if [[ $ret == 124 ]]; then
+    echo 4
+    rm -f $$bad.out $$good.out
+    exit 4
+fi
+
+echo "A" | timeout -s 9 $TIMEOUT $BAD $FILE >& $$bad.out
+ret=$?
+
+if grep -q "invalid model" $$bad.out; then
+    echo bug_invalid
+    rm -f $$bad.out $$good.out
+    exit 0
+fi
+
+
+if grep -q "Parse Error" $$bad.out; then
+    echo 5
+    rm -f $$bad.out $$good.out
+    exit 5
+fi
+if grep -q "(error" $$bad.out; then
+    echo 6
+    rm -f $$bad.out $$good.out
+    exit 6
+fi
+
+if [[ $ret == 139 ]]; then
+    echo bug_crash
+    rm -f $$bad.out $$good.out
+    exit 0
+fi
+
+if grep -q "unknown" $$bad.out; then
+    echo 7
+    rm -f $$bad.out $$good.out
+    exit 7
+fi
+
+if [[ $ret == 124 ]]; then
+    echo 8
+    rm -f $$bad.out $$good.out
+    exit 8
+fi
+
+if  grep -q "ASSERTION VIOLATION" $$bad.out; then
+    echo bug_assertion
+    rm -f $$bad.out $$good.out
+    exit 0
+fi
+
+if  grep -q "LEAKED" $$bad.out; then
+    echo bug_leaked
+    rm -f $$bad.out $$good.out
+    exit 0
+fi
+
+if egrep "^sat$" $$bad.out ; then
+    if egrep "^unsat$" $$good.out ; then
+        echo unsat2sat
+        rm -f $$bad.out $$good.out
+        exit 0
+    fi
+fi
+
+if egrep "^unsat$" $$bad.out ; then
+    if egrep "^sat$" $$good.out ; then
+        echo sat2unsat
+        rm -f $$bad.out $$good.out
+        exit 0
+    fi
+fi
+
+echo 1
+rm -f $$bad.out $$good.out
+exit 1

scripts/test-bitvectors.sh

@@ -0,0 +1,18 @@
+#!/bin/bash
+
+# Start all benchmarks.
+BENCHMARKS="BV QF_BV QF_BVFP QF_ABV QF_ABVFP"
+ORACLES="sat unsat"
+for size in 30 70;
+  do
+  python3 /app/main.py --target $size.txt --theories bitvector --size $size --num_functions 30
+  for theory in $BENCHMARKS;
+  do  
+    for oracle in $ORACLES;
+    do
+      python3 /app/yinyang/bin/yinyang -t 40 -c /app/out/$size.txt -o $oracle "cvc5 --strings-exp" /app/semantic-fusion-seeds/$theory/$oracle &
+      python3 /app/yinyang/bin/yinyang -t 40 -c /app/out/$size.txt -o $oracle "z3 smt.string_solver=seq" /app/semantic-fusion-seeds/$theory/$oracle &
+    done
+  done
+done
+

scripts/test-strings.sh

@@ -0,0 +1,18 @@
+#!/bin/bash
+
+# Start all benchmarks.
+BENCHMARKS="QF_SLIA QF_S"
+ORACLES="sat unsat"
+for size in 20 35;
+  do
+  python3 /app/main.py --target $size.txt --theories string --size $size --num_functions 30
+  for theory in $BENCHMARKS;
+  do  
+    for oracle in $ORACLES;
+    do
+      python3 /app/yinyang/bin/yinyang -t 40 -c /app/out/$size.txt -o $oracle "cvc5 --strings-exp" /app/semantic-fusion-seeds/$theory/$oracle &
+      python3 /app/yinyang/bin/yinyang -t 40 -c /app/out/$size.txt -o $oracle "z3 smt.string_solver=seq" /app/semantic-fusion-seeds/$theory/$oracle &
+    done
+  done
+done
+