add bash scripts to run param experiments on an QF_RDL example to get datapoints

param_sweep_deterministic.sh

@@ -0,0 +1,94 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# --- Inputs ---
+FILE=$(realpath "$1")
+Z3=$(realpath "$2")
+N="${3:-99999999}"   # optional limit on number of tests
+
+TIMEOUT=100
+OUT="../sweep_results.csv"
+
+echo "id,params,result,time_s" > "$OUT"
+
+# --- Tunable parameters ---
+BOOL_PARAMS=(
+  "smt.arith.nl.branching"
+  "smt.arith.nl.cross_nested"
+  "smt.arith.nl.expensive_patching"
+  "smt.arith.nl.gb"
+  "smt.arith.nl.horner"
+  "smt.arith.nl.optimize_bounds"
+  "smt.arith.nl.propagate_linear_monomials"
+  "smt.arith.nl.tangents"
+)
+
+INT_PARAM1_KEY="smt.arith.nl.delay"
+INT_PARAM1_LO=5
+INT_PARAM1_HI=10
+
+INT_PARAM2_KEY="smt.arith.nl.horner_frequency"
+INT_PARAM2_LO=2
+INT_PARAM2_HI=6
+
+id=1
+
+# --- Deterministic nested loops over all parameter values ---
+for b0 in 0 1; do
+for b1 in 0 1; do
+for b2 in 0 1; do
+for b3 in 0 1; do
+for b4 in 0 1; do
+for b5 in 0 1; do
+for b6 in 0 1; do
+for b7 in 0 1; do
+
+  for d in $(seq "$INT_PARAM1_LO" "$INT_PARAM1_HI"); do
+  for hf in $(seq "$INT_PARAM2_LO" "$INT_PARAM2_HI"); do
+
+    # stop early if N reached
+    if (( id > N )); then
+        echo "✓ Done early at $((id-1)) combinations. Results in $OUT"
+        exit 0
+    fi
+
+    BOOLS=($b0 $b1 $b2 $b3 $b4 $b5 $b6 $b7)
+
+    PARAMS=()
+    for idx in "${!BOOL_PARAMS[@]}"; do
+        PARAMS+=("${BOOL_PARAMS[$idx]}=${BOOLS[$idx]}")
+    done
+    PARAMS+=("$INT_PARAM1_KEY=$d")
+    PARAMS+=("$INT_PARAM2_KEY=$hf")
+
+    PARAM_STR=$(IFS=, ; echo "${PARAMS[*]}")
+
+    printf "[%05d] %s\n" "$id" "$PARAM_STR"
+
+    # ----- Run Z3 -----
+    START=$(date +%s%N)
+    if timeout "$TIMEOUT" "$Z3" \
+        -v:1 -st \
+        "$FILE" \
+        smt.threads=2 \
+        tactic.default_tactic=smt \
+        smt_parallel.param_tuning=false \
+        smt_parallel.tunable_params="$PARAM_STR" \
+        >/tmp/z3_out.txt 2>&1
+    then
+        RESULT=$(grep -E "sat|unsat|unknown" /tmp/z3_out.txt | tail -1)
+        [[ -z "$RESULT" ]] && RESULT="unknown"
+    else
+        RESULT="timeout"
+    fi
+    END=$(date +%s%N)
+    TIME=$(awk "BEGIN{print ($END-$START)/1e9}")
+
+    echo "$id,\"$PARAM_STR\",$RESULT,$TIME" >> "$OUT"
+
+    ((id++))
+
+  done # hf
+  done # d
+
+done; done; done; done; done; done; done; done

param_sweep_random.sh

@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# --- Inputs ---
+FILE=$(realpath "$1")
+Z3=$(realpath "$2")
+N="${3:-2}"
+
+TIMEOUT=100
+OUT="../sweep_results.csv"
+
+echo "id,params,result,time_s" > "$OUT"
+
+# --- Tunable parameters ---
+BOOL_PARAMS=(
+  "smt.arith.nl.branching"
+  "smt.arith.nl.cross_nested"
+  "smt.arith.nl.expensive_patching"
+  "smt.arith.nl.gb"
+  "smt.arith.nl.horner"
+  "smt.arith.nl.optimize_bounds"
+  "smt.arith.nl.propagate_linear_monomials"
+  "smt.arith.nl.tangents"
+)
+
+INT_PARAMS=(
+  "smt.arith.nl.delay:5:10"
+  "smt.arith.nl.horner_frequency:2:6"
+)
+
+# --- Helpers ---
+random_bool() { echo $((RANDOM % 2)); }
+
+random_int() {
+  local lo=$1
+  local hi=$2
+  echo $((lo + RANDOM % (hi - lo + 1)))
+}
+
+# --- Track used parameter combinations ---
+declare -A SEEN
+
+i=1
+while (( i <= N )); do
+
+    # ----- generate a unique parameter string -----
+    while true; do
+        PARAMS=()
+
+        for p in "${BOOL_PARAMS[@]}"; do
+            PARAMS+=("$p=$(random_bool)")
+        done
+
+        for spec in "${INT_PARAMS[@]}"; do
+            IFS=':' read -r key lo hi <<<"$spec"
+            PARAMS+=("$key=$(random_int "$lo" "$hi")")
+        done
+
+        PARAM_STR=$(IFS=, ; echo "${PARAMS[*]}")
+
+        # Check uniqueness
+        if [[ -z "${SEEN[$PARAM_STR]+x}" ]]; then
+            SEEN["$PARAM_STR"]=1
+            break
+        fi
+    done
+
+    printf "[%03d/%03d] %s\n" "$i" "$N" "$PARAM_STR"
+
+    # ----- run Z3 -----
+    START=$(date +%s%N)
+
+    if timeout "$TIMEOUT" "$Z3" \
+        -v:1 -st \
+        "$FILE" \
+        smt.threads=2 \
+        tactic.default_tactic=smt \
+        smt_parallel.param_tuning=false \
+        smt_parallel.tunable_params="$PARAM_STR" \
+        >/tmp/z3_out.txt 2>&1
+    then
+        RESULT=$(grep -E "sat|unsat|unknown" /tmp/z3_out.txt | tail -1)
+        [[ -z "$RESULT" ]] && RESULT="unknown"
+    else
+        RESULT="timeout"
+    fi
+
+    END=$(date +%s%N)
+    TIME=$(awk "BEGIN{print ($END-$START)/1e9}")
+
+    echo "$i,\"$PARAM_STR\",$RESULT,$TIME" >> "$OUT"
+
+    ((i++))
+done
+
+echo "✓ Done. Results written to $OUT"

src/smt/smt_parallel.cpp

@@ -744,10 +744,9 @@ namespace smt {
                 else if (std::all_of(val.begin(), val.end(), ::isdigit)) {
                     ctx.m_params.set_uint(symbol(key.c_str()),
                         static_cast<unsigned>(std::stoul(val)));
-                }
+                } else {
-                else {
+                  IF_VERBOSE(1, 
-                    // if non-numeric and non-bool, just store as string/symbol
+                    verbose_stream() << "Ignoring invalid parameter override: " << kv << "\n";);
-                    ctx.m_params.set_str(symbol(key.c_str()), val.c_str());
                 }
             }