From 820ac7dcdeb8e20314ae7ee3a53e55aa8f65ba89 Mon Sep 17 00:00:00 2001
From: HSPyroblast <levsovga@ya.ru>
Date: Tue, 28 Jul 2026 20:37:07 +0300
Subject: [PATCH 1/3] fix build: update native extension toolchain

---
 build.py               | 8 ++++++--
 third_party/mockturtle | 2 +-
 third_party/pybind11   | 2 +-
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/build.py b/build.py
index 7d132a21..b0491444 100644
--- a/build.py
+++ b/build.py
@@ -25,7 +25,7 @@ def _parse_env_flag(name: str, default: bool = False) -> bool:
     if v is None:
         return default
     v = v.strip().lower()
-    return v not in ("", "0", "false", "no", "off")
+    return v not in ("", "0", "false", "no", "off", "release")
 
 
 # Disables building extensions and subdirectories related to ABC
@@ -50,7 +50,11 @@ def build_extension(self, ext: CMakeExtension) -> None:
         # Using this requires trailing slash for auto-detection & inclusion of
         # auxiliary "native" libs
 
-        debug = int(os.environ.get("DEBUG", 0)) if self.debug is None else self.debug
+        debug = (
+            _parse_env_flag("DEBUG", False)
+            if self.debug is None
+            else bool(self.debug)
+        )
         cfg = "Debug" if debug else "Release"
 
         # CMake lets you override the generator - we need to check this.
diff --git a/third_party/mockturtle b/third_party/mockturtle
index b2ce7f03..b78357b5 160000
--- a/third_party/mockturtle
+++ b/third_party/mockturtle
@@ -1 +1 @@
-Subproject commit b2ce7f039d93fd8569cd856ff3fef4dbfb46b50d
+Subproject commit b78357b5e93775c93f04c54f5a9df3c02eed7f02
diff --git a/third_party/pybind11 b/third_party/pybind11
index a2e59f0e..6b92b6e1 160000
--- a/third_party/pybind11
+++ b/third_party/pybind11
@@ -1 +1 @@
-Subproject commit a2e59f0e7065404b44dfe92a28aca47ba1378dc4
+Subproject commit 6b92b6e148ab2762950425f6de851f8d152d5b4f

From d76a1135a39a86787f330ad59d8e6acef5f00f0e Mon Sep 17 00:00:00 2001
From: HSPyroblast <levsovga@ya.ru>
Date: Tue, 28 Jul 2026 20:37:28 +0300
Subject: [PATCH 2/3] fix deps: pin python-sat 1.8.dev30

---
 poetry.lock    | 123 +++++++++++++++++++++++++------------------------
 pyproject.toml |   2 +-
 2 files changed, 63 insertions(+), 62 deletions(-)

diff --git a/poetry.lock b/poetry.lock
index 01503de6..f0443186 100644
--- a/poetry.lock
+++ b/poetry.lock
@@ -1,4 +1,4 @@
-# This file is automatically @generated by Poetry 2.2.1 and should not be changed by hand.
+# This file is automatically @generated by Poetry 2.1.1 and should not be changed by hand.
 
 [[package]]
 name = "alabaster"
@@ -535,7 +535,7 @@ description = "Read metadata from Python packages"
 optional = false
 python-versions = ">=3.9"
 groups = ["docs"]
-markers = "python_version == \"3.9\""
+markers = "python_version < \"3.10\""
 files = [
     {file = "importlib_metadata-8.7.1-py3-none-any.whl", hash = "sha256:5a1f80bf1daa489495071efbb095d75a634cf28a8bc299581244063b53176151"},
     {file = "importlib_metadata-8.7.1.tar.gz", hash = "sha256:49fef1ae6440c182052f407c8d34a68f72efc36db9ca90dc0113398f2fdde8bb"},
@@ -1053,67 +1053,68 @@ dev = ["argcomplete", "attrs (>=19.2)", "hypothesis (>=3.56)", "mock", "pygments
 
 [[package]]
 name = "python-sat"
-version = "1.8.dev26"
+version = "1.8.dev30"
 description = "A Python library for prototyping with SAT oracles"
 optional = false
 python-versions = "*"
 groups = ["main"]
 files = [
-    {file = "python_sat-1.8.dev26-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:507fef0876b8199a102915909b5b0643ce9b04cfe80812b51c0a81521c25acd2"},
-    {file = "python_sat-1.8.dev26-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:b1d6c267bf5f8a75747c22c301b2f463c91c7cc80621190e90596b778bc53530"},
-    {file = "python_sat-1.8.dev26-cp310-cp310-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:c049dfcdb536b9a8590a39c55ebcb12b19fc427929f9756926a60b81afa8ed1c"},
-    {file = "python_sat-1.8.dev26-cp310-cp310-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:e92715ade4ff60795fe878b48dcd8e88b3d9fb039a0789dd195aa4e1bf8ac3a7"},
-    {file = "python_sat-1.8.dev26-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:3655c70e4e0e3cf4591330f992e76da19ed980c15e56e4c83449718799e93628"},
-    {file = "python_sat-1.8.dev26-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:417b9fd7238d48421149fc6b6661cd5fbd53c911bad1675c2065b610efda8955"},
-    {file = "python_sat-1.8.dev26-cp310-cp310-win_amd64.whl", hash = "sha256:bbe494a10d4bda22026047d2048f56f3f989c9e660d90c1a00e2cfb90af0aab0"},
-    {file = "python_sat-1.8.dev26-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:e98162e2150c5cf220187e68cd2418ee5602fccd151174756a2bcbe983aedf7d"},
-    {file = "python_sat-1.8.dev26-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:8c5081b6ec014c510a45dbca96e3b781a95f716e332c528aeefe4f6e8e2113c4"},
-    {file = "python_sat-1.8.dev26-cp311-cp311-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:5786b4bbd01e25ed646476a80cb0474e3054afdf7ccba6a828c98527ce1498d9"},
-    {file = "python_sat-1.8.dev26-cp311-cp311-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:19e7e7edb90d27340e0ec8a8e6975288d75653c21f96946a9cf72537e11300b0"},
-    {file = "python_sat-1.8.dev26-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:bc929a9fb984122c982835414775c904d08d2438fef0626cbb290d98717140c1"},
-    {file = "python_sat-1.8.dev26-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:da06b28c5058cc4839c8376d5e3d0282c8ac01efda55342796ca481faea338e7"},
-    {file = "python_sat-1.8.dev26-cp311-cp311-win_amd64.whl", hash = "sha256:b7c078d99616771c00eca9fb9d4fbef53f525b6aca714cfab854e48699069df7"},
-    {file = "python_sat-1.8.dev26-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:3512d6484ffdd949f9162a94a74057d69891731107a33916b0aeab0b2caa1312"},
-    {file = "python_sat-1.8.dev26-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:9acdc90720dd6125478fd1c1676ce8c6a6593ef484e0dfaa48604313de9551bc"},
-    {file = "python_sat-1.8.dev26-cp312-cp312-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:b88a505b306cfadf493a1e39cd93198fc85229acc1be338e5f60609ab6759cc0"},
-    {file = "python_sat-1.8.dev26-cp312-cp312-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:605a9dfc1c26a5f583ed1f3d3554d2741e6ba217d767661159f9e84b23abc466"},
-    {file = "python_sat-1.8.dev26-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:03ec8673d87d6e07ad79d2d8654e7db4a8d2664fdafc5f552e4db833d2f398d2"},
-    {file = "python_sat-1.8.dev26-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:beda1c0e98dc3b565e76e8f09c149bf23ea7d8961f504600e22c7b6d01cb6df6"},
-    {file = "python_sat-1.8.dev26-cp312-cp312-win_amd64.whl", hash = "sha256:cc99c953ed2d22be4ecad55d108f8c628cc0fefa164d453fe96152bc0addf642"},
-    {file = "python_sat-1.8.dev26-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:28f377f875165721674ff9219c7a200d6c4752fd32f30bc94a834880916f3775"},
-    {file = "python_sat-1.8.dev26-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:e2425aadcb9ba46704eff414cbd42c05425925f6e0a73307bfd450e383159460"},
-    {file = "python_sat-1.8.dev26-cp313-cp313-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:5752402ce40cc066be4b04af8387df73f7116351fe6b506a5f48a6f28aca41f4"},
-    {file = "python_sat-1.8.dev26-cp313-cp313-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:99d8254c76b73ef4854ed707b1628ff4b053b3070b37b8e2e7b70545e61180b9"},
-    {file = "python_sat-1.8.dev26-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:f8f6bc4fea91cc94ab445f2e628161152b09ef8fb0c8541d738e77c757e0b552"},
-    {file = "python_sat-1.8.dev26-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:579af45b194051a88b87c50d82e24f1dffbf09faf1d9a281c9045c42e9864d92"},
-    {file = "python_sat-1.8.dev26-cp313-cp313-win_amd64.whl", hash = "sha256:86d6da543910252e98ee9c75456dc002294ddd949db834e7d64acd7c9a1c5b66"},
-    {file = "python_sat-1.8.dev26-cp314-cp314-macosx_10_13_x86_64.whl", hash = "sha256:c6ec2f8e5bd3725b1739bedd22b233ea4446903d289eb14709a3cb71322fcac1"},
-    {file = "python_sat-1.8.dev26-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:35b88f11cdf27ffa56876706b41cb18ca1118eb8a896842605c1864286c362a6"},
-    {file = "python_sat-1.8.dev26-cp314-cp314-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:6a4376619fcbfc9bbe46d8c65f41bab0678bdcda2118b6efbec76102245d2e25"},
-    {file = "python_sat-1.8.dev26-cp314-cp314-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:99cd9fc7fc17e107c0128befb5ff34f7a3370fd7175519d767d8a37759f796ae"},
-    {file = "python_sat-1.8.dev26-cp314-cp314-musllinux_1_2_aarch64.whl", hash = "sha256:4c0f8cf8659844684967eb23e67ec7288aa18a06fb8e69b917ee2cb52142a10a"},
-    {file = "python_sat-1.8.dev26-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:a6475ea7ea256c3f53c1bd2b8d75a2bc418dc99346d18fc6fb5cfad5be67c071"},
-    {file = "python_sat-1.8.dev26-cp314-cp314t-macosx_10_13_x86_64.whl", hash = "sha256:38fb4d1d131b568c45d2ad9d7c721d1977a856a80ae6b586a413af1a05c7282e"},
-    {file = "python_sat-1.8.dev26-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:29e64495d76e46ddbc3d8022b83916445610c4d8584aab60564f4f1666b5df80"},
-    {file = "python_sat-1.8.dev26-cp314-cp314t-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:8bbd11c5bc806286e3bd27efa4843035c4843f3a1ddbcfb438ef4639c3b11247"},
-    {file = "python_sat-1.8.dev26-cp314-cp314t-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:660e8e956134140fe36d4f1ab2cc7571697192f813b40f28cd53ea2a802088df"},
-    {file = "python_sat-1.8.dev26-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:21cd05a1dff39ed8f965c79237727ad5800f6704e889c83ab6c0ce0f0e99ad6b"},
-    {file = "python_sat-1.8.dev26-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:9635ec47443dd8b8d96a71eec170268a7e4eb62d75486859a19b45f1a7047e77"},
-    {file = "python_sat-1.8.dev26-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:52ccd972dac473dd8b5fdac1c3a552bb708a4bf9f6aa44a872558a414c14e38f"},
-    {file = "python_sat-1.8.dev26-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:8be851473de03fd4c76eee02e36ad69e20a83b9dcd9db7c4276b3691627b6252"},
-    {file = "python_sat-1.8.dev26-cp38-cp38-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:a324e9c71a8975f7f3553dac9dcb606f7daa33f8f446464f915e2d56850121a5"},
-    {file = "python_sat-1.8.dev26-cp38-cp38-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:60b4ba41211159dee5fd38659be574bbc14270177ea4853f69cb3d48448b5f59"},
-    {file = "python_sat-1.8.dev26-cp38-cp38-musllinux_1_2_aarch64.whl", hash = "sha256:b241b4149cba4d062bb153463777cec1a71f314edce6abfc34b41478765178db"},
-    {file = "python_sat-1.8.dev26-cp38-cp38-musllinux_1_2_x86_64.whl", hash = "sha256:015f2f53418ce626de24ff3202276394be33faef66ad8858f92c3ac663810133"},
-    {file = "python_sat-1.8.dev26-cp38-cp38-win_amd64.whl", hash = "sha256:22eb6b52122278cd16d9e135c2536532bcad0a9a4d8a84c2ebc1b845c1284f17"},
-    {file = "python_sat-1.8.dev26-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:85a413200f1c56c2ca8a1f0dbb610f53545f232eac6046752db012b0bb923380"},
-    {file = "python_sat-1.8.dev26-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:e313eedeacc12eea5f24b54a48d75bf522028c51e01a77554a808257f79169e5"},
-    {file = "python_sat-1.8.dev26-cp39-cp39-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:21ca369a4c1afb3e390cad9abcd0034efa01d020f44b8752835c370af04bf383"},
-    {file = "python_sat-1.8.dev26-cp39-cp39-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:c522ceed6035eee25a6b16160336815c2285a03b9bb5ac9a2b73e66db2e82da0"},
-    {file = "python_sat-1.8.dev26-cp39-cp39-musllinux_1_2_aarch64.whl", hash = "sha256:2104db337d7efc01f311cda35a0fefe31ee7254d48ccfffa6fe4d7d7baa4f705"},
-    {file = "python_sat-1.8.dev26-cp39-cp39-musllinux_1_2_x86_64.whl", hash = "sha256:1e4639081df5ad9dd15ffed53feebaefabc5f1add97bd45085378381ab45ff77"},
-    {file = "python_sat-1.8.dev26-cp39-cp39-win_amd64.whl", hash = "sha256:409676a0ff6bda15f90e75176f8320094fd2bed3be08157ad75b89b0fc71fb08"},
-    {file = "python_sat-1.8.dev26.tar.gz", hash = "sha256:097c98aaf9b48fd19b07c5957860bfa3aae346f24d0eab9a18b1864448087e87"},
+    {file = "python_sat-1.8.dev30-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:d0afc9b93002c72c50468fe38d2ed31ed2d38205fb6f849bd77cf0ac8f1c16b5"},
+    {file = "python_sat-1.8.dev30-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:e74edba1488c737c297a180b8b722b4595af89423add894c9b721fd38b5a47d5"},
+    {file = "python_sat-1.8.dev30-cp310-cp310-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:5b247b38bb2f79149b85a91c1f87147ce9e0ba2021f6bb8ef28fdddb89b05477"},
+    {file = "python_sat-1.8.dev30-cp310-cp310-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:223323a7f1812dc558b9d32b3a185251f2b6e6c0c63e5eea6891dea4de305c56"},
+    {file = "python_sat-1.8.dev30-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:9d33f811d23ec6fbf0eb171cdfaa79bdf2ee539b6cab52bde83250cf26264e04"},
+    {file = "python_sat-1.8.dev30-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:2386d375c6b59fd3a24b5458a20f2389999bbfdb50956038ebbe62b1546be45f"},
+    {file = "python_sat-1.8.dev30-cp310-cp310-win_amd64.whl", hash = "sha256:a52f9ccd87b33813b4e7de386e80b9d44e0188cf8491600febf6a49c10ccc534"},
+    {file = "python_sat-1.8.dev30-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:25f2b9dc81a50cb19e966ad178a50ae4292fe940e0e6373241f5810e4fe76084"},
+    {file = "python_sat-1.8.dev30-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:2e8176979deef383ece2c4e0e209cda28b264025bf194872bcd93b065b88f7e7"},
+    {file = "python_sat-1.8.dev30-cp311-cp311-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:bd3572a3cfa313270f2de353e9908a405bd525fb51a05d7560b0e1bb218f864a"},
+    {file = "python_sat-1.8.dev30-cp311-cp311-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:656a7f596cb004000c4f2b6ec31167e1c9efa7d39f013251715e8790fcc53ba7"},
+    {file = "python_sat-1.8.dev30-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:732114cff9083cdf35091260953120c7ef946f22d758ef826ca8a2ff1d551bf7"},
+    {file = "python_sat-1.8.dev30-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:928d0608a3d542ccb88d612d4b36827bafd6950d9b84af6588e766593210017a"},
+    {file = "python_sat-1.8.dev30-cp311-cp311-win_amd64.whl", hash = "sha256:7d5e6843431dd6a9780fa4e118e7937ece1567cdc020cc131ca27c42f6ddf9b1"},
+    {file = "python_sat-1.8.dev30-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:047decbfab9e8b6d43e943ac6b254f77f5b0849a1c03f17d46ba95a405b4eee6"},
+    {file = "python_sat-1.8.dev30-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:09b382b1ed330472c4a45931555e783d1fdbc410da1321bef2dc44f6c67eab25"},
+    {file = "python_sat-1.8.dev30-cp312-cp312-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:708c73d9987f83527d8fd13bd66a967fc5f346f9b035023d775a9b82d06bf511"},
+    {file = "python_sat-1.8.dev30-cp312-cp312-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:8bb8997cf4a68a70abbf3384c266b8959fbbc57c1ebc3de26ef0205c98b40c6e"},
+    {file = "python_sat-1.8.dev30-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:18df9ca91ad447e58def6f59599f9a8066795c28b41eb9b36b3034860dd516e0"},
+    {file = "python_sat-1.8.dev30-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:52606259a92de64051cdbed0cf6229b81b03a33b7911f8f34da215d4a4d2d6fe"},
+    {file = "python_sat-1.8.dev30-cp312-cp312-win_amd64.whl", hash = "sha256:47f3b0c68a0b4ac15328b7087bca7e0f25715448511cf6a93f74c6f5c8b5e37f"},
+    {file = "python_sat-1.8.dev30-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:be9f45b429b6d070cb91d009a6daa1aab9d6599ee37bbcab9b9302f077ad5afd"},
+    {file = "python_sat-1.8.dev30-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:f5fe8ae2381504e355b519e34040d554bffbe734d03c69b814413ea9f699a3df"},
+    {file = "python_sat-1.8.dev30-cp313-cp313-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:9272c75c4cc664d1744793b3eff04c9c6776c39960917a9c1b053d770b3217c7"},
+    {file = "python_sat-1.8.dev30-cp313-cp313-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:6df046a7f9a4f662850c9c17a230b9edd74b3ad2a6ccc5b4a685650bba77721e"},
+    {file = "python_sat-1.8.dev30-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:caaafd7f7c361b676a01e01cfb82b7fb0fcbf84744d4dd4f521d0d8d345d9c70"},
+    {file = "python_sat-1.8.dev30-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:4bcc39402125f1a69bce95483e761d7a4d355744a2fc1d192574f0d13ecac547"},
+    {file = "python_sat-1.8.dev30-cp313-cp313-win_amd64.whl", hash = "sha256:91e01a2911095df14e3b1f4ec28ffb7c676fc472b556b1a943ca23dc6e783b13"},
+    {file = "python_sat-1.8.dev30-cp314-cp314-macosx_10_13_x86_64.whl", hash = "sha256:ff4b4a7ffa1d31d83a44b57f06e4cdd979259f67ec1a948ab8085472405bc078"},
+    {file = "python_sat-1.8.dev30-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:7861bec740b7817360d1c05b54ae3cef57e03a4e0ecbc97c21b6e71eef2d4b4d"},
+    {file = "python_sat-1.8.dev30-cp314-cp314-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:f1f0b7af6af18e1d9316a0ad7a4aec4b6503b2c56e7cf8c70b9882496d3dbabc"},
+    {file = "python_sat-1.8.dev30-cp314-cp314-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ee125de6d61e852268bbb4b3ec04a7e5296c32d7f300ed104381df5774aaf3df"},
+    {file = "python_sat-1.8.dev30-cp314-cp314-musllinux_1_2_aarch64.whl", hash = "sha256:97192a14bc60784b015f6a938903a95c24c3474325de8017fd9e16407d5cd52b"},
+    {file = "python_sat-1.8.dev30-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:84f9ea644740f6d8e75ee688ce324b4c605edcd253af0da8d43a66ea0bd3f972"},
+    {file = "python_sat-1.8.dev30-cp314-cp314-win_amd64.whl", hash = "sha256:f2f0ea44ee872b007a675a2467e37eabf3da9b9c8f8f4745ae29e0c32d9956ea"},
+    {file = "python_sat-1.8.dev30-cp314-cp314t-macosx_10_13_x86_64.whl", hash = "sha256:022168d24e451f1bd8101d863e816ad810dcc0d2b5d753515ee16f882327fd74"},
+    {file = "python_sat-1.8.dev30-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:43d10d15f9a686b7839ddc66be063baba36d549b794a4805de6a7597b8c3a871"},
+    {file = "python_sat-1.8.dev30-cp314-cp314t-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:11b0718cd76d8bf5498f510ba74de0304cf699148d2a7aedce5db779a1042d00"},
+    {file = "python_sat-1.8.dev30-cp314-cp314t-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:7a01e631d4039599544ab6877cfa629fe4b3478d9b740351ac5b91ed1ae8d7ea"},
+    {file = "python_sat-1.8.dev30-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:a39bfb2a966f2e1052bc4d95b6568fd5c2ba741ec5e9cf0a5effcd9fadee2977"},
+    {file = "python_sat-1.8.dev30-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:ac13c80b149c6f45272d057d8b5f1ba0453279a690c0fb38034c6948b5bea803"},
+    {file = "python_sat-1.8.dev30-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:36e45585e0d76bcd13e7c5dc0ed739c42381acb9613f31e1ec3bc5be73ba2e92"},
+    {file = "python_sat-1.8.dev30-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:607d8cbb62ee26e247c004bf2e79e1ccd9e962a7c39275cb42c01c3fb669fedd"},
+    {file = "python_sat-1.8.dev30-cp38-cp38-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:60e1b10989b8462dd7a5df6a277decba23fc5f1bffe20edf0e6f706eaee812a0"},
+    {file = "python_sat-1.8.dev30-cp38-cp38-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:07ad049dc18e8b348c27181a465c84a7a38ff933db27f52ee3aab599e0952de0"},
+    {file = "python_sat-1.8.dev30-cp38-cp38-musllinux_1_2_aarch64.whl", hash = "sha256:dee889bf6ada47bbd54cbeb7bd24242a02fa35ea8192a3457ea59314c0857d94"},
+    {file = "python_sat-1.8.dev30-cp38-cp38-musllinux_1_2_x86_64.whl", hash = "sha256:5acd9729d0307552b20098803e2dbe3cc021c7b280e5b349e6f188affc7d8d37"},
+    {file = "python_sat-1.8.dev30-cp38-cp38-win_amd64.whl", hash = "sha256:686423fed7d7c721ddd5ce05f73bfeb732e700fa7b2b71a89ad60955025d3b73"},
+    {file = "python_sat-1.8.dev30-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:4c4cd2589d980f834c79e604fbf3b86436293803927895be6200ada891040890"},
+    {file = "python_sat-1.8.dev30-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:0ce86ee1cb390f05c204dd33c8fab11e0497ce29552b43e6eceb6f11a866f9b8"},
+    {file = "python_sat-1.8.dev30-cp39-cp39-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:4f168c6a751381ca33d1ffe8825b39490e77c3451c5b43c4af2ba7dddb3ba3bd"},
+    {file = "python_sat-1.8.dev30-cp39-cp39-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:474f7448a5ab05b3208abd661501e6d726e69c5c05076dbae235ef6f58089197"},
+    {file = "python_sat-1.8.dev30-cp39-cp39-musllinux_1_2_aarch64.whl", hash = "sha256:26f361ea6d4443e0ef680e767191a32b07ded27fe584bb4639928c136c65b342"},
+    {file = "python_sat-1.8.dev30-cp39-cp39-musllinux_1_2_x86_64.whl", hash = "sha256:7b9a16c65850127916b03d9ff4b6eb1307d992642048d2b16b3354c9a0b998ad"},
+    {file = "python_sat-1.8.dev30-cp39-cp39-win_amd64.whl", hash = "sha256:6bc0185e98e4b1868e57efc2f4cc8262863bbf1fdfdf56accd13b0ac294be2e8"},
+    {file = "python_sat-1.8.dev30.tar.gz", hash = "sha256:29a47a34f0fac3303459c633abfa6d44505e2343dfba6cff4b6ad596c0ca9d4e"},
 ]
 
 [package.dependencies]
@@ -1462,7 +1463,7 @@ description = "A list of Python Standard Libraries (2.7 through 3.14)."
 optional = false
 python-versions = ">=3.9"
 groups = ["docs"]
-markers = "python_version == \"3.9\""
+markers = "python_version < \"3.10\""
 files = [
     {file = "stdlib_list-0.12.0-py3-none-any.whl", hash = "sha256:df2d11e97f53812a1756fb5510393a11e3b389ebd9239dc831c7f349957f62f2"},
     {file = "stdlib_list-0.12.0.tar.gz", hash = "sha256:517824f27ee89e591d8ae7c1dd9ff34f672eae50ee886ea31bb8816d77535675"},
@@ -1650,7 +1651,7 @@ description = "Backport of pathlib-compatible object wrapper for zip files"
 optional = false
 python-versions = ">=3.9"
 groups = ["docs"]
-markers = "python_version == \"3.9\""
+markers = "python_version < \"3.10\""
 files = [
     {file = "zipp-3.23.0-py3-none-any.whl", hash = "sha256:071652d6115ed432f5ce1d34c336c0adfd6a884660d1e9712a256d3d3bd4b14e"},
     {file = "zipp-3.23.0.tar.gz", hash = "sha256:a07157588a12518c9d4034df3fbbee09c814741a33ff63c05fa29d26a2404166"},
@@ -1667,4 +1668,4 @@ type = ["pytest-mypy"]
 [metadata]
 lock-version = "2.1"
 python-versions = "^3.9"
-content-hash = "da8a43feb7e1d4cb4265c48175c9d169062ba70ef7d17473f6cf77bfaa4cd08f"
+content-hash = "81bd63e5d88d20162c6eafc388325d8d95eb4ca80d200404b3c61a34c5ebe85c"
diff --git a/pyproject.toml b/pyproject.toml
index 7f59bccd..89cd1504 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -41,7 +41,7 @@ keywords = ["circuit", "synthesis", "analysis"]
 dependencies = [
     "more-itertools >= 10.8.0",
     "typing-extensions >= 4.14.1",
-    "python-sat >= 1.8.dev26",
+    "python-sat (==1.8.dev30)",
     "pebble >= 5.1.3",
     "graphviz >= 0.21",
     "sortedcontainers (>=2.4.0,<3.0.0)",

From e33d71e8ce3ee9944fc39128cb86df32023141e6 Mon Sep 17 00:00:00 2001
From: HSPyroblast <levsovga@ya.ru>
Date: Tue, 28 Jul 2026 20:37:41 +0300
Subject: [PATCH 3/3] feat generation: add logarithmic-depth arithmetic
 circuits

---
 cirbo/core/circuit/circuit.py                 |  28 +
 cirbo/synthesis/generation/arithmetics/CRT.py | 204 ++++++
 .../generation/arithmetics/__init__.py        |  40 +-
 .../generation/arithmetics/div_mod.py         | 162 ++++-
 .../generation/arithmetics/multiplication.py  | 341 +++++++++-
 .../synthesis/generation/arithmetics/sqrt.py  |  35 +-
 .../generation/arithmetics/square.py          | 107 ++-
 .../generation/arithmetics/subtraction.py     | 268 ++++++--
 .../generation/arithmetics/summation.py       | 627 ++++++++++++++++--
 pyproject.toml                                |   8 +-
 .../synthesis/generation/arithmetics_test.py  | 228 ++++++-
 11 files changed, 1896 insertions(+), 152 deletions(-)
 create mode 100644 cirbo/synthesis/generation/arithmetics/CRT.py

diff --git a/cirbo/core/circuit/circuit.py b/cirbo/core/circuit/circuit.py
index 40cfdd55..0eab2abc 100644
--- a/cirbo/core/circuit/circuit.py
+++ b/cirbo/core/circuit/circuit.py
@@ -1244,6 +1244,34 @@ def bfs(
             topsort_unvisited=topsort_unvisited,
         )
 
+    def get_depth(
+        self,
+    ) -> int:
+        """
+        Computes the logical depth of the circuit.
+
+        The depth of a circuit is defined as the length of the longest path from any
+        input gate to any other gate in the circuit. Input gates have depth 0, and every
+        other gate has depth equal to 1 plus the maximum depth of its operands.
+
+        :return: integer value representing the maximum depth of the circuit
+
+        """
+        gates = self.gates
+        mem: dict[gate.Label, int] = {}
+
+        def depth(label: gate.Label) -> int:
+            if label in mem:
+                return mem[label]
+            gate = gates[label]
+            if gate.gate_type.name == "INPUT":
+                mem[label] = 0
+            else:
+                mem[label] = 1 + max(depth(op) for op in gate.operands)
+            return mem[label]
+
+        return max(depth(g.label) for g in gates.values())
+
     def evaluate_full_circuit(
         self,
         assignment: dict[gate.Label, GateState],
diff --git a/cirbo/synthesis/generation/arithmetics/CRT.py b/cirbo/synthesis/generation/arithmetics/CRT.py
new file mode 100644
index 00000000..96aaa1f3
--- /dev/null
+++ b/cirbo/synthesis/generation/arithmetics/CRT.py
@@ -0,0 +1,204 @@
+import typing as tp
+
+from cirbo.core.circuit import Circuit, gate
+from cirbo.synthesis.generation.arithmetics._utils import (
+    add_gate_from_tt,
+    reverse_if_big_endian,
+)
+from cirbo.synthesis.generation.arithmetics.div_mod import add_div_mod
+from cirbo.synthesis.generation.arithmetics.multiplication import add_mul_constant
+
+from cirbo.synthesis.generation.arithmetics.summation import add_sum_n_weighted_bits
+
+from cirbo.synthesis.generation.helpers import GenerationBasis
+
+
+def to_bin(circuit: Circuit, n: int):
+    """
+    Converts an integer constant to circuit labels representing its binary form.
+
+    :param circuit: The general circuit.
+    :param n: Integer constant to convert.
+    :return: A list of gate labels representing the integer in little-endian format.
+
+    """
+    label = circuit.inputs[0]
+    zero = add_gate_from_tt(
+        circuit,
+        label,
+        label,
+        '0000',
+    )
+    one = add_gate_from_tt(
+        circuit,
+        label,
+        label,
+        '1111',
+    )
+    res = []
+    for i in range(n.bit_length()):
+        if n & 1 << i:
+            res.append(one)
+        else:
+            res.append(zero)
+    return res
+
+
+def extended_euclidean(a, b):
+    """
+    Calculates the greatest common divisor and Bezout coefficients.
+
+    :param a: The first integer.
+    :param b: The second integer.
+    :return: A tuple ``(gcd, x, y)`` such that ``a * x + b * y == gcd``.
+
+    """
+    if b == 0:
+        return a, 1, 0
+    gcd, x, y = extended_euclidean(b, a % b)
+    return gcd, y, x - (a // b) * y
+
+
+def modular_inverse(M_i, m_i):
+    """
+    Calculates the modular inverse of ``M_i`` modulo ``m_i``.
+
+    :param M_i: Integer value whose inverse should be found.
+    :param m_i: Modulus for the inverse calculation.
+    :return: The value ``x`` such that ``M_i * x == 1 mod m_i``.
+    :raises ValueError: If the inverse does not exist.
+
+    """
+    gcd, x, _ = extended_euclidean(M_i, m_i)
+    if gcd != 1:
+        raise ValueError(f"Inverse does not exist for {M_i} mod {m_i}")
+    return x % m_i
+
+
+def _weighted_bits_to_labels(
+    circuit: Circuit,
+    weighted: list[tuple[int, gate.Label]],
+) -> list[gate.Label]:
+    """
+    Converts weighted bit labels to a flat little-endian bit list.
+
+    :param circuit: The general circuit.
+    :param weighted: List of pairs where the first element is the bit power and the
+        second element is the corresponding gate label.
+    :return: A list of gate labels ordered by bit power in little-endian format.
+
+    """
+    if not weighted:
+        return []
+    max_power = max(p for p, _ in weighted)
+    ref = weighted[0][1]
+    zero = add_gate_from_tt(circuit, ref, ref, '0000')
+    result: list[gate.Label] = [zero] * (max_power + 1)
+    for power, label in weighted:
+        result[power] = label
+    return result
+
+
+def add_crt(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    moduls: list[int],
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[gate.Label]:
+    """
+    Reconstructs a number from its residues using the Chinese Remainder Theorem.
+
+    :param circuit: The general circuit.
+    :param input_labels_a: Iterable of gate labels representing concatenated residues.
+        For each modulus ``m``, the residue occupies ``(m - 1).bit_length()`` bits.
+    :param moduls: List of pairwise coprime moduli.
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
+    :return: A list of gate labels representing the reconstructed number modulo the
+        product of all moduli.
+
+    """
+    input_labels_a = list(input_labels_a)
+
+    if big_endian:
+        input_labels_a.reverse()
+
+    product = 1
+    for mod in moduls:
+        product *= mod
+    M_i_list = [product // m for m in moduls]
+    inverse_elements = [modular_inverse(M_i, m_i) for M_i, m_i in zip(M_i_list, moduls)]
+
+    pointer = 0
+    power_bits = []
+    for i, mod in enumerate(moduls):
+        bit_len = (mod - 1).bit_length()
+        res = add_mul_constant(
+            circuit,
+            input_labels_a[pointer : pointer + bit_len],
+            inverse_elements[i] * M_i_list[i],
+            basis=basis,
+        )
+        for j in range(len(res)):
+            power_bits.append((j, res[j]))
+        pointer += bit_len
+
+    weighted_sum = add_sum_n_weighted_bits(circuit, power_bits, basis=basis)
+    sum_bits = _weighted_bits_to_labels(circuit, weighted_sum)
+    product_bits = to_bin(circuit, product)
+    _, ans = add_div_mod(circuit, sum_bits, product_bits)
+    return reverse_if_big_endian(ans, big_endian)
+
+
+def add_crt_calc(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    moduls: list[int],
+    factors: list[int],
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[gate.Label]:
+    """
+    Reconstructs a number from its residues using predefined CRT factors.
+
+    :param circuit: The general circuit.
+    :param input_labels_a: Iterable of gate labels representing concatenated residues.
+        For each modulus ``m``, the residue occupies ``(m - 1).bit_length()`` bits.
+    :param moduls: List of moduli defining how to split the input labels.
+    :param factors: Precomputed CRT factors. Each residue is multiplied by the factor
+        with the same index, and the last element is used as the final modulus.
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
+    :return: A list of gate labels representing the reconstructed number reduced by the
+        final modulus from ``factors``.
+
+    """
+    input_labels_a = list(input_labels_a)
+
+    if big_endian:
+        input_labels_a.reverse()
+
+    pointer = 0
+    power_bits = []
+    for i, mod in enumerate(moduls):
+        bit_len = (mod - 1).bit_length()
+        res = add_mul_constant(
+            circuit,
+            input_labels_a[pointer : pointer + bit_len],
+            factors[i],
+            basis=basis,
+        )
+        for j in range(len(res)):
+            power_bits.append((j, res[j]))
+        pointer += bit_len
+
+    weighted_sum = add_sum_n_weighted_bits(circuit, power_bits, basis=basis)
+    sum_bits = _weighted_bits_to_labels(circuit, weighted_sum)
+    product_bits = to_bin(circuit, factors[-1])
+    _, ans = add_div_mod(circuit, sum_bits, product_bits)
+    return reverse_if_big_endian(ans, big_endian)
diff --git a/cirbo/synthesis/generation/arithmetics/__init__.py b/cirbo/synthesis/generation/arithmetics/__init__.py
index 4f07e8ee..53cda2ae 100644
--- a/cirbo/synthesis/generation/arithmetics/__init__.py
+++ b/cirbo/synthesis/generation/arithmetics/__init__.py
@@ -1,26 +1,43 @@
 """Subpackage defines plenty of methods useful for generation of small arithmetic
 circuits by several methods."""
 
-from .div_mod import add_div_mod, generate_div_mod
+from .div_mod import (
+    add_div_mod,
+    add_div_predefined,
+    add_mod_predefined,
+    generate_div_mod,
+)
 from .equality import add_equal, generate_equal
 from .multiplication import (
     add_mul,
     add_mul_alter,
+    add_mul_constant,
     add_mul_dadda,
     add_mul_karatsuba,
     add_mul_karatsuba_with_efficient_sum,
+    add_mul_log_depth_sum,
     add_mul_pow2_m1,
     add_mul_wallace,
+    add_smul_dadda,
+    add_smul_wallace,
     generate_mul,
     MulMode,
 )
 from .sqrt import add_sqrt, generate_sqrt
-from .square import add_square, add_square_pow2_m1, generate_square, SquareMode
+from .square import (
+    add_square,
+    add_square_dadda,
+    add_square_pow2_m1,
+    generate_square,
+    SquareMode,
+)
 from .subtraction import (
     add_sub2,
     add_sub3,
     add_sub_two_numbers,
+    add_sub_two_numbers_log_depth,
     add_subtract_with_compare,
+    add_subtract_with_compare_log_depth,
     generate_sub_two_numbers,
 )
 from .summation import (
@@ -29,13 +46,18 @@
     add_sum_n_bits,
     add_sum_n_bits_easy,
     add_sum_n_weighted_bits,
+    add_sum_n_weighted_bits_log_depth,
     add_sum_n_weighted_bits_naive,
     add_sum_pow2_m1,
     add_sum_two_numbers,
+    add_sum_two_numbers_log_depth,
+    add_sum_two_numbers_log_depth_brent_kung,
+    add_sum_two_numbers_log_depth_krapchenko,
     add_sum_two_numbers_with_shift,
     generate_sum_n_bits,
     generate_sum_weighted_bits_efficient,
     generate_sum_weighted_bits_naive,
+    mdfa_sum_weighted_bits,
 )
 
 
@@ -43,6 +65,8 @@
     # div_mod.py
     'generate_div_mod',
     'add_div_mod',
+    'add_div_predefined',
+    'add_mod_predefined',
     # equality.py
     'add_equal',
     'generate_equal',
@@ -50,10 +74,14 @@
     'add_mul',
     'add_mul_karatsuba_with_efficient_sum',
     'add_mul_karatsuba',
+    'add_mul_log_depth_sum',
     'add_mul_alter',
     'add_mul_dadda',
     'add_mul_wallace',
     'add_mul_pow2_m1',
+    'add_smul_dadda',
+    'add_smul_wallace',
+    'add_mul_constant',
     'generate_mul',
     'MulMode',
     # sqrt.py
@@ -62,13 +90,16 @@
     # square.py
     'add_square',
     'add_square_pow2_m1',
+    'add_square_dadda',
     'generate_square',
     'SquareMode',
     # subtraction.py
     'add_sub2',
     'add_sub3',
     'add_sub_two_numbers',
+    'add_sub_two_numbers_log_depth',
     'add_subtract_with_compare',
+    'add_subtract_with_compare_log_depth',
     'generate_sub_two_numbers',
     # summation.py
     'generate_sum_n_bits',
@@ -78,9 +109,14 @@
     'add_sum_n_bits_easy',
     'add_sum_pow2_m1',
     'add_sum_two_numbers',
+    'add_sum_two_numbers_log_depth',
+    'add_sum_two_numbers_log_depth_brent_kung',
+    'add_sum_two_numbers_log_depth_krapchenko',
     'add_sum_two_numbers_with_shift',
     'add_sum_n_weighted_bits',
+    'add_sum_n_weighted_bits_log_depth',
     'add_sum_n_weighted_bits_naive',
     'generate_sum_weighted_bits_efficient',
     "generate_sum_weighted_bits_naive",
+    'mdfa_sum_weighted_bits',
 ]
diff --git a/cirbo/synthesis/generation/arithmetics/div_mod.py b/cirbo/synthesis/generation/arithmetics/div_mod.py
index 0b4a203a..3f650d48 100644
--- a/cirbo/synthesis/generation/arithmetics/div_mod.py
+++ b/cirbo/synthesis/generation/arithmetics/div_mod.py
@@ -6,16 +6,31 @@
     PLACEHOLDER_STR,
     validate_equal_sizes,
 )
-from cirbo.synthesis.generation.arithmetics.subtraction import add_subtract_with_compare
-
+from cirbo.synthesis.generation.arithmetics.multiplication import add_mul_constant
+from cirbo.synthesis.generation.arithmetics.subtraction import (
+    add_sub_two_numbers,
+    add_subtract_with_compare,
+)
+from cirbo.synthesis.generation.arithmetics.summation import (
+    add_sum_two_numbers,
+    xor_two_bits,
+)
+from cirbo.synthesis.generation.helpers import GenerationBasis
 
 __all__ = [
     'add_div_mod',
+    'add_div_predefined',
+    'add_mod_predefined',
     'generate_div_mod',
 ]
 
 
-def generate_div_mod(n: int, *, big_endian: bool = False) -> Circuit:
+def generate_div_mod(
+    n: int,
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> Circuit:
     """
     Generates a circuit that have div and mod two numbers (one number is first n bits,
     other is second n bits) in result.
@@ -23,6 +38,7 @@ def generate_div_mod(n: int, *, big_endian: bool = False) -> Circuit:
     :param n: the number of bits in each number.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :return: circuit that count div and mod.
 
     """
@@ -33,6 +49,7 @@ def generate_div_mod(n: int, *, big_endian: bool = False) -> Circuit:
         circuit.inputs[:n],
         circuit.inputs[n:],
         big_endian=big_endian,
+        basis=basis,
     )
     circuit.set_outputs(div + mod)
     return circuit
@@ -43,7 +60,9 @@ def add_div_mod(
     input_labels_a: tp.Iterable[gate.Label],
     input_labels_b: tp.Iterable[gate.Label],
     *,
+    zero_div: bool = False,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> tuple[list[gate.Label], list[gate.Label]]:
     """
     Function make div two integers with equal size.
@@ -53,6 +72,7 @@ def add_div_mod(
     :param input_labels_b: bits of divider in increase order.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :return: first list is result for div, second list is result for mod.
 
     """
@@ -61,7 +81,20 @@ def add_div_mod(
     if big_endian:
         input_labels_a.reverse()
         input_labels_b.reverse()
+
+    label = input_labels_a[0]
+    zero = add_gate_from_tt(
+        circuit,
+        label,
+        label,
+        '0000',
+    )
+    extra = 0
+    while len(input_labels_b) < len(input_labels_a):
+        input_labels_b.append(zero)
+        extra += 1
     validate_equal_sizes(input_labels_a, input_labels_b)
+
     n = len(input_labels_a)
 
     a = input_labels_a
@@ -83,7 +116,9 @@ def add_div_mod(
     for i in range(n - 1, 0, -1):  # chose shift for sub (> 0)
         prov = pref[i - 1]
         m = n - i  # intersection
-        sub_res, per = add_subtract_with_compare(circuit, now[(n - m) :], b[:m])
+        sub_res, per = add_subtract_with_compare(
+            circuit, now[(n - m) :], b[:m], basis=basis
+        )
         result[i] = add_gate_from_tt(circuit, prov, per, "1000")
         for j in range(m):
             now[j + n - m] = add_gate_from_tt(
@@ -94,7 +129,7 @@ def add_div_mod(
             )
 
     m = n  # intersection
-    sub_res, per = add_subtract_with_compare(circuit, now, b)
+    sub_res, per = add_subtract_with_compare(circuit, now, b, basis=basis)
     result[0] = add_gate_from_tt(circuit, per, per, "1000")
     for j in range(m):
         now[j] = add_gate_from_tt(
@@ -104,15 +139,118 @@ def add_div_mod(
             "0111",
         )
 
-    # if we need result A % 0 = 0 and B / 0 = 0
-    pref.append(add_gate_from_tt(circuit, pref[-1], b[0], "0111"))
-    for i in range(n):
-        result[i] = add_gate_from_tt(circuit, result[i], pref[-1], "0001")
-    for i in range(n):
-        now[i] = add_gate_from_tt(circuit, now[i], pref[-1], "0001")
+    if zero_div:  # if we need result A % 0 = 0 and B / 0 = 0
+        pref.append(add_gate_from_tt(circuit, pref[-1], b[0], "0111"))
+        for i in range(n):
+            result[i] = add_gate_from_tt(circuit, result[i], pref[-1], "0001")
+        for i in range(n):
+            now[i] = add_gate_from_tt(circuit, now[i], pref[-1], "0001")
+
+    else:  # if we need result A % 0 = A and B / 0 = B
+        pref.append(add_gate_from_tt(circuit, pref[-1], b[0], "0111"))
+        and1 = ["0" for i in range(n)]
+        and2 = ["0" for i in range(n)]
+        for i in range(n):
+            and1[i] = add_gate_from_tt(circuit, input_labels_a[i], pref[-1], "1000")
+            and1[i] = add_gate_from_tt(circuit, and1[i], result[i], "0001")
+            and2[i] = add_gate_from_tt(circuit, input_labels_a[i], pref[-1], "0010")
+            and2[i] = add_gate_from_tt(circuit, and2[i], result[i], "0010")
+            and1[i] = add_gate_from_tt(circuit, and1[i], and2[i], "0111")
+        for i in range(n):
+            result[i] = xor_two_bits(circuit, result[i], and1[i], basis=basis)
 
     if big_endian:
         result.reverse()
         now.reverse()
 
-    return result, now
+    return result, now[: n - extra]
+
+
+def precompute_unsigned(N, d):
+    if d == 0:
+        raise ValueError("Divisor cannot be zero")
+
+    length = d.bit_length() - 1
+    shift = length
+
+    if d == (1 << length):
+        mul = 1
+        add = 0
+    else:
+        big_one = 1 << (N + length)
+        m_down = big_one // d
+        m_up = m_down + 1
+        temp = (m_up * d) & ((1 << N) - 1)
+
+        if temp <= (1 << length):
+            shift += N
+            mul = m_up
+            add = 0
+        else:
+            shift += N
+            mul = m_down
+            add = m_down
+
+    return mul, add, shift
+
+
+def add_div_predefined(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    b: int,
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[gate.Label]:
+    input_labels_a = list(input_labels_a)
+    if big_endian:
+        input_labels_a.reverse()
+    n = len(input_labels_a)
+    if b == 0:
+        raise ValueError("Division by zero")
+
+    mul, add_val, shift = precompute_unsigned(n, b)
+
+    out = add_mul_constant(circuit, input_labels_a, mul, basis=basis)
+    if add_val != 0:
+        add_bits = _constant_to_bits(circuit, out[0], add_val)
+        out = add_sum_two_numbers(circuit, out, add_bits)
+
+    out = out[shift:]
+    return out
+
+
+def _constant_to_bits(
+    circuit: Circuit,
+    ref_label: gate.Label,
+    n: int,
+) -> list[gate.Label]:
+    """Convert integer constant n to a list of bit labels (little-endian)."""
+    zero = add_gate_from_tt(circuit, ref_label, ref_label, '0000')
+    one = add_gate_from_tt(circuit, ref_label, ref_label, '1111')
+    bits = []
+    for i in range(n.bit_length()):
+        bits.append(one if (n >> i) & 1 else zero)
+    return bits
+
+
+def add_mod_predefined(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    b: int,
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[gate.Label]:
+    from cirbo.synthesis.generation.arithmetics._utils import reverse_if_big_endian
+
+    input_labels_a = list(input_labels_a)
+    if big_endian:
+        input_labels_a.reverse()
+    if b == 0:
+        raise ValueError("Division by zero")
+
+    div = add_div_predefined(circuit, input_labels_a, b, big_endian=False, basis=basis)
+    sub = add_mul_constant(circuit, div, b, basis=basis)
+    res = add_sub_two_numbers(circuit, input_labels_a, sub, basis=basis)
+    return reverse_if_big_endian(res, big_endian)
diff --git a/cirbo/synthesis/generation/arithmetics/multiplication.py b/cirbo/synthesis/generation/arithmetics/multiplication.py
index cf5f1324..1f6efd7e 100644
--- a/cirbo/synthesis/generation/arithmetics/multiplication.py
+++ b/cirbo/synthesis/generation/arithmetics/multiplication.py
@@ -1,6 +1,7 @@
 import collections
 import enum
 import typing as tp
+from typing import Optional
 
 from cirbo.core.circuit import Circuit, gate
 from cirbo.synthesis.generation.arithmetics._utils import (
@@ -16,18 +17,24 @@
     add_sum_n_weighted_bits,
     add_sum_pow2_m1,
     add_sum_two_numbers,
+    add_sum_two_numbers_log_depth,
     add_sum_two_numbers_with_shift,
 )
+from cirbo.synthesis.generation.helpers import GenerationBasis
 
 
 __all__ = [
     'add_mul',
     'add_mul_karatsuba',
     'add_mul_karatsuba_with_efficient_sum',
+    'add_mul_log_depth_sum',
     'add_mul_alter',
     'add_mul_dadda',
     'add_mul_wallace',
     'add_mul_pow2_m1',
+    'add_smul_dadda',
+    'add_smul_wallace',
+    'add_mul_constant',
     'generate_mul',
     'MulMode',
 ]
@@ -42,6 +49,61 @@ class MulMode(enum.Enum):
     POW2_M1 = "POW2_M1"
 
 
+def add_mul_log_depth_sum(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    sum_func: tp.Callable[..., list[gate.Label]] = add_sum_two_numbers_log_depth,
+    big_endian: bool = False,
+) -> list[gate.Label]:
+    input_labels_a = list(input_labels_a)
+    input_labels_b = list(input_labels_b)
+    n = len(input_labels_a)
+    m = len(input_labels_b)
+
+    if n < m:
+        input_labels_a, input_labels_b = input_labels_b, input_labels_a
+        n, m = m, n
+
+    if big_endian:
+        input_labels_a.reverse()
+        input_labels_b.reverse()
+
+    c: list[list[str]] = [[] for _ in range(m)]
+    d = [i for i in range(m)]
+    for i in range(m):
+        for j in range(n):
+            c[i].append(
+                add_gate_from_tt(circuit, input_labels_a[j], input_labels_b[i], '0001')
+            )
+
+    def sum_with_shift(
+        shift: int, labels_a: list[gate.Label], labels_b: list[gate.Label]
+    ) -> list[gate.Label]:
+        res = []
+        for i in range(shift):
+            res.append(labels_a[i])
+
+        res += sum_func(circuit, labels_a[shift:], labels_b, basis=basis)
+        return res
+
+    while len(c) > 1:
+        new_c = []
+        new_d = []
+        for i in range(0, len(c), 2):
+            if i + 1 < len(c):
+                new_c.append(sum_with_shift(d[i + 1] - d[i], c[i], c[i + 1]))
+                new_d.append(d[i])
+            else:
+                new_c.append(c[i])
+                new_d.append(d[i])
+        c = new_c
+        d = new_d
+    return reverse_if_big_endian(c[0][: n + m], big_endian)
+
+
 def generate_mul(
     size_of_input_a: int,
     size_of_input_b: int,
@@ -436,11 +498,44 @@ def add_dadda_karatsuba(
     return reverse_if_big_endian(final_res[:out_size], big_endian)
 
 
+def add_fin_sum(
+    circuit: Circuit,
+    c: list[tp.Deque[str]],
+    *,
+    sum_func: tp.Callable[..., list[gate.Label]] = add_sum_two_numbers_log_depth,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[gate.Label]:
+    out = []
+    a = []
+    b = []
+    zero = add_gate_from_tt(circuit, c[0][0], c[0][0], '0000')
+    ch = 0
+    for i in range(0, len(c)):
+        if len(c[i]) == 0:
+            if ch == 0:
+                out.append(zero)
+        elif len(c[i]) == 1 and ch == 0:
+            out.append(c[i][0])
+        else:
+            ch = 1
+            if len(c[i]) > 1:
+                a.append(c[i].popleft())
+                b.append(c[i].popleft())
+            else:
+                a.append(c[i].popleft())
+                b.append(zero)
+
+    out += sum_func(circuit, a, b, basis=basis)
+    return out
+
+
 def add_mul_dadda(
     circuit: Circuit,
     input_labels_a: tp.Iterable[gate.Label],
     input_labels_b: tp.Iterable[gate.Label],
     *,
+    sum_func: tp.Callable[..., list[gate.Label]] = add_sum_two_numbers_log_depth,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
     big_endian: bool = False,
 ) -> list[gate.Label]:
     """
@@ -479,15 +574,19 @@ def add_mul_dadda(
 
     while di != 1:
         for i in range(1, n + m):
-            while len(c[i]) >= di:
-                if len(c[i]) == di:
-                    g1, g2 = add_sum2(circuit, [c[i].popleft(), c[i].popleft()])
+            while len(c[i]) > di:
+                if len(c[i]) == di + 1:
+                    g1, g2 = add_sum2(
+                        circuit, [c[i].popleft(), c[i].popleft()], basis=basis
+                    )
                     c[i].append(g1)
                     if i + 1 < n + m:
                         c[i + 1].append(g2)
                 else:
                     g1, g2 = add_sum3(
-                        circuit, [c[i].popleft(), c[i].popleft(), c[i].popleft()]
+                        circuit,
+                        [c[i].popleft(), c[i].popleft(), c[i].popleft()],
+                        basis=basis,
                     )
                     c[i].append(g1)
                     if i + 1 < n + m:
@@ -497,9 +596,175 @@ def add_mul_dadda(
         else:
             di = (2 * di + 2) // 3
 
-    out = []
-    for i in range(n + m):
-        out.append(c[i].popleft())
+    out = add_fin_sum(circuit, c, sum_func=sum_func, basis=basis)[: n + m]
+
+    return reverse_if_big_endian(out, big_endian)
+
+
+def add_smul_dadda(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    sum_func: tp.Callable[..., list[gate.Label]] = add_sum_two_numbers_log_depth,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    big_endian: bool = False,
+) -> list[gate.Label]:
+    """
+    Multiplies two signed numbers using the Dadda multiplication algorithm.
+
+    :param circuit: The general circuit.
+    :param input_labels_a: Iterable of gate labels representing the first input number.
+    :param input_labels_b: Iterable of gate labels representing the second input number.
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :return: A list of gate labels representing the product of the two input numbers.
+
+    """
+    input_labels_a = list(input_labels_a)
+    input_labels_b = list(input_labels_b)
+    n = len(input_labels_a)
+    m = len(input_labels_b)
+
+    if n < m:
+        input_labels_a, input_labels_b = input_labels_b, input_labels_a
+        n, m = m, n
+
+    if big_endian:
+        input_labels_a.reverse()
+        input_labels_b.reverse()
+
+    c: list[tp.Deque[str]] = [collections.deque() for _ in range(n + m)]
+    for i in range(m):
+        for j in range(n):
+            if (i == m - 1) ^ (j == n - 1):
+                c[i + j].append(
+                    add_gate_from_tt(
+                        circuit, input_labels_a[j], input_labels_b[i], '1110'
+                    )
+                )
+            else:
+                c[i + j].append(
+                    add_gate_from_tt(
+                        circuit, input_labels_a[j], input_labels_b[i], '0001'
+                    )
+                )
+    c[n].append(add_gate_from_tt(circuit, input_labels_a[0], input_labels_b[0], '1111'))
+    c[n + m - 1].append(
+        add_gate_from_tt(circuit, input_labels_a[0], input_labels_b[0], '1111')
+    )
+
+    if n == 1 or m == 1:
+        return reverse_if_big_endian([c[i][0] for i in range(m + n - 1)], big_endian)
+
+    di = 2
+    while 3 * di // 2 < min(n, m):
+        di = 3 * di // 2
+
+    while di != 1:
+        for i in range(1, n + m):
+            while len(c[i]) > di:
+                if len(c[i]) == di + 1:
+                    g1, g2 = add_sum2(
+                        circuit, [c[i].popleft(), c[i].popleft()], basis=basis
+                    )
+                    c[i].append(g1)
+                    if i + 1 < n + m:
+                        c[i + 1].append(g2)
+                else:
+                    g1, g2 = add_sum3(
+                        circuit,
+                        [c[i].popleft(), c[i].popleft(), c[i].popleft()],
+                        basis=basis,
+                    )
+                    c[i].append(g1)
+                    if i + 1 < n + m:
+                        c[i + 1].append(g2)
+        if di == 2:
+            di = 1
+        else:
+            di = (2 * di + 2) // 3
+
+    out = add_fin_sum(circuit, c, sum_func=sum_func, basis=basis)[: n + m]
+
+    return reverse_if_big_endian(out, big_endian)
+
+
+def add_smul_wallace(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    sum_func: tp.Callable[..., list[gate.Label]] = add_sum_two_numbers_log_depth,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[gate.Label]:
+    """
+    Multiplies two signed numbers using the Wallace multiplication algorithm.
+
+    :param circuit: The general circuit.
+    :param input_labels_a: Iterable of gate labels representing the first input number.
+    :param input_labels_b: Iterable of gate labels representing the second input number.
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :return: A list of gate labels representing the product of the two input numbers.
+
+    """
+    input_labels_a = list(input_labels_a)
+    input_labels_b = list(input_labels_b)
+    n = len(input_labels_a)
+    m = len(input_labels_b)
+
+    if big_endian:
+        input_labels_a.reverse()
+        input_labels_b.reverse()
+
+    c = [[PLACEHOLDER_STR] * m for _ in range(n + m)]
+    for i in range(m):
+        for j in range(n):
+            if (i == m - 1) ^ (j == n - 1):
+                c[i + j][i] = add_gate_from_tt(
+                    circuit, input_labels_a[j], input_labels_b[i], '1110'
+                )
+            else:
+                c[i + j][i] = add_gate_from_tt(
+                    circuit, input_labels_a[j], input_labels_b[i], '0001'
+                )
+    c[n][0] = add_gate_from_tt(circuit, input_labels_a[0], input_labels_b[0], '1111')
+    c[n + m - 1][m - 1] = add_gate_from_tt(
+        circuit, input_labels_a[0], input_labels_b[0], '1111'
+    )
+
+    if n == 1:
+        return reverse_if_big_endian([c[i][i] for i in range(m)], big_endian)
+
+    if m == 1:
+        return reverse_if_big_endian([c[i][0] for i in range(n)], big_endian)
+
+    while len(c[0]) != 2:
+        cn = [[PLACEHOLDER_STR] * (2 * (len(c[0]) // 3)) for _ in range(n + m)]
+        for row in range(0, len(c[0]) - len(c[0]) % 3, 3):
+            for col in range(n + m):
+                inp = []
+                for k in range(row, row + 3):
+                    if c[col][k] != PLACEHOLDER_STR:
+                        inp.append(c[col][k])
+
+                if len(inp) > 0:
+                    res = add_sum_n_bits(circuit, inp, basis=basis)
+                    for i in range(len(res)):
+                        if col + i < n + m:
+                            cn[col + i][2 * (row // 3) + i] = res[i]
+
+        for row in range(len(c[0]) - len(c[0]) % 3, len(c[0])):
+            for col in range(n + m):
+                cn[col].append(c[col][row])
+
+        c = cn
+
+    c_ = [collections.deque(x for x in col if x != PLACEHOLDER_STR) for col in c]
+    out = add_fin_sum(circuit, c_, sum_func=sum_func, basis=basis)[: n + m]
+
     return reverse_if_big_endian(out, big_endian)
 
 
@@ -508,10 +773,12 @@ def add_mul_wallace(
     input_labels_a: tp.Iterable[gate.Label],
     input_labels_b: tp.Iterable[gate.Label],
     *,
+    sum_func: tp.Callable[..., list[gate.Label]] = add_sum_two_numbers_log_depth,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
     """
-    Multiplies two numbers using the Dadda multiplication algorithm.
+    Multiplies two numbers using the Wallace multiplication algorithm.
 
     :param circuit: The general circuit.
     :param input_labels_a: Iterable of gate labels representing the first input number.
@@ -553,7 +820,7 @@ def add_mul_wallace(
                         inp.append(c[col][k])
 
                 if len(inp) > 0:
-                    res = add_sum_n_bits(circuit, inp)
+                    res = add_sum_n_bits(circuit, inp, basis=basis)
                     for i in range(len(res)):
                         if col + i < n + m:
                             cn[col + i][2 * (row // 3) + i] = res[i]
@@ -564,21 +831,42 @@ def add_mul_wallace(
 
         c = cn
 
-    labels_a = []
-    labels_b = []
-    shift = 0
-    for i in range(n + m):
-        if c[i][0] != PLACEHOLDER_STR:
-            labels_a.append(c[i][0])
-        if c[i][1] != PLACEHOLDER_STR:
-            labels_b.append(c[i][1])
-        elif len(labels_b) == 0:
-            shift += 1
-
-    return reverse_if_big_endian(
-        add_sum_two_numbers_with_shift(circuit, shift, labels_a, labels_b)[: n + m],
-        big_endian,
-    )
+    c_ = [collections.deque(x for x in col if x != PLACEHOLDER_STR) for col in c]
+    out = add_fin_sum(circuit, c_, sum_func=sum_func, basis=basis)[: n + m]
+
+    return reverse_if_big_endian(out, big_endian)
+
+
+def add_mul_constant(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    b: int,
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[gate.Label]:
+    input_labels_a = list(input_labels_a)
+    n = len(input_labels_a)
+
+    if big_endian:
+        input_labels_a.reverse()
+
+    labels_with_pow = list()
+    for i in range(b.bit_length()):
+        if b & (1 << i):
+            for j in range(n):
+                labels_with_pow.append((j + i, input_labels_a[j]))
+
+    weighted_sum = add_sum_n_weighted_bits(circuit, labels_with_pow, basis=basis)
+    max_power = max(p for p, _ in weighted_sum) if weighted_sum else -1
+    result: list[Optional[str]] = [None] * (max_power + 1)
+    for power, label in weighted_sum:
+        result[power] = label
+
+    label0 = input_labels_a[0]
+    zero = add_gate_from_tt(circuit, label0, label0, '0000')
+    out = [lbl if lbl is not None else zero for lbl in result]
+    return reverse_if_big_endian(out, big_endian)
 
 
 def add_mul_pow2_m1(
@@ -587,9 +875,10 @@ def add_mul_pow2_m1(
     input_labels_b: tp.Iterable[gate.Label],
     *,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
     """
-    Multiplies two numbers with lengths 2^k - 1 using a specific squaring method.
+    Multiplies two numbers using summators with lengths 2^k - 1.
 
     :param circuit: The general circuit.
     :param input_labels_a: Iterable of gate labels representing the first input number.
@@ -632,7 +921,7 @@ def add_mul_pow2_m1(
         if len(inp) == 1:
             out[i] = [[inp[0]]]
         else:
-            out[i] = add_sum_pow2_m1(circuit, inp)
+            out[i] = add_sum_pow2_m1(circuit, inp, basis=basis)
     return reverse_if_big_endian([out[i][0][0] for i in range(n + m)], big_endian)
 
 
diff --git a/cirbo/synthesis/generation/arithmetics/sqrt.py b/cirbo/synthesis/generation/arithmetics/sqrt.py
index 2ed04dc5..df47dc22 100644
--- a/cirbo/synthesis/generation/arithmetics/sqrt.py
+++ b/cirbo/synthesis/generation/arithmetics/sqrt.py
@@ -6,7 +6,11 @@
     reverse_if_big_endian,
 )
 from cirbo.synthesis.generation.arithmetics.subtraction import add_subtract_with_compare
-from cirbo.synthesis.generation.arithmetics.summation import add_sum_two_numbers
+from cirbo.synthesis.generation.arithmetics.summation import (
+    add_sum_two_numbers,
+    xor_two_bits,
+)
+from cirbo.synthesis.generation.helpers import GenerationBasis
 
 
 __all__ = [
@@ -19,6 +23,7 @@ def generate_sqrt(
     inp_len: int,
     *,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> Circuit:
     """
     Generates a circuit that have sqrt of number in result.
@@ -26,6 +31,7 @@ def generate_sqrt(
     :param inp_len: number of input bits (must be even)
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
 
     """
     circuit = Circuit.bare_circuit(inp_len)
@@ -33,13 +39,18 @@ def generate_sqrt(
         circuit,
         circuit.inputs,
         big_endian=big_endian,
+        basis=basis,
     )
     circuit.set_outputs(res)
     return circuit
 
 
 def add_sqrt(
-    circuit: Circuit, input_labels: tp.Iterable[gate.Label], *, big_endian: bool = False
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
     """
     Function find sqrt of integer.
@@ -48,6 +59,7 @@ def add_sqrt(
     :param input_labels: the bits of the integer we want to find the sqrt for.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :return: the sqrt of integer.
 
     """
@@ -57,8 +69,15 @@ def add_sqrt(
     x = input_labels
     if big_endian:
         x.reverse()
-    ZERO = add_gate_from_tt(circuit, x[0], x[0], "0110")
-    UNO = add_gate_from_tt(circuit, x[0], x[0], "1001")
+    ZERO = xor_two_bits(circuit, x[0], x[0], basis=basis)
+
+    _basis = GenerationBasis(basis.upper()) if isinstance(basis, str) else basis
+    if _basis == GenerationBasis.XAIG:
+        UNO = add_gate_from_tt(circuit, x[0], x[0], "1001")
+    else:
+        ab = add_gate_from_tt(circuit, x[0], x[0], '0001')
+        nab = add_gate_from_tt(circuit, x[0], x[0], '1000')
+        UNO = add_gate_from_tt(circuit, ab, nab, '0111')
 
     if n % 2 == 1:
         half += 1
@@ -67,9 +86,11 @@ def add_sqrt(
 
     c = [ZERO for _ in range(n)]
     for st in range(half - 1, -1, -1):
-        sm = add_sum_two_numbers(circuit, c[(2 * st) :], [UNO])
+        sm = add_sum_two_numbers(circuit, c[(2 * st) :], [UNO], basis=basis)
         sm = sm[:-1]
-        sub_res, per = add_subtract_with_compare(circuit, x[(2 * st) :], sm)
+        sub_res, per = add_subtract_with_compare(
+            circuit, x[(2 * st) :], sm, basis=basis
+        )
         for i in range(st * 2, n):
             x[i] = add_gate_from_tt(
                 circuit,
@@ -79,7 +100,7 @@ def add_sqrt(
             )
         c = c[1:]
         c.append(ZERO)
-        sm = add_sum_two_numbers(circuit, c[(2 * st) :], [UNO])[:-1]
+        sm = add_sum_two_numbers(circuit, c[(2 * st) :], [UNO], basis=basis)[:-1]
         for i in range(st * 2, n):
             c[i] = add_gate_from_tt(
                 circuit,
diff --git a/cirbo/synthesis/generation/arithmetics/square.py b/cirbo/synthesis/generation/arithmetics/square.py
index 330ca1eb..9b2333d7 100644
--- a/cirbo/synthesis/generation/arithmetics/square.py
+++ b/cirbo/synthesis/generation/arithmetics/square.py
@@ -1,3 +1,4 @@
+import collections
 import enum
 import typing as tp
 
@@ -7,15 +8,24 @@
     PLACEHOLDER_STR,
     reverse_if_big_endian,
 )
-from cirbo.synthesis.generation.arithmetics.multiplication import add_mul_karatsuba
+from cirbo.synthesis.generation.arithmetics.multiplication import (
+    add_fin_sum,
+    add_mul_karatsuba,
+)
 from cirbo.synthesis.generation.arithmetics.summation import (
+    add_sum2,
+    add_sum3,
     add_sum_pow2_m1,
+    add_sum_two_numbers_log_depth,
     add_sum_two_numbers_with_shift,
 )
+from cirbo.synthesis.generation.exceptions import BadBasisError
+from cirbo.synthesis.generation.helpers import GenerationBasis
 
 
 __all__ = [
     'add_square',
+    'add_square_dadda',
     'add_square_pow2_m1',
     'generate_square',
     'SquareMode',
@@ -25,6 +35,7 @@
 class SquareMode(enum.Enum):
     DEFAULT = "DEFAULT"
     POW2_M1 = "POW2_M1"
+    DADDA = "DADDA"
 
 
 def generate_square(
@@ -32,6 +43,7 @@ def generate_square(
     *,
     type: SquareMode = SquareMode.DEFAULT,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> Circuit:
     """
     Generates a circuit that have square of number in result.
@@ -40,6 +52,7 @@ def generate_square(
     :param type: what type of algorithm to use
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
 
     """
     circuit = Circuit.bare_circuit(number_inputs)
@@ -47,13 +60,18 @@ def generate_square(
         circuit,
         circuit.inputs,
         big_endian=big_endian,
+        basis=basis,
     )
     circuit.set_outputs(outputs)
     return circuit
 
 
 def add_square(
-    circuit: Circuit, input_labels: tp.Iterable[gate.Label], *, big_endian: bool = False
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
     """
     Compute the square of a number represented by the given input labels in the circuit.
@@ -62,9 +80,14 @@ def add_square(
     :param input_labels: Iterable of gate labels representing the input number.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG].
     :return: A list of gate labels representing the square of the input number.
 
     """
+    _basis = GenerationBasis(basis.upper()) if isinstance(basis, str) else basis
+    if _basis != GenerationBasis.XAIG:
+        raise BadBasisError("Only XAIG is supported for square")
+
     input_labels = list(input_labels)
     n = len(input_labels)
     if big_endian:
@@ -88,8 +111,82 @@ def add_square(
     return reverse_if_big_endian(final_res, big_endian)
 
 
+def add_square_dadda(
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    sum_func: tp.Callable[..., list[gate.Label]] = add_sum_two_numbers_log_depth,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    big_endian: bool = False,
+) -> list[gate.Label]:
+    """
+    Computes the square of a number using the Dadda multiplication algorithm.
+
+    :param circuit: The general circuit.
+    :param input_labels: Iterable of gate labels representing the input number.
+    :param sum_func: Function to use for summing intermediate results.
+    :param basis: Basis for the generated circuit.
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :return: A list of gate labels representing the square of the input number.
+
+    """
+    input_labels = list(input_labels)
+    n = len(input_labels)
+
+    if big_endian:
+        input_labels.reverse()
+
+    c: list[tp.Deque[str]] = [collections.deque() for _ in range(2 * n)]
+    for i in range(n):
+        for j in range(i + 1, n):
+            c[i + j + 1].append(
+                add_gate_from_tt(circuit, input_labels[i], input_labels[j], '0001')
+            )
+    for i in range(n):
+        c[2 * i].append(input_labels[i])
+
+    if n == 1:
+        return reverse_if_big_endian([c[i][0] for i in range(2 * n - 1)], big_endian)
+
+    di = 2
+    while 3 * di // 2 < n:
+        di = 3 * di // 2
+
+    while di != 1:
+        for i in range(2, 2 * n):
+            while len(c[i]) > di:
+                if len(c[i]) == di + 1:
+                    g1, g2 = add_sum2(
+                        circuit, [c[i].popleft(), c[i].popleft()], basis=basis
+                    )
+                    c[i].append(g1)
+                    if i + 1 < 2 * n:
+                        c[i + 1].append(g2)
+                else:
+                    g1, g2 = add_sum3(
+                        circuit,
+                        [c[i].popleft(), c[i].popleft(), c[i].popleft()],
+                        basis=basis,
+                    )
+                    c[i].append(g1)
+                    if i + 1 < 2 * n:
+                        c[i + 1].append(g2)
+        if di == 2:
+            di = 1
+        else:
+            di = (2 * di + 2) // 3
+
+    out = add_fin_sum(circuit, c, sum_func=sum_func, basis=basis)[: 2 * n]
+    return reverse_if_big_endian(out, big_endian)
+
+
 def add_square_pow2_m1(
-    circuit: Circuit, input_labels: tp.Iterable[gate.Label], *, big_endian: bool = False
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
     """
     Compute the square of a number with length 2^k - 1 using a specific squaring method.
@@ -98,6 +195,7 @@ def add_square_pow2_m1(
     :param input_labels: Iterable of gate labels representing the input number.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :return: A list of gate labels representing the square of the input number.
     """
     input_labels = list(input_labels)
@@ -142,7 +240,7 @@ def add_square_pow2_m1(
         if len(inp) == 1:
             d[i] = [[inp[0]]]
         else:
-            d[i] = add_sum_pow2_m1(circuit, inp)
+            d[i] = add_sum_pow2_m1(circuit, inp, basis=basis)
     res = [d[i][0][0] for i in range(2 * n)]
     return reverse_if_big_endian(res, big_endian)
 
@@ -150,4 +248,5 @@ def add_square_pow2_m1(
 _process_square: dict[SquareMode, tp.Callable[..., list[gate.Label]]] = {
     SquareMode.DEFAULT: add_square,
     SquareMode.POW2_M1: add_square_pow2_m1,
+    SquareMode.DADDA: add_square_dadda,
 }
diff --git a/cirbo/synthesis/generation/arithmetics/subtraction.py b/cirbo/synthesis/generation/arithmetics/subtraction.py
index cf176f18..511d448d 100644
--- a/cirbo/synthesis/generation/arithmetics/subtraction.py
+++ b/cirbo/synthesis/generation/arithmetics/subtraction.py
@@ -8,13 +8,18 @@
     validate_const_size,
     validate_equal_sizes,
 )
+from cirbo.synthesis.generation.arithmetics.summation import xor_two_bits
+from cirbo.synthesis.generation.exceptions import BadBasisError
+from cirbo.synthesis.generation.helpers import GenerationBasis
 
 
 __all__ = [
     "add_sub2",
     "add_sub3",
     "add_sub_two_numbers",
+    "add_sub_two_numbers_log_depth",
     "add_subtract_with_compare",
+    "add_subtract_with_compare_log_depth",
     "generate_sub_two_numbers",
 ]
 
@@ -24,6 +29,7 @@ def generate_sub_two_numbers(
     size_of_input_b: int,
     *,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> Circuit:
     """
     Generates a circuit that have subtract two binary numbers in result.
@@ -32,6 +38,7 @@ def generate_sub_two_numbers(
     :param size_of_input_b: the number of inputs representing the second number.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :return: circuit that difference of the two numbers.
 
     """
@@ -42,39 +49,78 @@ def generate_sub_two_numbers(
         circuit.inputs[:size_of_input_a],
         circuit.inputs[size_of_input_a:],
         big_endian=big_endian,
+        basis=basis,
     )
     circuit.set_outputs(outputs)
     return circuit
 
 
+def conventional_basis(basis: tp.Union[str, GenerationBasis]) -> GenerationBasis:
+    return GenerationBasis(basis.upper()) if isinstance(basis, str) else basis
+
+
 def add_sub2(
-    circuit: Circuit, input_labels: tp.Iterable[gate.Label], *, big_endian: bool = False
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
-    input_labels = list(input_labels)
+    _input_labels = list(input_labels)
     if big_endian:
-        input_labels.reverse()
-    validate_const_size(input_labels, 2)
-    [x1, x2] = input_labels
-    g1 = add_gate_from_tt(circuit, x1, x2, '0110')
-    g2 = add_gate_from_tt(circuit, x1, x2, '0100')
+        _input_labels.reverse()
+    validate_const_size(_input_labels, 2)
+    [x1, x2] = _input_labels
 
-    return list([g1, g2])  # res and balance
+    _basis = conventional_basis(basis)
+    if _basis == GenerationBasis.XAIG:
+        g1 = add_gate_from_tt(circuit, x1, x2, '0110')
+        g2 = add_gate_from_tt(circuit, x1, x2, '0100')
+
+        return list([g1, g2])  # res and balance
+    elif _basis == GenerationBasis.AIG:
+        g1 = add_gate_from_tt(circuit, x1, x2, '0100')
+        g2 = add_gate_from_tt(circuit, x1, x2, '0010')
+        g3 = add_gate_from_tt(circuit, g1, g2, '0111')
+
+        return [g3, g1]
+    else:
+        raise BadBasisError(f"Unsupported basis: {basis}")
 
 
 def add_sub3(
-    circuit: Circuit, input_labels: tp.Iterable[gate.Label], *, big_endian: bool = False
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
-    input_labels = list(input_labels)
+    _input_labels = list(input_labels)
     if big_endian:
-        input_labels.reverse()
-    validate_const_size(input_labels, 3)
-    x0, x1, x2 = input_labels  # A, B and balance (we do A - B)
-    x3 = add_gate_from_tt(circuit, x0, x1, '0110')
-    x4 = add_gate_from_tt(circuit, x1, x2, '0110')
-    x5 = add_gate_from_tt(circuit, x3, x4, '0111')
-    x6 = add_gate_from_tt(circuit, x2, x3, '0110')
-    x7 = add_gate_from_tt(circuit, x0, x5, '0110')
-    return list([x6, x7])
+        _input_labels.reverse()
+    validate_const_size(_input_labels, 3)
+
+    _basis = conventional_basis(basis)
+    if _basis == GenerationBasis.XAIG:
+        x0, x1, x2 = _input_labels  # A, B and balance (we do A - B)
+        x3 = add_gate_from_tt(circuit, x0, x1, '0110')
+        x4 = add_gate_from_tt(circuit, x1, x2, '0110')
+        x5 = add_gate_from_tt(circuit, x3, x4, '0111')
+        x6 = add_gate_from_tt(circuit, x2, x3, '0110')
+        x7 = add_gate_from_tt(circuit, x0, x5, '0110')
+        return list([x6, x7])
+    elif _basis == GenerationBasis.AIG:
+        x0, x1, x2 = _input_labels  # A, B and balance (we do A - B)
+        s3 = add_gate_from_tt(circuit, x0, x1, '1101')
+        s4 = add_gate_from_tt(circuit, x0, x1, '0100')
+        s5 = add_gate_from_tt(circuit, s3, s4, '0010')
+        s6 = add_gate_from_tt(circuit, x2, s5, '0001')
+        s7 = add_gate_from_tt(circuit, x2, s5, '0111')
+        s8 = add_gate_from_tt(circuit, s4, s6, '0111')
+        s9 = add_gate_from_tt(circuit, s6, s7, '1011')
+        return [s9, s8]
+    else:
+        raise BadBasisError(f"Unsupported basis: {basis}")
 
 
 def add_sub_two_numbers(
@@ -83,6 +129,7 @@ def add_sub_two_numbers(
     input_labels_b: tp.Iterable[gate.Label],
     *,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
     """
     Function to subtract two binary numbers represented by input labels.
@@ -92,28 +139,35 @@ def add_sub_two_numbers(
     :param input_labels_b: List of bits representing the second binary number.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :return: List of bits representing the difference of the two numbers.
 
     """
-    input_labels_a = list(input_labels_a)
-    input_labels_b = list(input_labels_b)
-    n = len(input_labels_a)
-    m = len(input_labels_b)
+    _input_labels_a = list(input_labels_a)
+    _input_labels_b = list(input_labels_b)
+    n = len(_input_labels_a)
+    m = len(_input_labels_b)
 
     if big_endian:
-        input_labels_a.reverse()
-        input_labels_b.reverse()
+        _input_labels_a.reverse()
+        _input_labels_b.reverse()
 
     res = [PLACEHOLDER_STR] * n
     bal = [PLACEHOLDER_STR] * n
-    res[0], bal[0] = add_sub2(circuit, [input_labels_a[0], input_labels_b[0]])
+    res[0], bal[0] = add_sub2(
+        circuit, [_input_labels_a[0], _input_labels_b[0]], basis=basis
+    )
     for i in range(1, n):
         if i < m:
             res[i], bal[i] = add_sub3(
-                circuit, [input_labels_a[i], input_labels_b[i], bal[i - 1]]
+                circuit,
+                [_input_labels_a[i], _input_labels_b[i], bal[i - 1]],
+                basis=basis,
             )
         else:
-            res[i], bal[i] = add_sub2(circuit, [input_labels_a[i], bal[i - 1]])
+            res[i], bal[i] = add_sub2(
+                circuit, [_input_labels_a[i], bal[i - 1]], basis=basis
+            )
 
     return reverse_if_big_endian(res, big_endian)
 
@@ -124,6 +178,7 @@ def add_subtract_with_compare(
     input_labels_b: tp.Iterable[gate.Label],
     *,
     big_endian: bool = False,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> tuple[list[gate.Label], gate.Label]:
     """
     Subtracts given integer b from integer a and return residual bit representing if
@@ -134,39 +189,170 @@ def add_subtract_with_compare(
     :param input_labels_b: labels representing integer b.
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :return: tuple (labels that carry subtraction result, label of gate that carries
         residual bit)
 
     """
-    input_labels_a = list(input_labels_a)
-    input_labels_b = list(input_labels_b)
+    _input_labels_a: list[str] = list(input_labels_a)
+    _input_labels_b: list[str] = list(input_labels_b)
 
     always_false = add_gate_from_tt(
-        circuit, input_labels_a[0], input_labels_b[0], "0000"
+        circuit, _input_labels_a[0], _input_labels_b[0], "0000"
     )
-    while len(input_labels_a) < len(input_labels_b):
-        input_labels_a.append(always_false)
-    while len(input_labels_a) > len(input_labels_b):
-        input_labels_b.append(always_false)
+    while len(_input_labels_a) < len(_input_labels_b):
+        _input_labels_a.append(always_false)
+    while len(_input_labels_a) > len(_input_labels_b):
+        _input_labels_b.append(always_false)
 
-    validate_equal_sizes(input_labels_a, input_labels_b)
+    validate_equal_sizes(_input_labels_a, _input_labels_b)
 
-    n = len(input_labels_a)
+    n = len(_input_labels_a)
 
     if big_endian:
-        input_labels_a.reverse()
-        input_labels_b.reverse()
+        _input_labels_a.reverse()
+        _input_labels_b.reverse()
 
     res = [PLACEHOLDER_STR] * n
     bal = [PLACEHOLDER_STR] * n
 
     res[0], bal[0] = add_sub2(
         circuit,
-        [input_labels_a[0], input_labels_b[0]],
+        [_input_labels_a[0], _input_labels_b[0]],
+        basis=basis,
     )
     for i in range(1, n):
         res[i], bal[i] = add_sub3(
             circuit,
-            [input_labels_a[i], input_labels_b[i], bal[i - 1]],
+            [_input_labels_a[i], _input_labels_b[i], bal[i - 1]],
+            basis=basis,
         )
     return reverse_if_big_endian(res, big_endian), bal[n - 1]
+
+
+def _kogge_stone_borrow_lookahead(
+    circuit: Circuit,
+    a: list[gate.Label],
+    b: list[gate.Label],
+    zero: gate.Label,
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> tuple[list[gate.Label], gate.Label]:
+    n = len(a)
+
+    difference_, borrow_gen_, borrow_prop_ = zip(
+        *[
+            (
+                xor_two_bits(circuit, a[i], b[i], basis=basis),
+                add_gate_from_tt(circuit, a[i], b[i], '0100'),
+                add_gate_from_tt(circuit, a[i], b[i], '1001'),
+            )
+            for i in range(n)
+        ]
+    )
+    difference: list[gate.Label] = list(difference_)
+    borrow_gen: list[gate.Label] = list(borrow_gen_)
+    borrow_prop: list[gate.Label] = list(borrow_prop_)
+
+    stride = 1
+    while stride < n:
+        for i in range(n - 1, stride - 1, -1):
+            t = add_gate_from_tt(
+                circuit, borrow_prop[i], borrow_gen[i - stride], '0001'
+            )
+            borrow_gen[i] = add_gate_from_tt(circuit, borrow_gen[i], t, '0111')
+        for i in range(n - 1, stride - 1, -1):
+            borrow_prop[i] = add_gate_from_tt(
+                circuit, borrow_prop[i], borrow_prop[i - stride], '0001'
+            )
+        stride *= 2
+
+    borrow_into = [zero] + borrow_gen
+    result = [
+        xor_two_bits(circuit, difference[i], borrow_into[i], basis=basis)
+        for i in range(n)
+    ]
+
+    return result, borrow_gen[n - 1]
+
+
+def add_sub_two_numbers_log_depth(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    big_endian: bool = False,
+) -> list[gate.Label]:
+    """
+    Subtract two binary numbers in O(log n) depth using a Kogge-Stone borrow-lookahead
+    network.
+
+    :param circuit: The general circuit.
+    :param input_labels_a: labels representing integer a.
+    :param input_labels_b: labels representing integer b.
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
+    :return: Bits representing (a - b) mod 2^n, where n = len(a).
+
+    """
+    a = list(input_labels_a)
+    b = list(input_labels_b)
+    n = len(a)
+    if big_endian:
+        a.reverse()
+        b.reverse()
+
+    zero = add_gate_from_tt(circuit, a[0], a[0], '0000')
+
+    b = b[:n]
+    while len(b) < n:
+        b.append(zero)
+
+    result, _ = _kogge_stone_borrow_lookahead(circuit, a, b, zero, basis=basis)
+
+    return reverse_if_big_endian(result, big_endian)
+
+
+def add_subtract_with_compare_log_depth(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    big_endian: bool = False,
+) -> tuple[list[gate.Label], gate.Label]:
+    """
+    Subtract b from a in O(log n) depth and return a residual borrow bit indicating
+    whether a < b (Kogge-Stone borrow-lookahead).
+
+    :param circuit: The general circuit.
+    :param input_labels_a: labels representing integer a.
+    :param input_labels_b: labels representing integer b.
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :return: (result labels, borrow bit). Borrow is 0 when a >= b, 1 when a < b.
+
+    """
+    a = list(input_labels_a)
+    b = list(input_labels_b)
+
+    always_false = add_gate_from_tt(circuit, a[0], b[0], '0000')
+    while len(a) < len(b):
+        a.append(always_false)
+    while len(a) > len(b):
+        b.append(always_false)
+
+    validate_equal_sizes(a, b)
+
+    if big_endian:
+        a.reverse()
+        b.reverse()
+
+    result, borrow_out = _kogge_stone_borrow_lookahead(
+        circuit, a, b, always_false, basis=basis
+    )
+
+    return reverse_if_big_endian(result, big_endian), borrow_out
diff --git a/cirbo/synthesis/generation/arithmetics/summation.py b/cirbo/synthesis/generation/arithmetics/summation.py
index d2e32f9b..e81f9622 100644
--- a/cirbo/synthesis/generation/arithmetics/summation.py
+++ b/cirbo/synthesis/generation/arithmetics/summation.py
@@ -1,7 +1,10 @@
+import math
 import typing as tp
+from collections import deque
 from itertools import zip_longest
+from typing import cast, Optional
 
-from sortedcontainers import SortedList  # type: ignore
+from sortedcontainers import SortedList
 
 from cirbo.core.circuit import Circuit, gate
 
@@ -23,19 +26,30 @@
     "add_sum_n_bits_easy",
     "add_sum_pow2_m1",
     "add_sum_two_numbers",
+    "add_sum_two_numbers_log_depth",
+    "add_sum_two_numbers_log_depth_brent_kung",
+    "add_sum_two_numbers_log_depth_krapchenko",
     "add_sum_two_numbers_with_shift",
     "add_sum_n_weighted_bits",
+    "add_sum_n_weighted_bits_log_depth",
     "add_sum_n_weighted_bits_naive",
     "generate_sum_weighted_bits_efficient",
     "generate_sum_weighted_bits_naive",
+    "mdfa_sum_weighted_bits",
+    "xor_two_bits",
 ]
 
 
+def conventional_basis(basis: tp.Union[str, GenerationBasis]) -> GenerationBasis:
+    return GenerationBasis(basis.upper()) if isinstance(basis, str) else basis
+
+
 def add_sum_two_numbers(
     circuit: Circuit,
     input_labels_a: tp.Iterable[gate.Label],
     input_labels_b: tp.Iterable[gate.Label],
     *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
     big_endian: bool = False,
 ) -> list[gate.Label]:
     """
@@ -44,6 +58,7 @@ def add_sum_two_numbers(
     :param circuit: The general circuit.
     :param input_labels_a: List of bits representing the first binary number.
     :param input_labels_b: List of bits representing the second binary number.
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
     :param big_endian: defines how to interpret numbers, big-endian or little-endian
         format
     :return: List of bits representing the sum of the two numbers.
@@ -61,16 +76,37 @@ def add_sum_two_numbers(
         n, m = m, n
         input_labels_a, input_labels_b = input_labels_b, input_labels_a
     d = [[PLACEHOLDER_STR] for _ in range(n + 1)]
-    d[0] = add_sum_n_bits(circuit, [input_labels_a[0], input_labels_b[0]])
+    d[0] = add_sum_n_bits(circuit, [input_labels_a[0], input_labels_b[0]], basis=basis)
     for i in range(1, n):
         inp = [d[i - 1][1], input_labels_a[i]]
         if i < m:
             inp.append(input_labels_b[i])
-        d[i] = list(add_sum_n_bits(circuit, inp))
+        d[i] = list(add_sum_n_bits(circuit, inp, basis=basis))
     d[n] = [d[n - 1][1]]
     return reverse_if_big_endian([d[i][0] for i in range(n + 1)], big_endian)
 
 
+def xor_two_bits(
+    circuit: Circuit,
+    a: gate.Label,
+    b: gate.Label,
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> gate.Label:
+    if isinstance(basis, str):
+        _basis = GenerationBasis(basis.upper())
+    else:
+        _basis = basis
+
+    if _basis == GenerationBasis.XAIG:
+        return add_gate_from_tt(circuit, a, b, '0110')
+    if _basis == GenerationBasis.AIG:
+        ab = add_gate_from_tt(circuit, a, b, '0001')
+        nab = add_gate_from_tt(circuit, a, b, '1000')
+        return add_gate_from_tt(circuit, ab, nab, '1000')
+    raise BadBasisError(f"Unsupported basis: {basis}")
+
+
 def add_sum_two_numbers_with_shift(
     circuit: Circuit,
     shift,
@@ -130,29 +166,539 @@ def add_sum_two_numbers_with_shift(
     )
 
 
+def add_sum_two_numbers_log_depth(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    big_endian: bool = False,
+) -> list[gate.Label]:
+    """
+    Function to add two binary numbers represented by input labels in O(log(n+m)) depth
+    and O(n*logn) size using Koggle-stone adder.
+
+    :param circuit: The general circuit.
+    :param input_labels_a: List of bits representing the first binary number.
+    :param input_labels_b: List of bits representing the second binary number.
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
+    :param big_endian: defines how to interpret numbers, big-endian or little-endian
+        format
+    :return: List of bits representing the sum of the two numbers.
+
+    """
+    input_labels_a = list(input_labels_a)
+    input_labels_b = list(input_labels_b)
+    n = len(input_labels_a)
+    m = len(input_labels_b)
+    if big_endian:
+        input_labels_a.reverse()
+        input_labels_b.reverse()
+
+    if n < m:
+        n, m = m, n
+        input_labels_a, input_labels_b = input_labels_b, input_labels_a
+
+    zero = add_gate_from_tt(circuit, input_labels_a[0], input_labels_a[0], '0000')
+
+    for i in range(n - m):
+        input_labels_b.append(zero)
+
+    p_, g_ = zip(
+        *[
+            add_sum2(circuit, [input_labels_a[i], input_labels_b[i]], basis=basis)
+            for i in range(n)
+        ]
+    )
+    p, g = list(p_), list(g_)
+
+    po = p.copy()
+    d = 1
+
+    while d < n:
+        for i in range(n - 1, d - 1, -1):
+            t = add_gate_from_tt(circuit, p[i], g[i - d], '0001')
+            g[i] = add_gate_from_tt(circuit, g[i], t, '0111')
+
+        for i in range(n - 1, d - 1, -1):
+            p[i] = add_gate_from_tt(circuit, p[i], p[i - d], '0001')
+
+        d *= 2
+
+    g = [zero] + g
+    s = [xor_two_bits(circuit, po[i], g[i], basis=basis) for i in range(n)]
+    s.append(g[n])
+
+    return reverse_if_big_endian(s, big_endian)
+
+
+def add_sum_two_numbers_log_depth_brent_kung(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    big_endian: bool = False,
+) -> list[gate.Label]:
+    """
+    Add two binary numbers using a Brent-Kung adder.
+    Depth: O(log n), Size: O(n).
+
+    :param circuit: The general circuit.
+    :param input_labels_a: Bits of first binary number.
+    :param input_labels_b: Bits of second binary number.
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
+    :param big_endian: Whether numbers are big-endian.
+    :return: Bits of the sum.
+    """
+    input_labels_a = list(input_labels_a)
+    input_labels_b = list(input_labels_b)
+    n = len(input_labels_a)
+    m = len(input_labels_b)
+    if big_endian:
+        input_labels_a.reverse()
+        input_labels_b.reverse()
+
+    if n < m:
+        n, m = m, n
+        input_labels_a, input_labels_b = input_labels_b, input_labels_a
+
+    zero = add_gate_from_tt(circuit, input_labels_a[0], input_labels_a[0], '0000')
+    for i in range(n - m):
+        input_labels_b.append(zero)
+
+    p_, g_ = zip(
+        *[
+            add_sum2(circuit, [input_labels_a[i], input_labels_b[i]], basis=basis)
+            for i in range(n)
+        ]
+    )
+    p, g = list(p_), list(g_)
+
+    prefix_p = p.copy()
+    prefix_g = g.copy()
+
+    s = 1
+    while s < n:
+        next_s = s * 2
+        for i in range(next_s - 1, n, next_s):
+            j = i - s
+            if j >= 0:
+                tmp = add_gate_from_tt(circuit, prefix_p[i], prefix_g[j], '0001')
+                new_g = add_gate_from_tt(circuit, prefix_g[i], tmp, '0111')
+                new_p = add_gate_from_tt(circuit, prefix_p[i], prefix_p[j], '0001')
+
+                prefix_g[i] = new_g
+                prefix_p[i] = new_p
+        s = next_s
+
+    s //= 2
+    while s > 1:
+        next_s = s // 2
+        for i in range(s - 1, n, s):
+            if i + next_s < n:
+                j = i + next_s
+                tmp = add_gate_from_tt(circuit, prefix_p[j], prefix_g[i], '0001')
+                new_g = add_gate_from_tt(circuit, prefix_g[j], tmp, '0111')
+                new_p = add_gate_from_tt(circuit, prefix_p[j], prefix_p[i], '0001')
+
+                prefix_g[j] = new_g
+                prefix_p[j] = new_p
+        s = next_s
+
+    carries = [zero]
+    for i in range(n - 1):
+        carries.append(prefix_g[i])
+
+    sum_bits = []
+    for i in range(n):
+        sum_bit = xor_two_bits(circuit, p[i], carries[i], basis=basis)
+        sum_bits.append(sum_bit)
+
+    sum_bits.append(prefix_g[n - 1])
+
+    return reverse_if_big_endian(sum_bits, big_endian)
+
+
+def add_sum_two_numbers_log_depth_krapchenko(
+    circuit: Circuit,
+    input_labels_a: tp.Iterable[gate.Label],
+    input_labels_b: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+    big_endian: bool = False,
+) -> list[gate.Label]:
+    """
+    Add two binary numbers using Krapchenko's adder (Theorem 1.3).
+
+    Depth: O(log n) with a low constant factor; size: O(n).
+    The implementation follows the five-part construction S1..S5.
+
+    """
+    a = list(input_labels_a)
+    b = list(input_labels_b)
+    if big_endian:
+        a.reverse()
+        b.reverse()
+
+    n = len(a)
+    m = len(b)
+    if n < m:
+        n, m = m, n
+        a, b = b, a
+
+    zero = add_gate_from_tt(circuit, a[0], a[0], '0000')
+    for _ in range(n - m):
+        b.append(zero)
+
+    u = []
+    v = []
+    for i in range(n):
+        p_i, g_i = add_sum2(circuit, [a[i], b[i]], basis=basis)
+        v.append(p_i)
+        u.append(g_i)
+
+    def krapchenko_core(u_list, v_list, N) -> list[str]:
+        if N <= 2:
+            carries: list[str] = []
+            prev = zero
+            for i in range(N):
+                and_uv = add_gate_from_tt(circuit, v_list[i], prev, '0001')
+                c_i = add_gate_from_tt(circuit, u_list[i], and_uv, '0111')
+                carries.append(c_i)
+                prev = c_i
+            return carries
+
+        m_val = int(math.log2(N))
+        tau = int(2 * math.sqrt(2 * m_val) + 3)
+        if tau >= m_val:
+            tau = m_val - 1
+
+        G = [[u_list[i] for i in range(N)]]
+        V = [[v_list[i] for i in range(N)]]
+
+        for c_length in range(1, tau + 1):
+            size = 1 << c_length
+            blocks = N // size
+            G_l = []
+            V_l = []
+            for i in range(blocks):
+                left = 2 * i
+                right = 2 * i + 1
+
+                and_left_right = add_gate_from_tt(
+                    circuit, G[c_length - 1][left], V[c_length - 1][right], '0001'
+                )
+                g_new = add_gate_from_tt(
+                    circuit, G[c_length - 1][right], and_left_right, '0111'
+                )
+                v_new = add_gate_from_tt(
+                    circuit, V[c_length - 1][left], V[c_length - 1][right], '0001'
+                )
+
+                G_l.append(g_new)
+                V_l.append(v_new)
+            G.append(G_l)
+            V.append(V_l)
+
+        u_prime = G[tau]
+        v_prime = V[tau]
+        M = len(u_prime)
+
+        block_carries = krapchenko_core(u_prime, v_prime, M)
+
+        new_carries: list[Optional[str]] = [None] * N
+        for j in range(M):
+            pos = (j + 1) * (1 << tau) - 1
+            new_carries[pos] = block_carries[j]
+
+        for s in range(tau - 1, -1, -1):
+            size = 1 << s
+            step = size * 2
+            for L in range(0, N, step):
+                R = L + step - 1
+                if R >= N:
+                    continue
+                left_carry = zero if L == 0 else new_carries[L - 1]
+                assert left_carry is not None
+                M_pos = L + size - 1
+                idx = L // size
+                G_block = G[s][idx]
+                V_block = V[s][idx]
+                and_vl = add_gate_from_tt(circuit, V_block, left_carry, '0001')
+                c_mid = add_gate_from_tt(circuit, G_block, and_vl, '0111')
+                new_carries[M_pos] = c_mid
+
+        return cast(list[str], new_carries)
+
+    orig_n = n
+    next_pow2 = 1
+    while next_pow2 < n:
+        next_pow2 <<= 1
+    if next_pow2 > n:
+        zero_u = zero
+        zero_v = zero
+        u.extend([zero_u] * (next_pow2 - n))
+        v.extend([zero_v] * (next_pow2 - n))
+        n = next_pow2
+
+    carries = krapchenko_core(u, v, n)
+
+    sum_bits = []
+    sum_bits.append(v[0])
+    for i in range(1, n):
+        s_i = xor_two_bits(circuit, v[i], carries[i - 1], basis=basis)
+        sum_bits.append(s_i)
+    sum_bits.append(carries[n - 1])
+
+    if next_pow2 > orig_n:
+        sum_bits = sum_bits[: orig_n + 1]
+
+    return reverse_if_big_endian(sum_bits, big_endian)
+
+
+def add_sum_n_weighted_bits_log_depth(
+    circuit: Circuit,
+    input_labels_with_pow: tp.Iterable[tuple[int, gate.Label]],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
+) -> list[tuple[int, gate.Label]]:
+    """
+    Function to add a variable number of bits using Full and Half adders.
+    Depth: O(log n), Size: O(n).
+
+    :param circuit: The general circuit.
+    :param input_labels: List of bits to be added.
+    :param basis: in which basis should generated function lie. Supported [XAIG, AIG].
+    :return: Tuple containing the sum in binary representation.
+    """
+    input_labels_with_pow = list(input_labels_with_pow)
+    c: dict[int, list[gate.Label]] = {}
+    for p in input_labels_with_pow:
+        c.setdefault(p[0], []).append(p[1])
+
+    while max(len(c[i]) for i in c.keys()) > 2:
+        cn: dict[int, list[gate.Label]] = {}
+        for key in c:
+            for i in range(0, len(c[key]), 3):
+                inp = []
+                for k in range(i, i + 3):
+                    if len(c[key]) > k:
+                        inp.append(c[key][k])
+
+                if len(inp) > 0:
+                    res = add_sum_n_bits(circuit, inp, basis=basis)
+                    for k in range(len(res)):
+                        cn.setdefault(key + k, []).append(res[k])
+        c = cn
+
+    consec: list[list[gate.Label]] = []
+    last = -1
+    zero = add_gate_from_tt(
+        circuit, input_labels_with_pow[0][1], input_labels_with_pow[0][1], '0000'
+    )
+    ans = []
+
+    def sum_block():
+        input_labels_a = []
+        input_labels_b = []
+        for p in consec:
+            input_labels_a.append(p[0])
+            if len(p) == 1:
+                input_labels_b.append(zero)
+            else:
+                input_labels_b.append(p[1])
+
+        result_sum = add_sum_two_numbers_log_depth_brent_kung(
+            circuit, input_labels_a, input_labels_b, basis=basis
+        )
+        for i in range(len(result_sum)):
+            ans.append((last - len(consec) + 1 + i, result_sum[i]))
+
+    for k in sorted(c.keys()):
+        if last == -1 or last == k - 1:
+            consec.append(c[k])
+            last = k
+        else:
+            sum_block()
+            last = k
+            consec = [c[k]]
+
+    sum_block()
+    return ans
+
+
+def mdfa_sum_weighted_bits(
+    circuit: Circuit,
+    input_labels_with_pow: tp.Iterable[tuple[int, gate.Label]],
+) -> list[tuple[int, gate.Label]]:
+    """
+    Function to add a variable number of bits with using MDFA.
+    Has better size and worse depth than add_sum_n_weighted_bits_log_depth.
+    Depth: O(log n), Size: O(n).
+    MDFA does not work in AIG basis, so no basis parameter,
+    just use add_sum_n_weighted_bits_log_depth.
+
+    :param input_labels_with_pow: Circuit label inputs with corresponding powers.
+    :param circuit: The general circuit.
+    :param input_labels: List of bits to be added.
+    :return: Tuple containing the sum in binary representation.
+    """
+    c: dict[int, deque[gate.Label]] = {}
+    d: dict[int, deque[gate.Label]] = {}
+    for p in input_labels_with_pow:
+        c.setdefault(p[0], deque()).append(p[1])
+
+    while (
+        max(len(c.get(i, deque())) + len(d.get(i, deque())) for i in set(c) | set(d))
+        > 6
+    ):
+        cn: dict[int, deque[gate.Label]] = {}
+        dn: dict[int, deque[gate.Label]] = {}
+        for key in set(c) | set(d):
+            single = c.get(key, deque()).copy()
+            pairs = d.get(key, deque()).copy()
+
+            while len(single) >= 1 and len(pairs) >= 4:
+                z, x, xy = add_mdfa(
+                    circuit, [single.popleft()] + [pairs.popleft() for _ in range(4)]
+                )
+                cn.setdefault(key, deque()).append(z)
+                dn.setdefault(key + 1, deque()).extend([x, xy])
+
+            while len(single) >= 3 and len(pairs) >= 2:
+                a1, b1 = single.popleft(), single.popleft()
+                ab1 = add_gate_from_tt(
+                    circuit,
+                    a1,
+                    b1,
+                    "0110",
+                )
+                a2, ab2 = pairs.popleft(), pairs.popleft()
+                z, x, xy = add_mdfa(circuit, [single.popleft(), a1, ab1, a2, ab2])
+                cn.setdefault(key, deque()).append(z)
+                dn.setdefault(key + 1, deque()).extend([x, xy])
+
+            while len(single) >= 5:
+                a1, b1 = single.popleft(), single.popleft()
+                ab1 = add_gate_from_tt(
+                    circuit,
+                    a1,
+                    b1,
+                    "0110",
+                )
+                a2, b2 = single.popleft(), single.popleft()
+                ab2 = add_gate_from_tt(
+                    circuit,
+                    a2,
+                    b2,
+                    "0110",
+                )
+                z, x, xy = add_mdfa(circuit, [single.popleft(), a1, ab1, a2, ab2])
+                cn.setdefault(key, deque()).append(z)
+                dn.setdefault(key + 1, deque()).extend([x, xy])
+            if len(single) == 4:
+                res = add_sum_n_bits(circuit, [single.popleft() for _ in range(3)])
+                cn.setdefault(key, deque()).extend([res[0], single.popleft()])
+                cn.setdefault(key + 1, deque()).append(res[1])
+
+            while len(pairs) >= 10:
+                a, ab = pairs.popleft(), pairs.popleft()
+                b = add_gate_from_tt(
+                    circuit,
+                    a,
+                    ab,
+                    "0110",
+                )
+                for e in [a, b]:
+                    z, x, xy = add_mdfa(
+                        circuit, [e] + [pairs.popleft() for _ in range(4)]
+                    )
+                    cn.setdefault(key, deque()).append(z)
+                    dn.setdefault(key + 1, deque()).extend([x, xy])
+            while len(pairs) >= 4:
+                z, x, xy = add_simplified_mdfa(
+                    circuit, [pairs.popleft() for _ in range(4)]
+                )
+                cn.setdefault(key, deque()).append(z)
+                dn.setdefault(key + 1, deque()).extend([x, xy])
+
+            cn.setdefault(key, deque()).extend(single)
+            dn.setdefault(key, deque()).extend(pairs)
+
+        c = cn
+        d = dn
+
+    weighted_bits = []
+    for key, value in c.items():
+        for i in value:
+            weighted_bits.append((key, i))
+    for key, value in d.items():
+        for idx in range(0, len(value), 2):
+            a, ab = value[idx], value[idx + 1]
+            b = add_gate_from_tt(
+                circuit,
+                a,
+                ab,
+                "0110",
+            )
+            weighted_bits.append((key, a))
+            weighted_bits.append((key, b))
+    return add_sum_n_weighted_bits_log_depth(circuit, weighted_bits)
+
+
 def add_sum2(
-    circuit: Circuit, input_labels: tp.Iterable[gate.Label]
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
-    input_labels = list(input_labels)
-    validate_const_size(input_labels, 2)
-    [x1, x2] = input_labels
-    g1 = add_gate_from_tt(circuit, x1, x2, '0110')
-    g2 = add_gate_from_tt(circuit, x1, x2, '0001')
-    return list([g1, g2])
+    if isinstance(basis, str):
+        _basis = GenerationBasis(basis.upper())
+    else:
+        _basis = basis
+    if _basis == GenerationBasis.AIG:
+        return add_sum2_aig(circuit, input_labels)
+    if _basis == GenerationBasis.XAIG:
+        input_labels = list(input_labels)
+        validate_const_size(input_labels, 2)
+        [x1, x2] = input_labels
+        g1 = add_gate_from_tt(circuit, x1, x2, '0110')
+        g2 = add_gate_from_tt(circuit, x1, x2, '0001')
+        return list([g1, g2])
+    raise BadBasisError(f"Unsupported basis: {basis}")
 
 
 def add_sum3(
-    circuit: Circuit, input_labels: tp.Iterable[gate.Label]
+    circuit: Circuit,
+    input_labels: tp.Iterable[gate.Label],
+    *,
+    basis: tp.Union[str, GenerationBasis] = GenerationBasis.XAIG,
 ) -> list[gate.Label]:
+    if isinstance(basis, str):
+        _basis = GenerationBasis(basis.upper())
+    else:
+        _basis = basis
     input_labels = list(input_labels)
     validate_const_size(input_labels, 3)
     x1, x2, x3 = input_labels
-    g1 = add_gate_from_tt(circuit, x1, x2, '0110')
-    g2 = add_gate_from_tt(circuit, x2, x3, '0110')
-    g3 = add_gate_from_tt(circuit, g1, g2, '0111')
-    g4 = add_gate_from_tt(circuit, g1, x3, '0110')
-    g5 = add_gate_from_tt(circuit, g3, g4, '0110')
-    return list([g4, g5])
+    if _basis == GenerationBasis.AIG:
+        g1 = add_gate_from_tt(circuit, x1, x2, '0001')
+        g2 = add_gate_from_tt(circuit, x1, x2, '0111')
+        g3 = add_gate_from_tt(circuit, g1, g2, '0100')
+        g4 = add_gate_from_tt(circuit, g3, x3, '0111')
+        g5 = add_gate_from_tt(circuit, g3, x3, '0001')
+        o1 = add_gate_from_tt(circuit, g5, g4, '0100')
+        o2 = add_gate_from_tt(circuit, g1, g5, '0111')
+    elif _basis == GenerationBasis.XAIG:
+        g1 = add_gate_from_tt(circuit, x1, x2, '0110')
+        g2 = add_gate_from_tt(circuit, x2, x3, '0110')
+        g3 = add_gate_from_tt(circuit, g1, g2, '0111')
+        o1 = add_gate_from_tt(circuit, g1, x3, '0110')
+        o2 = add_gate_from_tt(circuit, g3, o1, '0110')
+    else:
+        raise BadBasisError(f"Unsupported basis: {basis}")
+    return list([o1, o2])
 
 
 # given x1, x2, and (x2 oplus x3), computes the binary representation
@@ -479,20 +1025,11 @@ def _add_sum_n_bits(
                 now_solo.append(z)
                 next_x_xy.append((x1, x1y1))
             else:
-                z, x1, x1y1 = add_simplified_mdfa(
-                    circuit,
-                    [
-                        now_x_xy[-1][0],
-                        now_x_xy[-1][1],
-                        now_x_xy[-2][0],
-                        now_x_xy[-2][1],
-                    ],
+                now_solo.append(now_x_xy[-1][1])
+                next_solo.append(
+                    add_gate_from_tt(circuit, now_x_xy[-1][0], now_x_xy[-1][1], "0010")
                 )
-                for _ in range(2):
-                    now_x_xy.pop()
-
-                now_solo.append(z)
-                next_x_xy.append((x1, x1y1))
+                now_x_xy.pop()
         if len(now_x_xy) == 1:
             if len(now_solo) > 0:
                 x, y = add_stockmeyer_block(
@@ -696,20 +1233,11 @@ def add_sum_n_weighted_bits(
                 now_solo.append(z)
                 next_x_xy.append((x1, x1y1))
             else:
-                z, x1, x1y1 = add_simplified_mdfa(
-                    circuit,
-                    [
-                        now_x_xy[-1][0],
-                        now_x_xy[-1][1],
-                        now_x_xy[-2][0],
-                        now_x_xy[-2][1],
-                    ],
+                now_solo.append(now_x_xy[-1][1])
+                next_solo.append(
+                    add_gate_from_tt(circuit, now_x_xy[-1][0], now_x_xy[-1][1], "0010")
                 )
-                for _ in range(2):
-                    now_x_xy.pop()
-
-                now_solo.append(z)
-                next_x_xy.append((x1, x1y1))
+                now_x_xy.pop()
         if len(now_x_xy) == 1:
             if len(now_solo) > 0:
                 x, y = add_stockmeyer_block(
@@ -726,19 +1254,6 @@ def add_sum_n_weighted_bits(
                 )
                 now_x_xy.pop()
 
-        while len(now_solo) > 2:
-            x, y = add_sum3(circuit, now_solo[-1:-4:-1])
-            for _ in range(3):
-                now_solo.pop()
-            now_solo.append(x)
-            next_solo.append(y)
-        if len(now_solo) > 1:
-            x, y = add_sum2(circuit, now_solo[-1:-3:-1])
-            for _ in range(2):
-                now_solo.pop()
-            now_solo.append(x)
-            next_solo.append(y)
-
         res.append((now_level, now_solo[0]))
 
         for label in next_solo:
diff --git a/pyproject.toml b/pyproject.toml
index 89cd1504..6f82a161 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -150,7 +150,13 @@ check_untyped_defs = true
 
 [[tool.mypy.overrides]]
 ignore_missing_imports = true
-module = ["pysat.*", "pebble.*", "mockturtle_wrapper.*", "graphviz.*"]
+module = [
+    "pysat.*",
+    "pebble.*",
+    "mockturtle_wrapper.*",
+    "graphviz.*",
+    "sortedcontainers.*",
+]
 
 
 [tool.pytest.ini_options]
diff --git a/tests/cirbo/synthesis/generation/arithmetics_test.py b/tests/cirbo/synthesis/generation/arithmetics_test.py
index e7c65d67..002222b3 100644
--- a/tests/cirbo/synthesis/generation/arithmetics_test.py
+++ b/tests/cirbo/synthesis/generation/arithmetics_test.py
@@ -18,17 +18,27 @@
     add_sqrt,
     add_square,
     add_square_pow2_m1,
+    add_sub_two_numbers,
+    add_sub_two_numbers_log_depth,
+    add_subtract_with_compare,
+    add_subtract_with_compare_log_depth,
     add_sum_n_bits,
     add_sum_n_weighted_bits,
+    add_sum_n_weighted_bits_log_depth,
+    add_sum_two_numbers_log_depth,
+    add_sum_two_numbers_log_depth_brent_kung,
     generate_equal,
     generate_mul,
     generate_square,
+    generate_sub_two_numbers,
     generate_sum_n_bits,
     generate_sum_weighted_bits_efficient,
     generate_sum_weighted_bits_naive,
+    mdfa_sum_weighted_bits,
     MulMode,
     SquareMode,
 )
+from cirbo.synthesis.generation.arithmetics._utils import add_gate_from_tt
 
 TEST_SIZE = 100
 random.seed(42)
@@ -89,6 +99,18 @@ def sum_naive(inputs_a):
     return to_bin(a, len_res)
 
 
+def sum_two_numbers_naive(inputs_a, inputs_b):
+    a = to_num(inputs_a)
+    b = to_num(inputs_b)
+    return to_bin(a + b, max(len(inputs_a), len(inputs_b)) + 1)
+
+
+def sub_two_numbers_naive(inputs_a, inputs_b):
+    a = to_num(inputs_a)
+    b = to_num(inputs_b)
+    return to_bin((a - b) % (1 << len(inputs_a)), len(inputs_a))
+
+
 def sum_naive_with_powers(powers_and_values_list):
     res = 0
     mx = 0
@@ -104,6 +126,10 @@ def sum_naive_with_powers(powers_and_values_list):
     return to_bin(res, sz)
 
 
+def sum_weighted_bits_naive(weighted_bits, size):
+    return to_bin(sum(2 ** p[0] * p[1] for p in weighted_bits), size)[::-1]
+
+
 @pytest.mark.parametrize(
     "func",
     [
@@ -252,6 +278,105 @@ def test_gen_square(number_inputs, type, big_endian):
         assert square_naive(input_labels) == res
 
 
+@pytest.mark.parametrize(
+    "func",
+    [
+        add_sum_two_numbers_log_depth,
+        add_sum_two_numbers_log_depth_brent_kung,
+    ],
+)
+@pytest.mark.parametrize(
+    "size",
+    [
+        [1, 1],
+        [1, 7],
+        [7, 1],
+        [3, 6],
+        pytest.param([8, 2], marks=pytest.mark.slow),
+        pytest.param([16, 16], marks=pytest.mark.slow),
+        pytest.param([24, 15], marks=pytest.mark.slow),
+    ],
+)
+@pytest.mark.parametrize("big_endian", [True, False])
+def test_sum_two_numbers(func, size, big_endian):
+    x, y = size
+    ckt = Circuit()
+    input_labels = [f'x{i}' for i in range(x + y)]
+    for i in range(x + y):
+        ckt.add_gate(Gate(input_labels[i], INPUT))
+
+    res = func(ckt, input_labels[:x], input_labels[x:], big_endian=big_endian)
+    ckt.set_outputs(res)
+
+    for test in range(TEST_SIZE):
+        input_labels_a = [random.choice([0, 1]) for _ in range(x)]
+        input_labels_b = [random.choice([0, 1]) for _ in range(y)]
+        res = ckt.evaluate(input_labels_a + input_labels_b)
+        if big_endian:
+            input_labels_a.reverse()
+            input_labels_b.reverse()
+        else:
+            res.reverse()
+
+        assert sum_two_numbers_naive(input_labels_a, input_labels_b) == res
+
+
+def normalize_weighted_output(circuit, zero, weighted_bits):
+    a = [zero] * (max(p[0] for p in weighted_bits) + 1)
+    for p in weighted_bits:
+        a[p[0]] = p[1]
+    return a
+
+
+@pytest.mark.parametrize(
+    "func",
+    [
+        mdfa_sum_weighted_bits,
+        add_sum_n_weighted_bits_log_depth,
+    ],
+)
+@pytest.mark.parametrize(
+    "shape",
+    [
+        [0, 0, 10],
+        [1, 0, 1],
+        [1, 2, 3, 4, 3, 2, 1],  # Mult4
+        [8],  # Add8
+        [2, 2, 2, 2],  # Sum4
+        [1, 0, 2, 1, 3, 2, 4, 3, 4, 2, 3, 1, 2],  # Square7
+        pytest.param([30], marks=pytest.mark.slow),
+        pytest.param([16, 16], marks=pytest.mark.slow),
+        pytest.param([2] * 20, marks=pytest.mark.slow),
+    ],
+)
+def test_sum_weighted_bits(func, shape):
+    ckt = Circuit()
+    n = sum(k for k in shape)
+    input_labels = [f'x{i}' for i in range(n)]
+    for i in range(n):
+        ckt.add_gate(Gate(input_labels[i], INPUT))
+    zero = add_gate_from_tt(
+        ckt,
+        input_labels[0],
+        input_labels[0],
+        '0000',
+    )
+    weighted_bits = []
+    c = 0
+    for i in range(len(shape)):
+        for _ in range(shape[i]):
+            weighted_bits.append([i, input_labels[c]])
+            c += 1
+    res = func(ckt, weighted_bits)
+    res = normalize_weighted_output(ckt, zero, res)
+    ckt.set_outputs(res)
+    for test in range(TEST_SIZE):
+        labels_input = [random.choice([0, 1]) for _ in range(n)]
+        weighted_input = [[weighted_bits[i][0], labels_input[i]] for i in range(n)]
+        res = ckt.evaluate(labels_input)
+        assert sum_weighted_bits_naive(weighted_input, len(res)) == res
+
+
 @pytest.mark.parametrize("num", list(range(128)))
 def test_add_equal(num):
     r = 7
@@ -354,12 +479,13 @@ def test_div_mod(x, big_endian):
     ],
 )
 @pytest.mark.parametrize("big_endian", [True, False])
-def test_add_sum_n_bits(basis, n, big_endian):
+@pytest.mark.parametrize("func", [add_sum_n_bits])
+def test_add_sum_n_bits(func, basis, n, big_endian):
     ckt = Circuit()
     input_labels = [f'x{i}' for i in range(n)]
     for i in range(n):
         ckt.add_gate(Gate(input_labels[i], INPUT))
-    res = add_sum_n_bits(ckt, input_labels, basis=basis, big_endian=big_endian)
+    res = func(ckt, input_labels, basis=basis, big_endian=big_endian)
     ckt.set_outputs(res)
     for test in range(TEST_SIZE):
         input_labels = [random.choice([0, 1]) for _ in range(n)]
@@ -369,6 +495,102 @@ def test_add_sum_n_bits(basis, n, big_endian):
         assert sum_naive(input_labels) == res
 
 
+@pytest.mark.parametrize("basis", [GenerationBasis.XAIG, GenerationBasis.AIG])
+@pytest.mark.parametrize(
+    "size",
+    [
+        [1, 1],
+        [1, 7],
+        [7, 1],
+        [3, 6],
+        pytest.param([8, 2], marks=pytest.mark.slow),
+    ],
+)
+@pytest.mark.parametrize("big_endian", [True, False])
+@pytest.mark.parametrize("func", [add_sub_two_numbers, add_sub_two_numbers_log_depth])
+def test_sub_two_numbers(func, basis, size, big_endian):
+    x, y = size
+    ckt = Circuit()
+    input_labels = [f'x{i}' for i in range(x + y)]
+    for i in range(x + y):
+        ckt.add_gate(Gate(input_labels[i], INPUT))
+
+    res = func(
+        ckt, input_labels[:x], input_labels[x:], basis=basis, big_endian=big_endian
+    )
+    ckt.set_outputs(res)
+
+    for test in range(TEST_SIZE):
+        input_labels_a = [random.choice([0, 1]) for _ in range(x)]
+        input_labels_b = [random.choice([0, 1]) for _ in range(y)]
+        res = ckt.evaluate(input_labels_a + input_labels_b)
+        if big_endian:
+            input_labels_a.reverse()
+            input_labels_b.reverse()
+        else:
+            res.reverse()
+
+        assert sub_two_numbers_naive(input_labels_a, input_labels_b) == res
+
+
+@pytest.mark.parametrize("basis", [GenerationBasis.XAIG, GenerationBasis.AIG])
+@pytest.mark.parametrize(
+    "size",
+    [1, 2, 3, pytest.param(8, marks=pytest.mark.slow)],
+)
+@pytest.mark.parametrize("big_endian", [True, False])
+@pytest.mark.parametrize(
+    "func", [add_subtract_with_compare, add_subtract_with_compare_log_depth]
+)
+def test_subtract_with_compare(func, basis, size, big_endian):
+    ckt = Circuit()
+    input_labels = [f'x{i}' for i in range(2 * size)]
+    for i in range(2 * size):
+        ckt.add_gate(Gate(input_labels[i], INPUT))
+
+    res, borrow = func(
+        ckt,
+        input_labels[:size],
+        input_labels[size:],
+        basis=basis,
+        big_endian=big_endian,
+    )
+    ckt.set_outputs(res + [borrow])
+
+    for test in range(TEST_SIZE):
+        input_labels_a = [random.choice([0, 1]) for _ in range(size)]
+        input_labels_b = [random.choice([0, 1]) for _ in range(size)]
+        values = ckt.evaluate(input_labels_a + input_labels_b)
+        borrow_value = values[-1]
+        res = values[:-1]
+        if big_endian:
+            input_labels_a.reverse()
+            input_labels_b.reverse()
+        else:
+            res.reverse()
+
+        assert sub_two_numbers_naive(input_labels_a, input_labels_b) == res
+        assert borrow_value == int(to_num(input_labels_a) < to_num(input_labels_b))
+
+
+@pytest.mark.parametrize("basis", [GenerationBasis.XAIG, GenerationBasis.AIG])
+@pytest.mark.parametrize("big_endian", [True, False])
+@pytest.mark.parametrize("size", [1, 2, 3, pytest.param(8, marks=pytest.mark.slow)])
+def test_generate_sub_two_numbers(basis, size, big_endian):
+    ckt = generate_sub_two_numbers(size, size, basis=basis, big_endian=big_endian)
+    for test in range(TEST_SIZE):
+        input_labels_a = [random.choice([0, 1]) for _ in range(size)]
+        input_labels_b = [random.choice([0, 1]) for _ in range(size)]
+        res = ckt.evaluate(input_labels_a + input_labels_b)
+        if big_endian:
+            input_labels_a.reverse()
+            input_labels_b.reverse()
+        else:
+            res.reverse()
+
+        assert sub_two_numbers_naive(input_labels_a, input_labels_b) == res
+
+
 @pytest.mark.parametrize("basis", [GenerationBasis.XAIG, GenerationBasis.AIG])
 @pytest.mark.parametrize(
     "n",
@@ -439,7 +661,7 @@ def test_sum_weighted_bits_in_aig():
     ],
 )
 @pytest.mark.parametrize("density_in_percent", list(range(10, 101, 10)))
-def test_sum_weighted_bits_in_xaig(n, density_in_percent):
+def test_sum_weighted_bits_in_xaig_density(n, density_in_percent):
     max_level = n * density_in_percent // 100
     powers = [random.randint(0, max_level) for _ in range(n)]
     ckt = generate_sum_weighted_bits_efficient(powers)