From 02338930d0e92190c7c27a350a527db2c1b5c040 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 8 Jul 2010 17:25:12 +0000
Subject: [PATCH] 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.

---
 contrib/cluster-qf_lra-benchmark | 18 ++++++++++++++++++
 contrib/cluster-qf_lra-full      | 18 ++++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100755 contrib/cluster-qf_lra-benchmark
 create mode 100755 contrib/cluster-qf_lra-full

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 ""
+
-- 
2.30.2