1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
TO_EMAIL="taking@cs.nyu.edu"
CC_EMAIL=""
function RunClusterRegressions() {
local job_name="cvc4-$1"
local cvc4_binary="$2"
local config_line="$3"
mysql -u smt_cluster --password=`cat ~/.mysql_password` smt_cluster <<EOF
insert into Jobs values
(DEFAULT, "$job_name", "custom job", "19", "300", "2000", "26", "$TO_EMAIL $CC_EMAIL", "2", "$cvc4_binary", "1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29", DEFAULT);
EOF
}
JOB_TIME=`date +%s`
NAME="cluster-qf_lra-benchmark-$JOB_TIME"
RunClusterRegressions "$NAME" $1 ""
|
