From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 21 Jun 2017 15:24:11 +0000 (-0500)
Subject: Update casc and sygus comp scripts.
X-Git-Tag: cvc5-1.0.0~5761
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cdf019f8be3b4affdb582ceb95054b327006521c;p=cvc5.git

Update casc and sygus comp scripts.
---

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