From cdf019f8be3b4affdb582ceb95054b327006521c Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 21 Jun 2017 10:24:11 -0500
Subject: [PATCH] Update casc and sygus comp scripts.

---
 contrib/run-script-casc26-fnt                |  2 +-
 contrib/run-script-casc26-fof                |  5 ++--
 contrib/run-script-casc26-tfa                | 12 ++++-----
 contrib/run-script-sygusComp2017-INV         | 27 ++++++++++++++++----
 contrib/run-script-sygusComp2017-PBE_Strings |  2 +-
 5 files changed, 31 insertions(+), 17 deletions(-)

diff --git a/contrib/run-script-casc26-fnt b/contrib/run-script-casc26-fnt
index bc37180a6..c3c12f937 100644
--- a/contrib/run-script-casc26-fnt
+++ b/contrib/run-script-casc26-fnt
@@ -7,7 +7,7 @@ bench="$1"
 file=${bench##*/}
 filename=${file%.*}
 
-echo "------- cvc4-fnt casc j8 : $bench at $2..."
+echo "------- cvc4-fnt casc 26 : $bench at $2..."
 
 # use: trywith [params..]
 # to attempt a run.  If an SZS ontology result is printed, then
diff --git a/contrib/run-script-casc26-fof b/contrib/run-script-casc26-fof
index 77553a5ae..376d18b15 100644
--- a/contrib/run-script-casc26-fof
+++ b/contrib/run-script-casc26-fof
@@ -9,7 +9,7 @@ bench="$1"
 file=${bench##*/}
 filename=${file%.*}
 
-echo "------- cvc4-fof casc j8 : $bench at $2..."
+echo "------- cvc4-fof casc 26 : $bench at $2..."
 
 # use: trywith [params..]
 # to attempt a run.  If an SZS ontology result is printed, then
@@ -39,12 +39,11 @@ trywith 5 --multi-trigger-when-single --full-saturate-quant
 trywith 5 --trigger-sel=max --full-saturate-quant
 trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant  
 trywith 10 --multi-trigger-cache --full-saturate-quant
-trywith 5 --no-multi-trigger-linear --full-saturate-quant
-trywith 15 --finite-model-find --no-quant-cf --sort-inference --uf-ss-fair
 trywith 15 --prenex-quant=none --full-saturate-quant
 trywith 15 --fs-inst --decision=internal --full-saturate-quant
 trywith 15 --relevant-triggers --full-saturate-quant 
 trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --full-saturate-quant --macros-quant
 trywith 30 --fs-inst --full-saturate-quant
 trywith 30 --no-quant-cf --full-saturate-quant 
 finishwith --qcf-vo-exp --full-saturate-quant 
diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa
index 9f6749ed6..aa65a938f 100644
--- a/contrib/run-script-casc26-tfa
+++ b/contrib/run-script-casc26-tfa
@@ -7,7 +7,7 @@ bench="$1"
 file=${bench##*/}
 filename=${file%.*}
 
-echo "------- cvc4-tfa casc j8 : $bench at $2..."
+echo "------- cvc4-tfa casc 26 : $bench at $2..."
 
 # use: trywith [params..]
 # to attempt a run.  If an SZS ontology result is printed, then
@@ -31,11 +31,9 @@ function finishwith {
 
 trywith 10 --decision=internal --full-saturate-quant
 trywith 10 --finite-model-find --decision=internal
-trywith 10 --nl-ext --nl-ext-tplanes --decision=internal --full-saturate-quant
-trywith 10 --purify-quant --full-saturate-quant
+trywith 10 --nl-ext --nl-ext-tplanes --full-saturate-quant
 trywith 10 --partial-triggers --full-saturate-quant
-trywith 10 --no-e-matching --full-saturate-quant
-trywith 30 --cbqi-all --purify-triggers --full-saturate-quant 
-trywith 30 --nl-ext --fs-inst --full-saturate-quant
-finishwith --nl-ext --nl-ext-tplanes --full-saturate-quant
+trywith 15 --cbqi-all --purify-triggers --full-saturate-quant 
+trywith 15 --nl-ext --fs-inst --full-saturate-quant
+finishwith --full-saturate-quant --macros-quant
 # echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-sygusComp2017-INV b/contrib/run-script-sygusComp2017-INV
index a25a5f5c8..a21792fb9 100755
--- a/contrib/run-script-sygusComp2017-INV
+++ b/contrib/run-script-sygusComp2017-INV
@@ -3,14 +3,31 @@
 cvc4=./cvc4
 bench="$1"
 
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench
+}
+
 function trywith {
-  ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |
+    (read result w1;
+    case "$result" in
+    unsat) echo "$w1";cat;exit 0;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi  
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench 2>/dev/null |
   (read result w1;
   case "$result" in
   unsat) echo "$w1";cat;exit 0;;
-  esac; exit 1)
-  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  esac)
 }
 
-trywith --sygus-inv-templ=post
- 
+trywith 60 --sygus-inv-templ=pre
+finishwith --sygus-inv-templ=post
diff --git a/contrib/run-script-sygusComp2017-PBE_Strings b/contrib/run-script-sygusComp2017-PBE_Strings
index 0a845bd78..849835b28 100755
--- a/contrib/run-script-sygusComp2017-PBE_Strings
+++ b/contrib/run-script-sygusComp2017-PBE_Strings
@@ -12,5 +12,5 @@ function trywith {
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
 
-trywith --cegqi-si=none --strings-exp
+trywith --cegqi-si=none --sygus-fair=direct
  
-- 
2.30.2