diff options
| -rwxr-xr-x | contrib/cluster-qf_lra-benchmark | 18 | ||||
| -rwxr-xr-x | contrib/cluster-qf_lra-full | 18 |
2 files changed, 36 insertions, 0 deletions
diff --git a/contrib/cluster-qf_lra-benchmark b/contrib/cluster-qf_lra-benchmark new file mode 100755 index 000000000..1311d869c --- /dev/null +++ b/contrib/cluster-qf_lra-benchmark @@ -0,0 +1,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 "" + diff --git a/contrib/cluster-qf_lra-full b/contrib/cluster-qf_lra-full new file mode 100755 index 000000000..0fbfbecfe --- /dev/null +++ b/contrib/cluster-qf_lra-full @@ -0,0 +1,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", "27", "$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 "" + |