From 9d73c45c858c9411172b1970fb92a0fd84f34f38 Mon Sep 17 00:00:00 2001 From: Dmitry Messerman Date: Wed, 13 May 2026 11:00:39 +0300 Subject: [PATCH 1/8] Enhanced z3 version check - now checking version used by smlp --- .../Dockerfile.smlp-test-build-ubuntu_24.04-python311 | 8 +++----- scripts/venv/Dockerfile.readme_venv | 6 ++---- 2 files changed, 5 insertions(+), 9 deletions(-) diff --git a/scripts/docker/Dockerfile.smlp-test-build-ubuntu_24.04-python311 b/scripts/docker/Dockerfile.smlp-test-build-ubuntu_24.04-python311 index 2871df27..18087e39 100644 --- a/scripts/docker/Dockerfile.smlp-test-build-ubuntu_24.04-python311 +++ b/scripts/docker/Dockerfile.smlp-test-build-ubuntu_24.04-python311 @@ -78,12 +78,10 @@ RUN ./validate.sh # 7. ─── Validate Z3 version ────────────────────────────────────────────────────────────── ENV PATH=/home/${USERNAME}/.venv/bin:${PATH} RUN printf '#!/usr/bin/env python3.11\n' > z3_version.py \ - && printf 'from glob import glob\n' >> z3_version.py \ && printf 'from ctypes import cdll, c_char_p\n' >> z3_version.py \ - && printf 'from os.path import dirname\n' >> z3_version.py \ - && printf 'import smlp\n' >> z3_version.py \ - && printf 'libz3=cdll.LoadLibrary(glob(dirname(dirname(smlp.__file__)) + "/smlptech.libs/" + "libz3*so")[0])\n' >> z3_version.py \ - && printf 'z3_version=libz3.Z3_get_full_version\n' >> z3_version.py \ + && printf 'from smlp import core\n' >> z3_version.py \ + && printf 'libsmlp=cdll.LoadLibrary(core.libsmlp.__file__)\n' >> z3_version.py \ + && printf 'z3_version=libsmlp.Z3_get_full_version\n' >> z3_version.py \ && printf 'z3_version.restype=c_char_p\n' >> z3_version.py \ && printf 'print(z3_version().decode())\n' >> z3_version.py \ && chmod +x z3_version.py && ./z3_version.py diff --git a/scripts/venv/Dockerfile.readme_venv b/scripts/venv/Dockerfile.readme_venv index 4fb6ecbb..4c6b9c5c 100644 --- a/scripts/venv/Dockerfile.readme_venv +++ b/scripts/venv/Dockerfile.readme_venv @@ -17,12 +17,10 @@ COPY README_venv.sourceme . RUN bash -c 'source README_venv.sourceme' ENV PATH=/home/${USERNAME}/.venv/bin:${PATH} RUN printf '#!/usr/bin/env python3.11\n' > z3_version.py \ - && printf 'from glob import glob\n' >> z3_version.py \ && printf 'from ctypes import cdll, c_char_p\n' >> z3_version.py \ - && printf 'from os.path import dirname\n' >> z3_version.py \ && printf 'from smlp import core\n' >> z3_version.py \ - && printf 'libz3=cdll.LoadLibrary(glob(dirname(dirname(dirname(core.__file__))) + "/smlptech.libs/" + "libz3*so")[0])\n' >> z3_version.py \ - && printf 'z3_version=libz3.Z3_get_full_version\n' >> z3_version.py \ + && printf 'libsmlp=cdll.LoadLibrary(core.libsmlp.__file__)\n' >> z3_version.py \ + && printf 'z3_version=libsmlp.Z3_get_full_version\n' >> z3_version.py \ && printf 'z3_version.restype=c_char_p\n' >> z3_version.py \ && printf 'print(z3_version().decode())\n' >> z3_version.py \ && chmod +x z3_version.py From 4e5c5db6e3e2fbc54f465f7082276b67b3fd9532 Mon Sep 17 00:00:00 2001 From: Dmitry Messerman Date: Sat, 16 May 2026 15:31:16 +0300 Subject: [PATCH 2/8] Merge with master Fixed z3 version printing in Dockerfile.readme_system --- .gitattributes | 3 + README.md | 144 ++++++++++++++++++-------- misc/quickstart.zip | Bin 0 -> 3654 bytes quickstart/constraint_dora.json | 2 +- quickstart/quickstart.sh | 3 + quickstart/results/.gitignore | 3 + scripts/venv/Dockerfile.readme_system | 6 +- 7 files changed, 111 insertions(+), 50 deletions(-) create mode 100644 .gitattributes create mode 100644 misc/quickstart.zip create mode 100644 quickstart/results/.gitignore diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 00000000..da468e91 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,3 @@ +*.zip binary +*.whl binary + diff --git a/README.md b/README.md index 47f4f1e0..559086f9 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ SMLP uses symbolic reasoning for ML model exploration and optimisation under ver SMLP Overview -### Industry adoption: used at Intel in production for optimization of package/board layouts and signal integrity +**Industry adoption:** SMLP is used at **Intel** for optimization of package/board layouts and signal integrity
SMLP applications in Intel and why stability is important
@@ -25,7 +25,7 @@ can be dependent on the intended value itself.

-**[Combination of robustness and formal assurance of results validity](https://korovin.gitlab.io/pub/fmcad_bkk_2020.pdf) is a distinctive strength of SMLP, not found in other optimization or model‑analysis tools.** +**[Combination of robustness and formal assurance of results validity](https://korovin.gitlab.io/pub/fmcad_bkk_2020.pdf)** is a distinctive strength of SMLP, not found in other optimization or model‑analysis tools. SMLP exploration modes: @@ -349,35 +349,52 @@ tests/install/test_container_install mdmitry1/python311-dev ## Quickstart -### Problem: find minimal distance between point (2,1) and unit circle
+### Problem: find minimal distance between point (2,1) and unit circle

Minimal Distance Problem

- Analytical solution for this problem:
+ Analytical solution for this problem is:
` f(x*) = 6 - 2√5 ≈ 1.527864`, where `x* = (2/√5,1/√5) ≈ (0.894427, 0.447214)` -

- Solution: see `bash` script [quickstart.sh](https://raw.githubusercontent.com/SMLP-Systems/smlp/master/quickstart/quickstart.sh)

- The script has 2 steps
- - Step 1: Create input dataset and visualize the problem
- - Step 2: Run SMLP
- SMLP creates polynomial model and finds approximate solution
- SMLP results - `f(x*) = 1.527865, x* = (0.894531, 0.447004)`
- are within 0.05% accuracy for `f(x*)` and `x*` - -Running the script: -```bash -smlp_package_path=$(python3.11 -c 'import smlp; from os.path import dirname; print(dirname(smlp.__file__))') -$smlp_package_path/quickstart/quickstart.sh +
+ +Let's solve this problem using SMLP. + +Download and unzip [quickstart.zip](https://raw.githubusercontent.com/SMLP-Systems/smlp/master/misc/quickstart.zip) +(or if you cloned smlp cd to quickstart) + +Let's treat this problem as black-box function optimization. + +
+ + Step 1: Generate samples of the distance function from the point (2,1) (for simplicity we use square of the distance as this does not change the optimum point): + + +Run: + ``` -
+./constraint_dora_dataset.py +``` + +This should generate `Constraint_dora.csv.gz`, inside `Constraint_dora.csv` we have: + +``` +X1,X2,Y1 +-1.5,-1.5,18.5 +-1.495995995995996,-1.5,18.471988004020037 +-1.491991991991992,-1.5,18.4440080721362 +-1.487987987987988,-1.5,18.41606020434849 +...... +``` +
- Test case description
- **1.** *constraint_dora.json* - spec in json format
+ +Step 2: Create specification file (or use provided `constraint_dora.json`) where we specify types and ranges of variables and that the solution should be constrained to the unit circle: + + ``` { @@ -387,11 +404,12 @@ $smlp_package_path/quickstart/quickstart.sh {"label":"X2", "interface":"knob", "type":"real", "range":[-1.5,2.0], "rad-abs": 0.0}, {"label":"Y1", "interface":"output", "type":"real"} ], - "alpha": "X1*X1+X2*X2<=1", - "objectives": {"objective1": "-Y1"} + "beta": "X1*X1+X2*X2<=1", + "objectives": { + "objective1": "-Y1" + } } ``` - Legend:
``` @@ -400,44 +418,73 @@ $smlp_package_path/quickstart/quickstart.sh Y1 - output function rad-abs - sensitivity radius. Zero radius means that solution sensitivity check is skipped - alpha - constraint depending on controllable variables + beta - constraint depending on controllable variables objective1 - optimization goal ``` -
+Note SMLP by default maximizes the objective function so we use `-Y1` as the objective function. - **2.** SMLP command line arguments
+
+ +
+ +Step 3: Run SMLP on data file and specification file: + + + +``` +smlp -data ./Constraint_dora.csv.gz -spec ./constraint_dora.json -pref Constraint_dora -out_dir results -mode optimize -model poly_sklearn -epsilon 0.0000005 +``` + +SMLP command line arguments:
``` - -data ${name}.csv.gz # input CSV dataset - -spec ${script_path}/${name_lc}.json # JSON spec file - -pref ${name} # output file prefix + -data ./Constraint_dora.csv.gz # input CSV dataset + -spec ./constraint_dora.json.json # JSON spec file + -pref Constraint_dora # output file prefix + -out_dir results # output directory -mode optimize # operation mode -model poly_sklearn # model type -epsilon 0.0000005 # convergence threshold ``` + +3 graphs will pop-up which show quality of the generated model on train/test/train+test datasets, (these need to be closed to proceed).
+The generated results can be found in `results/` folder.
+ +`results/Constraint_dora_Constraint_dora_optimization_results.csv` contains the generated solution: + +``` +X1 = 0.89453125 +X2 = 0.4470043182373047 +Y1 = 1.5278653812777188 +``` + +Solution found by SMLP corresponds to the analytical solution (`constraint_dora_poly_optimization_results_expected.txt`) with the specified precision: + +``` +X1 = 0.89453125 +X2 = 0.4470043182373047 +Y1 = 1.5278653812779421 +```
-### Problem modification in the user area +Steps 1 - 3 are wrapped in a script: `./quickstart.sh` + +
+ Step 4: As an example, let's modify the problem in order to get solution in rational numbers. +
+ Let's change circle radius to 2/√5, so squared radius will be 4/5.
+ In order to do this, edit specification file `constraint_dora.json` and change the right side of the inequality in the constraint to be 4/5: + + `"beta": "X1*X1+X2*X2<=4/5,"` + + Run the script from current directory -- Step 1: Copy the problem to the current directory and enter problem work area
-```bash -smlp_package_path=$(python3.11 -c 'import smlp; from os.path import dirname; print(dirname(smlp.__file__))') -\cp -rp $smlp_package_path/quickstart . -cd quickstart -``` -- Step 2: As an example, change constraint in order to get solution in rational numbers
- Let's change circle radius to 2/√5, so squared radius will be 4/5
- In order to do this, edit `constraint_dora.json` file and change right side of the inequality to be 4/5:
- `"alpha": "X1*X1+X2*X2<=4/5",`

- [Analytical solution](https://www.wolframalpha.com/input?i=Minimize%3A+f%28x1%2C+x2%29+%3D+%28x1+-+2%29%5E2+%2B+%28x2+-+1%29%5E2+subject+to+x1%5E2+%2B+x2%5E2+-+4%2F5+%3C%3D+0) for modified problem:
- ` -f(x*) = 9/5 = 1.8`, where `x* = (4/5,2/5) = (0.8, 0.4)`

-- Step 3: Run the script from current directory ```bash ./quickstart.sh ``` + Expected SMLP results are within 0.03% accuracy for `f(x*)` and `x*`: ```bash Working directory: /quickstart/Constraint_dora_results_ @@ -446,6 +493,13 @@ X2 = 0.3999021053314209 Y1 = 1.8000002980730385 ``` + [Analytical solution](https://www.wolframalpha.com/input?i=Minimize%3A+f%28x1%2C+x2%29+%3D+%28x1+-+2%29%5E2+%2B+%28x2+-+1%29%5E2+subject+to+x1%5E2+%2B+x2%5E2+-+4%2F5+%3C%3D+0) for this modified problem:
+ + `f(x*) = 9/5 = 1.8`, where `x* = (4/5,2/5) = (0.8, 0.4)` + +
+ + ## [Tutorial](https://github.com/SMLP-Systems/smlp/tree/master/tutorial) - Black-box optimization Eggholder Function diff --git a/misc/quickstart.zip b/misc/quickstart.zip new file mode 100644 index 0000000000000000000000000000000000000000..98b52d228422da22feae70835441479dfa743260 GIT binary patch literal 3654 zcma){OQNAS8)K<}g`in88R>wn@b+OGI&EBt{fv zNhFjtV;3S>ax(U)coFZYa~(&gy58rxe)BwkJlFTWf8XDIU-xHhtk~E=fUPUE>ZZ%r zm%n~^0DA!bf!H(N1R^?sxZlB^8^C6nG>5ffu0RqGfQ5a91pr`&GC#Lriflc(0GEqy zy7(2OcI&eO03PfBfXGgfZ9Qdz*H^`M@*K8*T(UL0mw~qF-B+50rc4=;suNyw}==Wf|OFL|^n2@CPs9|6r(nif*=^(xw z)0!3S!RY~Y6uB)vSAGKOmQsgs-4~BdcsU{$3PUl_qjHtKEg>%{iy<^6PijOjXpCD% z971q<@SqlFtD4#U*4#oW;U3q+*Z?Ie!CJfQ(hEnvXY7|u{W>+eD%bU0-n3f!c;+W8 zay4W~Qs>GAVu$&UmU>>y&5V0|cxB-gYM?0~B3kXzD*UkkfdlR2qha>8lq_(T?Oko1 zccok16|-Cx8GGBh5MG+r87zDt_Uf2=MD_!`?~{-@_BISZN9Uu4TESW*iAVSz<_!4t z#Hw_^-R6`JHD>Hak}B+XvZE!jiIdthvoCeX?x{?}2-|&2FN*hLXuAjpYr_=hl}~w- zwy5k0gT96s=Yxd(C1RgYU)qA7INDE-#I&ggma6NNi{CgEw9krFFMSy`$IXQigOmrq zZCE|`Sk0;C;+oao3`eQer8j;1JJ3j}Vu;4>YkI&&HI_FkMnYkHD(-#b-lwF&r^eua zn9V=A6t)tX+`$<8!>h7zs`%;Kd3u=Xc+{Py5Z(E-*-k5aje=+OR=4bTO}`&m5_<3(Ddy4kzP>)f_t&pPI% zd@FoZgc0(KmNpOltHzga3-W?~3mq$pz8t@hgnnd)^mxXyvm6O^@4!0D;xu9|^U?Mi}P~}zz_m`hy*tb36D8L#CRwZNyNYF zcB^*3t6Pbd+FfBPV78izxs&V;GuqnZqQe6h`Pti(=1vc*IpQ25GGDjpuo%MJ{MM5A zv6!+amWcKA!v$czZf@<;92OS+ugxJqQrjPbKs#-geqpQd5(oga@&Ev`JEMGWvj>`p zCSZul_>jM??EJTtWJh|ypeA4S61;4Ybi`R*wkv4Nt0l-zi$Ro2`+aQVv8@EJSvXW6 z{xp}3;pca+<@#WubAs<~o`gw4M&%i-PQghD?(_GImG0F>39&i1X1UPP z6ynw;i_Sg$BTx=RL)3wEDYq@_1A@$}4xKMnOJJ9`P9@R>Ne=LWnlox+WN90Ip;WjKgo373KC)BzhLW0uDs#PzDo+o+6))}hjkDB8o z$2tIY*XBD7@k{UDhMh)ihXzN2A(6X9%bNJOYn27aaG_(Rwmfv<_!4Z^Av|>- zdSvf#DLA5?U(aOX!@{3*LwV==h6+fEYy+^H0Z;Y{%`Uf4A|`#9%X8>c8LlF;nQnd@ z{@_pQ^X?tg)iJ0R=V-j8NF$^Qx=!17UM;yto-TG;iTN{XlFg9+zhOd{!fK4|t>m@C%WI4aq$l9d&mV0Z7=p}y zTE132FK)M4^niO!9%3SM-t)4QKxB%-E$dli=V2BlaL%Ocm`zVwil#aco0HsRe7`7S z(as)pB$+PmZu@>BUzX51mnhQ{nci~3v6vQZn*=+(8e((6r7Hh=^r*G?Tq5*XmqnpM zTEmre@4M1c`L!O$3w-#gcYuT;_YA>Y4c%xAQ%8^b8s*onqcB&uduA2ZoK~`L?}cTw+$DX~O5UKlU)9y`8I}Hc0kWZR&M){NEI6zr zn9LtLFtJiU;XS`9J(JS@3Q6ap<&9AMy1Yhm28x3`MQNc6$Rv%?=~up9@RtWAt<(i0 zXV17!_gir`3*3_lUy(O1Li@H>GCM5^AADB+dqjP8}e zNKY7EH`nEmlxxDfJFzo5rkiTm>_boR*;yBJD^4sC4rC2sDN~3V$?nPb`3(^k2|iGR zdRVoszXUk-vKTVQ8I63VuY;FUc$lG@hazRhD0vB1gg3snaEgl??bkUm%Kd8cGxym7 zeMU)@YxJj@`@EfIgWw9F9bfm{%FzJ6ZmAYB2T)KdaP1#HC~_@ zuY4x5Nk#K>ZtaUa->0Ijqz6k9Y9EPa_42x!IyBd@$?joZ&HT+p9ntCHtH;Z_WE?&` zxNTF3nuvkxa*@`z60A6mHK8jZ(+)=~FPvP5q*cTDVPM;nCw4-jr9Y z^*?oBaSIwS3if{g!W`n05+t|LPGQ7JWN<#vGv2qUK%T7)EHcGwiPm8c#n7Ic3k+x& zyhh|XX&w^~W8hHrB^HDpiA33?IFuVYx(G*!m>5J2q%(rDNrM9W(O+^|;iyBgy%1c((@&d1(<-!il@IF~_ow8=ruvf@CdkSfn-PbbNqn_^9a>{KtLbwswjNRisd(OY0(QD7L81Pow*)Ny+wMZYug zaqllDh4NVf&hPIT@q=-j5nl{?E(tYXK2NDq)exX4W_^KJHD%J2$^;@+!v)rt^CdtG zn@JL+im*2r$rs^Jabl3)nfm85G~63_01lZ`Q91Bz%M7s8>_FCFF3Ee!p2VB){1Y5 zQ3vJ9=5n@Kw#CV>4mY+`idDHT8J)bps&eywzLQ9Zg2@L~8!Hx87~9WyTZC!K*2M>y zHQst|(=v0~1HaMtcf9dU@MrA(O^|6bU^d)*r{K2sR}yEc|G?hw)pw%Qw)&m$9wzT^ zOYZ-E;{U&3^{X^~Mo0g2?K0brG`3lZDZIr>KXmVBr1a1I_5N6R8;8Cg&=xoSFvRu& z?Zl+*5VPTW%)d*&u<)PI^edaTL+$Ld?NE2ZG0ZLhJk(!Z_p=~Cj;-3{WZremL-%9i H9suw^Z`{CL literal 0 HcmV?d00001 diff --git a/quickstart/constraint_dora.json b/quickstart/constraint_dora.json index 3b6f1472..43f1c707 100644 --- a/quickstart/constraint_dora.json +++ b/quickstart/constraint_dora.json @@ -5,7 +5,7 @@ {"label":"X2", "interface":"knob", "type":"real", "range":[-1.5,2.0], "rad-abs": 0.0}, {"label":"Y1", "interface":"output", "type":"real"} ], - "alpha": "X1*X1+X2*X2<=1", + "beta": "X1*X1+X2*X2<=1", "objectives": { "objective1": "-Y1" } diff --git a/quickstart/quickstart.sh b/quickstart/quickstart.sh index 44778722..b6f4e2ec 100755 --- a/quickstart/quickstart.sh +++ b/quickstart/quickstart.sh @@ -1,4 +1,7 @@ #!/usr/bin/env bash + +set -x + script_path="$(dirname "$(realpath "$0")")" name=Constraint_dora if [[ $# -gt 0 ]]; then diff --git a/quickstart/results/.gitignore b/quickstart/results/.gitignore new file mode 100644 index 00000000..a5baada1 --- /dev/null +++ b/quickstart/results/.gitignore @@ -0,0 +1,3 @@ +* +!.gitignore + diff --git a/scripts/venv/Dockerfile.readme_system b/scripts/venv/Dockerfile.readme_system index 1425b9c7..639a1727 100644 --- a/scripts/venv/Dockerfile.readme_system +++ b/scripts/venv/Dockerfile.readme_system @@ -16,12 +16,10 @@ WORKDIR /home/${USERNAME} COPY README_system.sourceme . RUN bash -c 'source README_system.sourceme' RUN printf '#!/usr/bin/env python3.11\n' > z3_version.py \ - && printf 'from glob import glob\n' >> z3_version.py \ && printf 'from ctypes import cdll, c_char_p\n' >> z3_version.py \ - && printf 'from os.path import dirname\n' >> z3_version.py \ && printf 'from smlp import core\n' >> z3_version.py \ - && printf 'libz3=cdll.LoadLibrary(glob(dirname(dirname(dirname(core.__file__))) + "/smlptech.libs/" + "libz3*so")[0])\n' >> z3_version.py \ - && printf 'z3_version=libz3.Z3_get_full_version\n' >> z3_version.py \ + && printf 'libsmlp=cdll.LoadLibrary(core.libsmlp.__file__)\n' >> z3_version.py \ + && printf 'z3_version=libsmlp.Z3_get_full_version\n' >> z3_version.py \ && printf 'z3_version.restype=c_char_p\n' >> z3_version.py \ && printf 'print(z3_version().decode())\n' >> z3_version.py \ && chmod +x z3_version.py From 29a4bbbd7ce5e578ef8f3eabdaadbfaaeedcb573 Mon Sep 17 00:00:00 2001 From: Dmitry Messerman Date: Sat, 16 May 2026 21:21:13 +0300 Subject: [PATCH 3/8] Merge with master [2] --- tutorial/examples/si/smlp/plot_results.py | 80 +++++++++++++++++++---- 1 file changed, 69 insertions(+), 11 deletions(-) diff --git a/tutorial/examples/si/smlp/plot_results.py b/tutorial/examples/si/smlp/plot_results.py index 1dc80713..a73d804b 100755 --- a/tutorial/examples/si/smlp/plot_results.py +++ b/tutorial/examples/si/smlp/plot_results.py @@ -1,11 +1,41 @@ -#!/usr/bin/env python3.11 +#!/usr/bin/env python3 +import os +import platform +import shutil +import subprocess +import tempfile + +cache_root = os.path.join(tempfile.gettempdir(), "smlp-cache") +os.environ.setdefault("XDG_CACHE_HOME", cache_root) +os.environ.setdefault("MPLCONFIGDIR", os.path.join(cache_root, "matplotlib")) + +import matplotlib + +IS_MACOS = platform.system() == "Darwin" + +try: + import tkinter as tk + from matplotlib.backends.backend_tkagg import FigureCanvasTkAgg + HAS_TK = True + TK_IMPORT_ERROR = None +except ImportError as exc: + tk = None + FigureCanvasTkAgg = None + HAS_TK = False + TK_IMPORT_ERROR = exc + +# Configure the backend before importing pyplot or seaborn. Use TkAgg when Tk +# is present because this script embeds the figure in a Tk window; otherwise +# fall back to Agg so pyenv/macOS Python builds without _tkinter can still save +# and open the PNG. +if HAS_TK: + matplotlib.use("TkAgg") +else: + matplotlib.use("Agg") + import pandas as pd import seaborn as sns -import matplotlib import matplotlib.pyplot as plt -import matplotlib.patches as mpatches -from matplotlib.backends.backend_tkagg import FigureCanvasTkAgg -import tkinter as tk import numpy as np import re from math import inf @@ -153,7 +183,8 @@ bbox=dict(boxstyle="round,pad=0.5", facecolor="#dce3ec", edgecolor="#aab4c2", alpha=0.9) ) plt.tight_layout(rect=[0, 0.08, 1, 1]) -plt.savefig(f"{plot_name}.png", dpi=150, bbox_inches="tight") +png_path = Path(f"{plot_name}.png").resolve() +plt.savefig(png_path, dpi=150, bbox_inches="tight") # ── Scrollable Tk window ────────────────────────────────────────────────────── timeout = inf @@ -161,11 +192,26 @@ if '-timeout' == argv[2]: timeout = int(argv[3]) +if not HAS_TK: + print(f"Saved plot to {png_path}") + if IS_MACOS and shutil.which("open") and timeout == inf: + subprocess.Popen(["open", str(png_path)]) + elif IS_MACOS and timeout != inf: + print("Skipping macOS Preview auto-open because -timeout was requested.") + else: + print(f"Tk viewer unavailable: {TK_IMPORT_ERROR}") + exit(0) + root = tk.Tk() root.title(f"{plot_name} — Optimization Results") -# Get screen dimensions and set window to full screen height -root.geometry("1280x1024") +# Size the window within the available screen. This avoids oversized windows +# on smaller MacBook displays while preserving the original Linux dimensions. +screen_w = root.winfo_screenwidth() +screen_h = root.winfo_screenheight() +window_w = min(1280, screen_w) +window_h = min(1024, screen_h) +root.geometry(f"{window_w}x{window_h}") # Outer frame holds canvas + scrollbars outer = tk.Frame(root) @@ -194,11 +240,20 @@ mpl_canvas.draw() -# Mouse-wheel horizontal scroll (Shift+wheel or middle-drag) +# Mouse-wheel horizontal scroll (Shift+wheel). macOS trackpads usually emit +# small deltas, while X11/Windows wheels typically emit multiples of 120. +def _wheel_units(delta): + if delta == 0: + return 0 + if IS_MACOS and abs(delta) < 120: + return -1 if delta > 0 else 1 + return int(-1 * (delta / 120)) + def _on_mousewheel(event): - tk_canvas.yview_scroll(int(-1 * (event.delta / 120)), "units") + tk_canvas.yview_scroll(_wheel_units(event.delta), "units") + def _on_shift_mousewheel(event): - tk_canvas.xview_scroll(int(-1 * (event.delta / 120)), "units") + tk_canvas.xview_scroll(_wheel_units(event.delta), "units") root.bind_all("", _on_mousewheel) root.bind_all("", _on_shift_mousewheel) @@ -214,6 +269,9 @@ def _quit(e=None): root.bind_all("", _quit) root.bind_all("", _quit) +if IS_MACOS: + root.bind_all("", _quit) + root.createcommand("tk::mac::Quit", _quit) if not inf == timeout: root.after(int(timeout * 1000), _quit) From 8303b866d3cc264f004eaa9dc27b22cff1193fb6 Mon Sep 17 00:00:00 2001 From: Dmitry Messerman Date: Sun, 17 May 2026 12:49:44 +0300 Subject: [PATCH 4/8] Moving to Z3 4.16.0 --- .github/workflows/install-z3.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/install-z3.sh b/.github/workflows/install-z3.sh index e242c1d4..1b9e86ae 100755 --- a/.github/workflows/install-z3.sh +++ b/.github/workflows/install-z3.sh @@ -6,7 +6,7 @@ source "$(dirname "${BASH_SOURCE[0]}")"/install-gmp.sh P=z3 -eval ${P}_V=${V:-4.8.12} # version +eval ${P}_V=${V:-4.16.0} # version eval ${P}_F=${F:-$P-\$`echo \${P}_V`.tar.xz} # source archive name eval ${P}_W=${W:-$HOME/$P} # workdir root eval ${P}_S=${S:-\$`echo ${P}_W`/$P-$P-\$`echo \${P}_V`} # source dir From de73ea1dea0998005b36a7c9536a7cc11891eebc Mon Sep 17 00:00:00 2001 From: Dmitry Messerman Date: Sun, 17 May 2026 12:52:47 +0300 Subject: [PATCH 5/8] Reverting back incorrect commit --- .github/workflows/install-z3.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/install-z3.sh b/.github/workflows/install-z3.sh index 1b9e86ae..e242c1d4 100755 --- a/.github/workflows/install-z3.sh +++ b/.github/workflows/install-z3.sh @@ -6,7 +6,7 @@ source "$(dirname "${BASH_SOURCE[0]}")"/install-gmp.sh P=z3 -eval ${P}_V=${V:-4.16.0} # version +eval ${P}_V=${V:-4.8.12} # version eval ${P}_F=${F:-$P-\$`echo \${P}_V`.tar.xz} # source archive name eval ${P}_W=${W:-$HOME/$P} # workdir root eval ${P}_S=${S:-\$`echo ${P}_W`/$P-$P-\$`echo \${P}_V`} # source dir From 70d444c48aa5976b0041dc4b0e84bbe7d0d13e56 Mon Sep 17 00:00:00 2001 From: Dmitry Messerman Date: Sun, 17 May 2026 18:10:36 +0300 Subject: [PATCH 6/8] Synch with master --- scripts/github/smlp_release_info.py | 103 ++++++++++++++++++++++++++++ scripts/venv/run_dora | 16 +++++ setup.py | 1 - 3 files changed, 119 insertions(+), 1 deletion(-) create mode 100755 scripts/github/smlp_release_info.py diff --git a/scripts/github/smlp_release_info.py b/scripts/github/smlp_release_info.py new file mode 100755 index 00000000..58f39135 --- /dev/null +++ b/scripts/github/smlp_release_info.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3.11 +import requests +from bs4 import BeautifulSoup +import re +from sys import argv +from os.path import basename + +def get_commit_info_from_github_release(url): + """ + Extracts the commit hash and commit date from a GitHub release page URL + without using git. + + Args: + url (str): The URL of the GitHub release page (e.g., + "https://github.com/SMLP-Systems/smlp/releases/tag/v1.2.3rc7"). + + Returns: + dict or None: A dictionary with 'commit_hash' and 'commit_date' if found, + otherwise None. + """ + headers = { + # Mimic a real browser to avoid being blocked by GitHub + "User-Agent": ( + "Mozilla/5.0 (Windows NT 10.0; Win64; x64) " + "AppleWebKit/537.36 (KHTML, like Gecko) " + "Chrome/124.0.0.0 Safari/537.36" + ) + } + + try: + response = requests.get(url, headers=headers) + response.raise_for_status() + except requests.exceptions.RequestException as e: + print(f"Error fetching the URL '{url}': {e}") + return None + + soup = BeautifulSoup(response.text, 'html.parser') + + commit_hash = None + commit_date = None + + commit_link_pattern = re.compile(r'/commit/([0-9a-fA-F]{40})') + + # --- Strategy 1: Find the commit link and look for a sibling