mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

change multithread to multiprocess seems to have resolved current deadlock

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-19 15:34:49 -07:00
parent 629408ba87
commit 2480b5a359
1 changed files with 15 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

35
param-tuning-experiment.py
View file

@ -1,7 +1,7 @@
import os import os
from more_itertools import iterate from more_itertools import iterate
from z3 import * from z3 import *
import threading from multiprocessing import Process
import math, random import math, random
MAX_CONFLICTS = 1000 MAX_CONFLICTS = 1000
@ -208,32 +208,27 @@ def prefix_probe_thread(filepath, manager):
# Main # Main
# -------------------------- # --------------------------
def run_main_solver(filepath):
set_param("parallel.enable", True)
main_solver = solver_from_file(filepath)
apply_param_state(main_solver, BASE_PARAM_CANDIDATES)
print(f"[Main] Started main solver on {os.path.basename(filepath)} with parallel.enable=True")
r = main_solver.check()
print(f"[Main] {os.path.basename(filepath)} → {r}")
def main(): def main():
manager = BatchManager() manager = BatchManager()
for benchmark in os.listdir(bench_dir): for benchmark in os.listdir(bench_dir):
if benchmark != "From_T2__hqr.t2_fixed__term_unfeasibility_1_0.smt2": if benchmark != "From_T2__hqr.t2_fixed__term_unfeasibility_1_0.smt2":
continue continue
filepath = os.path.join(bench_dir, benchmark) filepath = os.path.join(bench_dir, benchmark)
prefix_proc = Process(target=prefix_probe_thread, args=(filepath, manager))
# --- start prefix probing thread --- main_proc = Process(target=run_main_solver, args=(filepath,))
prefix_thread = threading.Thread(target=prefix_probe_thread, args=(filepath, manager)) prefix_proc.start()
prefix_thread.start() main_proc.start()
prefix_proc.join()
# --- start main solver (same formula, in parallel mode, uses cube search tree) --- main_proc.join()
set_param("parallel.enable", True)
main_solver = solver_from_file(filepath)
main_solver.set("smt.auto_config", False)
apply_param_state(main_solver, BASE_PARAM_CANDIDATES)
print(f"[Main] Started main solver on {os.path.basename(filepath)} with parallel.enable=True")
# --- run main solver on full formula (need to enable live param injection in z3 internals) ---
r = main_solver.check()
print(f"[Main] {os.path.basename(filepath)} → {r}")
# --- wait for prefix thread to finish ---
prefix_thread.join()
if manager.best_param_state: if manager.best_param_state:
print(f"\n[GLOBAL] Best parameter state: {manager.best_param_state} with score {manager.best_score}") print(f"\n[GLOBAL] Best parameter state: {manager.best_param_state} with score {manager.best_score}")