Commit abdb518d authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'cvc4_config' into 'master'

Add --stats to cvc4 to allow querying steps

See merge request !126
parents 08e25d93 963257d7
......@@ -77,12 +77,15 @@ run () {
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' | \
sed -r 's/(Timeout.*$|Unknown \(unknown\).*$)/Timeout or Unknown/' | \
# ad hoc sed to remove the directory of the stdlib that can be found
# inside labels attribute [@at:'Old:loc:/home/.../stdlib/array.mlw
# TODO temporary as this comes from incorrect locations generated in
# a[i] <- x like terms.
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' >> "$f.out"
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' | \
# Remove steps informations
sed -r 's/Unknown \(sat\).*$/Unknown \(sat\)/' | \
sed -r 's/Valid \(.*$/Valid/' >> "$f.out"
str_oracle=$(tr -d ' \n' < "${oracle_file}")
str_out=$(tr -d ' \n' < "$f.out")
decide_fail $f
......
......@@ -35,7 +35,7 @@ version_ok = "1.7"
driver = "cvc4_16_counterexample"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command = "%e --stats --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
# CVC4 version >= 1.6
......@@ -51,7 +51,7 @@ version_ok = "1.7"
driver = "cvc4_16"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit=%t000 --lang=smt2 %f"
command = "%e --stats --tlimit=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
use_at_auto_level = 1
......@@ -67,7 +67,7 @@ version_ok = "1.5"
driver = "cvc4_15_counterexample"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command = "%e --stats --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
# CVC4 version 1.5
......@@ -81,7 +81,7 @@ version_ok = "1.5"
driver = "cvc4_15"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit=%t000 --lang=smt2 %f"
command = "%e --stats --tlimit=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
use_at_auto_level = 1
......
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