Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 31 additions & 9 deletions .github/workflows/python-checks.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -35,50 +35,72 @@ jobs:
matrix:
# >=3.14 is blocked by dependencies (`docformatter` seems blocked by `untokenize`).
# FIXME: try replace docformatter dependency to unblock version.
python-version: [ "3.9", "3.13" ]
python-version: ["3.9", "3.13"]
poetry-version: ["2.1.1"]
os: [ubuntu-latest, macos-14, macos-15-intel]
os: [ubuntu-latest, macos-14, macos-15-intel, windows-latest]

runs-on: ${{ matrix.os }}

# To use bash commands syntax on Windows.
defaults:
run:
shell: bash

# checks should not take more than 20 minutes (including build and setup step).
# If it is the case probably something heavy trespassed to unit tests.
timeout-minutes: 20

env:
DISABLE_ABC_CEXT: "1"
CMAKE_BUILD_PARALLEL_LEVEL: "8"

steps:
- name: Checkout repository
uses: actions/checkout@v2
uses: actions/checkout@v4
with:
submodules: 'true'

- name: Set up Python ${{ matrix.python-version }}
uses: actions/setup-python@v2
uses: actions/setup-python@v5
with:
python-version: ${{ matrix.python-version }}

- name: Update CMake
uses: jwlawson/actions-setup-cmake@v2.0

- name: Install poetry
uses: snok/install-poetry@v1
with:
version: ${{ matrix.poetry-version }}
virtualenvs-create: true
virtualenvs-in-project: true
- run: (export DISABLE_ABC_CEXT=1 && poetry build --no-interaction)
env:
DISABLE_ABC_CEXT: 1
CMAKE_BUILD_PARALLEL_LEVEL: 8
- run: (export DISABLE_ABC_CEXT=1 && poetry install --no-interaction)

- name: Build
run: poetry build --no-interaction

- name: Install deps
run: poetry install --no-interaction

- name: mypy
if: always()
run: poetry run mypy -p cirbo

- name: flake8
if: always()
run: poetry run flake8 cirbo tests tools

- name: pytest
if: always()
run: poetry run pytest tests -v -m 'not (manual or slow or ABC)'

- name: usort
if: always()
run: poetry run usort check cirbo tests tools

- name: docformatter
if: always()
run: poetry run docformatter --check --diff cirbo/ tests/ tools/

- name: black
if: always()
run: poetry run black --check --diff cirbo/ tests/ tools/
4 changes: 0 additions & 4 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -19,20 +19,16 @@ add_subdirectory(third_party/pybind11)
add_subdirectory(third_party/mockturtle)

pybind11_add_module(mockturtle_wrapper extensions/mockturtle_wrapper/src/module.cpp)

target_link_libraries(mockturtle_wrapper PRIVATE mockturtle)

target_include_directories(mockturtle_wrapper PRIVATE third_party)


# ABC related libs can be disabled using environment variable.
IF(NOT DISABLE_ABC_CEXT)
add_subdirectory(third_party/abc)
# Needed for correct library compilation.
target_compile_options(libabc PRIVATE -fPIC)

pybind11_add_module(abc_wrapper extensions/abc_wrapper/src/module.cpp)

target_link_libraries(abc_wrapper PRIVATE libabc)
target_include_directories(abc_wrapper PRIVATE third_party)
ENDIF(NOT DISABLE_ABC_CEXT)
48 changes: 27 additions & 21 deletions cirbo/synthesis/circuit_search.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@
import itertools
import logging
import multiprocessing as mp
import os
import typing as tp

from concurrent.futures import TimeoutError

from pebble import concurrent

import pebble
from pysat.formula import CNF, IDPool
from pysat.solvers import Solver

Expand Down Expand Up @@ -162,6 +162,20 @@ def _get_GateType_by_tt(gate_tt: tp.List[bool]) -> GateType:
return _tt_to_gate_type[tuple(gate_tt)]


def _mp_ctx():
# 'spawn' will be used on windows instead of a 'fork'.
return mp.get_context("spawn" if os.name == "nt" else "fork")


def _solve_cnf(solver_name: str, clauses: list[list[int]]) -> tp.Optional[tp.List[int]]:
s = Solver(name=solver_name, bootstrap_with=clauses)
try:
sat = s.solve()
return s.get_model() if sat else None
finally:
s.delete()


class CircuitFinderSat:
"""
A class for finding Boolean circuits using SAT-solvers.
Expand Down Expand Up @@ -288,27 +302,19 @@ def find_circuit(
raise NoSolutionError()

logger.debug(f"Running {solver_name.value}")
s = Solver(name=solver_name.value, bootstrap_with=self._cnf.clauses)
if time_limit:

# `pebble` has strange typing and argument actually is called
# `context` and not `mp_contest` as stated in typed signature.
@concurrent.process(timeout=time_limit, context=mp.get_context('fork')) # type: ignore
def cnf_from_bench_wrapper():
s.solve()
return s.get_model()

try:
future = cnf_from_bench_wrapper()
model = future.result()
except TimeoutError as te:
logger.debug("Solver timed out and is being stopped.")
s.delete()
raise SolverTimeOutError() from te
with pebble.ProcessPool(max_workers=1, context=_mp_ctx()) as pool:
future = pool.schedule(
_solve_cnf,
args=[solver_name.value, self._cnf.clauses],
timeout=time_limit,
)
try:
model = future.result()
except TimeoutError as te:
raise SolverTimeOutError() from te
else:
s.solve()
model = s.get_model()
s.delete()
model = _solve_cnf(solver_name.value, self._cnf.clauses)

if model is None:
raise NoSolutionError()
Expand Down
10 changes: 10 additions & 0 deletions extensions/abc_wrapper/src/module.cpp
Original file line number Diff line number Diff line change
@@ -1,3 +1,13 @@
#ifdef _WIN32
#ifndef WIN32_LEAN_AND_MEAN
#define WIN32_LEAN_AND_MEAN
#endif
#ifndef NOMINMAX
#define NOMINMAX
#endif
#include <Windows.h>
#endif

#include <pybind11/pybind11.h>
#include <pybind11/stl.h>
#include "run_abc.h"
Expand Down
10 changes: 10 additions & 0 deletions extensions/mockturtle_wrapper/src/module.cpp
Original file line number Diff line number Diff line change
@@ -1,3 +1,13 @@
#ifdef _WIN32
#ifndef WIN32_LEAN_AND_MEAN
#define WIN32_LEAN_AND_MEAN
#endif
#ifndef NOMINMAX
#define NOMINMAX
#endif
#include <Windows.h>
#endif

#include <pybind11/pybind11.h>
#include <pybind11/stl.h>
#include "cut_enumerates.hpp"
Expand Down
4 changes: 2 additions & 2 deletions pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@ Repository = "https://github.com/SPbSAT/cirbo"

[build-system]
requires = [
"poetry-core>=1.0.0",
"setuptools>=45",
"poetry-core>=2.0.0,<3.0.0",
"setuptools>=65",
"wheel",
]
build-backend = "poetry.core.masonry.api"
Expand Down