From ee54513184ba578f4a5289740eeb8dc717a17aab Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Wed, 12 Nov 2025 17:02:11 -0800 Subject: [PATCH] add bash scripts to run param experiments on an QF_RDL example to get datapoints --- param_sweep_deterministic.sh | 94 +++++++++++++++++++++++++++++++++++ param_sweep_random.sh | 96 ++++++++++++++++++++++++++++++++++++ src/smt/smt_parallel.cpp | 7 ++- 3 files changed, 193 insertions(+), 4 deletions(-) create mode 100755 param_sweep_deterministic.sh create mode 100755 param_sweep_random.sh diff --git a/param_sweep_deterministic.sh b/param_sweep_deterministic.sh new file mode 100755 index 000000000..2fe659431 --- /dev/null +++ b/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 diff --git a/param_sweep_random.sh b/param_sweep_random.sh new file mode 100755 index 000000000..3ead8019c --- /dev/null +++ b/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" diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 65ac8385a..389a3b8b1 100644 --- a/src/smt/smt_parallel.cpp +++ b/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(std::stoul(val))); - } - else { - // if non-numeric and non-bool, just store as string/symbol - ctx.m_params.set_str(symbol(key.c_str()), val.c_str()); + } else { + IF_VERBOSE(1, + verbose_stream() << "Ignoring invalid parameter override: " << kv << "\n";); } }