Update casc and sygus comp scripts.

diff --git a/contrib/run-script-casc26-fnt b/contrib/run-script-casc26-fnt
index bc37180a6199460717c8f5c948e3bda95bcde4d7..c3c12f937be53b7dfdf34fcd1ef593c84a881685 100644 (file)
--- 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 77553a5ae2b7341a21675beeb1e8ea43c526fe3e..376d18b153fc549a6cf8ef8d4f7f7f9d59d8d079 100644 (file)
--- 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 9f6749ed67fa1fbdc1453b4303ae40eed395802a..aa65a938f2f9703f2a0579554487424e76197f22 100644 (file)
--- 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 a25a5f5c80bf76a9048c74f54633d92991c582bb..a21792fb9c5b8054c5acdbbac24a3a6c89ffde12 100755 (executable)
--- 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 0a845bd78680419bca6399aad76a26536057c067..849835b282cc81e26056bf60715c94f7545ba8f2 100755 (executable)
--- 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