-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathrun_tests.sh
executable file
·25 lines (21 loc) · 1.44 KB
/
run_tests.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
#!/bin/sh
N=$(cat /proc/cpuinfo | grep processor | wc -l)
echo "Using $N threads."
PR=../testsuite/precision-recall/PrecisionRecall.hs
COMMON="--cvc4 --alt-ergo --spass --verbosity=40 --lint-poly-fol -N$N +RTS -N4 -RTS"
cd examples
hipspec HOF.hs --auto=False --success=NothingUnproved $COMMON || exit $?
hipspec Properties.hs --auto=False --success=NothingUnproved $COMMON || exit $?
hipspec $PR --extra-trans=++,foldl,foldr --success=NothingUnproved $COMMON || exit $?
hipspec $PR --extra-trans=++,map,reverse --success=NothingUnproved $COMMON || exit $?
hipspec Nat.hs --extra-trans=* --success=NothingUnproved $COMMON || exit $?
hipspec List.hs --auto=False --success=NothingUnproved $COMMON || exit $?
hipspec Reverse.hs --only-user-stated --success=ProvesUserStated $COMMON || exit $?
hipspec Concat.hs --auto=False --success=NothingUnproved $COMMON || exit $?
hipspec BinLists.hs --success=NothingUnproved $COMMON || exit $?
hipspec Rotate.hs --only-user-stated --success=ProvesUserStated $COMMON || exit $?
cd ..
for i in $(ls tfp1/tests/*.hs); do
echo $i
hipspec --tr-mod --translate-only --lint-poly-fol $i || exit $?
done