diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-07-08 17:25:12 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-07-08 17:25:12 +0000 |
| commit | 02338930d0e92190c7c27a350a527db2c1b5c040 (patch) | |
| tree | dd59d108af77c0f0642995fcd140e14ddd736acd /contrib | |
| parent | 8a0dcb9cb4bbf83f03b31343eaa6437ae829f1c9 (diff) | |
I am adding my smt-crunch scripts to source control. Others may find them useful. To use them, log into goedel, sudo su acsys-user, and run ./cluster-script PATH_TO_EXECUTABLE. Be sure to change the email address in the script before using it. Improvements are of course welcome.
Diffstat (limited to 'contrib')
| -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 "" + |