new bench file for division and modulo

parent 81b10179
......@@ -32,11 +32,11 @@ goods () {
bads () {
for f in $1/*.why; do
echo -n " "$f"... "
if $pgm $2 $f > /dev/null 2>&1; then
if $pgm $2 $f > /dev/null 2>&1; then
echo "$pgm $2 $f"
echo "FAILED!"
exit 1
else
exit 1
else
echo "ok"
fi
done
......@@ -59,13 +59,13 @@ drivers () {
programs () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if ! $pgml -L modules $pgml_options $f $2 > /dev/null 2>&1; then
echo
if ! $pgml -L modules $pgml_options $f $2 > /dev/null 2>&1; then
echo
echo "$pgml $pgml_options $f $2"
$pgml -L modules $pgml_options $f $2
echo "FAILED!"
exit 1
else
exit 1
else
echo "ok"
fi
done
......@@ -74,12 +74,12 @@ programs () {
bad_programs () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgml -L modules $pgml_options $f > /dev/null 2>&1; then
echo
if $pgml -L modules $pgml_options $f > /dev/null 2>&1; then
echo
echo "$pgml $pgml_options $f"
echo "SHOULD FAIL!"
exit 1
else
exit 1
else
echo "ok"
fi
done
......@@ -93,7 +93,7 @@ valid_goals () {
echo "$pgml -P alt-ergo $f"
$pgml -L modules -t 10 -P alt-ergo $f
exit 1
else
else
echo "ok"
fi
done
......
(* Division and modulo *)
theory Euclidean
use import int.Int
use import int.EuclideanDivision
(* -2,-1,0,1,2 div/mod 2 *)
goal div_m2_2: div (-2) 2 = -1
goal div_m1_2: div (-1) 2 = -1
goal div__0_2: div 0 2 = 0
goal div__1_2: div 1 2 = 0
goal div__2_2: div 2 2 = 1
goal mod_m2_2: mod (-2) 2 = 0
goal mod_m1_2: mod (-1) 2 = 1
goal mod__0_2: mod 0 2 = 0
goal mod__1_2: mod 1 2 = 1
goal mod__2_2: mod 2 2 = 0
(* -2,-1,0,1,2 div/mod -2 *)
goal div_m2_m2: div (-2) (-2) = 1
goal div_m1_m2: div (-1) (-2) = 1
goal div__0_m2: div 0 (-2) = 0
goal div__1_m2: div 1 (-2) = -1
goal div__2_m2: div 2 (-2) = -1
goal mod_m2_m2: mod (-2) (-2) = 0
goal mod_m1_m2: mod (-1) (-2) = 1
goal mod__0_m2: mod 0 (-2) = 0
goal mod__1_m2: mod 1 (-2) = 1
goal mod__2_m2: mod 2 (-2) = 0
end
theory Computer
use import int.Int
use import int.ComputerDivision
(* -2,-1,0,1,2 div/mod 2 *)
goal div_m2_2: div (-2) 2 = -1
goal div_m1_2: div (-1) 2 = 0
goal div__0_2: div 0 2 = 0
goal div__1_2: div 1 2 = 0
goal div__2_2: div 2 2 = 1
goal mod_m2_2: mod (-2) 2 = 0
goal mod_m1_2: mod (-1) 2 = -1
goal mod__0_2: mod 0 2 = 0
goal mod__1_2: mod 1 2 = 1
goal mod__2_2: mod 2 2 = 0
(* -2,-1,0,1,2 div/mod -2 *)
goal div_m2_m2: div (-2) (-2) = 1
goal div_m1_m2: div (-1) (-2) = 0
goal div__0_m2: div 0 (-2) = 0
goal div__1_m2: div 1 (-2) = 0
goal div__2_m2: div 2 (-2) = -1
goal mod_m2_m2: mod (-2) (-2) = 0
goal mod_m1_m2: mod (-1) (-2) = -1
goal mod__0_m2: mod 0 (-2) = 0
goal mod__1_m2: mod 1 (-2) = 1
goal mod__2_m2: mod 2 (-2) = 0
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment