mirror of
https://github.com/Veridise/Picus.git
synced 2026-04-19 03:00:11 -04:00
8432a9bfb6
We almost always only want the weak safety (checking that output signals of the main component are deterministic), not strong safety (checking that all signals are deterministic). However, currently the strong safety mode is the default. This makes it cumbersome to invoke Picus, since we need to indicate that we want the weak safety explicitly. This commit inverts the behavior by removing the flag `--weak` and adds the flag `--strong` (for strong safety), which is defaulted to false.
29 lines
786 B
Bash
Executable File
29 lines
786 B
Bash
Executable File
#!/bin/bash
|
|
# usage: this.sh <timeout:seconds> <log_path> <target_folder> <precondition_folder>
|
|
# example: ./batch-run-picus.sh z3 600 ./logs/test/ ./benchmarks/circomlib-cff5ab6/ ./tests/ecne-unique-set/circomlib-cff5ab6/
|
|
|
|
solver=$1
|
|
otime=$2
|
|
logpath=$3
|
|
targetfolder=$4
|
|
prefolder=$5
|
|
|
|
mkdir -p ${logpath}
|
|
|
|
for fp in ${targetfolder}/*.r1cs
|
|
do
|
|
fn=$(basename ${fp})
|
|
bn="${fn%.*}"
|
|
bp="${fp%.*}"
|
|
echo "=================== checking: ${fn} ==================="
|
|
echo "==== start: $(date -u)"
|
|
st="$(date -u +%s)"
|
|
|
|
timeout ${otime} racket ./picus.rkt --timeout 5000 --solver ${solver} --r1cs ${fp} --precondition ${prefolder}/${bn}.pre.json > ${logpath}/${bn}.log 2>&1
|
|
|
|
et="$(date -u +%s)"
|
|
echo "==== end: $(date -u)"
|
|
ct="$(($et-$st))"
|
|
echo "==== elapsed: ${ct} seconds"
|
|
done
|