Open
Description
z3 can be slow, very slow when codebase grows. On-disk caching would help a lot during development (only new things would be computed).
I tried to do ad-hoc caching with the following wrapper around z3:
#!/bin/bash -e
# Cache directory
CACHE_DIR="$HOME/.z3cache"
mkdir -p "$CACHE_DIR"
# Check if SMT file is provided
if [ "$#" -ne 1 ]; then
echo "Usage: $0 <smt-file>" >&2
exit 1
fi
SMT_FILE="$1"
# Ensure the file exists
if [ ! -f "$SMT_FILE" ]; then
echo "Error: File '$SMT_FILE' not found!" >&2
exit 1
fi
# Generate a hash of the SMT file for caching
FILE_HASH=$(sha256sum "$SMT_FILE" | awk '{print $1}')
CACHE_FILE="$CACHE_DIR/$FILE_HASH.result"
# Check if result is already cached
if [ -f "$CACHE_FILE" ]; then
echo "[CACHE HIT] Returning cached result." >&2
cat "$CACHE_FILE"
exit 0
fi
cat "$SMT_FILE" >"$CACHE_DIR/$FILE_HASH.smt"
# Run Z3 and cache the result
echo "[CACHE MISS] Running Z3..." >&2
"$0".orig "$SMT_FILE" | tee "$CACHE_FILE"It almost works, but the problem is that the variable identifiers change from run to run (e.g. it's p_x_uint256_9fdce11_00 one run, and p_x_uint256_7721c25_00 another). How to make those identifiers deterministic? From what piece of code do they come from?
In long term a better solution could be made, e.g. with popular joblib.Memory library.