This commit is contained in:
aqjune 2019-02-01 10:37:43 +09:00 коммит произвёл Juneyoung Lee
Родитель a6dba0c6d0
Коммит e744f08668
4 изменённых файлов: 5 добавлений и 6 удалений

Просмотреть файл

@ -4,11 +4,11 @@ import sys
def matches(s1, s2):
s1 = s1.strip()
s2 = s2.strip()
if s1 != "sat" and s1 != "unsat":
if s1 != "Correct" and s1 != "Incorrect":
# Unknown output.
return 0
if (s1 == "unsat" and s2 == "Optimization is correct!") or \
(s1 == "sat" and s2.startswith("ERROR:")):
if (s1 == "Correct" and s2 == "Optimization is correct!") or \
(s1 == "Incorrect" and s2.startswith("ERROR:")):
# Correct.
return 1
# Incorrect!

3
run-alive.sh Normal file → Executable file
Просмотреть файл

@ -2,8 +2,7 @@ for i in "inputs/alive/instcombine" "inputs/alive/unit"; do
echo "Running ${i}/*.opt .."
find ${i} -name "opt*" -print0 | sort -z | xargs --null cat > ${i}/all.opt
lean -q --run src/main.lean -verifyopt ${i}/all.opt > output.txt
grep -E '^sat$|^unsat$' output.txt > output_summarized.txt
python3 check_diff.py output_summarized.txt ${i}/answ.txt
python3 check_diff.py output.txt ${i}/answ.txt
rm ${i}/all.opt
echo
done

Просмотреть файл

@ -1,5 +1,5 @@
# of testing
n=10000
n=5000
# clang path
clang=~/clang-7.0.1/bin/clang
# verbosity, replace n with y if want the script to be verbose

0
run-proptest.sh Normal file → Executable file
Просмотреть файл