From c3da87ca126e5cdc4e32a8f8c5710ed218a086d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:15:29 -0700 Subject: [PATCH] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 4f1cff598..36ff74d15 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -2,7 +2,10 @@ -We track notes for updates to smt/parallel.cpp and possibly solver/parallel\_tactic.cpp +We track notes for updates to +[smt/parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/smt/smt_parallel.cpp) +and possibly +[https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactic.cpp](solver/parallel_tactic.cpp). @@ -116,4 +119,4 @@ Threads can work on more than one cube in a batch. ### Synchronization * The first thread to time out or finish could kill other threads instead of joining on all threads to finish. -* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in sat/sat_parallel.cpp. +* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in [sat/sat_parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_parallel.cpp)