mirror of
https://github.com/Z3Prover/z3
synced 2025-09-12 20:51:27 +00:00
52 lines
1.2 KiB
Python
52 lines
1.2 KiB
Python
import os
|
|
import z3
|
|
|
|
MAX_CONFLICTS = 5000
|
|
MAX_EXAMPLES = 5
|
|
bench_dir = "/home/t-ilshapiro/z3-poly-testing/inputs/QF_LIA"
|
|
|
|
params = [
|
|
("smt.arith.eager_eq_axioms", False),
|
|
("smt.restart_factor", 1.2),
|
|
("smt.restart_factor", 1.4),
|
|
("smt.relevancy", 0),
|
|
("smt.phase_caching_off", 200),
|
|
("smt.phase_caching_on", 600),
|
|
]
|
|
|
|
# Iterate through all .smt2 files in the directory
|
|
num_examples = 0
|
|
for benchmark in os.listdir(bench_dir):
|
|
if num_examples > MAX_EXAMPLES:
|
|
break
|
|
if not benchmark.endswith(".smt2"):
|
|
continue
|
|
|
|
filepath = os.path.join(bench_dir, benchmark)
|
|
print(f"Running {filepath}\n")
|
|
|
|
scores = {}
|
|
for n, v in params:
|
|
s = z3.SimpleSolver()
|
|
s.from_file(filepath)
|
|
|
|
s.set("smt.auto_config", False)
|
|
s.set(n, v)
|
|
s.set("smt.max_conflicts", MAX_CONFLICTS)
|
|
|
|
r = s.check()
|
|
st = s.statistics()
|
|
|
|
try:
|
|
conf = st.get_key_value('conflicts')
|
|
except:
|
|
try:
|
|
conf = st.num_conflicts()
|
|
except AttributeError:
|
|
conf = None
|
|
|
|
scores[(n, v)] = conf
|
|
|
|
num_examples += 1
|
|
|
|
print(f"Scores for {benchmark}: {scores}")
|